lustrec / src / init_calculus.ml @ 22fe1c93
History  View  Annotate  Download (11.5 KB)
1 
(*  

2 
* SchedMCore  A MultiCore Scheduling Framework 
3 
* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE 
4 
* 
5 
* This file is part of Prelude 
6 
* 
7 
* Prelude is free software; you can redistribute it and/or 
8 
* modify it under the terms of the GNU Lesser General Public License 
9 
* as published by the Free Software Foundation ; either version 2 of 
10 
* the License, or (at your option) any later version. 
11 
* 
12 
* Prelude is distributed in the hope that it will be useful, but 
13 
* WITHOUT ANY WARRANTY ; without even the implied warranty of 
14 
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 
15 
* Lesser General Public License for more details. 
16 
* 
17 
* You should have received a copy of the GNU Lesser General Public 
18 
* License along with this program ; if not, write to the Free Software 
19 
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307 
20 
* USA 
21 
* *) 
22  
23 
(** Main typing module. Classic inference algorithm with destructive 
24 
unification. *) 
25  
26 
(* Though it shares similarities with the clock calculus module, no code 
27 
is shared. Simple environments, very limited identifier scoping, no 
28 
identifier redefinition allowed. *) 
29  
30 
open Utils 
31 
(* Yes, opening both modules is dirty as some type names will be 
32 
overwritten, yet this makes notations far lighter.*) 
33 
open Corelang 
34 
open Init 
35 
open Format 
36  
37 
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in 
38 
type [ty]. False otherwise. *) 
39 
let rec occurs tvar ty = 
40 
let ty = repr ty in 
41 
match ty.tdesc with 
42 
 Ivar > ty=tvar 
43 
 Iarrow (t1, t2) > 
44 
(occurs tvar t1)  (occurs tvar t2) 
45 
 Ituple tl > 
46 
List.exists (occurs tvar) tl 
47 
 Ilink t > occurs tvar t 
48 
 Isucc t > occurs tvar t 
49 
 Iunivar > false 
50  
51 
(** Promote monomorphic type variables to polymorphic type variables. *) 
52 
(* Generalize by sideeffects *) 
53 
let rec generalize ty = 
54 
match ty.tdesc with 
55 
 Ivar > 
56 
(* No scopes, always generalize *) 
57 
ty.idesc < Iunivar 
58 
 Iarrow (t1,t2) > 
59 
generalize t1; generalize t2 
60 
 Ituple tlist > 
61 
List.iter generalize tlist 
62 
 Ilink t > 
63 
generalize t 
64 
 Isucc t > 
65 
generalize t 
66 
 Tunivar > () 
67  
68 
(** Downgrade polymorphic type variables to monomorphic type variables *) 
69 
let rec instanciate inst_vars ty = 
70 
let ty = repr ty in 
71 
match ty.idesc with 
72 
 Ivar > ty 
73 
 Iarrow (t1,t2) > 
74 
{ty with idesc = 
75 
Iarrow ((instanciate inst_vars t1), (instanciate inst_vars t2))} 
76 
 Ituple tlist > 
77 
{ty with idesc = Ituple (List.map (instanciate inst_vars) tlist)} 
78 
 Isucc t > 
79 
(* should not happen *) 
80 
{ty with idesc = Isucc (instanciate inst_vars t)} 
81 
 Ilink t > 
82 
(* should not happen *) 
83 
{ty with idesc = Ilink (instanciate inst_vars t)} 
84 
 Iunivar > 
85 
try 
86 
List.assoc ty.iid !inst_vars 
87 
with Not_found > 
88 
let var = new_var () in 
89 
inst_vars := (ty.iid, var)::!inst_vars; 
90 
var 
91  
92 
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify 
93 
(t1,t2)] if the types are not unifiable.*) 
94  
95 
(* Standard destructive unification *) 
96 
(* may loop for omega types *) 
97 
let rec unify t1 t2 = 
98 
let t1 = repr t1 in 
99 
let t2 = repr t2 in 
100 
if t1=t2 then 
101 
() 
102 
else 
103 
(* No type abbreviations resolution for now *) 
104 
match t1.idesc,t2.idesc with 
105 
(* This case is not mandory but will keep "older" types *) 
106 
 Ivar, Ivar > 
107 
if t1.iid < t2.iid then 
108 
t2.idesc < Ilink t1 
109 
else 
110 
t1.idesc < Ilink t2 
111 
 (Ivar, _) when (not (occurs t1 t2)) > 
112 
t1.idesc < Ilink t2 
113 
 (_,Ivar) when (not (occurs t2 t1)) > 
114 
t2.idesc < Ilink t1 
115 
 Isucc t1, Isucc t1' > unify t1 t1' 
116 
 Iarrow (t1,t2), Iarrow (t1',t2') > 
117 
unify t1 t1'; unify t2 t2' 
118 
 Ituple tlist1, Ituple tlist2 > 
119 
if (List.length tlist1) <> (List.length tlist2) then 
120 
raise (Unify (t1, t2)) 
121 
else 
122 
List.iter2 unify tlist1 tlist2 
123 
 Iunivar,_  _, Iunivar > 
124 
() 
125 
 _,_ > raise (Unify (t1, t2)) 
126  
127 
let init_of_const c = 
128 
Init_predef.init_zero 
129  
130 
let rec init_expect env in_main expr ty = 
131 
let texpr = init_expr env in_main expr in 
132 
try 
133 
unify texpr ty 
134 
with Unify (t1,t2) > 
135 
raise (Error (expr.expr_loc, Init_clash (t1,t2))) 
136  
137 
and init_ident env in_main id loc = 
138 
init_expr env in_main (expr_of_ident id loc) 
139  
140 
(** [type_expr env in_main expr] types expression [expr] in environment 
141 
[env]. *) 
142 
and init_expr env in_main expr = 
143 
match expr.expr_desc with 
144 
 Expr_const c > 
145 
let ty = init_of_const c in 
146 
expr.expr_init < ty; 
147 
ty 
148 
 Expr_ident v > 
149 
let tyv = 
150 
try 
151 
Env.lookup_value env v 
152 
with Not_found > 
153 
raise (Error (expr.expr_loc, Unbound_value v)) 
154 
in 
155 
let ty = instanciate (ref []) tyv in 
156 
expr.expr_init < ty; 
157 
ty 
158 
 Expr_tuple elist > 
159 
let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in 
160 
expr.expr_init < ty; 
161 
ty 
162 
 Expr_appl (id, args, r) > 
163 
(match r with 
164 
 None > () 
165 
 Some x > let expr_x = expr_of_ident x expr.expr_loc in 
166 
init_expect env in_main expr_x Init_predef.init_zero); 
167 
let tfun = type_ident env in_main id expr.expr_loc in 
168 
let tins,touts= split_arrow tfun in 
169 
type_expect env in_main args tins; 
170 
expr.expr_type < touts; 
171 
touts 
172 
 Expr_arrow (e1,e2) > 
173 
let ty = type_expr env in_main e1 in 
174 
type_expect env in_main e2 ty; 
175 
expr.expr_type < ty; 
176 
ty 
177 
 Expr_fby (init,e) > 
178 
let ty = type_of_const init in 
179 
type_expect env in_main e ty; 
180 
expr.expr_type < ty; 
181 
ty 
182 
 Expr_concat (hd,e) > 
183 
let ty = type_of_const hd in 
184 
type_expect env in_main e ty; 
185 
expr.expr_type < ty; 
186 
ty 
187 
 Expr_tail e > 
188 
let ty = type_expr env in_main e in 
189 
expr.expr_type < ty; 
190 
ty 
191 
 Expr_pre e > 
192 
let ty = type_expr env in_main e in 
193 
expr.expr_type < ty; 
194 
ty 
195 
 Expr_when (e1,c)  Expr_whennot (e1,c) > 
196 
let expr_c = expr_of_ident c expr.expr_loc in 
197 
type_expect env in_main expr_c Type_predef.type_bool; 
198 
let tlarg = type_expr env in_main e1 in 
199 
expr.expr_type < tlarg; 
200 
tlarg 
201 
 Expr_merge (c,e2,e3) > 
202 
let expr_c = expr_of_ident c expr.expr_loc in 
203 
type_expect env in_main expr_c Type_predef.type_bool; 
204 
let te2 = type_expr env in_main e2 in 
205 
type_expect env in_main e3 te2; 
206 
expr.expr_type < te2; 
207 
te2 
208 
 Expr_uclock (e,k)  Expr_dclock (e,k) > 
209 
let ty = type_expr env in_main e in 
210 
expr.expr_type < ty; 
211 
ty 
212 
 Expr_phclock (e,q) > 
213 
let ty = type_expr env in_main e in 
214 
expr.expr_type < ty; 
215 
ty 
216  
217 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
218 
let type_eq env in_main undefined_vars eq = 
219 
(* Check multiple variable definitions *) 
220 
let define_var id uvars = 
221 
try 
222 
ignore(IMap.find id uvars); 
223 
IMap.remove id uvars 
224 
with Not_found > 
225 
raise (Error (eq.eq_loc, Already_defined id)) 
226 
in 
227 
let undefined_vars = 
228 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in 
229 
(* Type lhs *) 
230 
let get_value_type id = 
231 
try 
232 
Env.lookup_value env id 
233 
with Not_found > 
234 
raise (Error (eq.eq_loc, Unbound_value id)) 
235 
in 
236 
let tyl_lhs = List.map get_value_type eq.eq_lhs in 
237 
let ty_lhs = type_of_type_list tyl_lhs in 
238 
(* Type rhs *) 
239 
type_expect env in_main eq.eq_rhs ty_lhs; 
240 
undefined_vars 
241  
242 
(* [type_coretype cty] types the type declaration [cty] *) 
243 
let type_coretype cty = 
244 
match cty with 
245 
 Tydec_any > new_var () 
246 
 Tydec_int > Type_predef.type_int 
247 
 Tydec_real > Type_predef.type_real 
248 
 Tydec_float > Type_predef.type_real 
249 
 Tydec_bool > Type_predef.type_bool 
250 
 Tydec_clock > Type_predef.type_clock 
251  
252 
(* [type_coreclock env ck id loc] types the type clock declaration [ck] 
253 
in environment [env] *) 
254 
let type_coreclock env ck id loc = 
255 
match ck.ck_dec_desc with 
256 
 Ckdec_any  Ckdec_pclock (_,_) > () 
257 
 Ckdec_bool cl > 
258 
let dummy_id_expr = expr_of_ident id loc in 
259 
let when_expr = 
260 
List.fold_left 
261 
(fun expr c > 
262 
match c with 
263 
 Wtrue id > 
264 
{expr_tag = new_tag (); 
265 
expr_desc=Expr_when (expr,id); 
266 
expr_type = new_var (); 
267 
expr_clock = Clocks.new_var true; 
268 
expr_loc=loc} 
269 
 Wfalse id > 
270 
{expr_tag = new_tag (); 
271 
expr_desc=Expr_whennot (expr,id); 
272 
expr_type = new_var (); 
273 
expr_clock = Clocks.new_var true; 
274 
expr_loc=loc}) 
275 
dummy_id_expr cl 
276 
in 
277 
ignore (type_expr env false when_expr) 
278  
279 
let type_var_decl env vdecl = 
280 
if (Env.exists_value env vdecl.var_id) then 
281 
raise (Error (vdecl.var_loc,Already_bound vdecl.var_id)) 
282 
else 
283 
let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in 
284 
let new_env = Env.add_value env vdecl.var_id ty in 
285 
type_coreclock new_env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; 
286 
vdecl.var_type < ty; 
287 
new_env 
288  
289 
let type_var_decl_list env l = 
290 
List.fold_left type_var_decl env l 
291  
292 
let type_of_vlist vars = 
293 
let tyl = List.map (fun v > v.var_type) vars in 
294 
type_of_type_list tyl 
295 

296 
(** [type_node env nd loc] types node [nd] in environment env. The 
297 
location is used for error reports. *) 
298 
let type_node env nd loc = 
299 
let is_main = nd.node_id = !Options.main_node in 
300 
let delta_env = type_var_decl_list IMap.empty nd.node_inputs in 
301 
let delta_env = type_var_decl_list delta_env nd.node_outputs in 
302 
let delta_env = type_var_decl_list delta_env nd.node_locals in 
303 
let new_env = Env.overwrite env delta_env in 
304 
let undefined_vars_init = 
305 
List.fold_left 
306 
(fun uvs v > IMap.add v.var_id () uvs) 
307 
IMap.empty (nd.node_outputs@nd.node_locals) in 
308 
let undefined_vars = 
309 
List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs 
310 
in 
311 
(* check that table is empty *) 
312 
if (not (IMap.is_empty undefined_vars)) then 
313 
raise (Error (loc,Undefined_var undefined_vars)); 
314 
let ty_ins = type_of_vlist nd.node_inputs in 
315 
let ty_outs = type_of_vlist nd.node_outputs in 
316 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
317 
generalize ty_node; 
318 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
319 
nd.node_type < ty_node; 
320 
Env.add_value env nd.node_id ty_node 
321  
322 
let type_imported_node env nd loc = 
323 
let new_env = type_var_decl_list env nd.nodei_inputs in 
324 
ignore(type_var_decl_list new_env nd.nodei_outputs); 
325 
let ty_ins = type_of_vlist nd.nodei_inputs in 
326 
let ty_outs = type_of_vlist nd.nodei_outputs in 
327 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
328 
generalize ty_node; 
329 
if (is_polymorphic ty_node) then 
330 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
331 
let new_env = Env.add_value env nd.nodei_id ty_node in 
332 
nd.nodei_type < ty_node; 
333 
new_env 
334  
335 
let type_top_decl env decl = 
336 
match decl.top_decl_desc with 
337 
 Node nd > 
338 
type_node env nd decl.top_decl_loc 
339 
 ImportedNode nd > 
340 
type_imported_node env nd decl.top_decl_loc 
341 
 SensorDecl _  ActuatorDecl _  Consts _ > env 
342  
343 
let type_top_consts env decl = 
344 
match decl.top_decl_desc with 
345 
 Consts clist > 
346 
List.fold_left (fun env (id, c) > 
347 
let ty = type_of_const c in 
348 
Env.add_value env id ty 
349 
) env clist 
350 
 Node _  ImportedNode _  SensorDecl _  ActuatorDecl _ > env 
351  
352 
let type_prog env decls = 
353 
let new_env = List.fold_left type_top_consts env decls in 
354 
ignore(List.fold_left type_top_decl new_env decls) 
355  
356 
(* Local Variables: *) 
357 
(* compilecommand:"make C .." *) 
358 
(* End: *) 