Revision 66359a5e
Added by Pierre-Loïc Garoche about 7 years ago
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
[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