lustrec / src / typing.ml @ b1655a21
History  View  Annotate  Download (28.1 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT  LIFL *) 
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 
(* This file was originally from the Prelude compiler *) 
11 
(* *) 
12 
(********************************************************************) 
13  
14 
(** Main typing module. Classic inference algorithm with destructive 
15 
unification. *) 
16  
17 
let debug fmt args = () (* Format.eprintf "%a" *) 
18 
(* Though it shares similarities with the clock calculus module, no code 
19 
is shared. Simple environments, very limited identifier scoping, no 
20 
identifier redefinition allowed. *) 
21  
22 
open Utils 
23 
(* Yes, opening both modules is dirty as some type names will be 
24 
overwritten, yet this makes notations far lighter.*) 
25 
open LustreSpec 
26 
open Corelang 
27 
open Types 
28 
open Format 
29  
30 
let pp_typing_env fmt env = 
31 
Env.pp_env print_ty fmt env 
32  
33 
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in 
34 
type [ty]. False otherwise. *) 
35 
let rec occurs tvar ty = 
36 
let ty = repr ty in 
37 
match ty.tdesc with 
38 
 Tvar > ty=tvar 
39 
 Tarrow (t1, t2) > 
40 
(occurs tvar t1)  (occurs tvar t2) 
41 
 Ttuple tl > 
42 
List.exists (occurs tvar) tl 
43 
 Tstruct fl > 
44 
List.exists (fun (f, t) > occurs tvar t) fl 
45 
 Tarray (_, t) 
46 
 Tstatic (_, t) 
47 
 Tclock t 
48 
 Tlink t > occurs tvar t 
49 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > 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 
 Tvar > 
56 
(* No scopes, always generalize *) 
57 
ty.tdesc < Tunivar 
58 
 Tarrow (t1,t2) > 
59 
generalize t1; generalize t2 
60 
 Ttuple tl > 
61 
List.iter generalize tl 
62 
 Tstruct fl > 
63 
List.iter (fun (f, t) > generalize t) fl 
64 
 Tstatic (d, t) 
65 
 Tarray (d, t) > Dimension.generalize d; generalize t 
66 
 Tclock t 
67 
 Tlink t > 
68 
generalize t 
69 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > () 
70  
71 
(** Downgrade polymorphic type variables to monomorphic type variables *) 
72 
let rec instantiate inst_vars inst_dim_vars ty = 
73 
let ty = repr ty in 
74 
match ty.tdesc with 
75 
 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat > ty 
76 
 Tarrow (t1,t2) > 
77 
{ty with tdesc = 
78 
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} 
79 
 Ttuple tlist > 
80 
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)} 
81 
 Tstruct flist > 
82 
{ty with tdesc = Tstruct (List.map (fun (f, t) > (f, instantiate inst_vars inst_dim_vars t)) flist)} 
83 
 Tclock t > 
84 
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)} 
85 
 Tstatic (d, t) > 
86 
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
87 
 Tarray (d, t) > 
88 
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
89 
 Tlink t > 
90 
(* should not happen *) 
91 
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)} 
92 
 Tunivar > 
93 
try 
94 
List.assoc ty.tid !inst_vars 
95 
with Not_found > 
96 
let var = new_var () in 
97 
inst_vars := (ty.tid, var)::!inst_vars; 
98 
var 
99  
100 
(* [type_coretype cty] types the type declaration [cty] *) 
101 
let rec type_coretype type_dim cty = 
102 
match (*get_repr_type*) cty with 
103 
 Tydec_any > new_var () 
104 
 Tydec_int > Type_predef.type_int 
105 
 Tydec_real > Type_predef.type_real 
106 
 Tydec_float > Type_predef.type_real 
107 
 Tydec_bool > Type_predef.type_bool 
108 
 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty) 
109 
 Tydec_const c > Type_predef.type_const c 
110 
 Tydec_enum tl > Type_predef.type_enum tl 
111 
 Tydec_struct fl > Type_predef.type_struct (List.map (fun (f, ty) > (f, type_coretype type_dim ty)) fl) 
112 
 Tydec_array (d, ty) > 
113 
begin 
114 
type_dim d; 
115 
Type_predef.type_array d (type_coretype type_dim ty) 
116 
end 
117  
118 
(* [coretype_type] is the reciprocal of [type_typecore] *) 
119 
let rec coretype_type ty = 
120 
match (repr ty).tdesc with 
121 
 Tvar > Tydec_any 
122 
 Tint > Tydec_int 
123 
 Treal > Tydec_real 
124 
 Tbool > Tydec_bool 
125 
 Tconst c > Tydec_const c 
126 
 Tclock t > Tydec_clock (coretype_type t) 
127 
 Tenum tl > Tydec_enum tl 
128 
 Tstruct fl > Tydec_struct (List.map (fun (f, t) > (f, coretype_type t)) fl) 
129 
 Tarray (d, t) > Tydec_array (d, coretype_type t) 
130 
 Tstatic (_, t) > coretype_type t 
131 
 _ > assert false 
132  
133 
let get_type_definition tname = 
134 
try 
135 
type_coretype (fun d > ()) (Hashtbl.find type_table (Tydec_const tname)) 
136 
with Not_found > raise (Error (Location.dummy_loc, Unbound_type tname)) 
137  
138 
(* Equality on ground types only *) 
139 
(* Should be used between local variables which must have a ground type *) 
140 
let rec eq_ground t1 t2 = 
141 
let t1 = repr t1 in 
142 
let t2 = repr t2 in 
143 
t1==t2  
144 
match t1.tdesc, t2.tdesc with 
145 
 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal > true 
146 
 Tenum tl, Tenum tl' when tl == tl' > true 
147 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > List.for_all2 eq_ground tl tl' 
148 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > List.for_all2 (fun (_, t) (_, t') > eq_ground t t') fl fl' 
149 
 (Tconst t, _) > 
150 
let def_t = get_type_definition t in 
151 
eq_ground def_t t2 
152 
 (_, Tconst t) > 
153 
let def_t = get_type_definition t in 
154 
eq_ground t1 def_t 
155 
 Tarrow (t1,t2), Tarrow (t1',t2') > eq_ground t1 t1' && eq_ground t2 t2' 
156 
 Tclock t1', Tclock t2' > eq_ground t1' t2' 
157 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
158 
 Tarray (e1, t1'), Tarray (e2, t2') > Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' 
159 
 _ > false 
160  
161 
(** [unify t1 t2] unifies types [t1] and [t2] 
162 
using standard destructive unification. 
163 
Raises [Unify (t1,t2)] if the types are not unifiable. 
164 
[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type, 
165 
so in case of unification error: expected type [t1], got type [t2]. 
166 
If [sub]typing is allowed, [t2] may be a subtype of [t1]. 
167 
If [semi] unification is required, 
168 
[t1] should furthermore be an instance of [t2] 
169 
and constants are handled differently.*) 
170 
let unify ?(sub=false) ?(semi=false) t1 t2 = 
171 
let rec unif t1 t2 = 
172 
let t1 = repr t1 in 
173 
let t2 = repr t2 in 
174 
if t1==t2 then 
175 
() 
176 
else 
177 
match t1.tdesc,t2.tdesc with 
178 
(* strictly subtyping cases first *) 
179 
 _ , Tclock t2 when sub && (get_clock_base_type t1 = None) > 
180 
unif t1 t2 
181 
 _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) > 
182 
unif t1 t2 
183 
(* This case is not mandatory but will keep "older" types *) 
184 
 Tvar, Tvar > 
185 
if t1.tid < t2.tid then 
186 
t2.tdesc < Tlink t1 
187 
else 
188 
t1.tdesc < Tlink t2 
189 
 Tvar, _ when (not semi) && (not (occurs t1 t2)) > 
190 
t1.tdesc < Tlink t2 
191 
 _, Tvar when (not (occurs t2 t1)) > 
192 
t2.tdesc < Tlink t1 
193 
 Tarrow (t1,t2), Tarrow (t1',t2') > 
194 
begin 
195 
unif t2 t2'; 
196 
unif t1' t1 
197 
end 
198 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 
199 
List.iter2 unif tl tl' 
200 
 Ttuple [t1] , _ > unif t1 t2 
201 
 _ , Ttuple [t2] > unif t1 t2 
202 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 
203 
List.iter2 (fun (_, t) (_, t') > unif t t') fl fl' 
204 
 Tclock _, Tstatic _ 
205 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 
206 
 Tclock t1', Tclock t2' > unif t1' t2' 
207 
 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal 
208 
 Tunivar, _  _, Tunivar > () 
209 
 (Tconst t, _) > 
210 
let def_t = get_type_definition t in 
211 
unif def_t t2 
212 
 (_, Tconst t) > 
213 
let def_t = get_type_definition t in 
214 
unif t1 def_t 
215 
 Tenum tl, Tenum tl' when tl == tl' > () 
216 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
217 
 Tarray (e1, t1'), Tarray (e2, t2') > 
218 
let eval_const = 
219 
if semi 
220 
then (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) 
221 
else (fun c > None) in 
222 
begin 
223 
unif t1' t2'; 
224 
Dimension.eval Basic_library.eval_env eval_const e1; 
225 
Dimension.eval Basic_library.eval_env eval_const e2; 
226 
Dimension.unify ~semi:semi e1 e2; 
227 
end 
228 
 _,_ > raise (Unify (t1, t2)) 
229 
in unif t1 t2 
230  
231 
(* Expected type ty1, got type ty2 *) 
232 
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc = 
233 
try 
234 
unify ~sub:sub ~semi:semi ty1 ty2 
235 
with 
236 
 Unify _ > 
237 
raise (Error (loc, Type_clash (ty1,ty2))) 
238 
 Dimension.Unify _ > 
239 
raise (Error (loc, Type_clash (ty1,ty2))) 
240  
241 
let rec type_struct_const_field loc (label, c) = 
242 
if Hashtbl.mem field_table label 
243 
then let tydec = Hashtbl.find field_table label in 
244 
let tydec_struct = get_struct_type_fields tydec in 
245 
let ty_label = type_coretype (fun d > ()) (List.assoc label tydec_struct) in 
246 
begin 
247 
try_unify ty_label (type_const loc c) loc; 
248 
type_coretype (fun d > ()) tydec 
249 
end 
250 
else raise (Error (loc, Unbound_value ("struct field " ^ label))) 
251  
252 
and type_const loc c = 
253 
match c with 
254 
 Const_int _ > Type_predef.type_int 
255 
 Const_real _ > Type_predef.type_real 
256 
 Const_float _ > Type_predef.type_real 
257 
 Const_array ca > let d = Dimension.mkdim_int loc (List.length ca) in 
258 
let ty = new_var () in 
259 
List.iter (fun e > try_unify ty (type_const loc e) loc) ca; 
260 
Type_predef.type_array d ty 
261 
 Const_tag t > 
262 
if Hashtbl.mem tag_table t 
263 
then type_coretype (fun d > ()) (Hashtbl.find tag_table t) 
264 
else raise (Error (loc, Unbound_value ("enum tag " ^ t))) 
265 
 Const_struct fl > 
266 
let ty_struct = new_var () in 
267 
begin 
268 
let used = 
269 
List.fold_left 
270 
(fun acc (l, c) > 
271 
if List.mem l acc 
272 
then raise (Error (loc, Already_bound ("struct field " ^ l))) 
273 
else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc) 
274 
[] fl in 
275 
try 
276 
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in 
277 
(* List.iter (fun l > Format.eprintf "total: %s@." l) total; 
278 
List.iter (fun l > Format.eprintf "used: %s@." l) used; *) 
279 
let undef = List.find (fun l > not (List.mem l used)) total 
280 
in raise (Error (loc, Unbound_value ("struct field " ^ undef))) 
281 
with Not_found > 
282 
ty_struct 
283 
end 
284 
 Const_string _ > assert false (* string should only appear in annotations *) 
285  
286 
(* The following typing functions take as parameter an environment [env] 
287 
and whether the element being typed is expected to be constant [const]. 
288 
[env] is a pair composed of: 
289 
 a map from ident to type, associating to each ident, i.e. 
290 
variables, constants and (imported) nodes, its type including whether 
291 
it is constant or not. This latter information helps in checking constant 
292 
propagation policy in Lustre. 
293 
 a vdecl list, in order to modify types of declared variables that are 
294 
later discovered to be clocks during the typing process. 
295 
*) 
296 
let check_constant loc const_expected const_real = 
297 
if const_expected && not const_real 
298 
then raise (Error (loc, Not_a_constant)) 
299  
300 
let rec type_add_const env const arg targ = 
301 
if const 
302 
then let d = 
303 
if is_dimension_type targ 
304 
then dimension_of_expr arg 
305 
else Dimension.mkdim_var () in 
306 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 
307 
Dimension.eval Basic_library.eval_env eval_const d; 
308 
let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in 
309 
(match Types.get_static_value targ with 
310 
 None > () 
311 
 Some d' > try_unify targ real_static_type arg.expr_loc); 
312 
real_static_type 
313 
else targ 
314  
315 
(* emulates a subtyping relation between types t and (d : t), 
316 
used during node applications and assignments *) 
317 
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = 
318 
let loc = real_arg.expr_loc in 
319 
let const = const  (Types.get_static_value formal_type <> None) in 
320 
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in 
321 
(*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;*) 
322 
try_unify ~sub:sub formal_type real_type loc 
323  
324 
and type_ident env in_main loc const id = 
325 
type_expr env in_main const (expr_of_ident id loc) 
326  
327 
(* typing an application implies: 
328 
 checking that const formal parameters match real const (maybe symbolic) arguments 
329 
 checking type adequation between formal and real arguments 
330 
An application may embed an homomorphic/internal function, in which case we need to split 
331 
it in many calls 
332 
*) 
333 
and type_appl env in_main loc const f args = 
334 
let targs = List.map (type_expr env in_main const) args in 
335 
if Basic_library.is_internal_fun f && List.exists is_tuple_type targs 
336 
then 
337 
try 
338 
let targs = Utils.transpose_list (List.map type_list_of_type targs) in 
339 
Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs) 
340 
with 
341 
Utils.TransposeError (l, l') > raise (Error (loc, WrongMorphism (l, l'))) 
342 
else 
343 
type_dependent_call env in_main loc const f (List.combine args targs) 
344  
345 
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *) 
346 
and type_dependent_call env in_main loc const f targs = 
347 
let tins, touts = new_var (), new_var () in 
348 
let tfun = Type_predef.type_arrow tins touts in 
349 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
350 
let tins = type_list_of_type tins in 
351 
if List.length targs <> List.length tins then 
352 
raise (Error (loc, WrongArity (List.length tins, List.length targs))) 
353 
else 
354 
begin 
355 
List.iter2 (fun (a,t) ti > 
356 
let t' = type_add_const env (const  Types.get_static_value ti <> None) a t 
357 
in try_unify ~sub:true ti t' a.expr_loc) targs tins; 
358 
touts 
359 
end 
360  
361 
(* type a simple call without dependent types 
362 
but possible homomorphic extension. 
363 
[targs] is here a list of arguments' types. *) 
364 
and type_simple_call env in_main loc const f targs = 
365 
let tins, touts = new_var (), new_var () in 
366 
let tfun = Type_predef.type_arrow tins touts in 
367 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
368 
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*) 
369 
try_unify ~sub:true tins (type_of_type_list targs) loc; 
370 
touts 
371  
372 
(** [type_expr env in_main expr] types expression [expr] in environment 
373 
[env], expecting it to be [const] or not. *) 
374 
and type_expr env in_main const expr = 
375 
let resulting_ty = 
376 
match expr.expr_desc with 
377 
 Expr_const c > 
378 
let ty = type_const expr.expr_loc c in 
379 
let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in 
380 
expr.expr_type < ty; 
381 
ty 
382 
 Expr_ident v > 
383 
let tyv = 
384 
try 
385 
Env.lookup_value (fst env) v 
386 
with Not_found > 
387 
Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr; 
388 
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) 
389 
in 
390 
let ty = instantiate (ref []) (ref []) tyv in 
391 
let ty' = 
392 
if const 
393 
then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ()) 
394 
else new_var () in 
395 
try_unify ty ty' expr.expr_loc; 
396 
expr.expr_type < ty; 
397 
ty 
398 
 Expr_array elist > 
399 
let ty_elt = new_var () in 
400 
List.iter (fun e > try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist; 
401 
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in 
402 
let ty = Type_predef.type_array d ty_elt in 
403 
expr.expr_type < ty; 
404 
ty 
405 
 Expr_access (e1, d) > 
406 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; 
407 
let ty_elt = new_var () in 
408 
let d = Dimension.mkdim_var () in 
409 
type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt); 
410 
expr.expr_type < ty_elt; 
411 
ty_elt 
412 
 Expr_power (e1, d) > 
413 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 
414 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; 
415 
Dimension.eval Basic_library.eval_env eval_const d; 
416 
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
417 
let ty = Type_predef.type_array d ty_elt in 
418 
expr.expr_type < ty; 
419 
ty 
420 
 Expr_tuple elist > 
421 
let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in 
422 
expr.expr_type < ty; 
423 
ty 
424 
 Expr_ite (c, t, e) > 
425 
type_subtyping_arg env in_main const c Type_predef.type_bool; 
426 
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in 
427 
expr.expr_type < ty; 
428 
ty 
429 
 Expr_appl (id, args, r) > 
430 
(* application of non internal function is not legal in a constant 
431 
expression *) 
432 
(match r with 
433 
 None > () 
434 
 Some (x, l) > 
435 
check_constant expr.expr_loc const false; 
436 
let expr_x = expr_of_ident x expr.expr_loc in 
437 
let typ_l = 
438 
Type_predef.type_clock 
439 
(type_const expr.expr_loc (Const_tag l)) in 
440 
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); 
441 
let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in 
442 
expr.expr_type < touts; 
443 
touts 
444 
 Expr_fby (e1,e2) 
445 
 Expr_arrow (e1,e2) > 
446 
(* fby/arrow is not legal in a constant expression *) 
447 
check_constant expr.expr_loc const false; 
448 
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in 
449 
expr.expr_type < ty; 
450 
ty 
451 
 Expr_pre e > 
452 
(* pre is not legal in a constant expression *) 
453 
check_constant expr.expr_loc const false; 
454 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in 
455 
expr.expr_type < ty; 
456 
ty 
457 
 Expr_when (e1,c,l) > 
458 
(* when is not legal in a constant expression *) 
459 
check_constant expr.expr_loc const false; 
460 
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in 
461 
let expr_c = expr_of_ident c expr.expr_loc in 
462 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
463 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
464 
expr.expr_type < ty; 
465 
ty 
466 
 Expr_merge (c,hl) > 
467 
(* merge is not legal in a constant expression *) 
468 
check_constant expr.expr_loc const false; 
469 
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in 
470 
let expr_c = expr_of_ident c expr.expr_loc in 
471 
let typ_l = Type_predef.type_clock typ_in in 
472 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
473 
expr.expr_type < typ_out; 
474 
typ_out 
475 
in 
476 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty); 
477 
resulting_ty 
478  
479 
and type_branches env in_main loc const hl = 
480 
let typ_in = new_var () in 
481 
let typ_out = new_var () in 
482 
try 
483 
let used_labels = 
484 
List.fold_left (fun accu (t, h) > 
485 
unify typ_in (type_const loc (Const_tag t)); 
486 
type_subtyping_arg env in_main const h typ_out; 
487 
if List.mem t accu 
488 
then raise (Error (loc, Already_bound t)) 
489 
else t :: accu) [] hl in 
490 
let type_labels = get_enum_type_tags (coretype_type typ_in) in 
491 
if List.sort compare used_labels <> List.sort compare type_labels 
492 
then let unbound_tag = List.find (fun t > not (List.mem t used_labels)) type_labels in 
493 
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) 
494 
else (typ_in, typ_out) 
495 
with Unify (t1, t2) > 
496 
raise (Error (loc, Type_clash (t1,t2))) 
497  
498 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
499 
let type_eq env in_main undefined_vars eq = 
500 
(* Check undefined variables, type lhs *) 
501 
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 
502 
let ty_lhs = type_expr env in_main false expr_lhs in 
503 
(* Check multiple variable definitions *) 
504 
let define_var id uvars = 
505 
try 
506 
ignore(IMap.find id uvars); 
507 
IMap.remove id uvars 
508 
with Not_found > 
509 
raise (Error (eq.eq_loc, Already_defined id)) 
510 
in 
511 
(* check assignment of declared constant, assignment of clock *) 
512 
let ty_lhs = 
513 
type_of_type_list 
514 
(List.map2 (fun ty id > 
515 
if get_static_value ty <> None 
516 
then raise (Error (eq.eq_loc, Assigned_constant id)) else 
517 
match get_clock_base_type ty with 
518 
 None > ty 
519 
 Some ty > ty) 
520 
(type_list_of_type ty_lhs) eq.eq_lhs) in 
521 
let undefined_vars = 
522 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in 
523 
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned 
524 
to a (always nonconstant) lhs variable *) 
525 
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; 
526 
undefined_vars 
527  
528  
529 
(* [type_coreclock env ck id loc] types the type clock declaration [ck] 
530 
in environment [env] *) 
531 
let type_coreclock env ck id loc = 
532 
match ck.ck_dec_desc with 
533 
 Ckdec_any  Ckdec_pclock (_,_) > () 
534 
 Ckdec_bool cl > 
535 
let dummy_id_expr = expr_of_ident id loc in 
536 
let when_expr = 
537 
List.fold_left 
538 
(fun expr (x, l) > 
539 
{expr_tag = new_tag (); 
540 
expr_desc= Expr_when (expr,x,l); 
541 
expr_type = new_var (); 
542 
expr_clock = Clocks.new_var true; 
543 
expr_delay = Delay.new_var (); 
544 
expr_loc=loc; 
545 
expr_annot = None}) 
546 
dummy_id_expr cl 
547 
in 
548 
ignore (type_expr env false false when_expr) 
549  
550 
let rec check_type_declaration loc cty = 
551 
match cty with 
552 
 Tydec_clock ty 
553 
 Tydec_array (_, ty) > check_type_declaration loc ty 
554 
 Tydec_const tname > 
555 
if not (Hashtbl.mem type_table cty) 
556 
then raise (Error (loc, Unbound_type tname)); 
557 
 _ > () 
558  
559 
let type_var_decl vd_env env vdecl = 
560 
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; 
561 
let eval_const id = Types.get_static_value (Env.lookup_value env id) in 
562 
let type_dim d = 
563 
begin 
564 
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int; 
565 
Dimension.eval Basic_library.eval_env eval_const d; 
566 
end in 
567 
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in 
568 
let ty_status = 
569 
if vdecl.var_dec_const 
570 
then Type_predef.type_static (Dimension.mkdim_var ()) ty 
571 
else ty in 
572 
let new_env = Env.add_value env vdecl.var_id ty_status in 
573 
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; 
574 
vdecl.var_type < ty_status; 
575 
new_env 
576  
577 
let type_var_decl_list vd_env env l = 
578 
List.fold_left (type_var_decl vd_env) env l 
579  
580 
let type_of_vlist vars = 
581 
let tyl = List.map (fun v > v.var_type) vars in 
582 
type_of_type_list tyl 
583  
584 
let add_vdecl vd_env vdecl = 
585 
if List.exists (fun v > v.var_id = vdecl.var_id) vd_env 
586 
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) 
587 
else vdecl::vd_env 
588  
589 
let check_vd_env vd_env = 
590 
ignore (List.fold_left add_vdecl [] vd_env) 
591  
592 
(** [type_node env nd loc] types node [nd] in environment env. The 
593 
location is used for error reports. *) 
594 
let type_node env nd loc = 
595 
let is_main = nd.node_id = !Options.main_node in 
596 
let vd_env_ol = nd.node_outputs@nd.node_locals in 
597 
let vd_env = nd.node_inputs@vd_env_ol in 
598 
check_vd_env vd_env; 
599 
let init_env = env in 
600 
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in 
601 
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in 
602 
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in 
603 
let new_env = Env.overwrite env delta_env in 
604 
let undefined_vars_init = 
605 
List.fold_left 
606 
(fun uvs v > IMap.add v.var_id () uvs) 
607 
IMap.empty vd_env_ol in 
608 
let undefined_vars = 
609 
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs 
610 
in 
611 
(* Typing asserts *) 
612 
List.iter (fun assert_ > 
613 
let assert_expr = assert_.assert_expr in 
614 
type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool 
615 
) nd.node_asserts; 
616 

617 
(* check that table is empty *) 
618 
if (not (IMap.is_empty undefined_vars)) then 
619 
raise (Error (loc, Undefined_var undefined_vars)); 
620 
let ty_ins = type_of_vlist nd.node_inputs in 
621 
let ty_outs = type_of_vlist nd.node_outputs in 
622 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
623 
generalize ty_node; 
624 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
625 
nd.node_type < ty_node; 
626 
Env.add_value env nd.node_id ty_node 
627  
628 
let type_imported_node env nd loc = 
629 
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in 
630 
let vd_env = nd.nodei_inputs@nd.nodei_outputs in 
631 
check_vd_env vd_env; 
632 
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs); 
633 
let ty_ins = type_of_vlist nd.nodei_inputs in 
634 
let ty_outs = type_of_vlist nd.nodei_outputs in 
635 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
636 
generalize ty_node; 
637 
(* 
638 
if (is_polymorphic ty_node) then 
639 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
640 
*) 
641 
let new_env = Env.add_value env nd.nodei_id ty_node in 
642 
nd.nodei_type < ty_node; 
643 
new_env 
644  
645 
let type_top_consts env clist = 
646 
List.fold_left (fun env cdecl > 
647 
let ty = type_const cdecl.const_loc cdecl.const_value in 
648 
let d = 
649 
if is_dimension_type ty 
650 
then dimension_of_const cdecl.const_loc cdecl.const_value 
651 
else Dimension.mkdim_var () in 
652 
let ty = Type_predef.type_static d ty in 
653 
let new_env = Env.add_value env cdecl.const_id ty in 
654 
cdecl.const_type < ty; 
655 
new_env) env clist 
656  
657 
let type_top_decl env decl = 
658 
match decl.top_decl_desc with 
659 
 Node nd > ( 
660 
try 
661 
type_node env nd decl.top_decl_loc 
662 
with Error (loc, err) as exc > ( 
663 
if !Options.global_inline then 
664 
Format.eprintf "Type error: failing node@.%a@.@?" 
665 
Printers.pp_node nd 
666 
; 
667 
raise exc) 
668 
) 
669 
 ImportedNode nd > 
670 
type_imported_node env nd decl.top_decl_loc 
671 
 Consts clist > 
672 
type_top_consts env clist 
673 
 Type _ 
674 
 Open _ > env 
675  
676 
let type_prog env decls = 
677 
try 
678 
List.fold_left type_top_decl env decls 
679 
with Failure _ as exc > raise exc 
680  
681 
(* Once the Lustre program is fully typed, 
682 
we must get back to the original description of dimensions, 
683 
with constant parameters, instead of unifiable internal variables. *) 
684  
685 
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types, 
686 
i.e. replacing unifiable second_order variables with the original static parameters. 
687 
Once restored in this formulation, dimensions may be meaningfully printed. 
688 
*) 
689 
let uneval_vdecl_generics vdecl = 
690 
if vdecl.var_dec_const 
691 
then 
692 
match get_static_value vdecl.var_type with 
693 
 None > (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false) 
694 
 Some d > Dimension.uneval vdecl.var_id d 
695  
696 
let uneval_node_generics vdecls = 
697 
List.iter uneval_vdecl_generics vdecls 
698  
699 
let uneval_top_generics decl = 
700 
match decl.top_decl_desc with 
701 
 Node nd > 
702 
uneval_node_generics (nd.node_inputs @ nd.node_outputs) 
703 
 ImportedNode nd > 
704 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
705 
 Consts _ 
706 
 Type _ 
707 
 Open _ > () 
708  
709 
let uneval_prog_generics prog = 
710 
List.iter uneval_top_generics prog 
711  
712 
let rec get_imported_node decls id = 
713 
match decls with 
714 
 [] > assert false 
715 
 decl::q > 
716 
(match decl.top_decl_desc with 
717 
 ImportedNode nd when id = nd.nodei_id > decl 
718 
 _ > get_imported_node q id) 
719  
720 
let check_env_compat header declared computed = 
721 
uneval_prog_generics header; 
722 
Env.iter declared (fun k decl_type_k > 
723 
let computed_t = instantiate (ref []) (ref []) 
724 
(try Env.lookup_value computed k 
725 
with Not_found > 
726 
let loc = (get_imported_node header k).top_decl_loc in 
727 
raise (Error (loc, Declared_but_undefined k))) in 
728 
(*Types.print_ty Format.std_formatter decl_type_k; 
729 
Types.print_ty Format.std_formatter computed_t;*) 
730 
try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc 
731 
) 
732 
let check_typedef_top decl = 
733 
match decl.top_decl_desc with 
734 
 Type ty > 
735 
Format.eprintf "check_typedef %a %a@." Printers.pp_var_type_dec_desc ty.ty_def_desc Printers.pp_var_type_dec_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id)); 
736 
if coretype_equal ty.ty_def_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id)) then () 
737 
else raise (Error (decl.top_decl_loc, Type_mismatch ty.ty_def_id)) 
738 
 _ > () 
739  
740 
let check_typedef_compat header = 
741 
List.iter check_typedef_top header 
742  
743 
(* Local Variables: *) 
744 
(* compilecommand:"make C .." *) 
745 
(* End: *) 