diff options
| -rw-r--r-- | src/type_check.ml | 8 | ||||
| -rw-r--r-- | src/type_internal.ml | 7 | ||||
| -rw-r--r-- | src/type_internal.mli | 2 |
3 files changed, 10 insertions, 7 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index b350baf9..4c59791e 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -1485,7 +1485,7 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : let cs = if is_top_level then resolve_constraints cs@cs1@cs2 else cs@cs1@cs2 in let ef = union_effects ef ef2 in let tannot = if is_top_level - then check_tannot l (Base((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) + then check_tannot l (Base((params,t),tag,cs,ef)) None cs ef (*in top level, must be pure_e*) else (Base ((params,t),tag,cs,ef)) in (LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,ef) @@ -1496,7 +1496,7 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : let (e,t',_,cs2,ef) = check_exp envs imp_param u e in let cs = if is_top_level then resolve_constraints cs1@cs2 else cs1@cs2 in let tannot = - if is_top_level then check_tannot l (Base(([],t'),emp_tag,cs,ef)) cs ef (* see above *) + if is_top_level then check_tannot l (Base(([],t'),emp_tag,cs,ef)) None cs ef (* see above *) else (Base (([],t'),emp_tag,cs,ef)) in (LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,ef) @@ -1685,7 +1685,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in let cs' = resolve_constraints cs@constraints in - let tannot = check_tannot l tannot cs' ef in + let tannot = check_tannot l tannot imp_param cs' ef in (*let _ = Printf.printf "check_tannot ok for %s\n" id in*) let funcls = match imp_param with | None | Some {nexp = Nconst _} -> funcls @@ -1698,7 +1698,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let funcls,cs_ef = check t_env None in let cs,ef = ((fun (cses,efses) -> (List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in let cs' = resolve_constraints cs in - let tannot = check_tannot l tannot cs' ef in + let tannot = check_tannot l tannot None cs' ef in (*let _ = Printf.printf "done funcheck case2\n" in*) (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot))) diff --git a/src/type_internal.ml b/src/type_internal.ml index a3b2e0f2..95f48461 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -2240,7 +2240,7 @@ let resolve_constraints cs = complex_constraints -let check_tannot l annot constraints efs = +let check_tannot l annot imp_param constraints efs = match annot with | Base((params,t),tag,cs,e) -> ignore(effects_eq (Specc l) efs e); @@ -2248,7 +2248,10 @@ let check_tannot l annot constraints efs = let params = Envmap.to_list s_env in ignore (remove_internal_unifications s_env); (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *) - Base((params,t),tag,cs,e) + let t' = match (t.t,imp_param) with + | Tfn(p,r,_,e),Some x -> {t = Tfn(p,r,IP_var x,e) } + | _ -> t in + Base((params,t'),tag,cs,e) | NoTyp -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation") | Overload _ -> raise (Reporting_basic.err_unreachable l "check_tannot given overload") diff --git a/src/type_internal.mli b/src/type_internal.mli index d8e99ae9..90127d35 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -167,7 +167,7 @@ val resolve_constraints : nexp_range list -> nexp_range list val do_resolve_constraints : bool ref (*May raise an exception if effects do not match tannot effects, will lift unification variables to fresh type variables *) -val check_tannot : Parse_ast.l -> tannot -> nexp_range list -> effect -> tannot +val check_tannot : Parse_ast.l -> tannot -> nexp option -> nexp_range list -> effect -> tannot val nexp_eq : nexp -> nexp -> bool |