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

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