lustrec / src / typing.ml @ 2196a0a6
History  View  Annotate  Download (30.4 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 
let debug fmt args = () (* Format.eprintf "%a" *) 
27 
(* Though it shares similarities with the clock calculus module, no code 
28 
is shared. Simple environments, very limited identifier scoping, no 
29 
identifier redefinition allowed. *) 
30  
31 
open Utils 
32 
(* Yes, opening both modules is dirty as some type names will be 
33 
overwritten, yet this makes notations far lighter.*) 
34 
open Corelang 
35 
open Types 
36 
open Format 
37  
38 
let pp_typing_env fmt env = 
39 
Env.pp_env print_ty fmt env 
40  
41 
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in 
42 
type [ty]. False otherwise. *) 
43 
let rec occurs tvar ty = 
44 
let ty = repr ty in 
45 
match ty.tdesc with 
46 
 Tvar > ty=tvar 
47 
 Tarrow (t1, t2) > 
48 
(occurs tvar t1)  (occurs tvar t2) 
49 
 Ttuple tl > 
50 
List.exists (occurs tvar) tl 
51 
 Tstruct fl > 
52 
List.exists (fun (f, t) > occurs tvar t) fl 
53 
 Tarray (_, t) 
54 
 Tstatic (_, t) 
55 
 Tclock t 
56 
 Tlink t > occurs tvar t 
57 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Tstring  Trat > false 
58  
59 
(** Promote monomorphic type variables to polymorphic type variables. *) 
60 
(* Generalize by sideeffects *) 
61 
let rec generalize ty = 
62 
match ty.tdesc with 
63 
 Tvar > 
64 
(* No scopes, always generalize *) 
65 
ty.tdesc < Tunivar 
66 
 Tarrow (t1,t2) > 
67 
generalize t1; generalize t2 
68 
 Ttuple tl > 
69 
List.iter generalize tl 
70 
 Tstruct fl > 
71 
List.iter (fun (f, t) > generalize t) fl 
72 
 Tstatic (d, t) 
73 
 Tarray (d, t) > Dimension.generalize d; generalize t 
74 
 Tclock t 
75 
 Tlink t > 
76 
generalize t 
77 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat  Tstring > () 
78  
79 
(** Downgrade polymorphic type variables to monomorphic type variables *) 
80 
let rec instantiate inst_vars inst_dim_vars ty = 
81 
let ty = repr ty in 
82 
match ty.tdesc with 
83 
 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat  Tstring > ty 
84 
 Tarrow (t1,t2) > 
85 
{ty with tdesc = 
86 
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} 
87 
 Ttuple tlist > 
88 
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)} 
89 
 Tstruct flist > 
90 
{ty with tdesc = Tstruct (List.map (fun (f, t) > (f, instantiate inst_vars inst_dim_vars t)) flist)} 
91 
 Tclock t > 
92 
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)} 
93 
 Tstatic (d, t) > 
94 
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
95 
 Tarray (d, t) > 
96 
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
97 
 Tlink t > 
98 
(* should not happen *) 
99 
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)} 
100 
 Tunivar > 
101 
try 
102 
List.assoc ty.tid !inst_vars 
103 
with Not_found > 
104 
let var = new_var () in 
105 
inst_vars := (ty.tid, var)::!inst_vars; 
106 
var 
107  
108 
(* [type_coretype cty] types the type declaration [cty] *) 
109 
let rec type_coretype type_dim cty = 
110 
match (*get_repr_type*) cty with 
111 
 Tydec_any > new_var () 
112 
 Tydec_int > Type_predef.type_int 
113 
 Tydec_real > Type_predef.type_real 
114 
 Tydec_float > Type_predef.type_real 
115 
 Tydec_bool > Type_predef.type_bool 
116 
 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty) 
117 
 Tydec_const c > Type_predef.type_const c 
118 
 Tydec_enum tl > Type_predef.type_enum tl 
119 
 Tydec_struct fl > Type_predef.type_struct (List.map (fun (f, ty) > (f, type_coretype type_dim ty)) fl) 
120 
 Tydec_array (d, ty) > 
121 
begin 
122 
type_dim d; 
123 
Type_predef.type_array d (type_coretype type_dim ty) 
124 
end 
125  
126 
(* [coretype_type] is the reciprocal of [type_typecore] *) 
127 
let rec coretype_type ty = 
128 
match (repr ty).tdesc with 
129 
 Tvar > Tydec_any 
130 
 Tint > Tydec_int 
131 
 Treal > Tydec_real 
132 
 Tbool > Tydec_bool 
133 
 Tconst c > Tydec_const c 
134 
 Tclock t > Tydec_clock (coretype_type t) 
135 
 Tenum tl > Tydec_enum tl 
136 
 Tstruct fl > Tydec_struct (List.map (fun (f, t) > (f, coretype_type t)) fl) 
137 
 Tarray (d, t) > Tydec_array (d, coretype_type t) 
138 
 Tstatic (_, t) > coretype_type t 
139 
 _ > assert false 
140  
141 
let get_type_definition tname = 
142 
try 
143 
type_coretype (fun d > ()) (Hashtbl.find type_table (Tydec_const tname)) 
144 
with Not_found > raise (Error (Location.dummy_loc, Unbound_type tname)) 
145  
146 
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify 
147 
(t1,t2)] if the types are not unifiable.*) 
148 
(* Standard destructive unification *) 
149 
let rec unify t1 t2 = 
150 
let t1 = repr t1 in 
151 
let t2 = repr t2 in 
152 
if t1=t2 then 
153 
() 
154 
else 
155 
(* No type abbreviations resolution for now *) 
156 
match t1.tdesc,t2.tdesc with 
157 
(* This case is not mandory but will keep "older" types *) 
158 
 Tvar, Tvar > 
159 
if t1.tid < t2.tid then 
160 
t2.tdesc < Tlink t1 
161 
else 
162 
t1.tdesc < Tlink t2 
163 
 (Tvar, _) when (not (occurs t1 t2)) > 
164 
t1.tdesc < Tlink t2 
165 
 (_,Tvar) when (not (occurs t2 t1)) > 
166 
t2.tdesc < Tlink t1 
167 
 Tarrow (t1,t2), Tarrow (t1',t2') > 
168 
begin 
169 
unify t1 t1'; 
170 
unify t2 t2' 
171 
end 
172 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 
173 
List.iter2 unify tl tl' 
174 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 
175 
List.iter2 (fun (_, t) (_, t') > unify t t') fl fl' 
176 
 Tclock _, Tstatic _ 
177 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 
178 
 Tclock t1', _ > unify t1' t2 
179 
 _, Tclock t2' > unify t1 t2' 
180 
 Tint, Tint  Tbool, Tbool  Trat, Trat 
181 
 Tunivar, _  _, Tunivar > () 
182 
 (Tconst t, _) > 
183 
let def_t = get_type_definition t in 
184 
unify def_t t2 
185 
 (_, Tconst t) > 
186 
let def_t = get_type_definition t in 
187 
unify t1 def_t 
188 
 Tenum tl, Tenum tl' when tl == tl' > () 
189 
 Tstruct fl, Tstruct fl' when fl == fl' > () 
190 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
191 
 Tarray (e1, t1'), Tarray (e2, t2') > 
192 
begin 
193 
unify t1' t2'; 
194 
Dimension.eval Basic_library.eval_env (fun c > None) e1; 
195 
Dimension.eval Basic_library.eval_env (fun c > None) e2; 
196 
Dimension.unify e1 e2; 
197 
end 
198 
 _,_ > raise (Unify (t1, t2)) 
199  
200 
(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify 
201 
(t1,t2)] if the types are not semiunifiable.*) 
202 
(* Standard destructive semiunification *) 
203 
let rec semi_unify t1 t2 = 
204 
let t1 = repr t1 in 
205 
let t2 = repr t2 in 
206 
if t1=t2 then 
207 
() 
208 
else 
209 
(* No type abbreviations resolution for now *) 
210 
match t1.tdesc,t2.tdesc with 
211 
(* This case is not mandory but will keep "older" types *) 
212 
 Tvar, Tvar > 
213 
if t1.tid < t2.tid then 
214 
t2.tdesc < Tlink t1 
215 
else 
216 
t1.tdesc < Tlink t2 
217 
 (Tvar, _) > raise (Unify (t1, t2)) 
218 
 (_,Tvar) when (not (occurs t2 t1)) > 
219 
t2.tdesc < Tlink t1 
220 
 Tarrow (t1,t2), Tarrow (t1',t2') > 
221 
begin 
222 
semi_unify t1 t1'; 
223 
semi_unify t2 t2' 
224 
end 
225 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 
226 
List.iter2 semi_unify tl tl' 
227 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 
228 
List.iter2 (fun (_, t) (_, t') > semi_unify t t') fl fl' 
229 
 Tclock _, Tstatic _ 
230 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 
231 
 Tclock t1', _ > semi_unify t1' t2 
232 
 _, Tclock t2' > semi_unify t1 t2' 
233 
 Tint, Tint  Tbool, Tbool  Trat, Trat 
234 
 Tunivar, _  _, Tunivar > () 
235 
 (Tconst t, _) > 
236 
let def_t = get_type_definition t in 
237 
semi_unify def_t t2 
238 
 (_, Tconst t) > 
239 
let def_t = get_type_definition t in 
240 
semi_unify t1 def_t 
241 
 Tenum tl, Tenum tl' when tl == tl' > () 
242  
243 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
244 
 Tarray (e1, t1'), Tarray (e2, t2') > 
245 
begin 
246 
semi_unify t1' t2'; 
247 
Dimension.eval Basic_library.eval_env (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) e1; 
248 
Dimension.eval Basic_library.eval_env (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) e2; 
249 
Dimension.semi_unify e1 e2; 
250 
end 
251 
 _,_ > raise (Unify (t1, t2)) 
252  
253 
(* Expected type ty1, got type ty2 *) 
254 
let try_unify ty1 ty2 loc = 
255 
try 
256 
unify ty1 ty2 
257 
with 
258 
 Unify _ > 
259 
raise (Error (loc, Type_clash (ty1,ty2))) 
260 
 Dimension.Unify _ > 
261 
raise (Error (loc, Type_clash (ty1,ty2))) 
262  
263 
let try_semi_unify ty1 ty2 loc = 
264 
try 
265 
semi_unify ty1 ty2 
266 
with 
267 
 Unify _ > 
268 
raise (Error (loc, Type_clash (ty1,ty2))) 
269 
 Dimension.Unify _ > 
270 
raise (Error (loc, Type_clash (ty1,ty2))) 
271  
272 
(* ty1 is a subtype of ty2 *) 
273 
let rec sub_unify sub ty1 ty2 = 
274 
match (repr ty1).tdesc, (repr ty2).tdesc with 
275 
 Ttuple [t1] , Ttuple [t2] > sub_unify sub t1 t2 
276 
 Ttuple tl1 , Ttuple tl2 > 
277 
if List.length tl1 <> List.length tl2 
278 
then raise (Unify (ty1, ty2)) 
279 
else List.iter2 (sub_unify sub) tl1 tl2 
280 
 Ttuple [t1] , _ > sub_unify sub t1 ty2 
281 
 _ , Ttuple [t2] > sub_unify sub ty1 t2 
282 
 Tstruct tl1 , Tstruct tl2 > 
283 
if List.map fst tl1 <> List.map fst tl2 
284 
then raise (Unify (ty1, ty2)) 
285 
else List.iter2 (fun (_, t1) (_, t2) > sub_unify sub t1 t2) tl1 tl2 
286 
 Tstatic (d1, t1) , Tstatic (d2, t2) > 
287 
begin 
288 
sub_unify sub t1 t2; 
289 
Dimension.eval Basic_library.eval_env (fun c > None) d1; 
290 
Dimension.eval Basic_library.eval_env (fun c > None) d2; 
291 
Dimension.unify d1 d2 
292 
end 
293 
 Tstatic (r_d, t1) , _ when sub > sub_unify sub ty2 t1 
294 
 _ > unify ty2 ty1 
295  
296 
let try_sub_unify sub ty1 ty2 loc = 
297 
try 
298 
sub_unify sub ty1 ty2 
299 
with 
300 
 Unify _ > 
301 
raise (Error (loc, Type_clash (ty1,ty2))) 
302 
 Dimension.Unify _ > 
303 
raise (Error (loc, Type_clash (ty1,ty2))) 
304  
305 
let rec type_struct_const_field loc (label, c) = 
306 
if Hashtbl.mem field_table label 
307 
then let tydec = Hashtbl.find field_table label in 
308 
let tydec_struct = get_struct_type_fields tydec in 
309 
let ty_label = type_coretype (fun d > ()) (List.assoc label tydec_struct) in 
310 
begin 
311 
try_unify ty_label (type_const loc c) loc; 
312 
type_coretype (fun d > ()) tydec 
313 
end 
314 
else raise (Error (loc, Unbound_value ("struct field " ^ label))) 
315  
316 
and type_const loc c = 
317 
match c with 
318 
 Const_int _ > Type_predef.type_int 
319 
 Const_real _ > Type_predef.type_real 
320 
 Const_float _ > Type_predef.type_real 
321 
 Const_array ca > let d = Dimension.mkdim_int loc (List.length ca) in 
322 
let ty = new_var () in 
323 
List.iter (fun e > try_unify ty (type_const loc e) loc) ca; 
324 
Type_predef.type_array d ty 
325 
 Const_tag t > 
326 
if Hashtbl.mem tag_table t 
327 
then type_coretype (fun d > ()) (Hashtbl.find tag_table t) 
328 
else raise (Error (loc, Unbound_value ("enum tag " ^ t))) 
329 
 Const_string _ > Type_predef.type_string 
330 
 Const_struct fl > 
331 
let ty_struct = new_var () in 
332 
begin 
333 
let used = 
334 
List.fold_left 
335 
(fun acc (l, c) > 
336 
if List.mem l acc 
337 
then raise (Error (loc, Already_bound ("struct field " ^ l))) 
338 
else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc) 
339 
[] fl in 
340 
try 
341 
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in 
342 
(* List.iter (fun l > Format.eprintf "total: %s@." l) total; 
343 
List.iter (fun l > Format.eprintf "used: %s@." l) used; *) 
344 
let undef = List.find (fun l > not (List.mem l used)) total 
345 
in raise (Error (loc, Unbound_value ("struct field " ^ undef))) 
346 
with Not_found > 
347 
ty_struct 
348 
end 
349  
350 
(* The following typing functions take as parameter an environment [env] 
351 
and whether the element being typed is expected to be constant [const]. 
352 
[env] is a pair composed of: 
353 
 a map from ident to type, associating to each ident, i.e. 
354 
variables, constants and (imported) nodes, its type including whether 
355 
it is constant or not. This latter information helps in checking constant 
356 
propagation policy in Lustre. 
357 
 a vdecl list, in order to modify types of declared variables that are 
358 
later discovered to be clocks during the typing process. 
359 
*) 
360 
let check_constant loc const_expected const_real = 
361 
if const_expected && not const_real 
362 
then raise (Error (loc, Not_a_constant)) 
363  
364 
let rec type_standard_args env in_main const expr_list = 
365 
let ty_list = List.map (fun e > dynamic_type (type_expr env in_main const e)) expr_list in 
366 
let ty_res = new_var () in 
367 
List.iter2 (fun e ty > try_unify ty_res ty e.expr_loc) expr_list ty_list; 
368 
ty_res 
369  
370 
(* emulates a subtyping relation between types t and (d : t), 
371 
used during node applications and assignments *) 
372 
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = 
373 
let loc = real_arg.expr_loc in 
374 
let const = const  (Types.get_static_value formal_type <> None) in 
375 
let real_type = type_expr env in_main const real_arg in 
376 
let real_type = 
377 
if const 
378 
then let d = 
379 
if is_dimension_type real_type 
380 
then dimension_of_expr real_arg 
381 
else Dimension.mkdim_var () in 
382 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 
383 
Dimension.eval Basic_library.eval_env eval_const d; 
384 
let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in 
385 
(match Types.get_static_value real_type with 
386 
 None > () 
387 
 Some d' > try_unify real_type real_static_type loc); 
388 
real_static_type 
389 
else real_type in 
390 
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*) 
391 
try_sub_unify sub real_type formal_type loc 
392 
(* 
393 
and type_subtyping_tuple loc real_type formal_type = 
394 
let real_types = type_list_of_type real_type in 
395 
let formal_types = type_list_of_type formal_type in 
396 
if (List.length real_types) <> (List.length formal_types) 
397 
then raise (Unify (real_type, formal_type)) 
398 
else List.iter2 (type_subtyping loc sub) real_types formal_types 
399  
400 
and type_subtyping loc sub real_type formal_type = 
401 
match (repr real_type).tdesc, (repr formal_type).tdesc with 
402 
 Tstatic _ , Tstatic _ when sub > try_unify formal_type real_type loc 
403 
 Tstatic (r_d, r_ty), _ when sub > try_unify formal_type r_ty loc 
404 
 _ > try_unify formal_type real_type loc 
405 
*) 
406 
and type_ident env in_main loc const id = 
407 
type_expr env in_main const (expr_of_ident id loc) 
408  
409 
(* typing an application implies: 
410 
 checking that const formal parameters match real const (maybe symbolic) arguments 
411 
 checking type adequation between formal and real arguments 
412 
*) 
413 
and type_appl env in_main loc const f args = 
414 
let tfun = type_ident env in_main loc const f in 
415 
(* Format.eprintf "Typing function call %s: %a@.@?" f print_ty tfun ; *) 
416 
let tins, touts = split_arrow tfun in 
417 
let tins = type_list_of_type tins in 
418 
let args = expr_list_of_expr args in 
419 
List.iter2 (type_subtyping_arg env in_main const) args tins; 
420 
touts 
421  
422 
(** [type_expr env in_main expr] types expression [expr] in environment 
423 
[env], expecting it to be [const] or not. *) 
424 
and type_expr env in_main const expr = 
425 
(* Format.eprintf "Typing expr: %a@.@?" Printers.pp_expr expr; *) 
426 
let res = 
427 
match expr.expr_desc with 
428 
 Expr_const c > 
429 
(* Format.eprintf "const@.@?"; *) 
430 
let ty = type_const expr.expr_loc c in 
431 
let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in 
432 
expr.expr_type < ty; 
433 
ty 
434 
 Expr_ident v > 
435 
(* Format.eprintf "ident@.@?"; *) 
436 
let tyv = 
437 
try 
438 
Env.lookup_value (fst env) v 
439 
with Not_found > 
440 
Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr; 
441 
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) 
442 
in 
443 
let ty = instantiate (ref []) (ref []) tyv in 
444 
let ty' = 
445 
if const 
446 
then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ()) 
447 
else new_var () in 
448 
try_unify ty ty' expr.expr_loc; 
449 
expr.expr_type < ty; 
450 
ty 
451 
 Expr_array elist > 
452 
let ty_elt = type_standard_args env in_main const elist in 
453 
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in 
454 
let ty = Type_predef.type_array d ty_elt in 
455 
expr.expr_type < ty; 
456 
ty 
457 
 Expr_access (e1, d) > 
458 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; 
459 
let ty_elt = new_var () in 
460 
let d = Dimension.mkdim_var () in 
461 
type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt); 
462 
expr.expr_type < ty_elt; 
463 
ty_elt 
464 
 Expr_power (e1, d) > 
465 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 
466 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; 
467 
Dimension.eval Basic_library.eval_env eval_const d; 
468 
let ty_elt = type_standard_args env in_main const [e1] in 
469 
let ty = Type_predef.type_array d ty_elt in 
470 
expr.expr_type < ty; 
471 
ty 
472 
 Expr_tuple elist > 
473 
(* Format.eprintf "const@.@?"; *) 
474 
let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in 
475 
expr.expr_type < ty; 
476 
ty 
477 
 Expr_ite (c, t, e) > 
478 
type_subtyping_arg env in_main const c Type_predef.type_bool; 
479 
let ty = type_standard_args env in_main const [t; e] in 
480 
expr.expr_type < ty; 
481 
ty 
482 
 Expr_appl (id, args, r) > 
483 
(* Format.eprintf "app %s@.@?" id; *) 
484 
(* application of non internal function is not legal in a constant 
485 
expression *) 
486 
(match r with 
487 
 None > () 
488 
 Some (x, l) > 
489 
check_constant expr.expr_loc const false; 
490 
let expr_x = expr_of_ident x expr.expr_loc in 
491 
let typ_l = 
492 
Type_predef.type_clock 
493 
(type_const expr.expr_loc (Const_tag l)) in 
494 
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); 
495 
let touts = type_appl env in_main expr.expr_loc const id args in 
496 
expr.expr_type < touts; 
497 
touts 
498 
 Expr_fby (e1,e2) 
499 
 Expr_arrow (e1,e2) > 
500 
(* fby/arrow is not legal in a constant expression *) 
501 
check_constant expr.expr_loc const false; 
502 
let ty = type_standard_args env in_main const [e1; e2] in 
503 
expr.expr_type < ty; 
504 
ty 
505 
 Expr_pre e > 
506 
(* pre is not legal in a constant expression *) 
507 
check_constant expr.expr_loc const false; 
508 
let ty = type_standard_args env in_main const [e] in 
509 
expr.expr_type < ty; 
510 
ty 
511 
 Expr_when (e1,c,l) > 
512 
(* when is not legal in a constant expression *) 
513 
check_constant expr.expr_loc const false; 
514 
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in 
515 
let expr_c = expr_of_ident c expr.expr_loc in 
516 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
517 
update_clock env in_main c expr.expr_loc typ_l; 
518 
let ty = type_standard_args env in_main const [e1] in 
519 
expr.expr_type < ty; 
520 
ty 
521 
 Expr_merge (c,hl) > 
522 
(* merge is not legal in a constant expression *) 
523 
check_constant expr.expr_loc const false; 
524 
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in 
525 
let expr_c = expr_of_ident c expr.expr_loc in 
526 
let typ_l = Type_predef.type_clock typ_in in 
527 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
528 
update_clock env in_main c expr.expr_loc typ_l; 
529 
expr.expr_type < typ_out; 
530 
typ_out 
531 
 Expr_uclock (e,k)  Expr_dclock (e,k) > 
532 
let ty = type_expr env in_main const e in 
533 
expr.expr_type < ty; 
534 
ty 
535 
 Expr_phclock (e,q) > 
536 
let ty = type_expr env in_main const e in 
537 
expr.expr_type < ty; 
538 
ty 
539 
in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res 
540  
541 
and type_branches env in_main loc const hl = 
542 
let typ_in = new_var () in 
543 
let typ_out = new_var () in 
544 
try 
545 
let used_labels = 
546 
List.fold_left (fun accu (t, h) > 
547 
unify typ_in (type_const loc (Const_tag t)); 
548 
type_subtyping_arg env in_main const h typ_out; 
549 
if List.mem t accu 
550 
then raise (Error (loc, Already_bound t)) 
551 
else t :: accu) [] hl in 
552 
let type_labels = get_enum_type_tags (coretype_type typ_in) in 
553 
if List.sort compare used_labels <> List.sort compare type_labels 
554 
then let unbound_tag = List.find (fun t > not (List.mem t used_labels)) type_labels in 
555 
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) 
556 
else (typ_in, typ_out) 
557 
with Unify (t1, t2) > 
558 
raise (Error (loc, Type_clash (t1,t2))) 
559  
560 
and update_clock env in_main id loc typ = 
561 
(*Log.report ~level:1 (fun fmt > Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*) 
562 
try 
563 
let vdecl = List.find (fun v > v.var_id = id) (snd env) 
564 
in vdecl.var_type < typ 
565 
with 
566 
Not_found > 
567 
raise (Error (loc, Unbound_value ("clock " ^ id))) 
568  
569 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
570 
let type_eq env in_main undefined_vars eq = 
571 
(* Check undefined variables, type lhs *) 
572 
let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs) in 
573 
let ty_lhs = type_expr env in_main false expr_lhs in 
574 
(* Check multiple variable definitions *) 
575 
let define_var id uvars = 
576 
try 
577 
ignore(IMap.find id uvars); 
578 
IMap.remove id uvars 
579 
with Not_found > 
580 
raise (Error (eq.eq_loc, Already_defined id)) 
581 
in 
582 
let undefined_vars = 
583 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in 
584 
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned 
585 
to a (always nonconstant) lhs variable *) 
586 
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; 
587 
undefined_vars 
588  
589  
590 
(* [type_coreclock env ck id loc] types the type clock declaration [ck] 
591 
in environment [env] *) 
592 
let type_coreclock env ck id loc = 
593 
match ck.ck_dec_desc with 
594 
 Ckdec_any  Ckdec_pclock (_,_) > () 
595 
 Ckdec_bool cl > 
596 
let dummy_id_expr = expr_of_ident id loc in 
597 
let when_expr = 
598 
List.fold_left 
599 
(fun expr (x, l) > 
600 
{expr_tag = new_tag (); 
601 
expr_desc= Expr_when (expr,x,l); 
602 
expr_type = new_var (); 
603 
expr_clock = Clocks.new_var true; 
604 
expr_delay = Delay.new_var (); 
605 
expr_loc=loc; 
606 
expr_annot = None}) 
607 
dummy_id_expr cl 
608 
in 
609 
ignore (type_expr env false false when_expr) 
610  
611 
let rec check_type_declaration loc cty = 
612 
match cty with 
613 
 Tydec_clock ty 
614 
 Tydec_array (_, ty) > check_type_declaration loc ty 
615 
 Tydec_const tname > 
616 
if not (Hashtbl.mem type_table cty) 
617 
then raise (Error (loc, Unbound_type tname)); 
618 
 _ > () 
619  
620 
let type_var_decl vd_env env vdecl = 
621 
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; 
622 
let eval_const id = Types.get_static_value (Env.lookup_value env id) in 
623 
let type_dim d = 
624 
begin 
625 
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int; 
626 
Dimension.eval Basic_library.eval_env eval_const d; 
627 
end in 
628 
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in 
629 
let ty_status = 
630 
if vdecl.var_dec_const 
631 
then Type_predef.type_static (Dimension.mkdim_var ()) ty 
632 
else ty in 
633 
let new_env = Env.add_value env vdecl.var_id ty_status in 
634 
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; 
635 
vdecl.var_type < ty_status; 
636 
new_env 
637  
638 
let type_var_decl_list vd_env env l = 
639 
List.fold_left (type_var_decl vd_env) env l 
640  
641 
let type_of_vlist vars = 
642 
let tyl = List.map (fun v > v.var_type) vars in 
643 
type_of_type_list tyl 
644  
645 
let add_vdecl vd_env vdecl = 
646 
if List.exists (fun v > v.var_id = vdecl.var_id) vd_env 
647 
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) 
648 
else vdecl::vd_env 
649  
650 
let check_vd_env vd_env = 
651 
ignore (List.fold_left add_vdecl [] vd_env) 
652  
653 
let type_eexpr (env, vdecl) ee = 
654 
let quantified_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in 
655 
let env = type_var_decl_list vdecl env quantified_vars in 
656 
let ty = type_expr (env, vdecl) false (* not in main *) false (* not in const *) ee.eexpr_qfexpr in 
657 
ee.eexpr_type < ty 
658  
659 
let type_spec env ns = 
660 
let type_ee_list l = List.iter (fun e > ignore (type_eexpr env e) ) l in 
661 
let type_beh (_, req, ens, beh_loc) = 
662 
type_ee_list req; type_ee_list ens 
663 
in 
664 
List.iter type_beh (("default", ns.requires, ns.ensures, ns.spec_loc)::ns.behaviors) 
665  
666 
let type_annot env na = 
667 
List.iter (fun (_, ee) > type_eexpr env ee) na.annots 
668  
669 
(** [type_node env nd loc] types node [nd] in environment env. The 
670 
location is used for error reports. *) 
671 
let type_node env nd loc = 
672 
let is_main = nd.node_id = !Options.main_node in 
673 
let vd_env_ol = nd.node_outputs@nd.node_locals in 
674 
let vd_env = nd.node_inputs@vd_env_ol in 
675 
check_vd_env vd_env; 
676 
let init_env = env in 
677 
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in 
678 
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in 
679  
680 
(* Typing specification *) 
681 
let _ = 
682 
match nd.node_spec with 
683 
 Some ns > ( 
684 
try 
685 
(* Format.eprintf "Typing specification: %a@.@?" *) 
686 
(* Printers.pp_spec ns; *) 
687 
type_spec (delta_env, vd_env) ns 
688 
with _ as exc > ( 
689 
Format.eprintf "Error typing specification: %a@." 
690 
Printers.pp_spec ns; 
691 
raise exc 
692 
) 
693 
) 
694 
 None > () 
695 
in 
696  
697 
(* Typing node content *) 
698 
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in 
699 
let new_env = Env.overwrite env delta_env in 
700 
let undefined_vars_init = 
701 
List.fold_left 
702 
(fun uvs v > IMap.add v.var_id () uvs) 
703 
IMap.empty vd_env_ol in 
704 
let undefined_vars = 
705 
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs 
706 
in 
707 
(* check that table is empty *) 
708 
if (not (IMap.is_empty undefined_vars)) then 
709 
raise (Error (loc, Undefined_var undefined_vars)); 
710 

711 
(* Typing node annotations *) 
712 
let _ = List.map (fun ann > 
713 
type_annot (new_env, vd_env) ann 
714 
) nd.node_annot in 
715  
716 
let ty_ins = type_of_vlist nd.node_inputs in 
717 
let ty_outs = type_of_vlist nd.node_outputs in 
718 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
719 
generalize ty_node; 
720 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
721 
nd.node_type < ty_node; 
722 
(* Format.eprintf "Node %s type is %a@." nd.node_id Types.print_ty ty_node; *) 
723 
Env.add_value env nd.node_id ty_node 
724  
725 
let type_imported_node env nd loc = 
726 
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in 
727 
let vd_env = nd.nodei_inputs@nd.nodei_outputs in 
728 
check_vd_env vd_env; 
729 
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs); 
730 
let ty_ins = type_of_vlist nd.nodei_inputs in 
731 
let ty_outs = type_of_vlist nd.nodei_outputs in 
732 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
733 
generalize ty_node; 
734 
(* 
735 
if (is_polymorphic ty_node) then 
736 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
737 
*) 
738 
let new_env = Env.add_value env nd.nodei_id ty_node in 
739 
nd.nodei_type < ty_node; 
740 
new_env 
741  
742 
let type_imported_fun env nd loc = 
743 
let new_env = type_var_decl_list nd.fun_inputs env nd.fun_inputs in 
744 
let vd_env = nd.fun_inputs@nd.fun_outputs in 
745 
check_vd_env vd_env; 
746 
ignore(type_var_decl_list vd_env new_env nd.fun_outputs); 
747 
let ty_ins = type_of_vlist nd.fun_inputs in 
748 
let ty_outs = type_of_vlist nd.fun_outputs in 
749 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
750 
generalize ty_node; 
751 
(* 
752 
if (is_polymorphic ty_node) then 
753 
raise (Error (loc, Poly_imported_node nd.fun_id)); 
754 
*) 
755 
let new_env = Env.add_value env nd.fun_id ty_node in 
756 
nd.fun_type < ty_node; 
757 
new_env 
758  
759 
let type_top_consts env clist = 
760 
List.fold_left (fun env cdecl > 
761 
let ty = type_const cdecl.const_loc cdecl.const_value in 
762 
let d = 
763 
if is_dimension_type ty 
764 
then dimension_of_const cdecl.const_loc cdecl.const_value 
765 
else Dimension.mkdim_var () in 
766 
let ty = Type_predef.type_static d ty in 
767 
let new_env = Env.add_value env cdecl.const_id ty in 
768 
cdecl.const_type < ty; 
769 
new_env) env clist 
770  
771 
let type_top_decl env decl = 
772 
match decl.top_decl_desc with 
773 
 Node nd > ( 
774 
try 
775 
type_node env nd decl.top_decl_loc 
776 
with Error (loc, err) as exc > ( 
777 
if !Options.global_inline then 
778 
Format.eprintf "Type error: failing node@.%a@.@?" 
779 
Printers.pp_node nd 
780 
; 
781 
raise exc) 
782 
) 
783 
 ImportedNode nd > 
784 
type_imported_node env nd decl.top_decl_loc 
785 
 ImportedFun nd > 
786 
type_imported_fun env nd decl.top_decl_loc 
787 
 Consts clist > 
788 
type_top_consts env clist 
789 
 Open _ > env 
790  
791 
let type_prog env decls = 
792 
try 
793 
List.fold_left type_top_decl env decls 
794 
with Failure _ as exc > raise exc 
795  
796 
(* Once the Lustre program is fully typed, 
797 
we must get back to the original description of dimensions, 
798 
with constant parameters, instead of unifiable internal variables. *) 
799  
800 
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types, 
801 
i.e. replacing unifiable second_order variables with the original static parameters. 
802 
Once restored in this formulation, dimensions may be meaningfully printed. 
803 
*) 
804 
let uneval_vdecl_generics vdecl = 
805 
if vdecl.var_dec_const 
806 
then 
807 
match get_static_value vdecl.var_type with 
808 
 None > (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false) 
809 
 Some d > Dimension.uneval vdecl.var_id d 
810  
811 
let uneval_node_generics vdecls = 
812 
List.iter uneval_vdecl_generics vdecls 
813  
814 
let uneval_top_generics decl = 
815 
match decl.top_decl_desc with 
816 
 Node nd > 
817 
uneval_node_generics (nd.node_inputs @ nd.node_outputs) 
818 
 ImportedNode nd > 
819 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
820 
 ImportedFun nd > 
821 
() 
822 
 Consts clist > () 
823 
 Open _ > () 
824  
825 
let uneval_prog_generics prog = 
826 
List.iter uneval_top_generics prog 
827  
828 
let check_env_compat header declared computed = 
829 
uneval_prog_generics header; 
830 
Env.iter declared (fun k decl_type_k > 
831 
let computed_t = instantiate (ref []) (ref []) (Env.lookup_value computed k) in 
832 
(*Types.print_ty Format.std_formatter decl_type_k; 
833 
Types.print_ty Format.std_formatter computed_t;*) 
834 
try_semi_unify decl_type_k computed_t Location.dummy_loc 
835 
) 
836  
837 
(* Local Variables: *) 
838 
(* compilecommand:"make C .." *) 
839 
(* End: *) 