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

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