diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/finite_map.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 21 | ||||
| -rw-r--r-- | src/type_internal.ml | 109 | ||||
| -rw-r--r-- | src/type_internal.mli | 6 |
4 files changed, 127 insertions, 11 deletions
diff --git a/src/finite_map.ml b/src/finite_map.ml index 32629fdc..6220e027 100644 --- a/src/finite_map.ml +++ b/src/finite_map.ml @@ -53,6 +53,7 @@ module type Fmap = sig val empty : 'a t val is_empty : 'a t -> bool val from_list : (k * 'a) list -> 'a t + val to_list : 'a t -> (k * 'a) list val from_list2 : k list -> 'a list -> 'a t val insert : 'a t -> (k * 'a) -> 'a t (* Keys from the right argument replace those from the left *) @@ -117,6 +118,7 @@ module Fmap_map(Key : Set.OrderedType) : Fmap if (M.mem k m2) then M.add k v res else res) m1 M.empty + let to_list m = M.fold (fun k v res -> (k,v)::res) m [] let remove m k = M.remove k m let pp_map pp_key pp_val ppf m = let l = M.fold (fun k v l -> (k,v)::l) m [] in diff --git a/src/type_check.ml b/src/type_check.ml index ccf079d0..e9f42ffb 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -18,9 +18,6 @@ let typ_error l msg = l (msg )) -let resolve_constraints a = a -let resolve_params a = a - let rec field_equivs fields fmaps = match fields with | [] -> Some [] @@ -1061,7 +1058,7 @@ and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * let t',cs' = type_consistent l d_env u t in let (e,t,_,cs2,ef2) = check_exp envs t' e in let cs = resolve_constraints cs@cs1@cs'@cs2 in - let tannot = resolve_params(Some((params,t),tag,cs,ef)) in + let tannot = check_tannot l (Some((params,t),tag,cs,ef)) cs ef (*in top level, must be pure_e*) in (LB_aux (LB_val_explicit(typ,pat',e),(l,tannot)),env,cs,ef) | None -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Some")) | LB_val_implicit(pat,e) -> @@ -1069,7 +1066,7 @@ and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * let (pat',env,cs1,u) = check_pattern envs (new_t ()) pat in let (e,t',_,cs2,ef) = check_exp envs u e in let cs = resolve_constraints cs1@cs2 in - let tannot = resolve_params(Some(([],t'),Emp,cs,ef)) in + let tannot = check_tannot l (Some(([],t'),Emp,cs,ef)) cs ef (* see above *) in (LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,ef) (*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*) @@ -1213,7 +1210,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let t = typ_to_t typ in let p_t = new_t () in let ef = new_e () in - t,p_t,Some((ids,{t=Tfn(p_t,t,ef)}),Emp,constraints,pure_e) in + t,p_t,Some((ids,{t=Tfn(p_t,t,ef)}),Emp,constraints,ef) in let check t_env = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) -> @@ -1221,23 +1218,25 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, let u,cs = type_consistent l d_env t' param_t in let exp',_,_,constraints,ef = check_exp (Env(d_env,Envmap.union t_env t_env')) ret_t exp in (*let _ = (Pretty_print.pp_exp Format.std_formatter) exp' in*) - (FCL_aux((FCL_Funcl(id,pat',exp')),(l,tannot)),constraints'@cs@constraints)) funcls) in + (FCL_aux((FCL_Funcl(id,pat',exp')),(l,tannot)),((constraints'@cs@constraints),ef))) funcls) in match (in_env,tannot) with | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),Emp,c',eft') -> let u,constraints,eft = subst params u constraints eft in let t,c',eft' = subst p' t c' eft' in let t',cs = type_consistent l d_env t u in let t_env = if is_rec then t_env else Envmap.remove t_env id in - let funcls,cs = check t_env in + let funcls,cs_ef = check t_env 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 = resolve_params tannot in + let tannot = check_tannot l tannot cs' ef in (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))), Env(d_env,Envmap.insert t_env (id,tannot)) | _ , _-> let t_env = if is_rec then Envmap.insert t_env (id,tannot) else t_env in - let funcls,cs = check t_env in + let funcls,cs_ef = check t_env 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 = resolve_params tannot in + let tannot = check_tannot l tannot cs' ef 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 67021cc9..a298d046 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -144,6 +144,33 @@ let lookup_field_type (field: string) ((id,r_kind,fields) : rec_env) : tannot = then List.assoc field fields else None +(* eval an nexp as much as possible *) +let rec eval_nexp n = + match n.nexp with + | Nconst i -> n + | Nmult(n1,n2) -> + (match (eval_nexp n1).nexp,(eval_nexp n2).nexp with + | Nconst i1, Nconst i2 -> {nexp=Nconst (i1*i2)} + | _,_ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const")) + | Nadd(n1,n2) -> + (match (eval_nexp n1).nexp,(eval_nexp n2).nexp with + | Nconst i1, Nconst i2 -> {nexp=Nconst (i1+i2)} + | _,_ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const")) + | Nneg n1 -> + (match (eval_nexp n1).nexp with + | Nconst i -> {nexp = Nconst(- i)} + | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const")) + | N2n n1 -> + (match (eval_nexp n1).nexp with + | Nconst i -> + let rec two_pow = function + | 0 -> 1; + | n -> 2* (two_pow n-1) in + {nexp = Nconst(two_pow i)} + | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const")) + | Nvar _ | Nuvar _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Var found in eval_to_nexp_const") + + let v_count = ref 0 let t_count = ref 0 let n_count = ref 0 @@ -177,6 +204,25 @@ let new_e _ = let i = !e_count in e_count := i + 1; { effect = Euvar { eindex = i; esubst = None }} + +let rec fresh_var i mkr bindings = + let v = "v" ^ (string_of_int i) in + match Envmap.apply bindings v with + | Some _ -> fresh_var (i+1) mkr bindings + | None -> mkr v + +let fresh_tvar bindings t = + match t.t with + | Tuvar { index = i } -> fresh_var i (fun v -> t.t <- Tvar v; (v,{k=K_Typ})) bindings +let fresh_nvar bindings n = + match n.nexp with + | Nuvar { nindex = i } -> fresh_var i (fun v -> n.nexp <- Nvar v; (v,{k=K_Nat})) bindings +let fresh_ovar bindings o = + match o.order with + | Ouvar { oindex = i } -> fresh_var i (fun v -> o.order <- Ovar v; (v,{k=K_Ord})) bindings +let fresh_evar bindings e = + match e.effect with + | Euvar { eindex = i } -> fresh_var i (fun v -> e.effect <- Evar v; (v,{k=K_Efct})) bindings let nat_t = {t = Tapp("enum",[TA_nexp{nexp= Nconst 0};TA_nexp{nexp = Nconst max_int};])} let unit_t = { t = Tid "unit" } @@ -297,6 +343,57 @@ let subst k_env t cs e = in t_subst subst_env t, cs_subst subst_env cs, e_subst subst_env e +let rec t_remove_unifications s_env t = + match t.t with + | Tvar _ | Tid _-> s_env + | Tuvar _ -> Envmap.insert s_env (fresh_tvar s_env t) + | Tfn(t1,t2,e) -> e_remove_unifications (t_remove_unifications (t_remove_unifications s_env t1) t2) e + | Ttup(ts) -> List.fold_right (fun t s_env -> t_remove_unifications s_env t) ts s_env + | Tapp(i,args) -> List.fold_right (fun t s_env -> ta_remove_unifications s_env t) args s_env + | Tabbrev(ti,ta) -> (t_remove_unifications (t_remove_unifications s_env ti) ta) +and ta_remove_unifications s_env ta = + match ta with + | TA_typ t -> (t_remove_unifications s_env t) + | TA_nexp n -> (n_remove_unifications s_env n) + | TA_eft e -> (e_remove_unifications s_env e) + | TA_ord o -> (o_remove_unifications s_env o) +and n_remove_unifications s_env n = + match n.nexp with + | Nvar _ | Nconst _-> s_env + | Nuvar _ -> Envmap.insert s_env (fresh_nvar s_env n) + | N2n n1 | Nneg n1 -> (n_remove_unifications s_env n1) + | Nadd(n1,n2) | Nmult(n1,n2) -> (n_remove_unifications (n_remove_unifications s_env n1) n2) +and o_remove_unifications s_env o = + match o.order with + | Ouvar _ -> Envmap.insert s_env (fresh_ovar s_env o) + | _ -> s_env +and e_remove_unifications s_env e = + match e.effect with + | Euvar _ -> Envmap.insert s_env (fresh_evar s_env e) + | _ -> s_env + +let rec cs_subst t_env cs = + match cs with + | [] -> [] + | Eq(l,n1,n2)::cs -> Eq(l,n_subst t_env n1,n_subst t_env n2)::(cs_subst t_env cs) + | GtEq(l,n1,n2)::cs -> GtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs) + | LtEq(l,n1,n2)::cs -> LtEq(l,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs) + | In(l,s,ns)::cs -> InS(l,n_subst t_env {nexp=Nvar s},ns)::(cs_subst t_env cs) + | InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs) + +let subst k_env t cs e = + let subst_env = Envmap.from_list + (List.map (fun (id,k) -> (id, + match k.k with + | K_Typ -> TA_typ (new_t ()) + | K_Nat -> TA_nexp (new_n ()) + | K_Ord -> TA_ord (new_o ()) + | K_Efct -> TA_eft (new_e ()) + | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "substitution given an environment with a non-base-kind kind"))) k_env) + in + t_subst subst_env t, cs_subst subst_env cs, e_subst subst_env e + + let rec string_of_list sep string_of = function | [] -> "" | [x] -> string_of x @@ -634,3 +731,15 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 = | _,_ -> let t',cs = type_consistent l d_env t1 t2 in (t',cs,e) and type_coerce l d_env t1 e t2 = type_coerce_internal l d_env t1 [] e t2 [] + +let resolve_constraints a = a + + +let check_tannot l annot constraints efs = + match annot with + | Some((params,t),tag,cs,e) -> + effects_eq l efs e; + let params = Envmap.to_list (t_remove_unifications (Envmap.from_list params) t) in + Some((params,t),tag,cs,e) + | None -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation") + diff --git a/src/type_internal.mli b/src/type_internal.mli index 785f3c76..76223409 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -114,6 +114,12 @@ val new_e : unit -> effect val subst : (string * kind) list -> t -> nexp_range list -> effect -> t * nexp_range list * effect val get_abbrev : def_envs -> t -> (t * nexp_range list * effect) +(*May raise an exception if a contradiction is found*) +val resolve_constraints : nexp_range list -> nexp_range list + +(*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 + (* type_consistent is similar to a standard type equality, except in the case of [[consistent t1 t2]] where t1 and t2 are both enum types and t1 is contained within the range of t2: i.e. enum 2 5 is consistent with enum 0 10, but not vice versa. |