lustrec / src / typing.ml @ 19a1e66b
History  View  Annotate  Download (37.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 Lustre_types 
26 
open Corelang 
27 
open Format 
28  
29  
30 
module type EXPR_TYPE_HUB = 
31 
sig 
32 
type type_expr 
33 
val import: Types.Main.type_expr > type_expr 
34 
val export: type_expr > Types.Main.type_expr 
35 
end 
36  
37 
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) = 
38 
struct 
39  
40 
module TP = Type_predef.Make (T) 
41 
include TP 
42 

43 
let pp_typing_env fmt env = 
44 
Env.pp_env print_ty fmt env 
45  
46 
(****************************************************************) 
47 
(* Generic functions: occurs, instantiate and generalize *) 
48 
(****************************************************************) 
49 

50 
(** [occurs tvar ty] returns true if the type variable [tvar] 
51 
occurs in type [ty]. False otherwise. *) 
52 
let rec occurs tvar ty = 
53 
let ty = repr ty in 
54 
match type_desc ty with 
55 
 Tvar > ty=tvar 
56 
 Tarrow (t1, t2) > 
57 
(occurs tvar t1)  (occurs tvar t2) 
58 
 Ttuple tl > 
59 
List.exists (occurs tvar) tl 
60 
 Tstruct fl > 
61 
List.exists (fun (f, t) > occurs tvar t) fl 
62 
 Tarray (_, t) 
63 
 Tstatic (_, t) 
64 
 Tclock t 
65 
 Tlink t > occurs tvar t 
66 
 Tenum _  Tconst _  Tunivar  Tbasic _ > false 
67  
68 
(** Promote monomorphic type variables to polymorphic type 
69 
variables. *) 
70 
(* Generalize by sideeffects *) 
71 
let rec generalize ty = 
72 
match type_desc ty with 
73 
 Tvar > 
74 
(* No scopes, always generalize *) 
75 
ty.tdesc < Tunivar 
76 
 Tarrow (t1,t2) > 
77 
generalize t1; generalize t2 
78 
 Ttuple tl > 
79 
List.iter generalize tl 
80 
 Tstruct fl > 
81 
List.iter (fun (f, t) > generalize t) fl 
82 
 Tstatic (d, t) 
83 
 Tarray (d, t) > Dimension.generalize d; generalize t 
84 
 Tclock t 
85 
 Tlink t > 
86 
generalize t 
87 
 Tenum _  Tconst _  Tunivar  Tbasic _ > () 
88  
89 
(** Downgrade polymorphic type variables to monomorphic type 
90 
variables *) 
91 
let rec instantiate inst_vars inst_dim_vars ty = 
92 
let ty = repr ty in 
93 
match ty.tdesc with 
94 
 Tenum _  Tconst _  Tvar  Tbasic _ > ty 
95 
 Tarrow (t1,t2) > 
96 
{ty with tdesc = 
97 
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} 
98 
 Ttuple tlist > 
99 
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)} 
100 
 Tstruct flist > 
101 
{ty with tdesc = Tstruct (List.map (fun (f, t) > (f, instantiate inst_vars inst_dim_vars t)) flist)} 
102 
 Tclock t > 
103 
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)} 
104 
 Tstatic (d, t) > 
105 
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
106 
 Tarray (d, t) > 
107 
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
108 
 Tlink t > 
109 
(* should not happen *) 
110 
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)} 
111 
 Tunivar > 
112 
try 
113 
List.assoc ty.tid !inst_vars 
114 
with Not_found > 
115 
let var = new_var () in 
116 
inst_vars := (ty.tid, var)::!inst_vars; 
117 
var 
118  
119  
120  
121 
let basic_coretype_type t = 
122 
if is_real_type t then Tydec_real else 
123 
if is_int_type t then Tydec_int else 
124 
if is_bool_type t then Tydec_bool else 
125 
assert false 
126  
127 
(* [type_coretype cty] types the type declaration [cty] *) 
128 
let rec type_coretype type_dim cty = 
129 
match (*get_repr_type*) cty with 
130 
 Tydec_any > new_var () 
131 
 Tydec_int > type_int 
132 
 Tydec_real > (* Type_predef. *)type_real 
133 
(*  Tydec_float > Type_predef.type_real *) 
134 
 Tydec_bool > (* Type_predef. *)type_bool 
135 
 Tydec_clock ty > (* Type_predef. *)type_clock (type_coretype type_dim ty) 
136 
 Tydec_const c > (* Type_predef. *)type_const c 
137 
 Tydec_enum tl > (* Type_predef. *)type_enum tl 
138 
 Tydec_struct fl > (* Type_predef. *)type_struct (List.map (fun (f, ty) > (f, type_coretype type_dim ty)) fl) 
139 
 Tydec_array (d, ty) > 
140 
begin 
141 
let d = Dimension.copy (ref []) d in 
142 
type_dim d; 
143 
(* Type_predef. *)type_array d (type_coretype type_dim ty) 
144 
end 
145  
146 
(* [coretype_type] is the reciprocal of [type_typecore] *) 
147 
let rec coretype_type ty = 
148 
match (repr ty).tdesc with 
149 
 Tvar > Tydec_any 
150 
 Tbasic _ > basic_coretype_type ty 
151 
 Tconst c > Tydec_const c 
152 
 Tclock t > Tydec_clock (coretype_type t) 
153 
 Tenum tl > Tydec_enum tl 
154 
 Tstruct fl > Tydec_struct (List.map (fun (f, t) > (f, coretype_type t)) fl) 
155 
 Tarray (d, t) > Tydec_array (d, coretype_type t) 
156 
 Tstatic (_, t) > coretype_type t 
157 
 _ > assert false 
158  
159 
let get_coretype_definition tname = 
160 
try 
161 
let top = Hashtbl.find type_table (Tydec_const tname) in 
162 
match top.top_decl_desc with 
163 
 TypeDef tdef > tdef.tydef_desc 
164 
 _ > assert false 
165 
with Not_found > raise (Error (Location.dummy_loc, Unbound_type tname)) 
166  
167 
let get_type_definition tname = 
168 
type_coretype (fun d > ()) (get_coretype_definition tname) 
169  
170 
(* Equality on ground types only *) 
171 
(* Should be used between local variables which must have a ground type *) 
172 
let rec eq_ground t1 t2 = 
173 
let t1 = repr t1 in 
174 
let t2 = repr t2 in 
175 
t1==t2  
176 
match t1.tdesc, t2.tdesc with 
177 
 Tbasic t1, Tbasic t2 when t1 == t2 > true 
178 
 Tenum tl, Tenum tl' when tl == tl' > true 
179 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > List.for_all2 eq_ground tl tl' 
180 
 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' 
181 
 (Tconst t, _) > 
182 
let def_t = get_type_definition t in 
183 
eq_ground def_t t2 
184 
 (_, Tconst t) > 
185 
let def_t = get_type_definition t in 
186 
eq_ground t1 def_t 
187 
 Tarrow (t1,t2), Tarrow (t1',t2') > eq_ground t1 t1' && eq_ground t2 t2' 
188 
 Tclock t1', Tclock t2' > eq_ground t1' t2' 
189 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
190 
 Tarray (e1, t1'), Tarray (e2, t2') > Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' 
191 
 _ > false 
192  
193 
(** [unify t1 t2] unifies types [t1] and [t2] 
194 
using standard destructive unification. 
195 
Raises [Unify (t1,t2)] if the types are not unifiable. 
196 
[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type, 
197 
so in case of unification error: expected type [t1], got type [t2]. 
198 
If [sub]typing is allowed, [t2] may be a subtype of [t1]. 
199 
If [semi] unification is required, 
200 
[t1] should furthermore be an instance of [t2] 
201 
and constants are handled differently.*) 
202 
let unify ?(sub=false) ?(semi=false) t1 t2 = 
203 
let rec unif t1 t2 = 
204 
let t1 = repr t1 in 
205 
let t2 = repr t2 in 
206 
if t1==t2 then 
207 
() 
208 
else 
209 
match t1.tdesc,t2.tdesc with 
210 
(* strictly subtyping cases first *) 
211 
 _ , Tclock t2 when sub && (get_clock_base_type t1 = None) > 
212 
unif t1 t2 
213 
 _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) > 
214 
unif t1 t2 
215 
(* This case is not mandatory but will keep "older" types *) 
216 
 Tvar, Tvar > 
217 
if t1.tid < t2.tid then 
218 
t2.tdesc < Tlink t1 
219 
else 
220 
t1.tdesc < Tlink t2 
221 
 Tvar, _ when (not semi) && (not (occurs t1 t2)) > 
222 
t1.tdesc < Tlink t2 
223 
 _, Tvar when (not (occurs t2 t1)) > 
224 
t2.tdesc < Tlink t1 
225 
 Tarrow (t1,t2), Tarrow (t1',t2') > 
226 
begin 
227 
unif t2 t2'; 
228 
unif t1' t1 
229 
end 
230 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 
231 
List.iter2 unif tl tl' 
232 
 Ttuple [t1] , _ > unif t1 t2 
233 
 _ , Ttuple [t2] > unif t1 t2 
234 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 
235 
List.iter2 (fun (_, t) (_, t') > unif t t') fl fl' 
236 
 Tclock _, Tstatic _ 
237 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 
238 
 Tclock t1', Tclock t2' > unif t1' t2' 
239 
 Tbasic t1, Tbasic t2 when t1 == t2 > () 
240 
 Tunivar, _  _, Tunivar > () 
241 
 (Tconst t, _) > 
242 
let def_t = get_type_definition t in 
243 
unif def_t t2 
244 
 (_, Tconst t) > 
245 
let def_t = get_type_definition t in 
246 
unif t1 def_t 
247 
 Tenum tl, Tenum tl' when tl == tl' > () 
248 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
249 
 Tarray (e1, t1'), Tarray (e2, t2') > 
250 
let eval_const = 
251 
if semi 
252 
then (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) 
253 
else (fun c > None) in 
254 
begin 
255 
unif t1' t2'; 
256 
Dimension.eval Basic_library.eval_env eval_const e1; 
257 
Dimension.eval Basic_library.eval_env eval_const e2; 
258 
Dimension.unify ~semi:semi e1 e2; 
259 
end 
260 
(* Special cases for machine_types. Rules to unify static types infered 
261 
for numerical constants with non static ones for variables with 
262 
possible machine types *) 
263 
 Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 > BasicT.unify bt1 bt2 
264 
 _,_ > raise (Unify (t1, t2)) 
265 
in unif t1 t2 
266  
267 
(* Expected type ty1, got type ty2 *) 
268 
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc = 
269 
try 
270 
unify ~sub:sub ~semi:semi ty1 ty2 
271 
with 
272 
 Unify _ > 
273 
raise (Error (loc, Type_clash (ty1,ty2))) 
274 
 Dimension.Unify _ > 
275 
raise (Error (loc, Type_clash (ty1,ty2))) 
276  
277  
278 
(************************************************) 
279 
(* Typing function for each basic AST construct *) 
280 
(************************************************) 
281  
282 
let rec type_struct_const_field ?(is_annot=false) loc (label, c) = 
283 
if Hashtbl.mem field_table label 
284 
then let tydef = Hashtbl.find field_table label in 
285 
let tydec = (typedef_of_top tydef).tydef_desc in 
286 
let tydec_struct = get_struct_type_fields tydec in 
287 
let ty_label = type_coretype (fun d > ()) (List.assoc label tydec_struct) in 
288 
begin 
289 
try_unify ty_label (type_const ~is_annot loc c) loc; 
290 
type_coretype (fun d > ()) tydec 
291 
end 
292 
else raise (Error (loc, Unbound_value ("struct field " ^ label))) 
293  
294 
and type_const ?(is_annot=false) loc c = 
295 
match c with 
296 
 Const_int _ > (* Type_predef. *)type_int 
297 
 Const_real _ > (* Type_predef. *)type_real 
298 
 Const_array ca > let d = Dimension.mkdim_int loc (List.length ca) in 
299 
let ty = new_var () in 
300 
List.iter (fun e > try_unify ty (type_const ~is_annot loc e) loc) ca; 
301 
(* Type_predef. *)type_array d ty 
302 
 Const_tag t > 
303 
if Hashtbl.mem tag_table t 
304 
then 
305 
let tydef = typedef_of_top (Hashtbl.find tag_table t) in 
306 
let tydec = 
307 
if is_user_type tydef.tydef_desc 
308 
then Tydec_const tydef.tydef_id 
309 
else tydef.tydef_desc in 
310 
type_coretype (fun d > ()) tydec 
311 
else raise (Error (loc, Unbound_value ("enum tag " ^ t))) 
312 
 Const_struct fl > 
313 
let ty_struct = new_var () in 
314 
begin 
315 
let used = 
316 
List.fold_left 
317 
(fun acc (l, c) > 
318 
if List.mem l acc 
319 
then raise (Error (loc, Already_bound ("struct field " ^ l))) 
320 
else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc) 
321 
[] fl in 
322 
try 
323 
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in 
324 
(* List.iter (fun l > Format.eprintf "total: %s@." l) total; 
325 
List.iter (fun l > Format.eprintf "used: %s@." l) used; *) 
326 
let undef = List.find (fun l > not (List.mem l used)) total 
327 
in raise (Error (loc, Unbound_value ("struct field " ^ undef))) 
328 
with Not_found > 
329 
ty_struct 
330 
end 
331 
 Const_string _  Const_modeid _ > 
332 
if is_annot then (* Type_predef. *)type_string else assert false (* string datatype should only appear in annotations *) 
333  
334 
(* The following typing functions take as parameter an environment [env] 
335 
and whether the element being typed is expected to be constant [const]. 
336 
[env] is a pair composed of: 
337 
 a map from ident to type, associating to each ident, i.e. 
338 
variables, constants and (imported) nodes, its type including whether 
339 
it is constant or not. This latter information helps in checking constant 
340 
propagation policy in Lustre. 
341 
 a vdecl list, in order to modify types of declared variables that are 
342 
later discovered to be clocks during the typing process. 
343 
*) 
344 
let check_constant loc const_expected const_real = 
345 
if const_expected && not const_real 
346 
then raise (Error (loc, Not_a_constant)) 
347  
348 
let rec type_add_const env const arg targ = 
349 
(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*) 
350 
if const 
351 
then let d = 
352 
if is_dimension_type targ 
353 
then dimension_of_expr arg 
354 
else Dimension.mkdim_var () in 
355 
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in 
356 
Dimension.eval Basic_library.eval_env eval_const d; 
357 
let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in 
358 
(match (* Types. *)get_static_value targ with 
359 
 None > () 
360 
 Some d' > try_unify targ real_static_type arg.expr_loc); 
361 
real_static_type 
362 
else targ 
363  
364 
(* emulates a subtyping relation between types t and (d : t), 
365 
used during node applications and assignments *) 
366 
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = 
367 
let loc = real_arg.expr_loc in 
368 
let const = const  ((* Types. *)get_static_value formal_type <> None) in 
369 
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in 
370 
(*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;*) 
371 
try_unify ~sub:sub formal_type real_type loc 
372  
373 
(* typing an application implies: 
374 
 checking that const formal parameters match real const (maybe symbolic) arguments 
375 
 checking type adequation between formal and real arguments 
376 
An application may embed an homomorphic/internal function, in which case we need to split 
377 
it in many calls 
378 
*) 
379 
and type_appl env in_main loc const f args = 
380 
let targs = List.map (type_expr env in_main const) args in 
381 
if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs 
382 
then 
383 
try 
384 
let targs = Utils.transpose_list (List.map type_list_of_type targs) in 
385 
(* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs) 
386 
with 
387 
Utils.TransposeError (l, l') > raise (Error (loc, WrongMorphism (l, l'))) 
388 

389 
else ( 
390 
type_dependent_call env in_main loc const f (List.combine args targs) 
391 
) 
392 

393 
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *) 
394 
and type_dependent_call env in_main loc const f targs = 
395 
(* Format.eprintf "Typing.type_dependent_call %s@." f; *) 
396 
let tins, touts = new_var (), new_var () in 
397 
(* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *) 
398 
let tfun = (* Type_predef. *)type_arrow tins touts in 
399 
(* Format.eprintf "fun=%a@." print_ty tfun; *) 
400 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
401 
(* Format.eprintf "type subtyping@."; *) 
402 
let tins = type_list_of_type tins in 
403 
if List.length targs <> List.length tins then 
404 
raise (Error (loc, WrongArity (List.length tins, List.length targs))) 
405 
else 
406 
begin 
407 
List.iter2 ( 
408 
fun (a,t) ti > 
409 
let t' = type_add_const env (const  (* Types. *)get_static_value ti <> None) a t in 
410 
(* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *) 
411 
try_unify ~sub:true ti t' a.expr_loc; 
412 
(* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *) 
413 

414 
) 
415 
targs 
416 
tins; 
417 
touts 
418 
end 
419  
420 
(* type a simple call without dependent types 
421 
but possible homomorphic extension. 
422 
[targs] is here a list of arguments' types. *) 
423 
and type_simple_call env in_main loc const f targs = 
424 
let tins, touts = new_var (), new_var () in 
425 
let tfun = (* Type_predef. *)type_arrow tins touts in 
426 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
427 
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*) 
428 
try_unify ~sub:true tins (type_of_type_list targs) loc; 
429 
touts 
430  
431 
(** [type_expr env in_main expr] types expression [expr] in environment 
432 
[env], expecting it to be [const] or not. *) 
433 
and type_expr ?(is_annot=false) env in_main const expr = 
434 
let resulting_ty = 
435 
match expr.expr_desc with 
436 
 Expr_const c > 
437 
let ty = type_const ~is_annot expr.expr_loc c in 
438 
let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in 
439 
expr.expr_type < Expr_type_hub.export ty; 
440 
ty 
441 
 Expr_ident v > 
442 
let tyv = 
443 
try 
444 
Env.lookup_value (fst env) v 
445 
with Not_found > 
446 
Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr; 
447 
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) 
448 
in 
449 
let ty = instantiate (ref []) (ref []) tyv in 
450 
let ty' = 
451 
if const 
452 
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ()) 
453 
else new_var () in 
454 
try_unify ty ty' expr.expr_loc; 
455 
expr.expr_type < Expr_type_hub.export ty; 
456 
ty 
457 
 Expr_array elist > 
458 
let ty_elt = new_var () in 
459 
List.iter (fun e > try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist; 
460 
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in 
461 
let ty = (* Type_predef. *)type_array d ty_elt in 
462 
expr.expr_type < Expr_type_hub.export ty; 
463 
ty 
464 
 Expr_access (e1, d) > 
465 
type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int; 
466 
let ty_elt = new_var () in 
467 
let d = Dimension.mkdim_var () in 
468 
type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt); 
469 
expr.expr_type < Expr_type_hub.export ty_elt; 
470 
ty_elt 
471 
 Expr_power (e1, d) > 
472 
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in 
473 
type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int; 
474 
Dimension.eval Basic_library.eval_env eval_const d; 
475 
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
476 
let ty = (* Type_predef. *)type_array d ty_elt in 
477 
expr.expr_type < Expr_type_hub.export ty; 
478 
ty 
479 
 Expr_tuple elist > 
480 
let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in 
481 
expr.expr_type < Expr_type_hub.export ty; 
482 
ty 
483 
 Expr_ite (c, t, e) > 
484 
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool; 
485 
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in 
486 
expr.expr_type < Expr_type_hub.export ty; 
487 
ty 
488 
 Expr_appl (id, args, r) > 
489 
(* application of non internal function is not legal in a constant 
490 
expression *) 
491 
(match r with 
492 
 None > () 
493 
 Some c > 
494 
check_constant expr.expr_loc const false; 
495 
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool); 
496 
let args_list = expr_list_of_expr args in 
497 
let touts = type_appl env in_main expr.expr_loc const id args_list in 
498 
let targs = new_ty (Ttuple (List.map (fun a > Expr_type_hub.import a.expr_type) args_list)) in 
499 
args.expr_type < Expr_type_hub.export targs; 
500 
expr.expr_type < Expr_type_hub.export touts; 
501 
touts 
502 
 Expr_fby (e1,e2) 
503 
 Expr_arrow (e1,e2) > 
504 
(* fby/arrow is not legal in a constant expression *) 
505 
check_constant expr.expr_loc const false; 
506 
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in 
507 
expr.expr_type < Expr_type_hub.export ty; 
508 
ty 
509 
 Expr_pre e > 
510 
(* pre is not legal in a constant expression *) 
511 
check_constant expr.expr_loc const false; 
512 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in 
513 
expr.expr_type < Expr_type_hub.export ty; 
514 
ty 
515 
 Expr_when (e1,c,l) > 
516 
(* when is not legal in a constant expression *) 
517 
check_constant expr.expr_loc const false; 
518 
let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in 
519 
let expr_c = expr_of_ident c expr.expr_loc in 
520 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
521 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
522 
expr.expr_type < Expr_type_hub.export ty; 
523 
ty 
524 
 Expr_merge (c,hl) > 
525 
(* merge is not legal in a constant expression *) 
526 
check_constant expr.expr_loc const false; 
527 
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in 
528 
let expr_c = expr_of_ident c expr.expr_loc in 
529 
let typ_l = (* Type_predef. *)type_clock typ_in in 
530 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
531 
expr.expr_type < Expr_type_hub.export typ_out; 
532 
typ_out 
533 
in 
534 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty); 
535 
resulting_ty 
536  
537 
and type_branches ?(is_annot=false) env in_main loc const hl = 
538 
let typ_in = new_var () in 
539 
let typ_out = new_var () in 
540 
try 
541 
let used_labels = 
542 
List.fold_left (fun accu (t, h) > 
543 
unify typ_in (type_const ~is_annot loc (Const_tag t)); 
544 
type_subtyping_arg env in_main const h typ_out; 
545 
if List.mem t accu 
546 
then raise (Error (loc, Already_bound t)) 
547 
else t :: accu) [] hl in 
548 
let type_labels = get_enum_type_tags (coretype_type typ_in) in 
549 
if List.sort compare used_labels <> List.sort compare type_labels 
550 
then let unbound_tag = List.find (fun t > not (List.mem t used_labels)) type_labels in 
551 
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) 
552 
else (typ_in, typ_out) 
553 
with Unify (t1, t2) > 
554 
raise (Error (loc, Type_clash (t1,t2))) 
555  
556 
(* Eexpr are always in annotations. TODO: add the quantifiers variables to the env *) 
557 
let type_eexpr env eexpr = 
558 
(type_expr 
559 
~is_annot:true 
560 
env 
561 
false (* not in main *) 
562 
false (* not a const *) 
563 
eexpr.eexpr_qfexpr) 
564  
565  
566 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
567 
let type_eq env in_main undefined_vars eq = 
568 
(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*) 
569 
(* Check undefined variables, type lhs *) 
570 
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 
571 
let ty_lhs = type_expr env in_main false expr_lhs in 
572 
(* Check multiple variable definitions *) 
573 
let define_var id uvars = 
574 
if ISet.mem id uvars 
575 
then ISet.remove id uvars 
576 
else raise (Error (eq.eq_loc, Already_defined id)) 
577 
in 
578 
(* check assignment of declared constant, assignment of clock *) 
579 
let ty_lhs = 
580 
type_of_type_list 
581 
(List.map2 (fun ty id > 
582 
if get_static_value ty <> None 
583 
then raise (Error (eq.eq_loc, Assigned_constant id)) else 
584 
match get_clock_base_type ty with 
585 
 None > ty 
586 
 Some ty > ty) 
587 
(type_list_of_type ty_lhs) eq.eq_lhs) in 
588 
let undefined_vars = 
589 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in 
590 
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned 
591 
to a (always nonconstant) lhs variable *) 
592 
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; 
593 
undefined_vars 
594  
595  
596 
(* [type_coreclock env ck id loc] types the type clock declaration [ck] 
597 
in environment [env] *) 
598 
let type_coreclock env ck id loc = 
599 
match ck.ck_dec_desc with 
600 
 Ckdec_any > () 
601 
 Ckdec_bool cl > 
602 
let dummy_id_expr = expr_of_ident id loc in 
603 
let when_expr = 
604 
List.fold_left 
605 
(fun expr (x, l) > 
606 
{expr_tag = new_tag (); 
607 
expr_desc= Expr_when (expr,x,l); 
608 
expr_type = Types.Main.new_var (); 
609 
expr_clock = Clocks.new_var true; 
610 
expr_delay = Delay.new_var (); 
611 
expr_loc=loc; 
612 
expr_annot = None}) 
613 
dummy_id_expr cl 
614 
in 
615 
ignore (type_expr env false false when_expr) 
616  
617 
let rec check_type_declaration loc cty = 
618 
match cty with 
619 
 Tydec_clock ty 
620 
 Tydec_array (_, ty) > check_type_declaration loc ty 
621 
 Tydec_const tname > 
622 
(* Format.eprintf "TABLE: %a@." print_type_table (); *) 
623 
if not (Hashtbl.mem type_table cty) 
624 
then raise (Error (loc, Unbound_type tname)); 
625 
 _ > () 
626  
627 
let type_var_decl vd_env env vdecl = 
628 
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*) 
629 
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; 
630 
let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in 
631 
let type_dim d = 
632 
begin 
633 
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int; 
634 
Dimension.eval Basic_library.eval_env eval_const d; 
635 
end in 
636 
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in 
637  
638 
let ty_static = 
639 
if vdecl.var_dec_const 
640 
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty 
641 
else ty in 
642 
(match vdecl.var_dec_value with 
643 
 None > () 
644 
 Some v > type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static); 
645 
try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc; 
646 
let new_env = Env.add_value env vdecl.var_id ty_static in 
647 
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; 
648 
(*Format.eprintf "END %a@." Types.print_ty ty_static;*) 
649 
new_env 
650  
651 
let type_var_decl_list vd_env env l = 
652 
List.fold_left (type_var_decl vd_env) env l 
653  
654 
let type_of_vlist vars = 
655 
let tyl = List.map (fun v > Expr_type_hub.import v.var_type) vars in 
656 
type_of_type_list tyl 
657  
658 
let add_vdecl vd_env vdecl = 
659 
if List.exists (fun v > v.var_id = vdecl.var_id) vd_env 
660 
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) 
661 
else vdecl::vd_env 
662  
663 
let check_vd_env vd_env = 
664 
ignore (List.fold_left add_vdecl [] vd_env) 
665  
666 
let type_spec env c = 
667 
(*TODO 
668 
enrich env locally with locals and consts 
669 
type each pre/post as a boolean expr 
670 
I don't know if we want to update the global env with locally typed variables. 
671 
For the moment, returning the provided env 
672 
*) 
673 
env 
674 

675 
(** [type_node env nd loc] types node [nd] in environment env. The 
676 
location is used for error reports. *) 
677 
let type_node env nd loc = 
678 
let is_main = nd.node_id = !Options.main_node in 
679 
let vd_env_ol = nd.node_outputs@nd.node_locals in 
680 
let vd_env = nd.node_inputs@vd_env_ol in 
681 
check_vd_env vd_env; 
682 
let init_env = env in 
683 
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in 
684 
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in 
685 
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in 
686 
let new_env = Env.overwrite env delta_env in 
687 
let undefined_vars_init = 
688 
List.fold_left 
689 
(fun uvs v > ISet.add v.var_id uvs) 
690 
ISet.empty vd_env_ol in 
691 
let undefined_vars = 
692 
let eqs, auts = get_node_eqs nd in 
693 
(* TODO XXX: il faut typer les handlers de l'automate *) 
694 
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs 
695 
in 
696 
(* Typing asserts *) 
697 
List.iter (fun assert_ > 
698 
let assert_expr = assert_.assert_expr in 
699 
type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool 
700 
) nd.node_asserts; 
701 
(* Typing spec/contracts *) 
702 
(match nd.node_spec with None > ()  Some spec > ignore (type_spec (new_env, vd_env) spec)); 
703 
(* Typing annots *) 
704 
List.iter (fun annot > 
705 
List.iter (fun (_, eexpr) > ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots 
706 
) nd.node_annot; 
707 

708 
(* check that table is empty *) 
709 
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 
710 
let undefined_vars = ISet.diff undefined_vars local_consts in 
711 
if (not (ISet.is_empty undefined_vars)) then 
712 
raise (Error (loc, Undefined_var undefined_vars)); 
713 
let ty_ins = type_of_vlist nd.node_inputs in 
714 
let ty_outs = type_of_vlist nd.node_outputs in 
715 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
716 
generalize ty_node; 
717 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
718 
nd.node_type < Expr_type_hub.export ty_node; 
719 
Env.add_value env nd.node_id ty_node 
720  
721 
let type_imported_node env nd loc = 
722 
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in 
723 
let vd_env = nd.nodei_inputs@nd.nodei_outputs in 
724 
check_vd_env vd_env; 
725 
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs); 
726 
let ty_ins = type_of_vlist nd.nodei_inputs in 
727 
let ty_outs = type_of_vlist nd.nodei_outputs in 
728 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
729 
generalize ty_node; 
730 
(* 
731 
if (is_polymorphic ty_node) then 
732 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
733 
*) 
734 
let new_env = Env.add_value env nd.nodei_id ty_node in 
735 
nd.nodei_type < Expr_type_hub.export ty_node; 
736 
new_env 
737  
738 
let type_top_const env cdecl = 
739 
let ty = type_const cdecl.const_loc cdecl.const_value in 
740 
let d = 
741 
if is_dimension_type ty 
742 
then dimension_of_const cdecl.const_loc cdecl.const_value 
743 
else Dimension.mkdim_var () in 
744 
let ty = (* Type_predef. *)type_static d ty in 
745 
let new_env = Env.add_value env cdecl.const_id ty in 
746 
cdecl.const_type < Expr_type_hub.export ty; 
747 
new_env 
748  
749 
let type_top_consts env clist = 
750 
List.fold_left type_top_const env clist 
751  
752 
let rec type_top_decl env decl = 
753 
match decl.top_decl_desc with 
754 
 Node nd > ( 
755 
try 
756 
type_node env nd decl.top_decl_loc 
757 
with Error (loc, err) as exc > ( 
758 
if !Options.global_inline then 
759 
Format.eprintf "Type error: failing node@.%a@.@?" 
760 
Printers.pp_node nd 
761 
; 
762 
raise exc) 
763 
) 
764 
 ImportedNode nd > 
765 
type_imported_node env nd decl.top_decl_loc 
766 
 Const c > 
767 
type_top_const env c 
768 
 TypeDef _ > List.fold_left type_top_decl env (consts_of_enum_type decl) 
769 
 Include _  Open _ > env 
770 

771 
let get_type_of_call decl = 
772 
match decl.top_decl_desc with 
773 
 Node nd > 
774 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in 
775 
type_list_of_type in_typ, type_list_of_type out_typ 
776 
 ImportedNode nd > 
777 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in 
778 
type_list_of_type in_typ, type_list_of_type out_typ 
779 
 _ > assert false 
780  
781 
let type_prog env decls = 
782 
try 
783 
List.fold_left type_top_decl env decls 
784 
with Failure _ as exc > raise exc 
785  
786 
(* Once the Lustre program is fully typed, we must get back to the 
787 
original description of dimensions, with constant parameters, 
788 
instead of unifiable internal variables. *) 
789  
790 
(* The following functions aims at 'unevaluating' dimension 
791 
expressions occuring in array types, i.e. replacing unifiable 
792 
second_order variables with the original static parameters. 
793 
Once restored in this formulation, dimensions may be 
794 
meaningfully printed. *) 
795 
let uneval_vdecl_generics vdecl = 
796 
if vdecl.var_dec_const 
797 
then 
798 
match get_static_value (Expr_type_hub.import vdecl.var_type) with 
799 
 None > (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false) 
800 
 Some d > Dimension.uneval vdecl.var_id d 
801  
802 
let uneval_node_generics vdecls = 
803 
List.iter uneval_vdecl_generics vdecls 
804  
805 
let uneval_spec_generics spec = 
806 
List.iter uneval_vdecl_generics (spec.consts@spec.locals) 
807 

808 
let uneval_top_generics decl = 
809 
match decl.top_decl_desc with 
810 
 Node nd > 
811 
uneval_node_generics (nd.node_inputs @ nd.node_outputs) 
812 
 ImportedNode nd > 
813 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
814 
 Const _  TypeDef _  Open _  Include _ 
815 
> () 
816  
817 
let uneval_prog_generics prog = 
818 
List.iter uneval_top_generics prog 
819  
820 
let rec get_imported_symbol decls id = 
821 
match decls with 
822 
 [] > assert false 
823 
 decl::q > 
824 
(match decl.top_decl_desc with 
825 
 ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf > decl 
826 
 Const c when id = c.const_id && decl.top_decl_itf > decl 
827 
 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id 
828 
 _ > get_imported_symbol q id) 
829  
830 
let check_env_compat header declared computed = 
831 
uneval_prog_generics header; 
832 
Env.iter declared (fun k decl_type_k > 
833 
let loc = (get_imported_symbol header k).top_decl_loc in 
834 
let computed_t = 
835 
instantiate (ref []) (ref []) 
836 
(try Env.lookup_value computed k 
837 
with Not_found > raise (Error (loc, Declared_but_undefined k))) in 
838 
(*Types.print_ty Format.std_formatter decl_type_k; 
839 
Types.print_ty Format.std_formatter computed_t;*) 
840 
try_unify ~sub:true ~semi:true decl_type_k computed_t loc 
841 
) 
842  
843 
let check_typedef_top decl = 
844 
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*) 
845 
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*) 
846 
(*Format.eprintf "%a" Corelang.print_type_table ();*) 
847 
match decl.top_decl_desc with 
848 
 TypeDef ty > 
849 
let owner = decl.top_decl_owner in 
850 
let itf = decl.top_decl_itf in 
851 
let decl' = 
852 
try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id) 
853 
with Not_found > raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in 
854 
let owner' = decl'.top_decl_owner in 
855 
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*) 
856 
let itf' = decl'.top_decl_itf in 
857 
(match decl'.top_decl_desc with 
858 
 Const _  Node _  ImportedNode _ > assert false 
859 
 TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') > () 
860 
 _ > raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id))) 
861 
 _ > () 
862  
863 
let check_typedef_compat header = 
864 
List.iter check_typedef_top header 
865 
end 
866  
867 
include Make(Types.Main) (struct 
868 
type type_expr = Types.Main.type_expr 
869 
let import x = x 
870 
let export x = x 
871 
end) 
872 
(* Local Variables: *) 
873 
(* compilecommand:"make C .." *) 
874 
(* End: *) 