Project

General

Profile

« Previous | Next » 

Revision 66359a5e

Added by Pierre-Loïc Garoche about 7 years ago

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

View differences:

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 side-effects *)
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
(* compile-command:"make -C .." *)
794 841
(* End: *)

Also available in: Unified diff