Revision a38c681e src/typing.ml
src/typing.ml | ||
---|---|---|
244 | 244 |
| Dimension.Unify _ -> |
245 | 245 |
raise (Error (loc, Type_clash (ty1,ty2))) |
246 | 246 |
|
247 |
(* ty1 is a subtype of ty2 *) |
|
248 |
(* |
|
249 |
let rec sub_unify sub ty1 ty2 = |
|
250 |
match (repr ty1).tdesc, (repr ty2).tdesc with |
|
251 |
| Ttuple tl1 , Ttuple tl2 -> |
|
252 |
if List.length tl1 <> List.length tl2 |
|
253 |
then raise (Unify (ty1, ty2)) |
|
254 |
else List.iter2 (sub_unify sub) tl1 tl2 |
|
255 |
| Ttuple [t1] , _ -> sub_unify sub t1 ty2 |
|
256 |
| _ , Ttuple [t2] -> sub_unify sub ty1 t2 |
|
257 |
| Tstruct tl1 , Tstruct tl2 -> |
|
258 |
if List.map fst tl1 <> List.map fst tl2 |
|
259 |
then raise (Unify (ty1, ty2)) |
|
260 |
else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2 |
|
261 |
| Tclock t1 , Tclock t2 -> sub_unify sub t1 t2 |
|
262 |
| Tclock t1 , _ when sub -> sub_unify sub t1 ty2 |
|
263 |
| Tstatic (d1, t1) , Tstatic (d2, t2) -> |
|
264 |
begin |
|
265 |
sub_unify sub t1 t2; |
|
266 |
Dimension.eval Basic_library.eval_env (fun c -> None) d1; |
|
267 |
Dimension.eval Basic_library.eval_env (fun c -> None) d2; |
|
268 |
Dimension.unify d1 d2 |
|
269 |
end |
|
270 |
| Tstatic (r_d, t1) , _ when sub -> sub_unify sub t1 ty2 |
|
271 |
| _ -> unify ty1 ty2 |
|
272 |
*) |
|
273 |
|
|
274 | 247 |
let rec type_struct_const_field loc (label, c) = |
275 | 248 |
if Hashtbl.mem field_table label |
276 | 249 |
then let tydec = Hashtbl.find field_table label in |
... | ... | |
330 | 303 |
if const_expected && not const_real |
331 | 304 |
then raise (Error (loc, Not_a_constant)) |
332 | 305 |
|
333 |
let rec type_standard_args env in_main const expr_list = |
|
334 |
let ty_list = |
|
335 |
List.map |
|
336 |
(fun e -> let ty = dynamic_type (type_expr env in_main const e) in |
|
337 |
match get_clock_base_type ty with |
|
338 |
| None -> ty |
|
339 |
| Some ty -> ty) |
|
340 |
expr_list in |
|
341 |
let ty_res = new_var () in |
|
342 |
List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list; |
|
343 |
ty_res |
|
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 |
|
344 | 320 |
|
345 | 321 |
(* emulates a subtyping relation between types t and (d : t), |
346 | 322 |
used during node applications and assignments *) |
347 | 323 |
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type = |
348 | 324 |
let loc = real_arg.expr_loc in |
349 | 325 |
let const = const || (Types.get_static_value formal_type <> None) in |
350 |
let real_type = type_expr env in_main const real_arg in |
|
351 |
let real_type = |
|
352 |
if const |
|
353 |
then let d = |
|
354 |
if is_dimension_type real_type |
|
355 |
then dimension_of_expr real_arg |
|
356 |
else Dimension.mkdim_var () in |
|
357 |
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in |
|
358 |
Dimension.eval Basic_library.eval_env eval_const d; |
|
359 |
let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in |
|
360 |
(match Types.get_static_value real_type with |
|
361 |
| None -> () |
|
362 |
| Some d' -> try_unify real_type real_static_type loc); |
|
363 |
real_static_type |
|
364 |
else real_type in |
|
326 |
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in |
|
365 | 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;*) |
366 | 328 |
try_unify ~sub:sub formal_type real_type loc |
367 | 329 |
|
... | ... | |
375 | 337 |
it in many calls |
376 | 338 |
*) |
377 | 339 |
and type_appl env in_main loc const f args = |
378 |
let args = expr_list_of_expr args in
|
|
379 |
if Basic_library.is_internal_fun f && List.exists is_tuple_expr 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
|
|
380 | 342 |
then |
381 | 343 |
try |
382 |
let args = Utils.transpose_list (List.map expr_list_of_expr args) in
|
|
383 |
Types.type_of_type_list (List.map (type_call env in_main loc const f) args)
|
|
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)
|
|
384 | 346 |
with |
385 | 347 |
Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l'))) |
386 | 348 |
else |
387 |
type_call env in_main loc const f args
|
|
349 |
type_dependent_call env in_main loc const f (List.combine args targs)
|
|
388 | 350 |
|
389 |
(* type a (single) call. [args] is here a list of arguments. *)
|
|
390 |
and type_call env in_main loc const f args =
|
|
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 =
|
|
391 | 353 |
let tins, touts = new_var (), new_var () in |
392 | 354 |
let tfun = Type_predef.type_arrow tins touts in |
393 | 355 |
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; |
394 | 356 |
let tins = type_list_of_type tins in |
395 |
if List.length args <> List.length tins then |
|
396 |
raise (Error (loc, WrongArity (List.length tins, List.length args))) |
|
357 |
if List.length targs <> List.length tins then
|
|
358 |
raise (Error (loc, WrongArity (List.length tins, List.length targs)))
|
|
397 | 359 |
else |
398 |
List.iter2 (type_subtyping_arg env in_main const) args tins; |
|
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; |
|
399 | 376 |
touts |
400 | 377 |
|
401 | 378 |
(** [type_expr env in_main expr] types expression [expr] in environment |
... | ... | |
425 | 402 |
expr.expr_type <- ty; |
426 | 403 |
ty |
427 | 404 |
| Expr_array elist -> |
428 |
let ty_elt = type_standard_args env in_main const elist in |
|
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; |
|
429 | 407 |
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in |
430 | 408 |
let ty = Type_predef.type_array d ty_elt in |
431 | 409 |
expr.expr_type <- ty; |
... | ... | |
441 | 419 |
let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in |
442 | 420 |
type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int; |
443 | 421 |
Dimension.eval Basic_library.eval_env eval_const d; |
444 |
let ty_elt = type_standard_args env in_main const [e1] in
|
|
422 |
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
|
|
445 | 423 |
let ty = Type_predef.type_array d ty_elt in |
446 | 424 |
expr.expr_type <- ty; |
447 | 425 |
ty |
... | ... | |
451 | 429 |
ty |
452 | 430 |
| Expr_ite (c, t, e) -> |
453 | 431 |
type_subtyping_arg env in_main const c Type_predef.type_bool; |
454 |
let ty = type_standard_args env in_main const [t; e] in
|
|
432 |
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
|
|
455 | 433 |
expr.expr_type <- ty; |
456 | 434 |
ty |
457 | 435 |
| Expr_appl (id, args, r) -> |
... | ... | |
466 | 444 |
Type_predef.type_clock |
467 | 445 |
(type_const expr.expr_loc (Const_tag l)) in |
468 | 446 |
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); |
469 |
let touts = type_appl env in_main expr.expr_loc const id args in
|
|
447 |
let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in
|
|
470 | 448 |
expr.expr_type <- touts; |
471 | 449 |
touts |
472 | 450 |
| Expr_fby (e1,e2) |
473 | 451 |
| Expr_arrow (e1,e2) -> |
474 | 452 |
(* fby/arrow is not legal in a constant expression *) |
475 | 453 |
check_constant expr.expr_loc const false; |
476 |
let ty = type_standard_args env in_main const [e1; e2] in
|
|
454 |
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
|
|
477 | 455 |
expr.expr_type <- ty; |
478 | 456 |
ty |
479 | 457 |
| Expr_pre e -> |
480 | 458 |
(* pre is not legal in a constant expression *) |
481 | 459 |
check_constant expr.expr_loc const false; |
482 |
let ty = type_standard_args env in_main const [e] in
|
|
460 |
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
|
|
483 | 461 |
expr.expr_type <- ty; |
484 | 462 |
ty |
485 | 463 |
| Expr_when (e1,c,l) -> |
... | ... | |
488 | 466 |
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in |
489 | 467 |
let expr_c = expr_of_ident c expr.expr_loc in |
490 | 468 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
491 |
(*update_clock env in_main c expr.expr_loc typ_l;*) |
|
492 |
let ty = type_standard_args env in_main const [e1] in |
|
469 |
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in |
|
493 | 470 |
expr.expr_type <- ty; |
494 | 471 |
ty |
495 | 472 |
| Expr_merge (c,hl) -> |
... | ... | |
499 | 476 |
let expr_c = expr_of_ident c expr.expr_loc in |
500 | 477 |
let typ_l = Type_predef.type_clock typ_in in |
501 | 478 |
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; |
502 |
(*update_clock env in_main c expr.expr_loc typ_l;*) |
|
503 | 479 |
expr.expr_type <- typ_out; |
504 | 480 |
typ_out |
505 | 481 |
in |
... | ... | |
524 | 500 |
else (typ_in, typ_out) |
525 | 501 |
with Unify (t1, t2) -> |
526 | 502 |
raise (Error (loc, Type_clash (t1,t2))) |
527 |
(* |
|
528 |
and update_clock env in_main id loc typ = |
|
529 |
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*) |
|
530 |
try |
|
531 |
let vdecl = List.find (fun v -> v.var_id = id) (snd env) |
|
532 |
in vdecl.var_type <- typ |
|
533 |
with |
|
534 |
Not_found -> |
|
535 |
raise (Error (loc, Unbound_value ("clock " ^ id))) |
|
536 |
*) |
|
503 |
|
|
537 | 504 |
(** [type_eq env eq] types equation [eq] in environment [env] *) |
538 | 505 |
let type_eq env in_main undefined_vars eq = |
539 | 506 |
(* Check undefined variables, type lhs *) |
Also available in: Unified diff