| 493 |
|
|
| 494 |
let glb = State.ref "Typer.glb_env" TypeEnv.empty |
let glb = State.ref "Typer.glb_env" TypeEnv.empty |
| 495 |
|
|
|
|
|
| 496 |
let register_global_types b = |
let register_global_types b = |
| 497 |
List.iter |
List.iter |
| 498 |
(fun (v,p) -> |
(fun (v,p) -> |
| 499 |
if TypeEnv.mem v !glb |
if TypeEnv.mem v !glb |
| 500 |
then raise_loc_generic p.loc ("Multiple definition for type " ^ v) |
then raise_loc_generic p.loc ("Multiple definition for type " ^ v) |
| 501 |
) b; |
) b; |
| 502 |
|
let old_glb = !glb in |
| 503 |
|
try |
| 504 |
glb := derecurs_def !glb b; |
glb := derecurs_def !glb b; |
| 505 |
let b = List.map (fun (v,p) -> (v,p,compile (derecurs !glb p))) b in |
let b = List.map (fun (v,p) -> (v,p,compile (derecurs !glb p))) b in |
| 506 |
flush_defs (); |
flush_defs (); |
| 507 |
flush_fv (); |
flush_fv (); |
| 508 |
List.iter |
let b = |
| 509 |
|
List.map |
| 510 |
(fun (v,p,s) -> |
(fun (v,p,s) -> |
| 511 |
if not (IdSet.is_empty (fv_descr s)) then |
if not (IdSet.is_empty (fv_descr s)) then |
| 512 |
raise_loc_generic p.loc "Capture variables are not allowed in types"; |
raise_loc_generic p.loc |
| 513 |
|
"Capture variables are not allowed in types"; |
| 514 |
let t = typ s in |
let t = typ s in |
| 515 |
if (p.loc <> noloc) && (Types.is_empty t) then |
if (p.loc <> noloc) && (Types.is_empty t) then |
| 516 |
warning p.loc ("This definition yields an empty type for " ^ v); |
warning p.loc |
| 517 |
Types.Print.register_global v t) b |
("This definition yields an empty type for " ^ v); |
| 518 |
|
(v,t)) b in |
| 519 |
|
List.iter (fun (v,t) -> Types.Print.register_global v t) b |
| 520 |
|
with e -> |
| 521 |
|
glb := old_glb; |
| 522 |
|
raise e |
| 523 |
|
|
| 524 |
let dump_global_types ppf = |
let dump_global_types ppf = |
| 525 |
TypeEnv.iter (fun v _ -> Format.fprintf ppf " %s" v) !glb |
TypeEnv.iter (fun v _ -> Format.fprintf ppf " %s" v) !glb |
| 931 |
and type_rec_funs env l = |
and type_rec_funs env l = |
| 932 |
let types = |
let types = |
| 933 |
List.fold_left |
List.fold_left |
| 934 |
(fun accu -> function {let_body={exp_descr=Abstraction a}} as l -> |
(fun accu -> function |
| 935 |
let t = a.fun_typ in |
| { exp_descr=Abstraction { fun_typ = t; fun_name = Some f } } -> |
| 936 |
let acc = Types.descr (Patterns.accept l.let_pat) in |
(f,t) :: accu |
| 937 |
if not (Types.subtype t acc) then |
| _ -> assert false |
| 938 |
raise_loc l.let_body.exp_loc (NonExhaustive (Types.diff t acc)); |
) [] l |
|
let res = Patterns.filter t l.let_pat in |
|
|
List.fold_left (fun accu (x,t) -> (x, Types.descr t)::accu) accu res |
|
|
| _ -> assert false) [] l |
|
| 939 |
in |
in |
| 940 |
let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in |
let env' = List.fold_left (fun env (x,t) -> Env.add x t env) env types in |
| 941 |
List.iter |
List.iter (fun e -> ignore (type_check env' e Types.any false)) l; |
|
(function { let_body = { exp_descr = Abstraction a } } as l -> |
|
|
ignore (type_check env' l.let_body Types.any false) |
|
|
| _ -> assert false) l; |
|
| 942 |
types |
types |
| 943 |
|
|
| 944 |
|
|