lustrec / src / init_calculus.ml @ ba2f9fa1
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 sideeffects *) 
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 
(* compilecommand:"make C .." *) 
347 
(* End: *) 