diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/finite_map.ml | 17 | ||||
| -rw-r--r-- | src/pretty_print.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 179 | ||||
| -rw-r--r-- | src/type_internal.ml | 188 | ||||
| -rw-r--r-- | src/type_internal.mli | 6 |
5 files changed, 241 insertions, 151 deletions
diff --git a/src/finite_map.ml b/src/finite_map.ml index 6220e027..c7e427fd 100644 --- a/src/finite_map.ml +++ b/src/finite_map.ml @@ -58,8 +58,13 @@ module type Fmap = sig val insert : 'a t -> (k * 'a) -> 'a t (* Keys from the right argument replace those from the left *) val union : 'a t -> 'a t -> 'a t + (* Function merges the stored value when a key is in the right and the left map *) + val union_merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t val intersect : 'a t -> 'a t -> 'a t + (* Function merges the stored values for shared keys *) + val intersect_merge : ('a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t val big_union : 'a t list -> 'a t + val big_union_merge : ('a -> 'a -> 'a) -> 'a t list -> 'a t val merge : (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t val apply : 'a t -> k -> 'a option val in_dom : k -> 'a t -> bool @@ -94,6 +99,12 @@ module Fmap_map(Key : Set.OrderedType) : Fmap let insert m (k,v) = M.add k v m let union m1 m2 = M.merge (fun k v1 v2 -> match v2 with | None -> v1 | Some _ -> v2) m1 m2 + let union_merge f m1 m2 = + M.merge (fun k v1 v2 -> + match v1,v2 with + | None,None -> None + | None,Some v | Some v,None -> Some v + | Some v1, Some v2 -> Some (f v1 v2)) m1 m2 let merge f m1 m2 = M.merge f m1 m2 let apply m k = try @@ -118,6 +129,11 @@ module Fmap_map(Key : Set.OrderedType) : Fmap if (M.mem k m2) then M.add k v res else res) m1 M.empty + let intersect_merge f m1 m2 = + M.fold (fun k v res -> + match (apply m2 k) with + | None -> res + | Some v2 -> M.add k (f v v2) 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 = @@ -130,6 +146,7 @@ module Fmap_map(Key : Set.OrderedType) : Fmap pp_val v)) l let big_union l = List.fold_left union empty l + let big_union_merge f l = List.fold_left (union_merge f) empty l let domains_disjoint maps = match D.duplicates (List.concat (List.map (fun m -> List.map fst (M.bindings m)) maps)) with | D.No_dups _ -> true diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 5d6e45e7..ab6e0539 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -565,7 +565,7 @@ and pp_format_o o = ^ " Unknown)" let pp_format_tag = function - | Emp -> "Tag_empty" + | Emp_local | Emp_global -> "Tag_empty" | External (Some s) -> "(Tag_extern (Just \""^s^"\"))" | External None -> "(Tag_extern Nothing)" | Default -> "Tag_default" diff --git a/src/type_check.ml b/src/type_check.ml index 044b17c6..dbf55a1a 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -155,7 +155,7 @@ let into_register d_env (t : tannot) : tannot = | _ -> Some((ids, {t= Tapp("register",[TA_typ ty'])}),tag,constraints,eft)) | None -> None -let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * t) = +let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * t) = let (Env(d_env,t_env)) = envs in match p with | P_lit (L_aux(lit,l')) -> @@ -184,20 +184,20 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann | L_string s -> {t = Tid "string"},lit | L_undef -> typ_error l' "Cannot pattern match on undefined") in let t',cs = type_consistent l d_env t expect_t in - (P_aux(P_lit(L_aux(lit,l')),(l,Some(([],t),Emp,cs,pure_e))),Envmap.empty,[],t) + (P_aux(P_lit(L_aux(lit,l')),(l,Some(([],t),Emp_local,cs,pure_e))),Envmap.empty,[],t) | P_wild -> - (P_aux(p,(l,Some(([],expect_t),Emp,[],pure_e))),Envmap.empty,[],expect_t) + (P_aux(p,(l,Some(([],expect_t),Emp_local,[],pure_e))),Envmap.empty,[],expect_t) | P_as(pat,id) -> - let (pat',env,constraints,t) = check_pattern envs expect_t pat in - let tannot = Some(([],t),Emp,[],pure_e) in + let (pat',env,constraints,t) = check_pattern envs emp_tag expect_t pat in + let tannot = Some(([],t),emp_tag,[],pure_e) in (P_aux(P_as(pat',id),(l,tannot)),Envmap.insert env (id_to_string id,tannot),constraints,t) | P_typ(typ,pat) -> let t = typ_to_t typ in - let (pat',env,constraints,u) = check_pattern envs t pat in + let (pat',env,constraints,u) = check_pattern envs emp_tag t pat in let (t',constraint') = type_consistent l d_env u t in (*TODO: This should be a no-op now, should check*) - (P_aux(P_typ(typ,pat'),(l,Some(([],t'),Emp,[],pure_e))),env,constraints@constraint',t) + (P_aux(P_typ(typ,pat'),(l,Some(([],t'),Emp_local,[],pure_e))),env,constraints@constraint',t) | P_id id -> - let tannot = Some(([],expect_t),Emp,[],pure_e) in + let tannot = Some(([],expect_t),emp_tag,[],pure_e) in (P_aux(p,(l,tannot)),Envmap.from_list [(id_to_string id,tannot)],[],expect_t) | P_app(id,pats) -> let i = id_to_string id in @@ -215,12 +215,12 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann | [] -> let _ = type_consistent l d_env unit_t t1 in let t',constraints' = type_consistent l d_env t2 expect_t in (P_aux(P_app(id,[]),(l,Some(([],t'),Constructor,constraints,pure_e))),Envmap.empty,constraints@constraints',t') - | [p] -> let (p',env,constraints,u) = check_pattern envs t1 p in + | [p] -> let (p',env,constraints,u) = check_pattern envs emp_tag t1 p in let (t1',constraint') = type_consistent l d_env u t1 in (*TODO This should be a no-op now, should check *) let t',constraints' = type_consistent l d_env t2 expect_t in (P_aux(P_app(id,[p']),(l,Some(([],t'),Constructor,constraints,pure_e))),env,constraints@constraint'@constraints',t') | pats -> let ((P_aux(P_tup(pats'),_)),env,constraints,u) = - check_pattern envs t1 (P_aux(P_tup(pats),(l,annot))) in + check_pattern envs emp_tag t1 (P_aux(P_tup(pats),(l,annot))) in let (t1',constraint') = type_consistent l d_env u t1 in (*TODO This should be a no-op now, should check *) let t',constraints' = type_consistent l d_env t2 expect_t in (P_aux(P_app(id,pats'),(l,Some(([],t'),Constructor,constraints,pure_e))),env,constraint'@constraints@constraints',t')) @@ -234,7 +234,7 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann List.map (fun (tan,id,l,pat) -> let (Some((vs,t),tag,cs,eft)) = tan in let t,cs,_ = subst vs t cs eft in - let (pat,env,constraints,u) = check_pattern envs t pat in + let (pat,env,constraints,u) = check_pattern envs emp_tag t pat in let (t',cs') = type_consistent l d_env u t in let pat = FP_aux(FP_Fpat(id,pat),(l,Some(([],t'),tag,cs@cs',pure_e))) in (pat,env,cs@cs'@constraints)) typ_pats in @@ -244,7 +244,7 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann let constraints = List.fold_right (fun (_,_,cs) cons -> cs@cons) pat_checks [] in let t = {t=Tid id} in let t',cs' = type_consistent l d_env t expect_t in - (P_aux((P_record(pats',false)),(l,Some(([],t'),Emp,constraints@cs',pure_e))),env,constraints@cs',t')) + (P_aux((P_record(pats',false)),(l,Some(([],t'),Emp_local,constraints@cs',pure_e))),env,constraints@cs',t')) | P_vector pats -> let item_t = match expect_t.t with (*TODO check for abbrev, throw error if not a vector or tuvar*) | Tapp("vector",[b;r;o;TA_typ i]) -> i @@ -252,13 +252,13 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann let (pats',ts,t_envs,constraints) = List.fold_right (fun pat (pats,ts,t_envs,constraints) -> - let (pat',t_env,cons,t) = check_pattern envs item_t pat in + let (pat',t_env,cons,t) = check_pattern envs emp_tag item_t pat in ((pat'::pats),(t::ts),(t_env::t_envs),(cons@constraints))) pats ([],[],[],[]) in let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*) let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent l d_env u t in t',cs) ts (item_t,[]) in let t = {t = Tapp("vector",[(TA_nexp {nexp= Nconst 0});(TA_nexp {nexp= Nconst (List.length ts)});(TA_ord{order=Oinc});(TA_typ u)])} in - (P_aux(P_vector(pats'),(l,Some(([],t),Emp,cs,pure_e))), env,cs@constraints,t) + (P_aux(P_vector(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,cs@constraints,t) | P_vector_indexed(ipats) -> let item_t = match expect_t.t with | Tapp("vector",[b;r;o;TA_typ i]) -> i @@ -281,7 +281,7 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann let (pats',ts,t_envs,constraints) = List.fold_right (fun (i,pat) (pats,ts,t_envs,constraints) -> - let (pat',env,cons,t) = check_pattern envs item_t pat in + let (pat',env,cons,t) = check_pattern envs emp_tag item_t pat in (((i,pat')::pats),(t::ts),(env::t_envs),(cons@constraints))) ipats ([],[],[],[]) in let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*) @@ -293,7 +293,7 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann GtEq(l,rise, {nexp = Nconst (lst-fst)});]@cs else [GtEq(l,base, {nexp = Nconst fst}); LtEq(l,rise, { nexp = Nconst (fst -lst)});]@cs in - (P_aux(P_vector_indexed(pats'),(l,Some(([],t),Emp,cs,pure_e))), env,constraints@cs,t) + (P_aux(P_vector_indexed(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t) | P_tup(pats) -> let item_ts = match expect_t.t with | Ttup ts -> @@ -304,17 +304,17 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann let (pats',ts,t_envs,constraints) = List.fold_right (fun (pat,t) (pats,ts,t_envs,constraints) -> - let (pat',env,cons,t) = check_pattern envs t pat in + let (pat',env,cons,t) = check_pattern envs emp_tag t pat in ((pat'::pats),(t::ts),(env::t_envs),cons@constraints)) (List.combine pats item_ts) ([],[],[],[]) in let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*Need to check for non-duplication of variables*) let t = {t = Ttup ts} in - (P_aux(P_tup(pats'),(l,Some(([],t),Emp,[],pure_e))), env,constraints,t) + (P_aux(P_tup(pats'),(l,Some(([],t),Emp_local,[],pure_e))), env,constraints,t) | P_vector_concat pats -> let (pats',ts,envs,constraints) = List.fold_right (fun pat (pats,ts,t_envs,constraints) -> - let (pat',env,cons,t) = check_pattern envs expect_t pat in + let (pat',env,cons,t) = check_pattern envs emp_tag expect_t pat in (pat'::pats,t::ts,env::t_envs,cons@constraints)) pats ([],[],[],[]) in let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*) @@ -335,7 +335,7 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann | Tapp("vector",[(TA_nexp b);(TA_nexp r);(TA_ord o);(TA_typ u)]) -> {nexp = Nadd(r,rn)} | _ -> raise (Reporting_basic.err_unreachable l "vector concat pattern impossibility") ) (List.tl ts) r1 in let cs = [Eq(l,base,base_c);Eq(l,rise,range_c)]@(List.flatten cs) in - (P_aux(P_vector_concat(pats'),(l,Some(([],t),Emp,cs,pure_e))), env,constraints@cs,t) + (P_aux(P_vector_concat(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t) | P_list(pats) -> let item_t = match expect_t.t with | Tapp("list",[TA_typ i]) -> i @@ -343,13 +343,13 @@ let rec check_pattern envs expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tann let (pats',ts,envs,constraints) = List.fold_right (fun pat (pats,ts,t_envs,constraints) -> - let (pat',env,cons,t) = check_pattern envs item_t pat in + let (pat',env,cons,t) = check_pattern envs emp_tag item_t pat in (pat'::pats,t::ts,env::t_envs,cons@constraints)) pats ([],[],[],[]) in let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*Need to check for non-duplication of variables*) let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent l d_env u t in t',cs@cs') ts (item_t,[]) in let t = {t = Tapp("list",[TA_typ u])} in - (P_aux(P_list(pats'),(l,Some(([],t),Emp,cs,pure_e))), env,constraints@cs,t) + (P_aux(P_list(pats'),(l,Some(([],t),Emp_local,cs,pure_e))), env,constraints@cs,t) let rec check_exp envs expect_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 @@ -377,7 +377,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp | Some(Some(tp,Default,cs,ef)) | Some(Some(tp,Spec,cs,ef)) -> typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use") | Some(Some((params,t),tag,cs,ef)) -> - let t,cs,ef = subst params t cs ef in + let t,cs,ef = match tag with | Emp_global | External _ -> subst params t cs ef | _ -> t,cs,ef in let t,cs',ef' = get_abbrev d_env t in let cs,ef = cs@cs',union_effects ef ef' in let t_actual,expect_actual = match t.t,expect_t.t with @@ -388,7 +388,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (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')]) -> - let tannot = Some(([],t),Emp,cs,ef) in + let tannot = Some(([],t),Emp_local,cs,ef) in let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in (e',t,t_env,cs@cs',ef) | Tapp("register",[TA_typ(t')]),_ -> @@ -397,7 +397,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_actual in (e',t,t_env,cs@cs',ef) | Tapp("reg",[TA_typ(t')]),_ -> - let tannot = Some(([],t),Emp,cs,pure_e) in + let tannot = Some(([],t),Emp_local,cs,pure_e) in let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_actual in (e',t',t_env,cs@cs',pure_e) | _ -> @@ -443,7 +443,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp | L_string s -> {t = Tid "string"},lit,pure_e | L_undef -> new_t (),lit,{effect=Eset[BE_aux(BE_undef,l)]}) in let t',cs',e' = - type_coerce l d_env t (E_aux(E_lit(L_aux(lit',l')),(l,(Some(([],t),Emp,[],effect))))) expect_t in + type_coerce l d_env t (E_aux(E_lit(L_aux(lit',l')),(l,(Some(([],t),Emp_local,[],effect))))) expect_t in (e',t',t_env,cs',effect) | E_cast(typ,e) -> let t = typ_to_t typ in @@ -504,7 +504,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (e',t',_,c,ef) = check_exp envs t e in ((e'::exps),(t'::typs),c@consts,union_effects ef effect)) exps ts ([],[],[],pure_e) in let t = {t = Ttup typs} in - (E_aux(E_tuple(exps),(l,Some(([],t),Emp,[],pure_e))),t,t_env,consts,effect) + (E_aux(E_tuple(exps),(l,Some(([],t),Emp_local,[],pure_e))),t,t_env,consts,effect) else typ_error l ("Expected a tuple with length " ^ (string_of_int tl) ^ " found one of length " ^ (string_of_int el)) | _ -> let exps,typs,consts,effect = @@ -513,14 +513,14 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (e',t,_,c,ef) = check_exp envs (new_t ()) e in ((e'::exps),(t::typs),c@consts,union_effects ef effect)) exps ([],[],[],pure_e) in let t = { t=Ttup typs } in - let t',cs',e' = type_coerce l d_env t (E_aux(E_tuple(exps),(l,Some(([],t),Emp,[],pure_e)))) expect_t in + let t',cs',e' = type_coerce l d_env t (E_aux(E_tuple(exps),(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,consts@cs',effect)) | E_if(cond,then_,else_) -> let (cond',_,_,c1,ef1) = check_exp envs bool_t cond in let then',then_t,then_env,then_c,then_ef = check_exp envs expect_t then_ in let else',else_t,else_env,else_c,else_ef = check_exp envs expect_t else_ in - (E_aux(E_if(cond',then',else'),(l,Some(([],expect_t),Emp,[],pure_e))), - expect_t,Envmap.intersect then_env else_env,then_c@else_c@c1, + (E_aux(E_if(cond',then',else'),(l,Some(([],expect_t),Emp_local,[],pure_e))), + expect_t,Envmap.intersect_merge (tannot_merge l d_env) then_env else_env,then_c@else_c@c1, union_effects ef1 (union_effects then_ef else_ef)) | E_for(id,from,to_,step,order,block) -> let fb,fr,tb,tr,sb,sr = new_n(),new_n(),new_n(),new_n(),new_n(),new_n() in @@ -532,15 +532,15 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let new_annot,local_cs = match (aorder_to_ord order).order with | Oinc -> - (Some(([],{t=Tapp("enum",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp,[],pure_e), + (Some(([],{t=Tapp("enum",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}),Emp_local,[],pure_e), [LtEq(l,{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});LtEq(l,fb,tb)]) | Odec -> - (Some(([],{t=Tapp("enum",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}),Emp,[],pure_e), + (Some(([],{t=Tapp("enum",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}),Emp_local,[],pure_e), [GtEq(l,{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});GtEq(l,fb,tb)]) | _ -> (typ_error l "Order specification in a foreach loop must be either inc or dec, not polymorphic") in let (block',b_t,_,b_c,b_ef) = check_exp (Env(d_env,Envmap.insert t_env (id_to_string id,new_annot))) expect_t block in - (E_aux(E_for(id,from',to_',step',order,block'),(l,Some(([],b_t),Emp,local_cs,pure_e))),expect_t,Envmap.empty, + (E_aux(E_for(id,from',to_',step',order,block'),(l,Some(([],b_t),Emp_local,local_cs,pure_e))),expect_t,Envmap.empty, b_c@from_c@to_c@step_c@local_cs,(union_effects b_ef (union_effects step_ef (union_effects to_ef from_ef)))) | E_vector(es) -> let item_t = match expect_t.t with @@ -551,7 +551,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) (List.map (check_exp envs item_t) es) ([],[],pure_e)) in let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst 0});TA_nexp({nexp=Nconst (List.length es)});TA_ord({order=Oinc});TA_typ item_t])} in - let t',cs',e' = type_coerce l d_env t (E_aux(E_vector es,(l,Some(([],t),Emp,[],pure_e)))) expect_t in + let t',cs',e' = type_coerce l d_env t (E_aux(E_vector es,(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs@cs',effect) | E_vector_indexed eis -> let item_t = match expect_t.t with @@ -571,7 +571,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp eis) ([],[],pure_e,first)) in let t = {t = Tapp("vector",[TA_nexp({nexp=Nconst first});TA_nexp({nexp=Nconst (List.length eis)}); TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in - let t',cs',e' = type_coerce l d_env t (E_aux(E_vector_indexed es,(l,Some(([],t),Emp,[],pure_e)))) expect_t in + let t',cs',e' = type_coerce l d_env t (E_aux(E_vector_indexed es,(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs@cs',effect) | E_vector_access(vec,i) -> let base,rise,ord = new_n(),new_n(),new_o() in @@ -589,7 +589,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp [GtEq(l,base,min); LtEq(l,{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})] | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element" in - let t',cs',e' = type_coerce l d_env item_t (E_aux(E_vector_access(vec',i'),(l,Some(([],item_t),Emp,[],pure_e)))) expect_t in + let t',cs',e'=type_coerce l d_env item_t (E_aux(E_vector_access(vec',i'),(l,Some(([],item_t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs_loc@cs_i@cs@cs',union_effects ef ef_i) | E_vector_subrange(vec,i1,i2) -> let base,rise,ord = new_n(),new_n(),new_o() in @@ -619,7 +619,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp | _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in let nt = {t=Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord;TA_typ item_t])} in let (t,cs3,e') = - type_coerce l d_env nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,Some(([],nt),Emp,cs_loc,pure_e)))) expect_t in + type_coerce l d_env nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,Some(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc,(union_effects ef (union_effects ef_i1 ef_i2))) | E_vector_update(vec,i,e) -> let base,rise,ord = new_n(),new_n(),new_o() in @@ -642,7 +642,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp in let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in let (t,cs3,e') = - type_coerce l d_env nt (E_aux(E_vector_update(vec',i',e'),(l,Some(([],nt),Emp,cs_loc,pure_e)))) expect_t in + type_coerce l d_env nt (E_aux(E_vector_update(vec',i',e'),(l,Some(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in (e',t,t_env,cs3@cs@cs_i@cs_e@cs_loc,(union_effects ef (union_effects ef_i ef_e))) | E_vector_update_subrange(vec,i1,i2,e) -> let base,rise,ord = new_n(),new_n(),new_o() in @@ -676,7 +676,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp | _ -> typ_error l "A vector must be either increasing or decreasing to modify a slice" in let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in let (t,cs3,e') = - type_coerce l d_env nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,Some(([],nt),Emp,cs_loc,pure_e)))) expect_t in + type_coerce l d_env nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,Some(([],nt),Emp_local,cs_loc,pure_e)))) expect_t in (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc@cs_e,(union_effects ef (union_effects ef_i1 (union_effects ef_i2 ef_e)))) | E_list(es) -> let item_t = match expect_t.t with @@ -686,7 +686,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (List.fold_right (fun (e,_,_,c,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) (List.map (check_exp envs item_t) es) ([],[],pure_e)) in let t = {t = Tapp("list",[TA_typ item_t])} in - let t',cs',e' = type_coerce l d_env t (E_aux(E_list es,(l,Some(([],t),Emp,[],pure_e)))) expect_t in + let t',cs',e' = type_coerce l d_env t (E_aux(E_list es,(l,Some(([],t),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs@cs',effect) | E_cons(ls,i) -> let item_t = match expect_t.t with @@ -695,7 +695,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let lt = {t=Tapp("list",[TA_typ item_t])} in let (ls',t',_,cs,ef) = check_exp envs lt ls in let (i', ti, _,cs_i,ef_i) = check_exp envs item_t i in - let (t',cs',e') = type_coerce l d_env lt (E_aux(E_cons(ls',i'),(l,Some(([],lt),Emp,[],pure_e)))) expect_t in + let (t',cs',e') = type_coerce l d_env lt (E_aux(E_cons(ls',i'),(l,Some(([],lt),Emp_local,[],pure_e)))) expect_t in (e',t',t_env,cs@cs'@cs_i,(union_effects ef ef_i)) | E_record(FES_aux(FES_Fexps(fexps,_),l')) -> let u,_,_ = get_abbrev d_env expect_t in @@ -718,7 +718,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (e,t',_,c,ef) = check_exp envs et exp in (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef')) fexps ([],[],pure_e) in - E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],u),Emp,[],pure_e))),expect_t,t_env,cons,ef + E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],u),Emp_local,[],pure_e))),expect_t,t_env,cons,ef else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields") | Some(i,Register,fields) -> typ_error l ("Expected a value with register type, found a struct")) | Tuvar _ -> @@ -738,7 +738,7 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef')) fexps ([],[],pure_e) in expect_t.t <- Tid i; - E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,[],pure_e))),expect_t,t_env,cons,ef + E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef | Some(i,Register,fields) -> typ_error l "Expected a value with register type, found a struct") | _ -> typ_error l ("Expected an expression of type " ^ t_to_string expect_t ^ " but found a struct")) | E_record_update(exp,FES_aux(FES_Fexps(fexps,_),l')) -> @@ -763,7 +763,8 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let (e,t',_,c,ef) = check_exp envs et exp in (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef')) fexps ([],[],pure_e) in - E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,[],pure_e))),expect_t,t_env,cons,ef + E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), + (l,Some(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes")) | Tuvar _ -> let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in @@ -782,7 +783,8 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp (FE_aux(FE_Fexp(id,e),(l,Some(([],t'),tag,cs@c,ef)))::fexps,cons@cs@c,union_effects ef ef')) fexps ([],[],pure_e) in expect_t.t <- Tid i; - E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')),(l,Some(([],expect_t),Emp,[],pure_e))),expect_t,t_env,cons,ef + E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), + (l,Some(([],expect_t),Emp_local,[],pure_e))),expect_t,t_env,cons,ef | [(i,Register,fields)] -> typ_error l "Expected a value with register type, found a struct" | records -> typ_error l "Multiple structs contain this set of fields, try adding a cast to disambiguate") | _ -> typ_error l ("Expected a struct to update but found an expression of type " ^ t_to_string expect_t)) @@ -833,11 +835,11 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp let check_t = new_t() in let (e',t',_,cs,ef) = check_exp envs check_t exp in let (pexps',t,cs',ef') = check_cases envs check_t expect_t pexps in - (E_aux(E_case(e',pexps'),(l,Some(([],t),Emp,[],pure_e))),t,t_env,cs@cs',union_effects ef ef') + (E_aux(E_case(e',pexps'),(l,Some(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef') | E_let(lbind,body) -> - let (lb',t_env',cs,ef) = (check_lbind envs lbind) in - let (e,t,_,cs',ef') = check_exp (Env(d_env,Envmap.union t_env t_env')) expect_t body in - (E_aux(E_let(lb',e),(l,Some(([],t),Emp,[],pure_e))),t,t_env,cs@cs',union_effects ef ef') + let (lb',t_env',cs,ef) = (check_lbind envs Emp_local lbind) in + let (e,t,_,cs',ef') = check_exp (Env(d_env,Envmap.union_merge (tannot_merge l d_env) t_env t_env')) expect_t body in + (E_aux(E_let(lb',e),(l,Some(([],t),Emp_local,[],pure_e))),t,t_env,cs@cs',union_effects ef ef') | E_assign(lexp,exp) -> let (lexp',t',t_env',tag,cs,ef) = check_lexp envs true lexp in let (exp',t'',_,cs',ef') = check_exp envs t' exp in @@ -851,7 +853,7 @@ and check_block orig_envs envs expect_t exps : ((tannot exp) list * tannot * tan | [e] -> let (E_aux(e',(l,annot)),t,envs,sc,ef) = check_exp envs expect_t e in ([E_aux(e',(l,annot))],annot,orig_envs,sc,t,ef) | e::exps -> let (e',t',t_env',sc,ef') = check_exp envs unit_t e in - let (exps',annot',orig_envs,sc',t,ef) = check_block orig_envs (Env(d_env,Envmap.union t_env t_env')) expect_t exps in + let (exps',annot',orig_envs,sc',t,ef) = check_block orig_envs (Env(d_env,Envmap.union_merge (tannot_merge Parse_ast.Unknown d_env) t_env t_env')) expect_t exps in ((e'::exps'),annot',orig_envs,sc@sc',t,union_effects ef ef') and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_range list * effect) = @@ -859,16 +861,16 @@ and check_cases envs check_t expect_t pexps : ((tannot pexp) list * typ * nexp_r match pexps with | [] -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "switch with no cases found") | [(Pat_aux(Pat_exp(pat,exp),(l,annot)))] -> - let pat',env,cs_p,u = check_pattern envs (new_t ()) pat in + let pat',env,cs_p,u = check_pattern envs Emp_local (new_t ()) pat in let t',cs_p' = type_consistent l d_env u check_t in - let (e,t,_,cs2,ef2) = check_exp (Env(d_env,Envmap.union t_env env)) expect_t exp in - [Pat_aux(Pat_exp(pat',e),(l,Some(([],t),Emp,cs_p@cs_p'@cs2,ef2)))],t,cs_p@cs_p'@cs2,ef2 + let (e,t,_,cs2,ef2) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge l d_env) t_env env)) expect_t exp in + [Pat_aux(Pat_exp(pat',e),(l,Some(([],t),Emp_local,cs_p@cs_p'@cs2,ef2)))],t,cs_p@cs_p'@cs2,ef2 | ((Pat_aux(Pat_exp(pat,exp),(l,annot)))::pexps) -> - let pat',env,cs_p,u = check_pattern envs (new_t ()) pat in + let pat',env,cs_p,u = check_pattern envs Emp_local (new_t ()) pat in let t',cs_p' = type_consistent l d_env u check_t in - let (e,t,_,cs2,ef2) = check_exp (Env(d_env,Envmap.union t_env env)) expect_t exp in + let (e,t,_,cs2,ef2) = check_exp (Env(d_env,Envmap.union_merge (tannot_merge l d_env) t_env env)) expect_t exp in let (pes,t'',csl,efl) = check_cases envs check_t expect_t pexps in - ((Pat_aux(Pat_exp(pat',e),(l,(Some(([],t''),Emp,(csl@cs_p@cs_p'@cs2),(union_effects efl ef2))))))::pes, + ((Pat_aux(Pat_exp(pat',e),(l,(Some(([],t''),Emp_local,(csl@cs_p@cs_p'@cs2),(union_effects efl ef2))))))::pes, t'', csl@cs_p@cs_p'@cs2,union_effects efl ef2) @@ -881,7 +883,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan | Some(Some((parms,t),Default,_,_)) -> typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists") | Some(Some((parms,t),tag,cs,_)) -> - let t,cs,_ = subst parms t cs pure_e in + let t,cs,_ = match tag with | External _ | Emp_global -> subst parms t cs pure_e | _ -> t,cs,pure_e in let t,cs',_ = get_abbrev d_env t in let t_actual = match t.t with | Tabbrev(i,t) -> t @@ -891,20 +893,20 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in (LEXP_aux(lexp,(l,(Some(([],t),External (Some i),cs@cs',ef)))),u,Envmap.empty,External (Some i),[],ef) | Tapp("reg",[TA_typ u]),_ -> - (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs@cs',pure_e)))),u,Envmap.empty,Emp,[],pure_e) + (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs@cs',pure_e)))),u,Envmap.empty,Emp_local,[],pure_e) | Tapp("vector",_),false -> - (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs@cs',pure_e)))),t,Envmap.empty,Emp,[],pure_e) + (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs@cs',pure_e)))),t,Envmap.empty,Emp_local,[],pure_e) | _,_ -> if is_top then typ_error l ("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t) else - (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs@cs',pure_e)))),t,Envmap.empty,Emp,[],pure_e) (* TODO, make sure this is a record *)) + (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs@cs',pure_e)))),t,Envmap.empty,Emp_local,[],pure_e) (* TODO, make sure this is a record *)) | _ -> let u = new_t() in let t = {t=Tapp("reg",[TA_typ u])} in - let tannot = (Some(([],t),Emp,[],pure_e)) in - (LEXP_aux(lexp,(l,tannot)),u,Envmap.from_list [i,tannot],Emp,[],pure_e)) + let tannot = (Some(([],t),Emp_local,[],pure_e)) in + (LEXP_aux(lexp,(l,tannot)),u,Envmap.from_list [i,tannot],Emp_local,[],pure_e)) | LEXP_memory(id,exps) -> let i = id_to_string id in (match Envmap.apply t_env i with @@ -949,7 +951,7 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan | Some(Some((parms,t),Default,_,_)) -> typ_error l ("Identifier " ^ i ^ " cannot be assigned when only a default specification exists") | Some(Some((parms,t),tag,cs,_)) -> - let t,cs,_ = subst parms t cs pure_e in + let t,cs,_ = match tag with | External _ | Emp_global -> subst parms t cs pure_e | _ -> t,cs,pure_e in let t,cs',_ = get_abbrev d_env t in let t_actual = match t.t with | Tabbrev(_,t) -> t | _ -> t in (match t_actual.t,is_top with @@ -959,23 +961,23 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan (LEXP_aux(lexp,(l,(Some(([],t),External (Some i),cs,ef)))),ty,Envmap.empty,External (Some i),[],ef) | Tapp("reg",[TA_typ u]),_ -> let t',cs = type_consistent l d_env ty u in - (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e) + (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e) | Tapp("vector",_),false -> - (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e) + (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e) | Tuvar _,_ -> let u' = {t=Tapp("reg",[TA_typ ty])} in t.t <- u'.t; - (LEXP_aux(lexp,(l,(Some((([],u'),Emp,cs,pure_e))))),ty,Envmap.empty,Emp,[],pure_e) + (LEXP_aux(lexp,(l,(Some((([],u'),Emp_local,cs,pure_e))))),ty,Envmap.empty,Emp_local,[],pure_e) | _,_ -> if is_top then typ_error l ("Can only assign to identifiers with type register or reg, found identifier " ^ i ^ " with type " ^ t_to_string t) else - (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),ty,Envmap.empty,Emp,[],pure_e)) (* TODO, make sure this is a record *) + (LEXP_aux(lexp,(l,(Some(([],t),Emp_local,cs,pure_e)))),ty,Envmap.empty,Emp_local,[],pure_e)) (* TODO, make sure this is a record *) | _ -> let t = {t=Tapp("reg",[TA_typ ty])} in - let tannot = (Some(([],t),Emp,[],pure_e)) in - (LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp,[],pure_e)) + let tannot = (Some(([],t),Emp_local,[],pure_e)) in + (LEXP_aux(lexp,(l,tannot)),ty,Envmap.from_list [i,tannot],Emp_local,[],pure_e)) | LEXP_vector(vec,acc) -> let (vec',item_t,env,tag,csi,ef) = check_lexp envs false vec in let item_t,cs',_ = get_abbrev d_env item_t in @@ -1050,15 +1052,15 @@ and check_lexp envs is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tan (LEXP_aux(LEXP_field(vec',id),(l,(Some(([],vec_t),tag,csi@cs,ef)))),et,env,tag,csi@cs,ef))) | _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t))) -and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * effect = +and check_lbind envs emp_tag (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * effect = let Env(d_env,t_env) = envs in match lbind with | LB_val_explicit(typ,pat,e) -> - let tan = typschm_to_tannot envs typ Emp in + let tan = typschm_to_tannot envs typ emp_tag in (match tan with | Some((params,t),tag,cs,ef) -> let t,cs,ef = subst params t cs ef in - let (pat',env,cs1,u) = check_pattern envs t pat in + let (pat',env,cs1,u) = check_pattern envs emp_tag t pat in 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 @@ -1067,10 +1069,10 @@ and check_lbind envs (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * | None -> raise (Reporting_basic.err_unreachable l "typschm_to_tannot failed to produce a Some")) | LB_val_implicit(pat,e) -> let t = new_t () in - let (pat',env,cs1,u) = check_pattern envs (new_t ()) pat in + let (pat',env,cs1,u) = check_pattern envs emp_tag (new_t ()) pat in let (e,t',_,cs2,ef) = check_exp envs u e in let cs = resolve_constraints cs1@cs2 in - let tannot = check_tannot l (Some(([],t'),Emp,cs,ef)) cs ef (* see above *) in + let tannot = check_tannot l (Some(([],t'),emp_tag,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*) @@ -1078,15 +1080,15 @@ let check_type_def envs (TD_aux(td,(l,annot))) = let (Env(d_env,t_env)) = envs in match td with | TD_abbrev(id,nmscm,typschm) -> - let tan = typschm_to_tannot envs typschm Emp in + let tan = typschm_to_tannot envs typschm Emp_global in (TD_aux(td,(l,tan)), Env( { d_env with abbrevs = Envmap.insert d_env.abbrevs ((id_to_string id),tan)},t_env)) | TD_record(id,nmscm,typq,fields,_) -> let id' = id_to_string id in let (params,constraints) = typq_to_params envs typq in - let tyannot = Some((params,{t=Tid id'}),Emp,constraints,pure_e) in + let tyannot = Some((params,{t=Tid id'}),Emp_global,constraints,pure_e) in let fields' = List.map - (fun (ty,i)->(id_to_string i),Some((params,(typ_to_t ty)),Emp,constraints,pure_e)) fields in + (fun (ty,i)->(id_to_string i),Some((params,(typ_to_t ty)),Emp_global,constraints,pure_e)) fields in (TD_aux(td,(l,tyannot)),Env({d_env with rec_env = (id',Record,fields')::d_env.rec_env},t_env)) | TD_variant(id,nmscm,typq,arms,_) -> let id' = id_to_string id in @@ -1134,10 +1136,10 @@ let check_type_def envs (TD_aux(td,(l,annot))) = then {t=Tapp("vector",[TA_nexp {nexp=Nconst i1}; TA_nexp {nexp=Nconst (i2 - i1)}; TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])} else typ_error l ("register type declaration " ^ id' ^ " contains a field specification outside of the declared register size") else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing") - | BF_concat _ -> assert false (* What is this supposed to imply again?*)),Emp,[],pure_e))) + | BF_concat _ -> assert false (* What is this supposed to imply again?*)),Emp_global,[],pure_e))) ranges in - let tannot = into_register d_env (Some(([],ty),Emp,[],pure_e)) in + let tannot = into_register d_env (Some(([],ty),Emp_global,[],pure_e)) in (TD_aux(td,(l,tannot)), Env({d_env with rec_env = ((id',Register,franges)::d_env.rec_env); abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env))) @@ -1161,10 +1163,10 @@ let check_type_def envs (TD_aux(td,(l,annot))) = else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing") | BF_concat _ -> assert false (* What is this supposed to imply again?*) in ((id_to_string id), - Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp,[],pure_e))) + Some(([],{t=Tapp("vector",[TA_nexp base;TA_nexp climb;TA_ord({order=Odec});TA_typ({t= Tid "bit"})])}),Emp_global,[],pure_e))) ranges in - let tannot = into_register d_env (Some(([],ty),Emp,[],pure_e)) in + let tannot = into_register d_env (Some(([],ty),Emp_global,[],pure_e)) in (TD_aux(td,(l,tannot)), Env({d_env with rec_env = (id',Register,franges)::d_env.rec_env; abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env))) @@ -1212,23 +1214,24 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') -> let (ids,constraints) = typq_to_params envs typq in let t = typ_to_t typ in + let t,constraints,_ = subst ids t constraints pure_e 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,ef) in + t,p_t,Some((ids,{t=Tfn(p_t,t,ef)}),Emp_global,constraints,ef) in let check t_env = List.split (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) -> - let (pat',t_env',constraints',t') = check_pattern (Env(d_env,t_env)) param_t pat in + let (pat',t_env',constraints',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 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 _ = Printf.printf "checked function %s : %s,%s -> %s\n" (id_to_string id) (t_to_string t') (t_to_string param_t) (t_to_string ret_t) in *) + let exp',_,_,constraints,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge l d_env) t_env t_env')) ret_t exp in + (*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) (*let _ = (Pretty_print.pp_exp Format.std_formatter) exp' 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') -> + | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),_,c',eft') -> + (*let _ = Printf.printf "Function %s is in env\n" id in*) 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_ef = check t_env in @@ -1254,7 +1257,7 @@ let check_def envs (DEF_aux(def,(l,annot))) = (DEF_aux((DEF_type td),(l,annot)),envs) | DEF_fundef fdef -> let fd,envs = check_fundef envs fdef in (DEF_aux(DEF_fundef(fd),(l,annot)),envs) - | DEF_val letdef -> let (letbind,t_env_let,_,eft) = check_lbind envs letdef in + | DEF_val letdef -> let (letbind,t_env_let,_,eft) = check_lbind envs Emp_global letdef in (DEF_aux(DEF_val letbind,(l,annot)),Env(d_env,Envmap.union t_env t_env_let)) | DEF_spec spec -> let vs,envs = check_val_spec envs spec in (DEF_aux(DEF_spec(vs),(l,annot)),envs) diff --git a/src/type_internal.ml b/src/type_internal.ml index 7d613f3b..e2af4970 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -59,7 +59,8 @@ and t_arg = | TA_ord of order type tag = - | Emp + | Emp_local + | Emp_global | External of string option | Default | Constructor @@ -131,7 +132,8 @@ and o_to_string o = | Ouvar({oindex=i;osubst=a}) -> string_of_int i ^ "()" let tag_to_string = function - | Emp -> "Emp" + | Emp_local -> "Emp_local" + | Emp_global -> "Emp_global" | External None -> "External" | External (Some s) -> "External " ^ s | Default -> "Default" @@ -260,7 +262,9 @@ let new_e _ = { effect = Euvar { eindex = i; esubst = None }} exception Occurs_exn of t_arg -let rec resolve_tsubst (t : t) : t = match t.t with +let rec resolve_tsubst (t : t) : t = + (*let _ = Printf.printf "resolve_tsubst on %s\n" (t_to_string t) in*) + match t.t with | Tuvar({ subst=Some(t') } as u) -> let t'' = resolve_tsubst t' in (match t''.t with @@ -340,7 +344,8 @@ let equate_t (t_box : t) (t : t) : unit = | Tuvar(_) -> (match t_box.t with | Tuvar(u) -> - u.subst <- Some(t)) + u.subst <- Some(t) + | _ -> assert false) | _ -> t_box.t <- t.t) let equate_n (n_box : nexp) (n : nexp) : unit = @@ -352,7 +357,8 @@ let equate_n (n_box : nexp) (n : nexp) : unit = | Nuvar(_) -> (match n_box.nexp with | Nuvar(u) -> - u.nsubst <- Some(n)) + u.nsubst <- Some(n) + | _ -> assert false) | _ -> n_box.nexp <- n.nexp) let equate_o (o_box : order) (o : order) : unit = @@ -364,7 +370,8 @@ let equate_o (o_box : order) (o : order) : unit = | Ouvar(_) -> (match o_box.order with | Ouvar(u) -> - u.osubst <- Some(o)) + u.osubst <- Some(o) + | _ -> assert false) | _ -> o_box.order <- o.order) let equate_e (e_box : effect) (e : effect) : unit = @@ -376,7 +383,8 @@ let equate_e (e_box : effect) (e : effect) : unit = | Euvar(_) -> (match e_box.effect with | Euvar(u) -> - u.esubst <- Some(e)) + u.esubst <- Some(e) + | _ -> assert false) | _ -> e_box.effect <- e.effect) @@ -386,19 +394,54 @@ let rec fresh_var i mkr bindings = | Some _ -> fresh_var (i+1) mkr bindings | None -> mkr v -let fresh_tvar bindings t = +let rec fresh_tvar bindings t = match t.t with - | Tuvar { index = i } -> fresh_var i (fun v -> equate_t t {t = (Tvar v)}; (v,{k=K_Typ})) bindings -let fresh_nvar bindings n = + | Tuvar { index = i;subst = None } -> + fresh_var i (fun v -> equate_t t {t=Tvar v};Some (v,{k=K_Typ})) bindings + | Tuvar { index = i; subst = Some ({t = Tuvar _} as t') } -> + let kv = fresh_tvar bindings t' in + equate_t t t'; + kv + | Tuvar { index = i; subst = Some t' } -> + t.t <- t'.t; + None + | _ -> None +let rec fresh_nvar bindings n = match n.nexp with - | Nuvar { nindex = i } -> fresh_var i (fun v -> equate_n n {nexp = (Nvar v)}; (v,{k=K_Nat})) bindings -let fresh_ovar bindings o = + | Nuvar { nindex = i;nsubst = None } -> + fresh_var i (fun v -> equate_n n {nexp = (Nvar v)}; Some(v,{k=K_Nat})) bindings + | Nuvar { nindex = i; nsubst = Some({nexp=Nuvar _} as n')} -> + let kv = fresh_nvar bindings n' in + equate_n n n'; + kv + | Nuvar { nindex = i; nsubst = Some n' } -> + n.nexp <- n'.nexp; + None + | _ -> None +let rec fresh_ovar bindings o = match o.order with - | Ouvar { oindex = i } -> fresh_var i (fun v -> equate_o o {order = (Ovar v)}; (v,{k=K_Ord})) bindings -let fresh_evar bindings e = + | Ouvar { oindex = i;osubst = None } -> + fresh_var i (fun v -> equate_o o {order = (Ovar v)}; Some(v,{k=K_Nat})) bindings + | Ouvar { oindex = i; osubst = Some({order=Ouvar _} as o')} -> + let kv = fresh_ovar bindings o' in + equate_o o o'; + kv + | Ouvar { oindex = i; osubst = Some o' } -> + o.order <- o'.order; + None + | _ -> None +let rec fresh_evar bindings e = match e.effect with - | Euvar { eindex = i } -> fresh_var i (fun v -> equate_e e {effect = (Evar v)}; (v,{k=K_Efct})) bindings - + | Euvar { eindex = i;esubst = None } -> + fresh_var i (fun v -> equate_e e {effect = (Evar v)}; Some(v,{k=K_Nat})) bindings + | Euvar { eindex = i; esubst = Some({effect=Euvar _} as e')} -> + let kv = fresh_evar bindings e' in + equate_e e e'; + kv + | Euvar { eindex = i; esubst = Some e' } -> + e.effect <- e'.effect; + None + | _ -> None let nat_t = {t = Tapp("enum",[TA_nexp{nexp= Nconst 0};TA_nexp{nexp = Nconst max_int};])} let unit_t = { t = Tid "unit" } @@ -452,15 +495,17 @@ let initial_typ_env = let initial_abbrev_env = Envmap.from_list [ - ("nat",Some(([],nat_t),Emp,[],pure_e)); + ("nat",Some(([],nat_t),Emp_global,[],pure_e)); ] let rec t_subst s_env t = + (*let _ = Printf.printf "Calling t_subst on %s\n" (t_to_string t) in*) match t.t with | Tvar i -> (match Envmap.apply s_env i with | Some(TA_typ t1) -> t1 | _ -> t) - | Tuvar _ | Tid _ -> t + | Tuvar _ -> new_t() + | Tid _ -> t | Tfn(t1,t2,e) -> {t =Tfn((t_subst s_env t1),(t_subst s_env t2),(e_subst s_env e)) } | Ttup(ts) -> { t= Ttup(List.map (t_subst s_env) ts) } | Tapp(i,args) -> {t= Tapp(i,List.map (ta_subst s_env) args)} @@ -476,7 +521,8 @@ and n_subst s_env n = | Nvar i -> (match Envmap.apply s_env i with | Some(TA_nexp n1) -> n1 | _ -> n) - | Nuvar _ | Nconst _ -> n + | Nuvar _ -> new_n() + | Nconst _ -> n | N2n n1 -> { nexp = N2n (n_subst s_env n1) } | Nneg n1 -> { nexp = Nneg (n_subst s_env n1) } | Nadd(n1,n2) -> { nexp = Nadd(n_subst s_env n1,n_subst s_env n2) } @@ -486,12 +532,14 @@ and o_subst s_env o = | Ovar i -> (match Envmap.apply s_env i with | Some(TA_ord o1) -> o1 | _ -> o) + | Ouvar _ -> new_o () | _ -> o and e_subst s_env e = match e.effect with | Evar i -> (match Envmap.apply s_env i with | Some(TA_eft e1) -> e1 | _ -> e) + | Euvar _ -> new_e () | _ -> e let rec cs_subst t_env cs = @@ -518,7 +566,9 @@ let subst k_env t cs 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) + | Tuvar _ -> (match fresh_tvar s_env t with + | Some ks -> Envmap.insert s_env ks + | None -> s_env) | 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 @@ -532,16 +582,22 @@ and ta_remove_unifications s_env ta = 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) + | Nuvar _ -> (match fresh_nvar s_env n with + | Some ks -> Envmap.insert s_env ks + | None -> s_env) | 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) + | Ouvar _ -> (match fresh_ovar s_env o with + | Some ks -> Envmap.insert s_env ks + | None -> s_env) | _ -> s_env and e_remove_unifications s_env e = match e.effect with - | Euvar _ -> Envmap.insert s_env (fresh_evar s_env e) + | Euvar _ -> (match fresh_evar s_env e with + | Some ks -> Envmap.insert s_env ks + | None -> s_env) | _ -> s_env let rec cs_subst t_env cs = @@ -567,13 +623,14 @@ let subst k_env t cs e = let rec t_to_typ t = - Typ_aux ( - (match t.t with - | Tid i -> Typ_id (Id_aux((Id i), Parse_ast.Unknown)) - | Tvar i -> Typ_var (Kid_aux((Var i),Parse_ast.Unknown)) - | Tfn(t1,t2,e) -> Typ_fn (t_to_typ t1, t_to_typ t2, e_to_ef e) - | Ttup ts -> Typ_tup(List.map t_to_typ ts) - | Tapp(i,args) -> Typ_app(Id_aux((Id i), Parse_ast.Unknown),List.map targ_to_typ_arg args)), Parse_ast.Unknown) + match t.t with + | Tid i -> Typ_aux(Typ_id (Id_aux((Id i), Parse_ast.Unknown)),Parse_ast.Unknown) + | Tvar i -> Typ_aux(Typ_var (Kid_aux((Var i),Parse_ast.Unknown)),Parse_ast.Unknown) + | Tfn(t1,t2,e) -> Typ_aux(Typ_fn (t_to_typ t1, t_to_typ t2, e_to_ef e),Parse_ast.Unknown) + | Ttup ts -> Typ_aux(Typ_tup(List.map t_to_typ ts),Parse_ast.Unknown) + | Tapp(i,args) -> Typ_aux(Typ_app(Id_aux((Id i), Parse_ast.Unknown),List.map targ_to_typ_arg args),Parse_ast.Unknown) + | Tabbrev(t,_) -> t_to_typ t + | Tuvar _ -> assert false and targ_to_typ_arg targ = Typ_arg_aux( (match targ with @@ -589,18 +646,21 @@ and n_to_nexp n = | Nmult(n1,n2) -> Nexp_times(n_to_nexp n1,n_to_nexp n2) | Nadd(n1,n2) -> Nexp_sum(n_to_nexp n1,n_to_nexp n2) | N2n n -> Nexp_exp (n_to_nexp n) - | Nneg n -> Nexp_neg (n_to_nexp n)), Parse_ast.Unknown) + | Nneg n -> Nexp_neg (n_to_nexp n) + | Nuvar _ -> assert false), Parse_ast.Unknown) and e_to_ef ef = Effect_aux( (match ef.effect with | Evar i -> Effect_var (Kid_aux((Var i),Parse_ast.Unknown)) - | Eset effects -> Effect_set effects), Parse_ast.Unknown) + | Eset effects -> Effect_set effects + | Euvar _ -> assert false), Parse_ast.Unknown) and o_to_order o = Ord_aux( (match o.order with | Ovar i -> Ord_var (Kid_aux((Var i),Parse_ast.Unknown)) | Oinc -> Ord_inc - | Odec -> Ord_dec), Parse_ast.Unknown) + | Odec -> Ord_dec + | Ouvar _ -> assert false), Parse_ast.Unknown) let rec get_abbrev d_env t = @@ -742,18 +802,20 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 = let tl1,tl2 = List.length t1s,List.length t2s in if tl1=tl2 then let ids = List.map (fun _ -> Id_aux(Id (new_id ()),l)) t1s in - let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Some(([],t),Emp,[],pure_e)))) ids t1s in + let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Some(([],t),Emp_local,[],pure_e)))) ids t1s in let (coerced_ts,cs,coerced_vars) = List.fold_right2 (fun v (t1,t2) (ts,cs,es) -> let (t',c',e') = type_coerce l d_env t1 v t2 in ((t'::ts),c'@cs,(e'::es))) vars (List.combine t1s t2s) ([],[],[]) in if vars = coerced_vars then (t2,cs,e) - else let e' = E_aux(E_case(e,[(Pat_aux(Pat_exp(P_aux(P_tup (List.map2 (fun i t -> P_aux(P_id i,(l,(Some(([],t),Emp,[],pure_e))))) ids t1s),(l,Some(([],t1),Emp,[],pure_e))), - E_aux(E_tuple coerced_vars,(l,Some(([],t2),Emp,cs,pure_e)))), - (l,Some(([],t2),Emp,[],pure_e))))]), - (l,(Some(([],t2),Emp,[],pure_e)))) in + else let e' = E_aux(E_case(e,[(Pat_aux(Pat_exp(P_aux(P_tup (List.map2 + (fun i t -> P_aux(P_id i,(l,(Some(([],t),Emp_local,[],pure_e))))) + ids t1s),(l,Some(([],t1),Emp_local,[],pure_e))), + E_aux(E_tuple coerced_vars,(l,Some(([],t2),Emp_local,cs,pure_e)))), + (l,Some(([],t2),Emp_local,[],pure_e))))]), + (l,(Some(([],t2),Emp_local,[],pure_e)))) in (t2,cs,e') - else eq_error l ("A tuple of length " ^ (string_of_int tl1) ^ " cannot be used where a tuple of length " ^ (string_of_int tl2) ^ " is expected") + else eq_error l ("Found a tuple of length " ^ (string_of_int tl1) ^ " but expected a tuple of length " ^ (string_of_int tl2)) | Tapp(id1,args1),Tapp(id2,args2) -> if id1=id2 then let t',cs' = type_consistent l d_env t1 t2 in (t',cs',e) @@ -799,37 +861,38 @@ 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)) | Tid("bit"),Tapp("vector",[TA_nexp {nexp=Nconst i};TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]) -> let cs = [Eq(l,r1,{nexp = Nconst 1})] in - (t2,cs,E_aux(E_vector_indexed [(i,e)],(l,Some(([],t2),Emp,cs,pure_e)))) + (t2,cs,E_aux(E_vector_indexed [(i,e)],(l,Some(([],t2),Emp_local,cs,pure_e)))) | Tapp("vector",[TA_nexp ({nexp=Nconst i} as b1);TA_nexp r1;TA_ord o;TA_typ {t=Tid "bit"}]),Tid("bit") -> let cs = [Eq(l,r1,{nexp = Nconst 1})] in - (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)),(l,Some(([],{t=Tapp("enum",[TA_nexp b1;TA_nexp {nexp=Nconst 0}])}),Emp,cs,pure_e)))))), - (l,Some(([],t2),Emp,cs,pure_e)))) + (t2,cs,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num i,l)), + (l,Some(([],{t=Tapp("enum",[TA_nexp b1;TA_nexp {nexp=Nconst 0}])}),Emp_local,cs,pure_e)))))), + (l,Some(([],t2),Emp_local,cs,pure_e)))) | Tid("bit"),Tapp("enum",[TA_nexp b1;TA_nexp r1]) -> let t',cs'= type_consistent l d_env {t=Tapp("enum",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} t2 in - (t2,cs',E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Some(([],t1),Emp,[],pure_e))), - E_aux(E_lit(L_aux(L_num 0,l)),(l,Some(([],t2),Emp,[],pure_e)))), - (l,Some(([],t2),Emp,[],pure_e))); - Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_one,l)),(l,Some(([],t1),Emp,[],pure_e))), - E_aux(E_lit(L_aux(L_num 1,l)),(l,Some(([],t2),Emp,[],pure_e)))), - (l,Some(([],t2),Emp,[],pure_e)));]), - (l,Some(([],t2),Emp,[],pure_e)))) + (t2,cs',E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Some(([],t1),Emp_local,[],pure_e))), + E_aux(E_lit(L_aux(L_num 0,l)),(l,Some(([],t2),Emp_local,[],pure_e)))), + (l,Some(([],t2),Emp_local,[],pure_e))); + Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_one,l)),(l,Some(([],t1),Emp_local,[],pure_e))), + E_aux(E_lit(L_aux(L_num 1,l)),(l,Some(([],t2),Emp_local,[],pure_e)))), + (l,Some(([],t2),Emp_local,[],pure_e)));]), + (l,Some(([],t2),Emp_local,[],pure_e)))) | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid("bit") -> let t',cs'= type_consistent l d_env t1 {t=Tapp("enum",[TA_nexp{nexp=Nconst 0};TA_nexp{nexp=Nconst 1}])} - in (t2,cs',E_aux(E_if(E_aux(E_app(Id_aux(Id "is_zero",l),[e]),(l,Some(([],bool_t),Emp,[],pure_e))), - E_aux(E_lit(L_aux(L_zero,l)),(l,Some(([],bit_t),Emp,[],pure_e))), - E_aux(E_lit(L_aux(L_one,l)),(l,Some(([],bit_t),Emp,[],pure_e)))), - (l,Some(([],bit_t),Emp,cs',pure_e)))) + in (t2,cs',E_aux(E_if(E_aux(E_app(Id_aux(Id "is_one",l),[e]),(l,Some(([],bool_t),External None,[],pure_e))), + E_aux(E_lit(L_aux(L_one,l)),(l,Some(([],bit_t),Emp_local,[],pure_e))), + E_aux(E_lit(L_aux(L_zero,l)),(l,Some(([],bit_t),Emp_local,[],pure_e)))), + (l,Some(([],bit_t),Emp_local,cs',pure_e)))) | Tapp("enum",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> (match Envmap.apply d_env.enum_env i with | Some(enums) -> (t2,[Eq(l,b1,{nexp=Nconst 0});LtEq(l,r1,{nexp=Nconst (List.length enums)})], E_aux(E_case(e, List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_lit(L_aux((L_num i),l)), - (l,Some(([],t1),Emp,[],pure_e))), + (l,Some(([],t1),Emp_local,[],pure_e))), E_aux(E_id(Id_aux(Id a,l)), - (l,Some(([],t2),Emp,[],pure_e)))), - (l,Some(([],t2),Emp,[],pure_e)))) enums), - (l,Some(([],t2),Emp,[],pure_e)))) + (l,Some(([],t2),Emp_local,[],pure_e)))), + (l,Some(([],t2),Emp_local,[],pure_e)))) enums), + (l,Some(([],t2),Emp_local,[],pure_e)))) | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))) | Tid("bit"),Tid("bool") -> let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External None,[],pure_e))) in @@ -840,11 +903,11 @@ let rec type_coerce_internal l d_env t1 cs1 e t2 cs2 = (t2,[Eq(l,b1,{nexp=Nconst 0});GtEq(l,r1,{nexp=Nconst (List.length enums)})], E_aux(E_case(e, List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_id(Id_aux(Id a,l)), - (l,Some(([],t1),Emp,[],pure_e))), + (l,Some(([],t1),Emp_local,[],pure_e))), E_aux(E_lit(L_aux((L_num i),l)), - (l,Some(([],t2),Emp,[],pure_e)))), - (l,Some(([],t2),Emp,[],pure_e)))) enums), - (l,Some(([],t2),Emp,[],pure_e)))) + (l,Some(([],t2),Emp_local,[],pure_e)))), + (l,Some(([],t2),Emp_local,[],pure_e)))) enums), + (l,Some(([],t2),Emp_local,[],pure_e)))) | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2))) | _,_ -> let t',cs = type_consistent l d_env t1 t2 in (t',cs,e) @@ -858,6 +921,9 @@ let check_tannot l annot constraints efs = | 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 + (*let _ = Printf.printf "Checked tannot, t after removing uvars is %s\n" (t_to_string t) in *) Some((params,t),tag,cs,e) | None -> raise (Reporting_basic.err_unreachable l "check_tannot given the place holder annotation") + +let tannot_merge l denv t_older t_newer = t_newer diff --git a/src/type_internal.mli b/src/type_internal.mli index 76223409..8184c36f 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -54,7 +54,8 @@ and t_arg = | TA_ord of order type tag = - | Emp + | Emp_local + | Emp_global | External of string option | Default | Constructor @@ -129,3 +130,6 @@ val type_consistent : Parse_ast.l -> def_envs -> t -> t -> t * nexp_range list (* type_eq mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second and is inconsistent *) val type_coerce : Parse_ast.l -> def_envs -> t -> exp -> t -> t * nexp_range list * exp + +(* Merge tannots when intersection or unioning two environments. In case of default types, defer to tannot on right *) +val tannot_merge : Parse_ast.l -> def_envs -> tannot -> tannot -> tannot |