| 396 |
} |
} |
| 397 |
) |
) |
| 398 |
|
|
| 399 |
|
let let_decl p e = |
| 400 |
|
let (_,e) = expr e in |
| 401 |
|
{ Typed.let_pat = pat p; |
| 402 |
|
Typed.let_body = e; |
| 403 |
|
Typed.let_compiled = None } |
| 404 |
|
|
| 405 |
|
(* III. Type-checks *) |
| 406 |
|
|
| 407 |
module Env = StringMap |
module Env = StringMap |
| 408 |
|
type env = Types.descr Env.t |
| 409 |
|
|
| 410 |
open Typed |
open Typed |
| 411 |
|
|
| 412 |
|
let warning loc msg = |
| 413 |
|
Format.fprintf Format.std_formatter |
| 414 |
|
"Warning %a:@\n%s@\n" Location.print_loc loc msg |
| 415 |
|
|
| 416 |
let check loc t s msg = |
let check loc t s msg = |
| 417 |
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg)) |
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s, msg)) |
| 504 |
|
|
| 505 |
let constr' = Sequence.approx (Types.cap Sequence.any constr) in |
let constr' = Sequence.approx (Types.cap Sequence.any constr) in |
| 506 |
let exact = Types.subtype (Sequence.star constr') constr in |
let exact = Types.subtype (Sequence.star constr') constr in |
|
(* |
|
|
Format.fprintf Format.std_formatter |
|
|
"(Map) constr = %a@; exact = %b\n@." Types.Print.print_descr constr exact; |
|
|
*) |
|
| 507 |
(* Note: |
(* Note: |
| 508 |
- could be more precise by integrating the decomposition |
- could be more precise by integrating the decomposition |
| 509 |
of constr inside Sequence.map. |
of constr inside Sequence.map. |
| 632 |
tres |
tres |
| 633 |
) |
) |
| 634 |
|
|
| 635 |
|
and type_let_decl env l = |
| 636 |
|
let acc = Types.descr (Patterns.accept l.let_pat) in |
| 637 |
|
let t = type_check env l.let_body acc true in |
| 638 |
|
let res = Patterns.filter t l.let_pat in |
| 639 |
|
List.map (fun (x,t) -> (x, Types.descr t)) res |
| 640 |
|
|
| 641 |
|
and type_rec_funs env l = |
| 642 |
|
let types = |
| 643 |
|
List.fold_left |
| 644 |
|
(fun accu -> function {let_body={exp_descr=Abstraction a}} as l -> |
| 645 |
|
let t = a.fun_typ in |
| 646 |
|
let acc = Types.descr (Patterns.accept l.let_pat) in |
| 647 |
|
if not (Types.subtype t acc) then |
| 648 |
|
raise_loc l.let_body.exp_loc (NonExhaustive (Types.diff t acc)); |
| 649 |
|
let res = Patterns.filter t l.let_pat in |
| 650 |
|
List.fold_left (fun accu (x,t) -> (x, Types.descr t)::accu) accu res |
| 651 |
|
| _ -> assert false) [] l |
| 652 |
|
in |
| 653 |
|
let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in |
| 654 |
|
List.iter |
| 655 |
|
(function { let_body = { exp_descr = Abstraction a } } as l -> |
| 656 |
|
ignore (type_check env' l.let_body Types.any false) |
| 657 |
|
| _ -> assert false) l; |
| 658 |
|
types |
| 659 |
|
|
| 660 |
|
|
| 661 |
and type_op loc op args = |
and type_op loc op args = |
| 662 |
match (op,args) with |
match (op,args) with |
| 663 |
| "+", [loc1,t1; loc2,t2] -> |
| "+", [loc1,t1; loc2,t2] -> |
| 680 |
Types.any |
Types.any |
| 681 |
| "raise", [loc1,t1] -> |
| "raise", [loc1,t1] -> |
| 682 |
Types.empty |
Types.empty |
| 683 |
|
| "int_of", [loc1,t1] -> |
| 684 |
|
check loc1 t1 Sequence.string |
| 685 |
|
"The argument of int_of must a string"; |
| 686 |
|
if not (Types.subtype t1 Builtin.intstr) then |
| 687 |
|
warning loc "This application of int_of may fail"; |
| 688 |
|
Types.interval Intervals.any |
| 689 |
| _ -> assert false |
| _ -> assert false |
| 690 |
|
|
| 691 |
and type_int_binop f loc1 t1 loc2 t2 = |
and type_int_binop f loc1 t1 loc2 t2 = |
Parent Directory
| 
Revision Log
| 
Patch