lustrec / src / typing.ml @ 3c3414c5
History  View  Annotate  Download (32.7 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  
31 
module type EXPR_TYPE_HUB = 
32 
sig 
33 
type type_expr 
34 
val import: Types.Main.type_expr > type_expr 
35 
val export: type_expr > Types.Main.type_expr 
36 
end 
37  
38 
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) = 
39 
struct 
40  
41 
module TP = Type_predef.Make (T) 
42 
include TP 
43 

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

379 
else ( 
380 
type_dependent_call env in_main loc const f (List.combine args targs) 
381 
) 
382  
383 
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *) 
384 
and type_dependent_call env in_main loc const f targs = 
385 
(* Format.eprintf "Typing.type_dependent_call %s@." f; *) 
386 
let tins, touts = new_var (), new_var () in 
387 
(* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *) 
388 
let tfun = (* Type_predef. *)type_arrow tins touts in 
389 
(* Format.eprintf "fun=%a@." print_ty tfun; *) 
390 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
391 
(* Format.eprintf "type subtyping@."; *) 
392 
let tins = type_list_of_type tins in 
393 
if List.length targs <> List.length tins then 
394 
raise (Error (loc, WrongArity (List.length tins, List.length targs))) 
395 
else 
396 
begin 
397 
List.iter2 ( 
398 
fun (a,t) ti > 
399 
let t' = type_add_const env (const  (* Types. *)get_static_value ti <> None) a t in 
400 
(* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *) 
401 
try_unify ~sub:true ti t' a.expr_loc; 
402 
(* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *) 
403 

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

677 
(* check that table is empty *) 
678 
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 
679 
let undefined_vars = ISet.diff undefined_vars local_consts in 
680 
if (not (ISet.is_empty undefined_vars)) then 
681 
raise (Error (loc, Undefined_var undefined_vars)); 
682 
let ty_ins = type_of_vlist nd.node_inputs in 
683 
let ty_outs = type_of_vlist nd.node_outputs in 
684 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
685 
generalize ty_node; 
686 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
687 
nd.node_type < Expr_type_hub.export ty_node; 
688 
Env.add_value env nd.node_id ty_node 
689  
690 
let type_imported_node env nd loc = 
691 
let new_env = type_var_decl_list nd.nodei_inputs env nd.nodei_inputs in 
692 
let vd_env = nd.nodei_inputs@nd.nodei_outputs in 
693 
check_vd_env vd_env; 
694 
ignore(type_var_decl_list vd_env new_env nd.nodei_outputs); 
695 
let ty_ins = type_of_vlist nd.nodei_inputs in 
696 
let ty_outs = type_of_vlist nd.nodei_outputs in 
697 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
698 
generalize ty_node; 
699 
(* 
700 
if (is_polymorphic ty_node) then 
701 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
702 
*) 
703 
let new_env = Env.add_value env nd.nodei_id ty_node in 
704 
nd.nodei_type < Expr_type_hub.export ty_node; 
705 
new_env 
706  
707 
let type_top_const env cdecl = 
708 
let ty = type_const cdecl.const_loc cdecl.const_value in 
709 
let d = 
710 
if is_dimension_type ty 
711 
then dimension_of_const cdecl.const_loc cdecl.const_value 
712 
else Dimension.mkdim_var () in 
713 
let ty = (* Type_predef. *)type_static d ty in 
714 
let new_env = Env.add_value env cdecl.const_id ty in 
715 
cdecl.const_type < Expr_type_hub.export ty; 
716 
new_env 
717  
718 
let type_top_consts env clist = 
719 
List.fold_left type_top_const env clist 
720  
721 
let rec type_top_decl env decl = 
722 
match decl.top_decl_desc with 
723 
 Node nd > ( 
724 
try 
725 
type_node env nd decl.top_decl_loc 
726 
with Error (loc, err) as exc > ( 
727 
if !Options.global_inline then 
728 
Format.eprintf "Type error: failing node@.%a@.@?" 
729 
Printers.pp_node nd 
730 
; 
731 
raise exc) 
732 
) 
733 
 ImportedNode nd > 
734 
type_imported_node env nd decl.top_decl_loc 
735 
 Const c > 
736 
type_top_const env c 
737 
 TypeDef _ > List.fold_left type_top_decl env (consts_of_enum_type decl) 
738 
 Open _ > env 
739  
740 
let get_type_of_call decl = 
741 
match decl.top_decl_desc with 
742 
 Node nd > 
743 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in 
744 
type_list_of_type in_typ, type_list_of_type out_typ 
745 
 ImportedNode nd > 
746 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in 
747 
type_list_of_type in_typ, type_list_of_type out_typ 
748 
 _ > assert false 
749  
750 
let type_prog env decls = 
751 
try 
752 
List.fold_left type_top_decl env decls 
753 
with Failure _ as exc > raise exc 
754  
755 
(* Once the Lustre program is fully typed, 
756 
we must get back to the original description of dimensions, 
757 
with constant parameters, instead of unifiable internal variables. *) 
758  
759 
(* The following functions aims at 'unevaluating' dimension expressions occuring in array types, 
760 
i.e. replacing unifiable second_order variables with the original static parameters. 
761 
Once restored in this formulation, dimensions may be meaningfully printed. 
762 
*) 
763 
let uneval_vdecl_generics vdecl = 
764 
if vdecl.var_dec_const 
765 
then 
766 
match get_static_value (Expr_type_hub.import vdecl.var_type) with 
767 
 None > (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false) 
768 
 Some d > Dimension.uneval vdecl.var_id d 
769  
770 
let uneval_node_generics vdecls = 
771 
List.iter uneval_vdecl_generics vdecls 
772  
773 
let uneval_top_generics decl = 
774 
match decl.top_decl_desc with 
775 
 Node nd > 
776 
uneval_node_generics (nd.node_inputs @ nd.node_outputs) 
777 
 ImportedNode nd > 
778 
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) 
779 
 Const _ 
780 
 TypeDef _ 
781 
 Open _ > () 
782  
783 
let uneval_prog_generics prog = 
784 
List.iter uneval_top_generics prog 
785  
786 
let rec get_imported_symbol decls id = 
787 
match decls with 
788 
 [] > assert false 
789 
 decl::q > 
790 
(match decl.top_decl_desc with 
791 
 ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf > decl 
792 
 Const c when id = c.const_id && decl.top_decl_itf > decl 
793 
 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id 
794 
 _ > get_imported_symbol q id) 
795  
796 
let check_env_compat header declared computed = 
797 
uneval_prog_generics header; 
798 
Env.iter declared (fun k decl_type_k > 
799 
let loc = (get_imported_symbol header k).top_decl_loc in 
800 
let computed_t = 
801 
instantiate (ref []) (ref []) 
802 
(try Env.lookup_value computed k 
803 
with Not_found > raise (Error (loc, Declared_but_undefined k))) in 
804 
(*Types.print_ty Format.std_formatter decl_type_k; 
805 
Types.print_ty Format.std_formatter computed_t;*) 
806 
try_unify ~sub:true ~semi:true decl_type_k computed_t loc 
807 
) 
808  
809 
let check_typedef_top decl = 
810 
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*) 
811 
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*) 
812 
(*Format.eprintf "%a" Corelang.print_type_table ();*) 
813 
match decl.top_decl_desc with 
814 
 TypeDef ty > 
815 
let owner = decl.top_decl_owner in 
816 
let itf = decl.top_decl_itf in 
817 
let decl' = 
818 
try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id) 
819 
with Not_found > raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in 
820 
let owner' = decl'.top_decl_owner in 
821 
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*) 
822 
let itf' = decl'.top_decl_itf in 
823 
(match decl'.top_decl_desc with 
824 
 Const _  Node _  ImportedNode _ > assert false 
825 
 TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') > () 
826 
 _ > raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id))) 
827 
 _ > () 
828  
829 
let check_typedef_compat header = 
830 
List.iter check_typedef_top header 
831 
end 
832  
833 
include Make(Types.Main) (struct 
834 
type type_expr = Types.Main.type_expr 
835 
let import x = x 
836 
let export x = x 
837 
end) 
838 
(* Local Variables: *) 
839 
(* compilecommand:"make C .." *) 
840 
(* End: *) 