Revision b616fe7a src/typing.ml
| src/typing.ml | ||
|---|---|---|
| 417 | 417 |
(* typing an application implies: |
| 418 | 418 |
- checking that const formal parameters match real const (maybe symbolic) arguments |
| 419 | 419 |
- checking type adequation between formal and real arguments |
| 420 |
An application may embed an homomorphic/internal function, in which case we need to split |
|
| 421 |
it in many calls |
|
| 420 | 422 |
*) |
| 421 | 423 |
and type_appl env in_main loc const f args = |
| 424 |
let args = expr_list_of_expr args in |
|
| 425 |
if Basic_library.is_internal_fun f && List.exists is_tuple_expr args |
|
| 426 |
then |
|
| 427 |
try |
|
| 428 |
let args = Utils.transpose_list (List.map expr_list_of_expr args) in |
|
| 429 |
Types.type_of_type_list (List.map (type_call env in_main loc const f) args) |
|
| 430 |
with |
|
| 431 |
Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l'))) |
|
| 432 |
else |
|
| 433 |
type_call env in_main loc const f args |
|
| 434 |
|
|
| 435 |
(* type a (single) call. [args] is here a list of arguments. *) |
|
| 436 |
and type_call env in_main loc const f args = |
|
| 422 | 437 |
let tfun = type_ident env in_main loc const f in |
| 423 | 438 |
let tins, touts = split_arrow tfun in |
| 424 | 439 |
let tins = type_list_of_type tins in |
| 425 |
let args = expr_list_of_expr args in |
|
| 426 | 440 |
if List.length args <> List.length tins then |
| 427 | 441 |
raise (Error (loc, WrongArity (List.length args, List.length tins))) |
| 428 | 442 |
else |
| ... | ... | |
| 432 | 446 |
(** [type_expr env in_main expr] types expression [expr] in environment |
| 433 | 447 |
[env], expecting it to be [const] or not. *) |
| 434 | 448 |
and type_expr env in_main const expr = |
| 435 |
let res = |
|
| 449 |
let resulting_ty =
|
|
| 436 | 450 |
match expr.expr_desc with |
| 437 | 451 |
| Expr_const c -> |
| 438 | 452 |
let ty = type_const expr.expr_loc c in |
| ... | ... | |
| 541 | 555 |
let ty = type_expr env in_main const e in |
| 542 | 556 |
expr.expr_type <- ty; |
| 543 | 557 |
ty |
| 544 |
in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res |
|
| 558 |
in |
|
| 559 |
Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty); |
|
| 560 |
resulting_ty |
|
| 545 | 561 |
|
| 546 | 562 |
and type_branches env in_main loc const hl = |
| 547 | 563 |
let typ_in = new_var () in |
Also available in: Unified diff