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

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