lustrec / src / typing.ml @ 4034b51c
History  View  Annotate  Download (39.6 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT  LIFL *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(* This file was originally from the Prelude compiler *) 
11 
(* *) 
12 
(********************************************************************) 
13  
14 
(** Main typing module. Classic inference algorithm with destructive 
15 
unification. *) 
16  
17 
let debug fmt args = () (* Format.eprintf "%a" *) 
18 
(* Though it shares similarities with the clock calculus module, no code 
19 
is shared. Simple environments, very limited identifier scoping, no 
20 
identifier redefinition allowed. *) 
21  
22 
open Utils 
23 
(* Yes, opening both modules is dirty as some type names will be 
24 
overwritten, yet this makes notations far lighter.*) 
25 
open Lustre_types 
26 
open Corelang 
27 
open Format 
28  
29  
30 
(* TODO general remark: except in the add_vdecl, it seems to me that 
31 
all the pairs (env, vd_env) should be replace with just env, since 
32 
vd_env is never used and the env element is always extract with a 
33 
fst *) 
34  
35 

36 
module type EXPR_TYPE_HUB = 
37 
sig 
38 
type type_expr 
39 
val import: Types.Main.type_expr > type_expr 
40 
val export: type_expr > Types.Main.type_expr 
41 
end 
42  
43 
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) = 
44 
struct 
45  
46 
module TP = Type_predef.Make (T) 
47 
include TP 
48 

49 
let pp_typing_env fmt env = 
50 
Env.pp_env print_ty fmt env 
51  
52 
(****************************************************************) 
53 
(* Generic functions: occurs, instantiate and generalize *) 
54 
(****************************************************************) 
55 

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

395 
else ( 
396 
type_dependent_call env in_main loc const f (List.combine args targs) 
397 
) 
398 

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

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

712 
(** [type_node env nd loc] types node [nd] in environment env. The 
713 
location is used for error reports. *) 
714 
and type_node env nd loc = 
715 
(* Format.eprintf "Typing node %s@." nd.node_id; *) 
716 
let is_main = nd.node_id = !Options.main_node in 
717 
(* In contracts, outputs are considered as input values *) 
718 
let vd_env_ol = if nd.node_iscontract then nd.node_locals else nd.node_outputs@nd.node_locals in 
719 
let vd_env = nd.node_inputs@nd.node_outputs@nd.node_locals in 
720 
check_vd_env vd_env; 
721 
let init_env = env in 
722 
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in 
723 
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in 
724 
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in 
725 
let new_env = Env.overwrite env delta_env in 
726 
let undefined_vars_init = 
727 
List.fold_left 
728 
(fun uvs v > ISet.add v.var_id uvs) 
729 
ISet.empty vd_env_ol in 
730 
let undefined_vars = 
731 
let eqs, auts = get_node_eqs nd in 
732 
(* TODO XXX: il faut typer les handlers de l'automate *) 
733 
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs 
734 
in 
735 
(* Typing asserts *) 
736 
List.iter (fun assert_ > 
737 
let assert_expr = assert_.assert_expr in 
738 
type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool 
739 
) nd.node_asserts; 
740 
(* Typing spec/contracts *) 
741 
(match nd.node_spec with 
742 
 None > () 
743 
 Some spec > ignore (type_spec new_env spec loc)); 
744 
(* Typing annots *) 
745 
List.iter (fun annot > 
746 
List.iter (fun (_, eexpr) > ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots 
747 
) nd.node_annot; 
748 

749 
(* check that table is empty *) 
750 
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 
751 
let undefined_vars = ISet.diff undefined_vars local_consts in 
752 

753 
if (not (ISet.is_empty undefined_vars)) then 
754 
raise (Error (loc, Undefined_var undefined_vars)); 
755 
let ty_ins = type_of_vlist nd.node_inputs in 
756 
let ty_outs = type_of_vlist nd.node_outputs in 
757 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
758 
generalize ty_node; 
759 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
760 
nd.node_type < Expr_type_hub.export ty_node; 
761 
Env.add_value env nd.node_id ty_node 
762  
763 
let type_imported_node env nd loc = 
764 
let vd_env = nd.nodei_inputs@nd.nodei_outputs in 
765 
check_vd_env vd_env; 
766 
let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in 
767 
let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in 
768 
let new_env = Env.overwrite env delta_env in 
769 
(* Typing spec *) 
770 
(match nd.nodei_spec with 
771 
 None > () 
772 
 Some spec > ignore (type_spec new_env spec loc)); 
773 
let ty_ins = type_of_vlist nd.nodei_inputs in 
774 
let ty_outs = type_of_vlist nd.nodei_outputs in 
775 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
776 
generalize ty_node; 
777 
(* 
778 
if (is_polymorphic ty_node) then 
779 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
780 
*) 
781 
let new_env = Env.add_value env nd.nodei_id ty_node in 
782 
nd.nodei_type < Expr_type_hub.export ty_node; 
783 
new_env 
784  
785 
let type_top_const env cdecl = 
786 
let ty = type_const cdecl.const_loc cdecl.const_value in 
787 
let d = 
788 
if is_dimension_type ty 
789 
then dimension_of_const cdecl.const_loc cdecl.const_value 
790 
else Dimension.mkdim_var () in 
791 
let ty = (* Type_predef. *)type_static d ty in 
792 
let new_env = Env.add_value env cdecl.const_id ty in 
793 
cdecl.const_type < Expr_type_hub.export ty; 
794 
new_env 
795  
796 
let type_top_consts env clist = 
797 
List.fold_left type_top_const env clist 
798  
799 
let rec type_top_decl env decl = 
800 
match decl.top_decl_desc with 
801 
 Node nd > ( 
802 
try 
803 
type_node env nd decl.top_decl_loc 
804 
with Error (loc, err) as exc > ( 
805 
if !Options.global_inline then 
806 
Format.eprintf "Type error: failing node@.%a@.@?" 
807 
Printers.pp_node nd 
808 
; 
809 
raise exc) 
810 
) 
811 
 ImportedNode nd > 
812 
type_imported_node env nd decl.top_decl_loc 
813 
 Const c > 
814 
type_top_const env c 
815 
 TypeDef _ > List.fold_left type_top_decl env (consts_of_enum_type decl) 
816 
 Include _  Open _ > env 
817 

818 
let get_type_of_call decl = 
819 
match decl.top_decl_desc with 
820 
 Node nd > 
821 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in 
822 
type_list_of_type in_typ, type_list_of_type out_typ 
823 
 ImportedNode nd > 
824 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in 
825 
type_list_of_type in_typ, type_list_of_type out_typ 
826 
 _ > assert false 
827  
828 
let type_prog env decls = 
829 
try 
830 
List.fold_left type_top_decl env decls 
831 
with Failure _ as exc > raise exc 
832  
833 
(* Once the Lustre program is fully typed, we must get back to the 
834 
original description of dimensions, with constant parameters, 
835 
instead of unifiable internal variables. *) 
836  
837 
(* The following functions aims at 'unevaluating' dimension 
838 
expressions occuring in array types, i.e. replacing unifiable 
839 
second_order variables with the original static parameters. 
840 
Once restored in this formulation, dimensions may be 
841 
meaningfully printed. *) 
842 
let uneval_vdecl_generics vdecl = 
843 
if vdecl.var_dec_const 
844 
then 
845 
match get_static_value (Expr_type_hub.import vdecl.var_type) with 
846 
 None > (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false) 
847 
 Some d > Dimension.uneval vdecl.var_id d 
848  
849 
let uneval_node_generics vdecls = 
850 
List.iter uneval_vdecl_generics vdecls 
851  
852 
let uneval_spec_generics spec = 
853 
List.iter uneval_vdecl_generics (spec.consts@spec.locals) 
854 

855 
let uneval_top_generics decl = 
856 
match decl.top_decl_desc with 
857 
 Node nd > 
858 
uneval_node_generics (nd.node_inputs @ nd.node_outputs) 
859 
 ImportedNode nd > 
860 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
861 
 Const _  TypeDef _  Open _  Include _ 
862 
> () 
863  
864 
let uneval_prog_generics prog = 
865 
List.iter uneval_top_generics prog 
866  
867 
let rec get_imported_symbol decls id = 
868 
match decls with 
869 
 [] > assert false 
870 
 decl::q > 
871 
(match decl.top_decl_desc with 
872 
 ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf > decl 
873 
 Const c when id = c.const_id && decl.top_decl_itf > decl 
874 
 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id 
875 
 _ > get_imported_symbol q id) 
876  
877 
let check_env_compat header declared computed = 
878 
uneval_prog_generics header; 
879 
Env.iter declared (fun k decl_type_k > 
880 
let top = get_imported_symbol header k in 
881 
let loc = top.top_decl_loc in 
882 
try 
883 
let computed_t = Env.lookup_value computed k in 
884 
let computed_t = instantiate (ref []) (ref []) computed_t in 
885 
(*Types.print_ty Format.std_formatter decl_type_k; 
886 
Types.print_ty Format.std_formatter computed_t;*) 
887 
try_unify ~sub:true ~semi:true decl_type_k computed_t loc 
888 
with Not_found > 
889 
begin 
890 
(* If top is a contract we do not require the lustre 
891 
file to provide the same definition. *) 
892 
match top.top_decl_desc with 
893 
 Node nd > ( 
894 
match nd.node_spec with 
895 
 Some (Contract _) > () 
896 
 _ > raise (Error (loc, Declared_but_undefined k)) 
897 
) 
898 
 _ > 
899 
raise (Error (loc, Declared_but_undefined k)) 
900 
end 
901 
) 
902  
903 
let check_typedef_top decl = 
904 
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*) 
905 
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*) 
906 
(*Format.eprintf "%a" Corelang.print_type_table ();*) 
907 
match decl.top_decl_desc with 
908 
 TypeDef ty > 
909 
let owner = decl.top_decl_owner in 
910 
let itf = decl.top_decl_itf in 
911 
let decl' = 
912 
try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id) 
913 
with Not_found > raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in 
914 
let owner' = decl'.top_decl_owner in 
915 
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*) 
916 
let itf' = decl'.top_decl_itf in 
917 
(match decl'.top_decl_desc with 
918 
 Const _  Node _  ImportedNode _ > assert false 
919 
 TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') > () 
920 
 _ > raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id))) 
921 
 _ > () 
922  
923 
let check_typedef_compat header = 
924 
List.iter check_typedef_top header 
925 
end 
926  
927 
include Make(Types.Main) (struct 
928 
type type_expr = Types.Main.type_expr 
929 
let import x = x 
930 
let export x = x 
931 
end) 
932 
(* Local Variables: *) 
933 
(* compilecommand:"make C .." *) 
934 
(* End: *) 