diff options
| -rw-r--r-- | src/type_check.ml | 3 | ||||
| -rw-r--r-- | src/type_internal.ml | 22 |
2 files changed, 13 insertions, 12 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 17f2275b..fbcad6b2 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -433,6 +433,7 @@ let simp_exp e l t = E_aux(e,(l,Base(([],t),Emp_local,[],pure_e))) let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):tannot exp): (tannot exp * t * tannot emap * nexp_range list * effect) = let Env(d_env,t_env) = envs in + let expect_t,_ = get_abbrev d_env expect_t in let rebuild annot = E_aux(e,(l,annot)) in match e with | E_block exps -> @@ -474,6 +475,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Tabbrev(_,t),_ -> t,expect_t | _,Tabbrev(_,e) -> t,e | _,_ -> t,expect_t in + (*let _ = Printf.printf "On general id check, expect_t %s, t %s, tactual %s, expect_actual %s\n" (t_to_string expect_t) (t_to_string t) (t_to_string t_actual) (t_to_string expect_actual) in*) (match t_actual.t,expect_actual.t with | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value") | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> @@ -1653,6 +1655,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let check t_env imp_param = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) -> + (*let _ = Printf.printf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) let (pat',t_env',cs_p,t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in (*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*) let exp',_,_,cs_e,ef = diff --git a/src/type_internal.ml b/src/type_internal.ml index 069b6775..e0771218 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1679,10 +1679,9 @@ let rec type_consistent_internal co d_env t1 cs1 t2 cs2 = let t2,cs2' = get_abbrev d_env t2 in let cs1,cs2 = cs1@cs1',cs2@cs2' in let csp = cs1@cs2 in - match t1.t,t2.t with - | Tabbrev(_,t1),Tabbrev(_,t2) -> type_consistent_internal co d_env t1 cs1 t2 cs2 - | Tabbrev(_,t1),_ -> type_consistent_internal co d_env t1 cs1 t2 cs2 - | _,Tabbrev(_,t2) -> type_consistent_internal co d_env t1 cs1 t2 cs2 + let t1_actual = match t1.t with | Tabbrev(_,t1) -> t1 | _ -> t1 in + let t2_actual = match t2.t with | Tabbrev(_,t2) -> t2 | _ -> t2 in + match t1_actual.t,t2_actual.t with | Tvar v1,Tvar v2 -> if v1 = v2 then (t2,csp) else eq_error l ("Type variables " ^ v1 ^ " and " ^ v2 ^ " do not match and cannot be unified") @@ -1732,21 +1731,20 @@ let rec type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 = let l = get_c_loc co in let t1,cs1' = get_abbrev d_env t1 in let t2,cs2' = get_abbrev d_env t2 in + let t1_actual = match t1.t with | Tabbrev(_,t1) -> t1 | _ -> t1 in + let t2_actual = match t2.t with | Tabbrev(_,t2) -> t2 | _ -> t2 in let cs1,cs2 = cs1@cs1',cs2@cs2' in let csp = cs1@cs2 in - match t1.t,t2.t with - | Tabbrev(_,t1),Tabbrev(_,t2) -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 - | Tabbrev(_,t1),_ -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 - | _,Tabbrev(_,t2) -> type_coerce_internal co d_env is_explicit t1 cs1 e t2 cs2 + match t1_actual.t,t2_actual.t with | Toptions(to1,Some to2),_ -> - if (conforms_to_t d_env false true to1 t2 || conforms_to_t d_env false true to2 t2) - then begin t1.t <- t2.t; (t2,csp,pure_e,e) end + if (conforms_to_t d_env false true to1 t2_actual || conforms_to_t d_env false true to2 t2_actual) + then begin t1_actual.t <- t2_actual.t; (t2,csp,pure_e,e) end else eq_error l ("Neither " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2) ^ " can match expected type " ^ (t_to_string t2)) | Toptions(to1,None),_ -> (t2,csp,pure_e,e) | _,Toptions(to1,Some to2) -> - if (conforms_to_t d_env false true to1 t1 || conforms_to_t d_env false true to2 t1) - then begin t2.t <- t1.t; (t1,csp,pure_e,e) end + if (conforms_to_t d_env false true to1 t1_actual || conforms_to_t d_env false true to2 t1_actual) + then begin t2_actual.t <- t1_actual.t; (t1,csp,pure_e,e) end else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2)) | _,Toptions(to1,None) -> (t1,csp,pure_e,e) | Ttup t1s, Ttup t2s -> |