Revision 66359a5e src/typing.ml
src/typing.ml  

24  24 
overwritten, yet this makes notations far lighter.*) 
25  25 
open LustreSpec 
26  26 
open Corelang 
27 
open Types


27 
(* open Types *)


28  28 
open Format 
29  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  
30  52 
let pp_typing_env fmt env = 
31  53 
Env.pp_env print_ty fmt env 
32  54  
...  ...  
34  56 
type [ty]. False otherwise. *) 
35  57 
let rec occurs tvar ty = 
36  58 
let ty = repr ty in 
37 
match ty.tdesc with


59 
match type_desc ty with


38  60 
 Tvar > ty=tvar 
39  61 
 Tarrow (t1, t2) > 
40  62 
(occurs tvar t1)  (occurs tvar t2) 
...  ...  
46  68 
 Tstatic (_, t) 
47  69 
 Tclock t 
48  70 
 Tlink t > occurs tvar t 
49 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > false


71 
 Tenum _  Tconst _  Tunivar  Tbasic _ > false


50  72  
51  73 
(** Promote monomorphic type variables to polymorphic type variables. *) 
52  74 
(* Generalize by sideeffects *) 
53  75 
let rec generalize ty = 
54 
match ty.tdesc with


76 
match type_desc ty with


55  77 
 Tvar > 
56  78 
(* No scopes, always generalize *) 
57  79 
ty.tdesc < Tunivar 
...  ...  
66  88 
 Tclock t 
67  89 
 Tlink t > 
68  90 
generalize t 
69 
 Tenum _  Tconst _  Tunivar  Tint  Treal  Tbool  Trat > ()


91 
 Tenum _  Tconst _  Tunivar  Tbasic _ > ()


70  92  
71  93 
(** Downgrade polymorphic type variables to monomorphic type variables *) 
72  94 
let rec instantiate inst_vars inst_dim_vars ty = 
73  95 
let ty = repr ty in 
74  96 
match ty.tdesc with 
75 
 Tenum _  Tconst _  Tvar  Tint  Treal  Tbool  Trat > ty


97 
 Tenum _  Tconst _  Tvar  Tbasic _ > ty


76  98 
 Tarrow (t1,t2) > 
77  99 
{ty with tdesc = 
78  100 
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))} 
...  ...  
101  123 
let rec type_coretype type_dim cty = 
102  124 
match (*get_repr_type*) cty with 
103  125 
 Tydec_any > new_var () 
104 
 Tydec_int > Type_predef.type_int


105 
 Tydec_real > Type_predef.type_real


126 
 Tydec_int > type_int 

127 
 Tydec_real > (* Type_predef. *)type_real


106  128 
(*  Tydec_float > Type_predef.type_real *) 
107 
 Tydec_bool > Type_predef.type_bool


108 
 Tydec_clock ty > Type_predef.type_clock (type_coretype type_dim ty)


109 
 Tydec_const c > Type_predef.type_const c


110 
 Tydec_enum tl > Type_predef.type_enum tl


111 
 Tydec_struct fl > Type_predef.type_struct (List.map (fun (f, ty) > (f, type_coretype type_dim ty)) fl)


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)


112  134 
 Tydec_array (d, ty) > 
113  135 
begin 
114  136 
let d = Dimension.copy (ref []) d in 
115  137 
type_dim d; 
116 
Type_predef.type_array d (type_coretype type_dim ty)


138 
(* Type_predef. *)type_array d (type_coretype type_dim ty)


117  139 
end 
118  140  
119  141 
(* [coretype_type] is the reciprocal of [type_typecore] *) 
120  142 
let rec coretype_type ty = 
121  143 
match (repr ty).tdesc with 
122  144 
 Tvar > Tydec_any 
123 
 Tint > Tydec_int 

124 
 Treal > Tydec_real 

125 
 Tbool > Tydec_bool 

145 
 Tbasic _ > basic_coretype_type ty 

126  146 
 Tconst c > Tydec_const c 
127  147 
 Tclock t > Tydec_clock (coretype_type t) 
128  148 
 Tenum tl > Tydec_enum tl 
...  ...  
149  169 
let t2 = repr t2 in 
150  170 
t1==t2  
151  171 
match t1.tdesc, t2.tdesc with 
152 
 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal > true


172 
 Tbasic t1, Tbasic t2 when t1 == t2 > true


153  173 
 Tenum tl, Tenum tl' when tl == tl' > true 
154  174 
 Ttuple tl, Ttuple tl' when List.length tl = List.length tl' > List.for_all2 eq_ground tl tl' 
155  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' 
...  ...  
211  231 
 Tclock _, Tstatic _ 
212  232 
 Tstatic _, Tclock _ > raise (Unify (t1, t2)) 
213  233 
 Tclock t1', Tclock t2' > unif t1' t2' 
214 
 Tint, Tint  Tbool, Tbool  Trat, Trat  Treal, Treal


234 
 Tbasic t1, Tbasic t2 when t1 == t2 > ()


215  235 
 Tunivar, _  _, Tunivar > () 
216  236 
 (Tconst t, _) > 
217  237 
let def_t = get_type_definition t in 
...  ...  
232  252 
Dimension.eval Basic_library.eval_env eval_const e2; 
233  253 
Dimension.unify ~semi:semi e1 e2; 
234  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 

235  259 
 _,_ > raise (Unify (t1, t2)) 
236  260 
in unif t1 t2 
237  261  
...  ...  
245  269 
 Dimension.Unify _ > 
246  270 
raise (Error (loc, Type_clash (ty1,ty2))) 
247  271  
248 
let rec type_struct_const_field loc (label, c) = 

272 
let rec type_struct_const_field ?(is_annot=false) loc (label, c) =


249  273 
if Hashtbl.mem field_table label 
250  274 
then let tydef = Hashtbl.find field_table label in 
251  275 
let tydec = (typedef_of_top tydef).tydef_desc in 
252  276 
let tydec_struct = get_struct_type_fields tydec in 
253  277 
let ty_label = type_coretype (fun d > ()) (List.assoc label tydec_struct) in 
254  278 
begin 
255 
try_unify ty_label (type_const loc c) loc; 

279 
try_unify ty_label (type_const ~is_annot loc c) loc;


256  280 
type_coretype (fun d > ()) tydec 
257  281 
end 
258  282 
else raise (Error (loc, Unbound_value ("struct field " ^ label))) 
259  283  
260 
and type_const loc c = 

284 
and type_const ?(is_annot=false) loc c =


261  285 
match c with 
262 
 Const_int _ > Type_predef.type_int


263 
 Const_real _ > Type_predef.type_real


286 
 Const_int _ > (* Type_predef. *)type_int


287 
 Const_real _ > (* Type_predef. *)type_real


264  288 
(*  Const_float _ > Type_predef.type_real *) 
265  289 
 Const_array ca > let d = Dimension.mkdim_int loc (List.length ca) in 
266  290 
let ty = new_var () in 
267 
List.iter (fun e > try_unify ty (type_const loc e) loc) ca; 

268 
Type_predef.type_array d ty


291 
List.iter (fun e > try_unify ty (type_const ~is_annot loc e) loc) ca;


292 
(* Type_predef. *)type_array d ty


269  293 
 Const_tag t > 
270  294 
if Hashtbl.mem tag_table t 
271  295 
then 
...  ...  
284  308 
(fun acc (l, c) > 
285  309 
if List.mem l acc 
286  310 
then raise (Error (loc, Already_bound ("struct field " ^ l))) 
287 
else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc) 

311 
else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc)


288  312 
[] fl in 
289  313 
try 
290  314 
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in 
...  ...  
295  319 
with Not_found > 
296  320 
ty_struct 
297  321 
end 
298 
 Const_string _ > assert false (* string should only appear in annotations *) 

322 
 Const_string _ > if is_annot then (* Type_predef. *)type_string else assert false (* string should only appear in annotations *)


299  323  
300  324 
(* The following typing functions take as parameter an environment [env] 
301  325 
and whether the element being typed is expected to be constant [const]. 
...  ...  
318  342 
if is_dimension_type targ 
319  343 
then dimension_of_expr arg 
320  344 
else Dimension.mkdim_var () in 
321 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in


345 
let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in


322  346 
Dimension.eval Basic_library.eval_env eval_const d; 
323 
let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in


324 
(match Types.get_static_value targ with


347 
let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in


348 
(match (* Types. *)get_static_value targ with


325  349 
 None > () 
326  350 
 Some d' > try_unify targ real_static_type arg.expr_loc); 
327  351 
real_static_type 
...  ...  
331  355 
used during node applications and assignments *) 
332  356 
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = 
333  357 
let loc = real_arg.expr_loc in 
334 
let const = const  (Types.get_static_value formal_type <> None) in


358 
let const = const  ((* Types. *)get_static_value formal_type <> None) in


335  359 
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in 
336  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;*) 
337  361 
try_unify ~sub:sub formal_type real_type loc 
...  ...  
348  372 
then 
349  373 
try 
350  374 
let targs = Utils.transpose_list (List.map type_list_of_type targs) in 
351 
Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)


352 
with 

375 
(* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)


376 
with


353  377 
Utils.TransposeError (l, l') > raise (Error (loc, WrongMorphism (l, l'))) 
354 
else 

378 


379 
else ( 

355  380 
type_dependent_call env in_main loc const f (List.combine args targs) 
381 
) 

356  382  
357  383 
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *) 
358  384 
and type_dependent_call env in_main loc const f targs = 
359 
(*Format.eprintf "Typing.type_dependent_call %s@." f;*)


385 
(* Format.eprintf "Typing.type_dependent_call %s@." f; *)


360  386 
let tins, touts = new_var (), new_var () in 
361 
let tfun = Type_predef.type_arrow tins touts 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; *) 

362  390 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
391 
(* Format.eprintf "type subtyping@."; *) 

363  392 
let tins = type_list_of_type tins in 
364  393 
if List.length targs <> List.length tins then 
365  394 
raise (Error (loc, WrongArity (List.length tins, List.length targs))) 
366  395 
else 
367  396 
begin 
368 
List.iter2 (fun (a,t) ti > 

369 
let t' = type_add_const env (const  Types.get_static_value ti <> None) a t 

370 
in try_unify ~sub:true ti t' a.expr_loc) targs tins; 

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; 

371  407 
touts 
372  408 
end 
373  409  
...  ...  
376  412 
[targs] is here a list of arguments' types. *) 
377  413 
and type_simple_call env in_main loc const f targs = 
378  414 
let tins, touts = new_var (), new_var () in 
379 
let tfun = Type_predef.type_arrow tins touts in


415 
let tfun = (* Type_predef. *)type_arrow tins touts in


380  416 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 
381  417 
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*) 
382  418 
try_unify ~sub:true tins (type_of_type_list targs) loc; 
...  ...  
384  420  
385  421 
(** [type_expr env in_main expr] types expression [expr] in environment 
386  422 
[env], expecting it to be [const] or not. *) 
387 
and type_expr env in_main const expr = 

423 
and type_expr ?(is_annot=false) env in_main const expr =


388  424 
let resulting_ty = 
389  425 
match expr.expr_desc with 
390  426 
 Expr_const c > 
391 
let ty = type_const expr.expr_loc c in 

392 
let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in


393 
expr.expr_type < ty; 

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;


394  430 
ty 
395  431 
 Expr_ident v > 
396  432 
let tyv = 
397  433 
try 
398  434 
Env.lookup_value (fst env) v 
399  435 
with Not_found > 
400 
Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr; 

436 
Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr;


401  437 
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v))) 
402  438 
in 
403  439 
let ty = instantiate (ref []) (ref []) tyv in 
404  440 
let ty' = 
405  441 
if const 
406 
then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())


442 
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ())


407  443 
else new_var () in 
408  444 
try_unify ty ty' expr.expr_loc; 
409 
expr.expr_type < ty; 

445 
expr.expr_type < Expr_type_hub.export ty;


410  446 
ty 
411  447 
 Expr_array elist > 
412  448 
let ty_elt = new_var () in 
413  449 
List.iter (fun e > try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist; 
414  450 
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in 
415 
let ty = Type_predef.type_array d ty_elt in


416 
expr.expr_type < ty; 

451 
let ty = (* Type_predef. *)type_array d ty_elt in


452 
expr.expr_type < Expr_type_hub.export ty;


417  453 
ty 
418  454 
 Expr_access (e1, d) > 
419 
type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) Type_predef.type_int;


455 
type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;


420  456 
let ty_elt = new_var () in 
421  457 
let d = Dimension.mkdim_var () in 
422 
type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);


423 
expr.expr_type < ty_elt; 

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;


424  460 
ty_elt 
425  461 
 Expr_power (e1, d) > 
426 
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in


427 
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;


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;


428  464 
Dimension.eval Basic_library.eval_env eval_const d; 
429  465 
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
430 
let ty = Type_predef.type_array d ty_elt in


431 
expr.expr_type < ty; 

466 
let ty = (* Type_predef. *)type_array d ty_elt in


467 
expr.expr_type < Expr_type_hub.export ty;


432  468 
ty 
433  469 
 Expr_tuple elist > 
434 
let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in 

435 
expr.expr_type < ty; 

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;


436  472 
ty 
437  473 
 Expr_ite (c, t, e) > 
438 
type_subtyping_arg env in_main const c Type_predef.type_bool;


474 
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;


439  475 
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in 
440 
expr.expr_type < ty; 

476 
expr.expr_type < Expr_type_hub.export ty;


441  477 
ty 
442  478 
 Expr_appl (id, args, r) > 
443  479 
(* application of non internal function is not legal in a constant 
...  ...  
446  482 
 None > () 
447  483 
 Some c > 
448  484 
check_constant expr.expr_loc const false; 
449 
type_subtyping_arg env in_main const c Type_predef.type_bool);


485 
type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);


450  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; 

451  489 
let touts = type_appl env in_main expr.expr_loc const id args_list in 
452 
args.expr_type < new_ty (Ttuple (List.map (fun a > a.expr_type) args_list)); 

453 
expr.expr_type < touts; 

490 
expr.expr_type < Expr_type_hub.export touts; 

454  491 
touts 
455  492 
 Expr_fby (e1,e2) 
456  493 
 Expr_arrow (e1,e2) > 
457  494 
(* fby/arrow is not legal in a constant expression *) 
458  495 
check_constant expr.expr_loc const false; 
459  496 
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in 
460 
expr.expr_type < ty; 

497 
expr.expr_type < Expr_type_hub.export ty;


461  498 
ty 
462  499 
 Expr_pre e > 
463  500 
(* pre is not legal in a constant expression *) 
464  501 
check_constant expr.expr_loc const false; 
465  502 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in 
466 
expr.expr_type < ty; 

503 
expr.expr_type < Expr_type_hub.export ty;


467  504 
ty 
468  505 
 Expr_when (e1,c,l) > 
469  506 
(* when is not legal in a constant expression *) 
470  507 
check_constant expr.expr_loc const false; 
471 
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in


508 
let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in


472  509 
let expr_c = expr_of_ident c expr.expr_loc in 
473  510 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
474  511 
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in 
475 
expr.expr_type < ty; 

512 
expr.expr_type < Expr_type_hub.export ty;


476  513 
ty 
477  514 
 Expr_merge (c,hl) > 
478  515 
(* merge is not legal in a constant expression *) 
479  516 
check_constant expr.expr_loc const false; 
480  517 
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in 
481  518 
let expr_c = expr_of_ident c expr.expr_loc in 
482 
let typ_l = Type_predef.type_clock typ_in in


519 
let typ_l = (* Type_predef. *)type_clock typ_in in


483  520 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 
484 
expr.expr_type < typ_out; 

521 
expr.expr_type < Expr_type_hub.export typ_out;


485  522 
typ_out 
486  523 
in 
487 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);


524 
Log.report ~level:3 (fun fmt > Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty);


488  525 
resulting_ty 
489  526  
490 
and type_branches env in_main loc const hl = 

527 
and type_branches ?(is_annot=false) env in_main loc const hl =


491  528 
let typ_in = new_var () in 
492  529 
let typ_out = new_var () in 
493  530 
try 
494  531 
let used_labels = 
495  532 
List.fold_left (fun accu (t, h) > 
496 
unify typ_in (type_const loc (Const_tag t)); 

533 
unify typ_in (type_const ~is_annot loc (Const_tag t));


497  534 
type_subtyping_arg env in_main const h typ_out; 
498  535 
if List.mem t accu 
499  536 
then raise (Error (loc, Already_bound t)) 
...  ...  
548  585 
(fun expr (x, l) > 
549  586 
{expr_tag = new_tag (); 
550  587 
expr_desc= Expr_when (expr,x,l); 
551 
expr_type = new_var (); 

588 
expr_type = Types.Main.new_var ();


552  589 
expr_clock = Clocks.new_var true; 
553  590 
expr_delay = Delay.new_var (); 
554  591 
expr_loc=loc; 
...  ...  
571  608 
let type_var_decl vd_env env vdecl = 
572  609 
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*) 
573  610 
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; 
574 
let eval_const id = Types.get_static_value (Env.lookup_value env id) in


611 
let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in


575  612 
let type_dim d = 
576  613 
begin 
577 
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;


614 
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;


578  615 
Dimension.eval Basic_library.eval_env eval_const d; 
579  616 
end in 
580  617 
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in 
581  618  
582  619 
let ty_static = 
583  620 
if vdecl.var_dec_const 
584 
then Type_predef.type_static (Dimension.mkdim_var ()) ty


621 
then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty


585  622 
else ty in 
586  623 
(match vdecl.var_dec_value with 
587  624 
 None > () 
588  625 
 Some v > type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static); 
589 
try_unify ty_static vdecl.var_type vdecl.var_loc;


626 
try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;


590  627 
let new_env = Env.add_value env vdecl.var_id ty_static in 
591  628 
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc; 
592  629 
(*Format.eprintf "END %a@." Types.print_ty ty_static;*) 
...  ...  
596  633 
List.fold_left (type_var_decl vd_env) env l 
597  634  
598  635 
let type_of_vlist vars = 
599 
let tyl = List.map (fun v > v.var_type) vars in 

636 
let tyl = List.map (fun v > Expr_type_hub.import v.var_type) vars in


600  637 
type_of_type_list tyl 
601  638  
602  639 
let add_vdecl vd_env vdecl = 
...  ...  
631  668 
(* Typing asserts *) 
632  669 
List.iter (fun assert_ > 
633  670 
let assert_expr = assert_.assert_expr in 
634 
type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool


671 
type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool


635  672 
) nd.node_asserts; 
673 
(* Typing annots *) 

674 
List.iter (fun annot > 

675 
List.iter (fun (_, eexpr) > ignore (type_expr ~is_annot:true (new_env, vd_env) false false eexpr.eexpr_qfexpr)) annot.annots 

676 
) nd.node_annot; 

636  677 

637  678 
(* check that table is empty *) 
638  679 
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 
...  ...  
644  685 
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in 
645  686 
generalize ty_node; 
646  687 
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *) 
647 
nd.node_type < ty_node; 

688 
nd.node_type < Expr_type_hub.export ty_node;


648  689 
Env.add_value env nd.node_id ty_node 
649  690  
650  691 
let type_imported_node env nd loc = 
...  ...  
661  702 
raise (Error (loc, Poly_imported_node nd.nodei_id)); 
662  703 
*) 
663  704 
let new_env = Env.add_value env nd.nodei_id ty_node in 
664 
nd.nodei_type < ty_node; 

705 
nd.nodei_type < Expr_type_hub.export ty_node;


665  706 
new_env 
666  707  
667  708 
let type_top_const env cdecl = 
...  ...  
670  711 
if is_dimension_type ty 
671  712 
then dimension_of_const cdecl.const_loc cdecl.const_value 
672  713 
else Dimension.mkdim_var () in 
673 
let ty = Type_predef.type_static d ty in


714 
let ty = (* Type_predef. *)type_static d ty in


674  715 
let new_env = Env.add_value env cdecl.const_id ty in 
675 
cdecl.const_type < ty; 

716 
cdecl.const_type < Expr_type_hub.export ty;


676  717 
new_env 
677  718  
678  719 
let type_top_consts env clist = 
...  ...  
700  741 
let get_type_of_call decl = 
701  742 
match decl.top_decl_desc with 
702  743 
 Node nd > 
703 
let (in_typ, out_typ) = split_arrow nd.node_type in


744 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in


704  745 
type_list_of_type in_typ, type_list_of_type out_typ 
705  746 
 ImportedNode nd > 
706 
let (in_typ, out_typ) = split_arrow nd.nodei_type in


747 
let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in


707  748 
type_list_of_type in_typ, type_list_of_type out_typ 
708  749 
 _ > assert false 
709  750  
...  ...  
723  764 
let uneval_vdecl_generics vdecl = 
724  765 
if vdecl.var_dec_const 
725  766 
then 
726 
match get_static_value vdecl.var_type with


727 
 None > (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)


767 
match get_static_value (Expr_type_hub.import vdecl.var_type) with


768 
 None > (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)


728  769 
 Some d > Dimension.uneval vdecl.var_id d 
729  770  
730  771 
let uneval_node_generics vdecls = 
...  ...  
788  829  
789  830 
let check_typedef_compat header = 
790  831 
List.iter check_typedef_top header 
832 
end 

791  833  
834 
include Make(Types.Main) (struct 

835 
type type_expr = Types.Main.type_expr 

836 
let import x = x 

837 
let export x = x 

838 
end) 

792  839 
(* Local Variables: *) 
793  840 
(* compilecommand:"make C .." *) 
794  841 
(* End: *) 
Also available in: Unified diff