lustrec / src / init_calculus.ml @ b38ffff3
History | View | Annotate | Download (11.1 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
(** Main typing module. Classic inference algorithm with destructive |
13 |
unification. *) |
14 |
|
15 |
(* Though it shares similarities with the clock calculus module, no code |
16 |
is shared. Simple environments, very limited identifier scoping, no |
17 |
identifier redefinition allowed. *) |
18 |
|
19 |
open Utils |
20 |
(* Yes, opening both modules is dirty as some type names will be |
21 |
overwritten, yet this makes notations far lighter.*) |
22 |
open Corelang |
23 |
open Init |
24 |
open Format |
25 |
|
26 |
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in |
27 |
type [ty]. False otherwise. *) |
28 |
let rec occurs tvar ty = |
29 |
let ty = repr ty in |
30 |
match ty.tdesc with |
31 |
| Ivar -> ty=tvar |
32 |
| Iarrow (t1, t2) -> |
33 |
(occurs tvar t1) || (occurs tvar t2) |
34 |
| Ituple tl -> |
35 |
List.exists (occurs tvar) tl |
36 |
| Ilink t -> occurs tvar t |
37 |
| Isucc t -> occurs tvar t |
38 |
| Iunivar -> false |
39 |
|
40 |
(** Promote monomorphic type variables to polymorphic type variables. *) |
41 |
(* Generalize by side-effects *) |
42 |
let rec generalize ty = |
43 |
match ty.tdesc with |
44 |
| Ivar -> |
45 |
(* No scopes, always generalize *) |
46 |
ty.idesc <- Iunivar |
47 |
| Iarrow (t1,t2) -> |
48 |
generalize t1; generalize t2 |
49 |
| Ituple tlist -> |
50 |
List.iter generalize tlist |
51 |
| Ilink t -> |
52 |
generalize t |
53 |
| Isucc t -> |
54 |
generalize t |
55 |
| Tunivar -> () |
56 |
|
57 |
(** Downgrade polymorphic type variables to monomorphic type variables *) |
58 |
let rec instanciate inst_vars ty = |
59 |
let ty = repr ty in |
60 |
match ty.idesc with |
61 |
| Ivar -> ty |
62 |
| Iarrow (t1,t2) -> |
63 |
{ty with idesc = |
64 |
Iarrow ((instanciate inst_vars t1), (instanciate inst_vars t2))} |
65 |
| Ituple tlist -> |
66 |
{ty with idesc = Ituple (List.map (instanciate inst_vars) tlist)} |
67 |
| Isucc t -> |
68 |
(* should not happen *) |
69 |
{ty with idesc = Isucc (instanciate inst_vars t)} |
70 |
| Ilink t -> |
71 |
(* should not happen *) |
72 |
{ty with idesc = Ilink (instanciate inst_vars t)} |
73 |
| Iunivar -> |
74 |
try |
75 |
List.assoc ty.iid !inst_vars |
76 |
with Not_found -> |
77 |
let var = new_var () in |
78 |
inst_vars := (ty.iid, var)::!inst_vars; |
79 |
var |
80 |
|
81 |
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify |
82 |
(t1,t2)] if the types are not unifiable.*) |
83 |
|
84 |
(* Standard destructive unification *) |
85 |
(* may loop for omega types *) |
86 |
let rec unify t1 t2 = |
87 |
let t1 = repr t1 in |
88 |
let t2 = repr t2 in |
89 |
if t1=t2 then |
90 |
() |
91 |
else |
92 |
(* No type abbreviations resolution for now *) |
93 |
match t1.idesc,t2.idesc with |
94 |
(* This case is not mandory but will keep "older" types *) |
95 |
| Ivar, Ivar -> |
96 |
if t1.iid < t2.iid then |
97 |
t2.idesc <- Ilink t1 |
98 |
else |
99 |
t1.idesc <- Ilink t2 |
100 |
| (Ivar, _) when (not (occurs t1 t2)) -> |
101 |
t1.idesc <- Ilink t2 |
102 |
| (_,Ivar) when (not (occurs t2 t1)) -> |
103 |
t2.idesc <- Ilink t1 |
104 |
| Isucc t1, Isucc t1' -> unify t1 t1' |
105 |
| Iarrow (t1,t2), Iarrow (t1',t2') -> |
106 |
unify t1 t1'; unify t2 t2' |
107 |
| Ituple tlist1, Ituple tlist2 -> |
108 |
if (List.length tlist1) <> (List.length tlist2) then |
109 |
raise (Unify (t1, t2)) |
110 |
else |
111 |
List.iter2 unify tlist1 tlist2 |
112 |
| Iunivar,_ | _, Iunivar -> |
113 |
() |
114 |
| _,_ -> raise (Unify (t1, t2)) |
115 |
|
116 |
let init_of_const c = |
117 |
Init_predef.init_zero |
118 |
|
119 |
let rec init_expect env in_main expr ty = |
120 |
let texpr = init_expr env in_main expr in |
121 |
try |
122 |
unify texpr ty |
123 |
with Unify (t1,t2) -> |
124 |
raise (Error (expr.expr_loc, Init_clash (t1,t2))) |
125 |
|
126 |
and init_ident env in_main id loc = |
127 |
init_expr env in_main (expr_of_ident id loc) |
128 |
|
129 |
(** [type_expr env in_main expr] types expression [expr] in environment |
130 |
[env]. *) |
131 |
and init_expr env in_main expr = |
132 |
match expr.expr_desc with |
133 |
| Expr_const c -> |
134 |
let ty = init_of_const c in |
135 |
expr.expr_init <- ty; |
136 |
ty |
137 |
| Expr_ident v -> |
138 |
let tyv = |
139 |
try |
140 |
Env.lookup_value env v |
141 |
with Not_found -> |
142 |
raise (Error (expr.expr_loc, Unbound_value v)) |
143 |
in |
144 |
let ty = instanciate (ref []) tyv in |
145 |
expr.expr_init <- ty; |
146 |
ty |
147 |
| Expr_tuple elist -> |
148 |
let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in |
149 |
expr.expr_init <- ty; |
150 |
ty |
151 |
| Expr_appl (id, args, r) -> |
152 |
(match r with |
153 |
| None -> () |
154 |
| Some x -> let expr_x = expr_of_ident x expr.expr_loc in |
155 |
init_expect env in_main expr_x Init_predef.init_zero); |
156 |
let tfun = type_ident env in_main id expr.expr_loc in |
157 |
let tins,touts= split_arrow tfun in |
158 |
type_expect env in_main args tins; |
159 |
expr.expr_type <- touts; |
160 |
touts |
161 |
| Expr_arrow (e1,e2) -> |
162 |
let ty = type_expr env in_main e1 in |
163 |
type_expect env in_main e2 ty; |
164 |
expr.expr_type <- ty; |
165 |
ty |
166 |
| Expr_fby (init,e) -> |
167 |
let ty = type_of_const init in |
168 |
type_expect env in_main e ty; |
169 |
expr.expr_type <- ty; |
170 |
ty |
171 |
| Expr_concat (hd,e) -> |
172 |
let ty = type_of_const hd in |
173 |
type_expect env in_main e ty; |
174 |
expr.expr_type <- ty; |
175 |
ty |
176 |
| Expr_tail e -> |
177 |
let ty = type_expr env in_main e in |
178 |
expr.expr_type <- ty; |
179 |
ty |
180 |
| Expr_pre e -> |
181 |
let ty = type_expr env in_main e in |
182 |
expr.expr_type <- ty; |
183 |
ty |
184 |
| Expr_when (e1,c) | Expr_whennot (e1,c) -> |
185 |
let expr_c = expr_of_ident c expr.expr_loc in |
186 |
type_expect env in_main expr_c Type_predef.type_bool; |
187 |
let tlarg = type_expr env in_main e1 in |
188 |
expr.expr_type <- tlarg; |
189 |
tlarg |
190 |
| Expr_merge (c,e2,e3) -> |
191 |
let expr_c = expr_of_ident c expr.expr_loc in |
192 |
type_expect env in_main expr_c Type_predef.type_bool; |
193 |
let te2 = type_expr env in_main e2 in |
194 |
type_expect env in_main e3 te2; |
195 |
expr.expr_type <- te2; |
196 |
te2 |
197 |
| Expr_uclock (e,k) | Expr_dclock (e,k) -> |
198 |
let ty = type_expr env in_main e in |
199 |
expr.expr_type <- ty; |
200 |
ty |
201 |
| Expr_phclock (e,q) -> |
202 |
let ty = type_expr env in_main e in |
203 |
expr.expr_type <- ty; |
204 |
ty |
205 |
|
206 |
(** [type_eq env eq] types equation [eq] in environment [env] *) |
207 |
let type_eq env in_main undefined_vars eq = |
208 |
(* Check multiple variable definitions *) |
209 |
let define_var id uvars = |
210 |
try |
211 |
ignore(IMap.find id uvars); |
212 |
IMap.remove id uvars |
213 |
with Not_found -> |
214 |
raise (Error (eq.eq_loc, Already_defined id)) |
215 |
in |
216 |
let undefined_vars = |
217 |
List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in |
218 |
(* Type lhs *) |
219 |
let get_value_type id = |
220 |
try |
221 |
Env.lookup_value env id |
222 |
with Not_found -> |
223 |
raise (Error (eq.eq_loc, Unbound_value id)) |
224 |
in |
225 |
let tyl_lhs = List.map get_value_type eq.eq_lhs in |
226 |
let ty_lhs = type_of_type_list tyl_lhs in |
227 |
(* Type rhs *) |
228 |
type_expect env in_main eq.eq_rhs ty_lhs; |
229 |
undefined_vars |
230 |
|
231 |
(* [type_coretype cty] types the type declaration [cty] *) |
232 |
let type_coretype cty = |
233 |
match cty with |
234 |
| Tydec_any -> new_var () |
235 |
| Tydec_int -> Type_predef.type_int |
236 |
| Tydec_real -> Type_predef.type_real |
237 |
| Tydec_float -> Type_predef.type_real |
238 |
| Tydec_bool -> Type_predef.type_bool |
239 |
| Tydec_clock -> Type_predef.type_clock |
240 |
|
241 |
(* [type_coreclock env ck id loc] types the type clock declaration [ck] |
242 |
in environment [env] *) |
243 |
let type_coreclock env ck id loc = |
244 |
match ck.ck_dec_desc with |
245 |
| Ckdec_any | Ckdec_pclock (_,_) -> () |
246 |
| Ckdec_bool cl -> |
247 |
let dummy_id_expr = expr_of_ident id loc in |
248 |
let when_expr = |
249 |
List.fold_left |
250 |
(fun expr c -> |
251 |
match c with |
252 |
| Wtrue id -> |
253 |
{expr_tag = new_tag (); |
254 |
expr_desc=Expr_when (expr,id); |
255 |
expr_type = new_var (); |
256 |
expr_clock = Clocks.new_var true; |
257 |
expr_loc=loc} |
258 |
| Wfalse id -> |
259 |
{expr_tag = new_tag (); |
260 |
expr_desc=Expr_whennot (expr,id); |
261 |
expr_type = new_var (); |
262 |
expr_clock = Clocks.new_var true; |
263 |
expr_loc=loc}) |
264 |
dummy_id_expr cl |
265 |
in |
266 |
ignore (type_expr env false when_expr) |
267 |
|
268 |
let type_var_decl env vdecl = |
269 |
if (Env.exists_value env vdecl.var_id) then |
270 |
raise (Error (vdecl.var_loc,Already_bound vdecl.var_id)) |
271 |
else |
272 |
let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in |
273 |
let new_env = Env.add_value env vdecl.var_id ty in |
274 |
type_coreclock new_env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; |
275 |
vdecl.var_type <- ty; |
276 |
new_env |
277 |
|
278 |
let type_var_decl_list env l = |
279 |
List.fold_left type_var_decl env l |
280 |
|
281 |
let type_of_vlist vars = |
282 |
let tyl = List.map (fun v -> v.var_type) vars in |
283 |
type_of_type_list tyl |
284 |
|
285 |
(** [type_node env nd loc] types node [nd] in environment env. The |
286 |
location is used for error reports. *) |
287 |
let type_node env nd loc = |
288 |
let is_main = nd.node_id = !Options.main_node in |
289 |
let delta_env = type_var_decl_list IMap.empty nd.node_inputs in |
290 |
let delta_env = type_var_decl_list delta_env nd.node_outputs in |
291 |
let delta_env = type_var_decl_list delta_env nd.node_locals in |
292 |
let new_env = Env.overwrite env delta_env in |
293 |
let undefined_vars_init = |
294 |
List.fold_left |
295 |
(fun uvs v -> IMap.add v.var_id () uvs) |
296 |
IMap.empty (nd.node_outputs@nd.node_locals) in |
297 |
let undefined_vars = |
298 |
List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs |
299 |
in |
300 |
(* check that table is empty *) |
301 |
if (not (IMap.is_empty undefined_vars)) then |
302 |
raise (Error (loc,Undefined_var undefined_vars)); |
303 |
let ty_ins = type_of_vlist nd.node_inputs in |
304 |
let ty_outs = type_of_vlist nd.node_outputs in |
305 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
306 |
generalize ty_node; |
307 |
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) |
308 |
nd.node_type <- ty_node; |
309 |
Env.add_value env nd.node_id ty_node |
310 |
|
311 |
let type_imported_node env nd loc = |
312 |
let new_env = type_var_decl_list env nd.nodei_inputs in |
313 |
ignore(type_var_decl_list new_env nd.nodei_outputs); |
314 |
let ty_ins = type_of_vlist nd.nodei_inputs in |
315 |
let ty_outs = type_of_vlist nd.nodei_outputs in |
316 |
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in |
317 |
generalize ty_node; |
318 |
if (is_polymorphic ty_node) then |
319 |
raise (Error (loc, Poly_imported_node nd.nodei_id)); |
320 |
let new_env = Env.add_value env nd.nodei_id ty_node in |
321 |
nd.nodei_type <- ty_node; |
322 |
new_env |
323 |
|
324 |
let type_top_decl env decl = |
325 |
match decl.top_decl_desc with |
326 |
| Node nd -> |
327 |
type_node env nd decl.top_decl_loc |
328 |
| ImportedNode nd -> |
329 |
type_imported_node env nd decl.top_decl_loc |
330 |
| SensorDecl _ | ActuatorDecl _ | Consts _ -> env |
331 |
|
332 |
let type_top_consts env decl = |
333 |
match decl.top_decl_desc with |
334 |
| Consts clist -> |
335 |
List.fold_left (fun env (id, c) -> |
336 |
let ty = type_of_const c in |
337 |
Env.add_value env id ty |
338 |
) env clist |
339 |
| Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ -> env |
340 |
|
341 |
let type_prog env decls = |
342 |
let new_env = List.fold_left type_top_consts env decls in |
343 |
ignore(List.fold_left type_top_decl new_env decls) |
344 |
|
345 |
(* Local Variables: *) |
346 |
(* compile-command:"make -C .." *) |
347 |
(* End: *) |