lustrec / src / typing.ml @ a38c681e
History  View  Annotate  Download (27.8 KB)
1 
(*  

2 
* SchedMCore  A MultiCore Scheduling Framework 
3 
* Copyright (C) 20092011, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE 
4 
* 
5 
* This file is part of Prelude 
6 
* 
7 
* Prelude is free software; you can redistribute it and/or 
8 
* modify it under the terms of the GNU Lesser General Public License 
9 
* as published by the Free Software Foundation ; either version 2 of 
10 
* the License, or (at your option) any later version. 
11 
* 
12 
* Prelude is distributed in the hope that it will be useful, but 
13 
* WITHOUT ANY WARRANTY ; without even the implied warranty of 
14 
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 
15 
* Lesser General Public License for more details. 
16 
* 
17 
* You should have received a copy of the GNU Lesser General Public 
18 
* License along with this program ; if not, write to the Free Software 
19 
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 021111307 
20 
* USA 
21 
* *) 
22  
23 
(** Main typing module. Classic inference algorithm with destructive 
24 
unification. *) 
25  
26 
let debug fmt args = () (* Format.eprintf "%a" *) 
27 
(* Though it shares similarities with the clock calculus module, no code 
28 
is shared. Simple environments, very limited identifier scoping, no 
29 
identifier redefinition allowed. *) 
30  
31 
open Utils 
32 
(* Yes, opening both modules is dirty as some type names will be 
33 
overwritten, yet this makes notations far lighter.*) 
34 
open LustreSpec 
35 
open Corelang 
36 
open Types 
37 
open Format 
38  
39 
let pp_typing_env fmt env = 
40 
Env.pp_env print_ty fmt env 
41  
42 
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in 
43 
type [ty]. False otherwise. *) 
44 
let rec occurs tvar ty = 
45 
let ty = repr ty in 
46 
match ty.tdesc with 
47 
 Tvar > ty=tvar 
48 
 Tarrow (t1, t2) > 
49 
(occurs tvar t1)  (occurs tvar t2) 
50 
 Ttuple tl > 
51 
List.exists (occurs tvar) tl 
52 
 Tstruct fl > 
53 
List.exists (fun (f, t) > occurs tvar t) fl 
54 
 Tarray (_, t) 
55 
 Tstatic (_, t) 
56 
 Tclock t 
57 
 Tlink t > occurs tvar t 
58 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > false 
59  
60 
(** Promote monomorphic type variables to polymorphic type variables. *) 
61 
(* Generalize by sideeffects *) 
62 
let rec generalize ty = 
63 
match ty.tdesc with 
64 
 Tvar > 
65 
(* No scopes, always generalize *) 
66 
ty.tdesc < Tunivar 
67 
 Tarrow (t1,t2) > 
68 
generalize t1; generalize t2 
69 
 Ttuple tl > 
70 
List.iter generalize tl 
71 
 Tstruct fl > 
72 
List.iter (fun (f, t) > generalize t) fl 
73 
 Tstatic (d, t) 
74 
 Tarray (d, t) > Dimension.generalize d; generalize t 
75 
 Tclock t 
76 
 Tlink t > 
77 
generalize t 
78 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > () 
79  
80 
(** Downgrade polymorphic type variables to monomorphic type variables *) 
81 
let rec instantiate inst_vars inst_dim_vars ty = 
82 
let ty = repr ty in 
83 
match ty.tdesc with 
84 
 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat > ty 
85 
 Tarrow (t1,t2) > 
86 
{ty with tdesc = 
87 
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} 
88 
 Ttuple tlist > 
89 
{ty with tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist)} 
90 
 Tstruct flist > 
91 
{ty with tdesc = Tstruct (List.map (fun (f, t) > (f, instantiate inst_vars inst_dim_vars t)) flist)} 
92 
 Tclock t > 
93 
{ty with tdesc = Tclock (instantiate inst_vars inst_dim_vars t)} 
94 
 Tstatic (d, t) > 
95 
{ty with tdesc = Tstatic (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
96 
 Tarray (d, t) > 
97 
{ty with tdesc = Tarray (Dimension.instantiate inst_dim_vars d, instantiate inst_vars inst_dim_vars t)} 
98 
 Tlink t > 
99 
(* should not happen *) 
100 
{ty with tdesc = Tlink (instantiate inst_vars inst_dim_vars t)} 
101 
 Tunivar > 
102 
try 
103 
List.assoc ty.tid !inst_vars 
104 
with Not_found > 
105 
let var = new_var () in 
106 
inst_vars := (ty.tid, var)::!inst_vars; 
107 
var 
108  
109 
(* [type_coretype cty] types the type declaration [cty] *) 
110 
let rec type_coretype type_dim cty = 
111 
match (*get_repr_type*) cty with 
112 
 Tydec_any > new_var () 
113 
 Tydec_int > Type_predef.type_int 
114 
 Tydec_real > Type_predef.type_real 
115 
 Tydec_float > Type_predef.type_real 
116 
 Tydec_bool > Type_predef.type_bool 
117 
 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty) 
118 
 Tydec_const c > Type_predef.type_const c 
119 
 Tydec_enum tl > Type_predef.type_enum tl 
120 
 Tydec_struct fl > Type_predef.type_struct (List.map (fun (f, ty) > (f, type_coretype type_dim ty)) fl) 
121 
 Tydec_array (d, ty) > 
122 
begin 
123 
type_dim d; 
124 
Type_predef.type_array d (type_coretype type_dim ty) 
125 
end 
126  
127 
(* [coretype_type] is the reciprocal of [type_typecore] *) 
128 
let rec coretype_type ty = 
129 
match (repr ty).tdesc with 
130 
 Tvar > Tydec_any 
131 
 Tint > Tydec_int 
132 
 Treal > Tydec_real 
133 
 Tbool > Tydec_bool 
134 
 Tconst c > Tydec_const c 
135 
 Tclock t > Tydec_clock (coretype_type t) 
136 
 Tenum tl > Tydec_enum tl 
137 
 Tstruct fl > Tydec_struct (List.map (fun (f, t) > (f, coretype_type t)) fl) 
138 
 Tarray (d, t) > Tydec_array (d, coretype_type t) 
139 
 Tstatic (_, t) > coretype_type t 
140 
 _ > assert false 
141  
142 
let get_type_definition tname = 
143 
try 
144 
type_coretype (fun d > ()) (Hashtbl.find type_table (Tydec_const tname)) 
145 
with Not_found > raise (Error (Location.dummy_loc, Unbound_type tname)) 
146  
147 
(* Equality on ground types only *) 
148 
(* Should be used between local variables which must have a ground type *) 
149 
let rec eq_ground t1 t2 = 
150 
match t1.tdesc, t2.tdesc with 
151 
 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal > true 
152 
 Tenum tl, Tenum tl' when tl == tl' > true 
153 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > List.for_all2 eq_ground tl tl' 
154 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > List.for_all2 (fun (_, t) (_, t') > eq_ground t t') fl fl' 
155 
 (Tconst t, _) > 
156 
let def_t = get_type_definition t in 
157 
eq_ground def_t t2 
158 
 (_, Tconst t) > 
159 
let def_t = get_type_definition t in 
160 
eq_ground t1 def_t 
161 
 Tarrow (t1,t2), Tarrow (t1',t2') > eq_ground t1 t1' && eq_ground t2 t2' 
162 
 Tclock t1', Tclock t2' > eq_ground t1' t2' 
163 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
164 
 Tarray (e1, t1'), Tarray (e2, t2') > Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' 
165 
 _ > false 
166  
167 
(** [unify t1 t2] unifies types [t1] and [t2] 
168 
using standard destructive unification. 
169 
Raises [Unify (t1,t2)] if the types are not unifiable. 
170 
[t1] is a expected/formal/spec type, [t2] is a computed/real/implem type, 
171 
so in case of unification error: expected type [t1], got type [t2]. 
172 
If [sub]typing is allowed, [t2] may be a subtype of [t1]. 
173 
If [semi] unification is required, 
174 
[t1] should furthermore be an instance of [t2] 
175 
and constants are handled differently.*) 
176 
let unify ?(sub=false) ?(semi=false) t1 t2 = 
177 
let rec unif t1 t2 = 
178 
let t1 = repr t1 in 
179 
let t2 = repr t2 in 
180 
if t1==t2 then 
181 
() 
182 
else 
183 
match t1.tdesc,t2.tdesc with 
184 
(* strictly subtyping cases first *) 
185 
 _ , Tclock t2 when sub && (get_clock_base_type t1 = None) > 
186 
unif t1 t2 
187 
 _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) > 
188 
unif t1 t2 
189 
(* This case is not mandatory but will keep "older" types *) 
190 
 Tvar, Tvar > 
191 
if t1.tid < t2.tid then 
192 
t2.tdesc < Tlink t1 
193 
else 
194 
t1.tdesc < Tlink t2 
195 
 Tvar, _ when (not semi) && (not (occurs t1 t2)) > 
196 
t1.tdesc < Tlink t2 
197 
 _, Tvar when (not (occurs t2 t1)) > 
198 
t2.tdesc < Tlink t1 
199 
 Tarrow (t1,t2), Tarrow (t1',t2') > 
200 
begin 
201 
unif t2 t2'; 
202 
unif t1' t1 
203 
end 
204 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > 
205 
List.iter2 unif tl tl' 
206 
 Ttuple [t1] , _ > unif t1 t2 
207 
 _ , Ttuple [t2] > unif t1 t2 
208 
 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > 
209 
List.iter2 (fun (_, t) (_, t') > unif t t') fl fl' 
210 
 Tclock _, Tstatic _ 
211 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 
212 
 Tclock t1', Tclock t2' > unif t1' t2' 
213 
 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal 
214 
 Tunivar, _  _, Tunivar > () 
215 
 (Tconst t, _) > 
216 
let def_t = get_type_definition t in 
217 
unif def_t t2 
218 
 (_, Tconst t) > 
219 
let def_t = get_type_definition t in 
220 
unif t1 def_t 
221 
 Tenum tl, Tenum tl' when tl == tl' > () 
222 
 Tstatic (e1, t1'), Tstatic (e2, t2') 
223 
 Tarray (e1, t1'), Tarray (e2, t2') > 
224 
let eval_const = 
225 
if semi 
226 
then (fun c > Some (Dimension.mkdim_ident Location.dummy_loc c)) 
227 
else (fun c > None) in 
228 
begin 
229 
unif t1' t2'; 
230 
Dimension.eval Basic_library.eval_env eval_const e1; 
231 
Dimension.eval Basic_library.eval_env eval_const e2; 
232 
Dimension.unify ~semi:semi e1 e2; 
233 
end 
234 
 _,_ > raise (Unify (t1, t2)) 
235 
in unif t1 t2 
236  
237 
(* Expected type ty1, got type ty2 *) 
238 
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc = 
239 
try 
240 
unify ~sub:sub ~semi:semi ty1 ty2 
241 
with 
242 
 Unify _ > 
243 
raise (Error (loc, Type_clash (ty1,ty2))) 
244 
 Dimension.Unify _ > 
245 
raise (Error (loc, Type_clash (ty1,ty2))) 
246  
247 
let rec type_struct_const_field loc (label, c) = 
248 
if Hashtbl.mem field_table label 
249 
then let tydec = Hashtbl.find field_table label in 
250 
let tydec_struct = get_struct_type_fields tydec in 
251 
let ty_label = type_coretype (fun d > ()) (List.assoc label tydec_struct) in 
252 
begin 
253 
try_unify ty_label (type_const loc c) loc; 
254 
type_coretype (fun d > ()) tydec 
255 
end 
256 
else raise (Error (loc, Unbound_value ("struct field " ^ label))) 
257  
258 
and type_const loc c = 
259 
match c with 
260 
 Const_int _ > Type_predef.type_int 
261 
 Const_real _ > Type_predef.type_real 
262 
 Const_float _ > Type_predef.type_real 
263 
 Const_array ca > let d = Dimension.mkdim_int loc (List.length ca) in 
264 
let ty = new_var () in 
265 
List.iter (fun e > try_unify ty (type_const loc e) loc) ca; 
266 
Type_predef.type_array d ty 
267 
 Const_tag t > 
268 
if Hashtbl.mem tag_table t 
269 
then type_coretype (fun d > ()) (Hashtbl.find tag_table t) 
270 
else raise (Error (loc, Unbound_value ("enum tag " ^ t))) 
271 
 Const_struct fl > 
272 
let ty_struct = new_var () in 
273 
begin 
274 
let used = 
275 
List.fold_left 
276 
(fun acc (l, c) > 
277 
if List.mem l acc 
278 
then raise (Error (loc, Already_bound ("struct field " ^ l))) 
279 
else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc) 
280 
[] fl in 
281 
try 
282 
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in 
283 
(* List.iter (fun l > Format.eprintf "total: %s@." l) total; 
284 
List.iter (fun l > Format.eprintf "used: %s@." l) used; *) 
285 
let undef = List.find (fun l > not (List.mem l used)) total 
286 
in raise (Error (loc, Unbound_value ("struct field " ^ undef))) 
287 
with Not_found > 
288 
ty_struct 
289 
end 
290 
 Const_string _ > assert false (* string should only appear in annotations *) 
291  
292 
(* The following typing functions take as parameter an environment [env] 
293 
and whether the element being typed is expected to be constant [const]. 
294 
[env] is a pair composed of: 
295 
 a map from ident to type, associating to each ident, i.e. 
296 
variables, constants and (imported) nodes, its type including whether 
297 
it is constant or not. This latter information helps in checking constant 
298 
propagation policy in Lustre. 
299 
 a vdecl list, in order to modify types of declared variables that are 
300 
later discovered to be clocks during the typing process. 
301 
*) 
302 
let check_constant loc const_expected const_real = 
303 
if const_expected && not const_real 
304 
then raise (Error (loc, Not_a_constant)) 
305  
306 
let rec type_add_const env const arg targ = 
307 
if const 
308 
then let d = 
309 
if is_dimension_type targ 
310 
then dimension_of_expr arg 
311 
else Dimension.mkdim_var () in 
312 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 
313 
Dimension.eval Basic_library.eval_env eval_const d; 
314 
let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in 
315 
(match Types.get_static_value targ with 
316 
 None > () 
317 
 Some d' > try_unify targ real_static_type arg.expr_loc); 
318 
real_static_type 
319 
else targ 
320  
321 
(* emulates a subtyping relation between types t and (d : t), 
322 
used during node applications and assignments *) 
323 
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = 
324 
let loc = real_arg.expr_loc in 
325 
let const = const  (Types.get_static_value formal_type <> None) in 
326 
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in 
327 
(*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;*) 
328 
try_unify ~sub:sub formal_type real_type loc 
329  
330 
and type_ident env in_main loc const id = 
331 
type_expr env in_main const (expr_of_ident id loc) 
332  
333 
(* typing an application implies: 
334 
 checking that const formal parameters match real const (maybe symbolic) arguments 
335 
 checking type adequation between formal and real arguments 
336 
An application may embed an homomorphic/internal function, in which case we need to split 
337 
it in many calls 
338 
*) 
339 
and type_appl env in_main loc const f args = 
340 
let targs = List.map (type_expr env in_main const) args in 
341 
if Basic_library.is_internal_fun f && List.exists is_tuple_type targs 
342 
then 
343 
try 
344 
let targs = Utils.transpose_list (List.map type_list_of_type targs) in 
345 
Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs) 
346 
with 
347 
Utils.TransposeError (l, l') > raise (Error (loc, WrongMorphism (l, l'))) 
348 
else 
349 
type_dependent_call env in_main loc const f (List.combine args targs) 
350  
351 
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *) 
352 
and type_dependent_call env in_main loc const f targs = 
353 
let tins, touts = new_var (), new_var () in 
354 
let tfun = Type_predef.type_arrow tins touts in 
355 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
356 
let tins = type_list_of_type tins in 
357 
if List.length targs <> List.length tins then 
358 
raise (Error (loc, WrongArity (List.length tins, List.length targs))) 
359 
else 
360 
begin 
361 
List.iter2 (fun (a,t) ti > 
362 
let t' = type_add_const env (const  Types.get_static_value ti <> None) a t 
363 
in try_unify ~sub:true ti t' a.expr_loc) targs tins; 
364 
touts 
365 
end 
366  
367 
(* type a simple call without dependent types 
368 
but possible homomorphic extension. 
369 
[targs] is here a list of arguments' types. *) 
370 
and type_simple_call env in_main loc const f targs = 
371 
let tins, touts = new_var (), new_var () in 
372 
let tfun = Type_predef.type_arrow tins touts in 
373 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
374 
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*) 
375 
try_unify ~sub:true tins (type_of_type_list targs) loc; 
376 
touts 
377  
378 
(** [type_expr env in_main expr] types expression [expr] in environment 
379 
[env], expecting it to be [const] or not. *) 
380 
and type_expr env in_main const expr = 
381 
let resulting_ty = 
382 
match expr.expr_desc with 
383 
 Expr_const c > 
384 
let ty = type_const expr.expr_loc c in 
385 
let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in 
386 
expr.expr_type < ty; 
387 
ty 
388 
 Expr_ident v > 
389 
let tyv = 
390 
try 
391 
Env.lookup_value (fst env) v 
392 
with Not_found > 
393 
Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr; 
394 
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) 
395 
in 
396 
let ty = instantiate (ref []) (ref []) tyv in 
397 
let ty' = 
398 
if const 
399 
then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ()) 
400 
else new_var () in 
401 
try_unify ty ty' expr.expr_loc; 
402 
expr.expr_type < ty; 
403 
ty 
404 
 Expr_array elist > 
405 
let ty_elt = new_var () in 
406 
List.iter (fun e > try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist; 
407 
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in 
408 
let ty = Type_predef.type_array d ty_elt in 
409 
expr.expr_type < ty; 
410 
ty 
411 
 Expr_access (e1, d) > 
412 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; 
413 
let ty_elt = new_var () in 
414 
let d = Dimension.mkdim_var () in 
415 
type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt); 
416 
expr.expr_type < ty_elt; 
417 
ty_elt 
418 
 Expr_power (e1, d) > 
419 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in 
420 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; 
421 
Dimension.eval Basic_library.eval_env eval_const d; 
422 
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
423 
let ty = Type_predef.type_array d ty_elt in 
424 
expr.expr_type < ty; 
425 
ty 
426 
 Expr_tuple elist > 
427 
let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in 
428 
expr.expr_type < ty; 
429 
ty 
430 
 Expr_ite (c, t, e) > 
431 
type_subtyping_arg env in_main const c Type_predef.type_bool; 
432 
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in 
433 
expr.expr_type < ty; 
434 
ty 
435 
 Expr_appl (id, args, r) > 
436 
(* application of non internal function is not legal in a constant 
437 
expression *) 
438 
(match r with 
439 
 None > () 
440 
 Some (x, l) > 
441 
check_constant expr.expr_loc const false; 
442 
let expr_x = expr_of_ident x expr.expr_loc in 
443 
let typ_l = 
444 
Type_predef.type_clock 
445 
(type_const expr.expr_loc (Const_tag l)) in 
446 
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); 
447 
let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in 
448 
expr.expr_type < touts; 
449 
touts 
450 
 Expr_fby (e1,e2) 
451 
 Expr_arrow (e1,e2) > 
452 
(* fby/arrow is not legal in a constant expression *) 
453 
check_constant expr.expr_loc const false; 
454 
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in 
455 
expr.expr_type < ty; 
456 
ty 
457 
 Expr_pre e > 
458 
(* pre is not legal in a constant expression *) 
459 
check_constant expr.expr_loc const false; 
460 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in 
461 
expr.expr_type < ty; 
462 
ty 
463 
 Expr_when (e1,c,l) > 
464 
(* when is not legal in a constant expression *) 
465 
check_constant expr.expr_loc const false; 
466 
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in 
467 
let expr_c = expr_of_ident c expr.expr_loc in 
468 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
469 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
470 
expr.expr_type < ty; 
471 
ty 
472 
 Expr_merge (c,hl) > 
473 
(* merge is not legal in a constant expression *) 
474 
check_constant expr.expr_loc const false; 
475 
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in 
476 
let expr_c = expr_of_ident c expr.expr_loc in 
477 
let typ_l = Type_predef.type_clock typ_in in 
478 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
479 
expr.expr_type < typ_out; 
480 
typ_out 
481 
in 
482 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty); 
483 
resulting_ty 
484  
485 
and type_branches env in_main loc const hl = 
486 
let typ_in = new_var () in 
487 
let typ_out = new_var () in 
488 
try 
489 
let used_labels = 
490 
List.fold_left (fun accu (t, h) > 
491 
unify typ_in (type_const loc (Const_tag t)); 
492 
type_subtyping_arg env in_main const h typ_out; 
493 
if List.mem t accu 
494 
then raise (Error (loc, Already_bound t)) 
495 
else t :: accu) [] hl in 
496 
let type_labels = get_enum_type_tags (coretype_type typ_in) in 
497 
if List.sort compare used_labels <> List.sort compare type_labels 
498 
then let unbound_tag = List.find (fun t > not (List.mem t used_labels)) type_labels in 
499 
raise (Error (loc, Unbound_value ("branching tag " ^ unbound_tag))) 
500 
else (typ_in, typ_out) 
501 
with Unify (t1, t2) > 
502 
raise (Error (loc, Type_clash (t1,t2))) 
503  
504 
(** [type_eq env eq] types equation [eq] in environment [env] *) 
505 
let type_eq env in_main undefined_vars eq = 
506 
(* Check undefined variables, type lhs *) 
507 
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 
508 
let ty_lhs = type_expr env in_main false expr_lhs in 
509 
(* Check multiple variable definitions *) 
510 
let define_var id uvars = 
511 
try 
512 
ignore(IMap.find id uvars); 
513 
IMap.remove id uvars 
514 
with Not_found > 
515 
raise (Error (eq.eq_loc, Already_defined id)) 
516 
in 
517 
(* check assignment of declared constant, assignment of clock *) 
518 
let ty_lhs = 
519 
type_of_type_list 
520 
(List.map2 (fun ty id > 
521 
if get_static_value ty <> None 
522 
then raise (Error (eq.eq_loc, Assigned_constant id)) else 
523 
match get_clock_base_type ty with 
524 
 None > ty 
525 
 Some ty > ty) 
526 
(type_list_of_type ty_lhs) eq.eq_lhs) in 
527 
let undefined_vars = 
528 
List.fold_left (fun uvars v > define_var v uvars) undefined_vars eq.eq_lhs in 
529 
(* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned 
530 
to a (always nonconstant) lhs variable *) 
531 
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; 
532 
undefined_vars 
533  
534  
535 
(* [type_coreclock env ck id loc] types the type clock declaration [ck] 
536 
in environment [env] *) 
537 
let type_coreclock env ck id loc = 
538 
match ck.ck_dec_desc with 
539 
 Ckdec_any  Ckdec_pclock (_,_) > () 
540 
 Ckdec_bool cl > 
541 
let dummy_id_expr = expr_of_ident id loc in 
542 
let when_expr = 
543 
List.fold_left 
544 
(fun expr (x, l) > 
545 
{expr_tag = new_tag (); 
546 
expr_desc= Expr_when (expr,x,l); 
547 
expr_type = new_var (); 
548 
expr_clock = Clocks.new_var true; 
549 
expr_delay = Delay.new_var (); 
550 
expr_loc=loc; 
551 
expr_annot = None}) 
552 
dummy_id_expr cl 
553 
in 
554 
ignore (type_expr env false false when_expr) 
555  
556 
let rec check_type_declaration loc cty = 
557 
match cty with 
558 
 Tydec_clock ty 
559 
 Tydec_array (_, ty) > check_type_declaration loc ty 
560 
 Tydec_const tname > 
561 
if not (Hashtbl.mem type_table cty) 
562 
then raise (Error (loc, Unbound_type tname)); 
563 
 _ > () 
564  
565 
let type_var_decl vd_env env vdecl = 
566 
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; 
567 
let eval_const id = Types.get_static_value (Env.lookup_value env id) in 
568 
let type_dim d = 
569 
begin 
570 
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int; 
571 
Dimension.eval Basic_library.eval_env eval_const d; 
572 
end in 
573 
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in 
574 
let ty_status = 
575 
if vdecl.var_dec_const 
576 
then Type_predef.type_static (Dimension.mkdim_var ()) ty 
577 
else ty in 
578 
let new_env = Env.add_value env vdecl.var_id ty_status in 
579 
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; 
580 
vdecl.var_type < ty_status; 
581 
new_env 
582  
583 
let type_var_decl_list vd_env env l = 
584 
List.fold_left (type_var_decl vd_env) env l 
585  
586 
let type_of_vlist vars = 
587 
let tyl = List.map (fun v > v.var_type) vars in 
588 
type_of_type_list tyl 
589  
590 
let add_vdecl vd_env vdecl = 
591 
if List.exists (fun v > v.var_id = vdecl.var_id) vd_env 
592 
then raise (Error (vdecl.var_loc, Already_bound vdecl.var_id)) 
593 
else vdecl::vd_env 
594  
595 
let check_vd_env vd_env = 
596 
ignore (List.fold_left add_vdecl [] vd_env) 
597  
598 
(** [type_node env nd loc] types node [nd] in environment env. The 
599 
location is used for error reports. *) 
600 
let type_node env nd loc = 
601 
let is_main = nd.node_id = !Options.main_node in 
602 
let vd_env_ol = nd.node_outputs@nd.node_locals in 
603 
let vd_env = nd.node_inputs@vd_env_ol in 
604 
check_vd_env vd_env; 
605 
let init_env = env in 
606 
let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in 
607 
let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in 
608 
let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in 
609 
let new_env = Env.overwrite env delta_env in 
610 
let undefined_vars_init = 
611 
List.fold_left 
612 
(fun uvs v > IMap.add v.var_id () uvs) 
613 
IMap.empty vd_env_ol in 
614 
let undefined_vars = 
615 
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs 
616 
in 
617 
(* Typing asserts *) 
618 
List.iter (fun assert_ > 
619 
let assert_expr = assert_.assert_expr in 
620 
type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool 
621 
) nd.node_asserts; 
622 

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