lustrec / src / init_calculus.ml @ bde99c3f
History | View | Annotate | Download (11.1 KB)
1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|
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 | 22fe1c93 | ploc | |
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: *) |