diff options
| author | Kathy Gray | 2015-03-19 13:23:51 +0000 |
|---|---|---|
| committer | Kathy Gray | 2015-03-19 13:23:59 +0000 |
| commit | 910ffcef82bb984cf08b04a1cb66bed514df711e (patch) | |
| tree | 499680d139f696ff59386dacb25a89f7e2a6bfd7 | |
| parent | 43453cecde967d2ffa61ca11ac62860ec7699ae2 (diff) | |
Begin adding new information to constraints to get tightness of bounds properly
| -rw-r--r-- | src/type_check.ml | 265 | ||||
| -rw-r--r-- | src/type_internal.ml | 273 | ||||
| -rw-r--r-- | src/type_internal.mli | 12 |
3 files changed, 272 insertions, 278 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 1939d5c9..7ed4f19f 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -157,10 +157,11 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env,tp_env)) as env) qis : (t_para | K_Efct -> TA_eft { effect = Evar i} in ((i,k)::ids,targ::typarms,cs)) | QI_const(NC_aux(nconst,l')) -> + (*TODO: somehow the requirement vs best guarantee needs to be derived from user or context*) (match nconst with | NC_fixed(n1,n2) -> (ids,typarms,Eq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_bounded_ge(n1,n2) -> (ids,typarms,GtEq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) - | NC_bounded_le(n1,n2) -> (ids,typarms,LtEq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_bounded_ge(n1,n2) -> (ids,typarms,GtEq(Specc l',Require,anexp_to_nexp n1,anexp_to_nexp n2)::cs) + | NC_bounded_le(n1,n2) -> (ids,typarms,LtEq(Specc l',Require,anexp_to_nexp n1,anexp_to_nexp n2)::cs) | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,typarms,In(Specc l',i,bounds)::cs))) let typq_to_params envs (TypQ_aux(tq,l)) = @@ -226,7 +227,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) | L_string s -> {t = Tid "string"},lit | L_undef -> typ_error l' "Cannot pattern match on undefined") in (* let _ = Printf.printf "checking pattern literal. expected type is %s. t is %s\n" (t_to_string expect_t) (t_to_string t) in*) - let t',cs' = type_consistent (Patt l) d_env true t expect_t in + let t',cs' = type_consistent (Patt l) d_env Require true t expect_t in let cs_l = cs@cs' in (P_aux(P_lit(L_aux(lit,l')),(l,cons_tag_annot t emp_tag cs_l)),Envmap.empty,cs_l,nob,t) | P_wild -> @@ -241,7 +242,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) let t = typ_to_t false false typ in let t = typ_subst tp_env t in let (pat',env,constraints,bounds,u) = check_pattern envs emp_tag t pat in - let t,cs_consistent = type_consistent (Patt l) d_env false t expect_t in + let t,cs_consistent = type_consistent (Patt l) d_env Guarantee false t expect_t in (P_aux(P_typ(typ,pat'),(l,tag_annot t emp_tag)),env,cs@constraints@cs_consistent,bounds,t) | P_id id -> let i = id_to_string id in @@ -255,7 +256,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) | Tfn({t = Tid "unit"},t',IP_none,ef) -> if conforms_to_t d_env false false t' expect_t then - let tp,cp = type_consistent (Expr l) d_env false t' expect_t in + let tp,cp = type_consistent (Expr l) d_env Guarantee false t' expect_t in (P_aux(P_app(id,[]),(l,tag_annot t Constructor)),Envmap.empty,cs@cp,bounds,tp) else default | Tfn(t1,t',IP_none,e) -> @@ -273,13 +274,13 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) let t,dec_cs,_,_ = subst params t constraints eft in (match t.t with | Tid id -> if pats = [] - then let t',ret_cs = type_consistent (Patt l) d_env false t expect_t in + then let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t expect_t in (P_aux(p,(l,cons_tag_annot t' Constructor dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t') else typ_error l ("Constructor " ^ i ^ " does not expect arguments") | Tfn(t1,t2,IP_none,ef) -> - let t',ret_cs = type_consistent (Patt l) d_env false t2 expect_t in + let t',ret_cs = type_consistent (Patt l) d_env Guarantee false t2 expect_t in (match pats with - | [] -> let _ = type_consistent (Patt l) d_env false unit_t t1 in + | [] -> let _ = type_consistent (Patt l) d_env Guarantee false unit_t t1 in (P_aux(P_app(id,[]),(l,cons_tag_annot t' Constructor dec_cs)), Envmap.empty,dec_cs@ret_cs,nob,t') | [p] -> let (p',env,p_cs,bounds,u) = check_pattern envs emp_tag t1 p in @@ -311,7 +312,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) let constraints = (List.fold_right (fun (_,_,cs,_) cons -> cs@cons) pat_checks [])@cs in let bounds = List.fold_right (fun (_,_,_,bounds) b_env -> merge_bounds bounds b_env) pat_checks nob in let t = {t=Tid id} in - let t',cs' = type_consistent (Patt l) d_env false t expect_t in + let t',cs' = type_consistent (Patt l) d_env Guarantee false t expect_t in (P_aux((P_record(pats',false)),(l,cons_tag_annot t' emp_tag (cs@cs'))),env,constraints@cs',bounds,t')) | P_vector pats -> let (item_t, base, rise, ord) = match expect_actual.t with @@ -325,7 +326,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) ((pat'::pats),(t::ts),(t_env::t_envs),(cons@constraints),merge_bounds bs bounds)) pats ([],[],[],[],nob) 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 (Patt l) d_env true u t in t',cs) ts (item_t,[]) in + let (u,cs) = List.fold_right (fun u (t,cs) -> let t',cs = type_consistent (Patt l) d_env Require true u t in t',cs) ts (item_t,[]) in let len = List.length ts in let t = match (ord.order,d_env.default_o.order) with @@ -370,14 +371,14 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) ipats ([],[],[],[],nob) in let co = Patt l in let env = List.fold_right (fun e env -> Envmap.union e env) t_envs Envmap.empty in (*TODO Need to check for non-duplication of variables*) - let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent co d_env true u t) ts (item_t,[]) in + let (u,cs) = List.fold_right (fun u (t,cs) -> type_consistent co d_env Require true u t) ts (item_t,[]) in let t = {t = Tapp("vector",[(TA_nexp base);(TA_nexp rise); (TA_ord{order=(if inc_or_dec then Oinc else Odec)});(TA_typ u)])} in let cs = if inc_or_dec - then [LtEq(co, base, {nexp = Nconst (big_int_of_int fst)}); - GtEq(co,rise, {nexp = Nconst (big_int_of_int (lst-fst))});]@cs - else [GtEq(co,base, {nexp = Nconst (big_int_of_int fst)}); - LtEq(co,rise, { nexp = Nconst (big_int_of_int (fst -lst))});]@cs in + then [LtEq(co, Require, base, {nexp = Nconst (big_int_of_int fst)}); + GtEq(co,Require, rise, {nexp = Nconst (big_int_of_int (lst-fst))});]@cs + else [GtEq(co, Require, base, {nexp = Nconst (big_int_of_int fst)}); + LtEq(co,Require, rise, { nexp = Nconst (big_int_of_int (fst -lst))});]@cs in (P_aux(P_vector_indexed(pats'),(l,cons_tag_annot t emp_tag cs)), env,constraints@cs,bounds,t) | P_tup(pats) -> let item_ts = match expect_actual.t with @@ -434,7 +435,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) (pat'::pats,t::ts,env::t_envs,cons@constraints,merge_bounds new_bounds bounds)) pats ([],[],[],[],nob) in let env = List.fold_right (fun e env -> Envmap.union e env) envs Envmap.empty in (*TODO Need to check for non-duplication of variables*) - let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent (Patt l) d_env true u t in t',cs@cs') ts (item_t,[]) in + let u,cs = List.fold_right (fun u (t,cs) -> let t',cs' = type_consistent (Patt l) d_env Require true 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,cons_tag_annot t emp_tag cs)), env,constraints@cs,bounds,t) @@ -452,7 +453,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let (ces, sc, ef) = List.fold_right (fun e (es,sc,ef) -> let (e,_,_,sc',_,ef') = (check_exp envs imp_param unit_t e) in (e::es,sc@sc',union_effects ef ef')) exps ([],[],pure_e) in - let _,cs = type_consistent (Expr l) d_env false unit_t expect_t in + let _,cs = type_consistent (Expr l) d_env Require false unit_t expect_t in (E_aux (E_nondet ces,(l,cons_ef_annot unit_t sc ef)),unit_t,t_env,sc,nob,ef) | E_id id -> let i = id_to_string id in @@ -461,7 +462,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let t,cs,ef,_ = subst params t cs ef in (match t.t with | Tfn({t = Tid "unit"},t',IP_none,ef) -> - let t',cs',ef',e' = type_coerce (Expr l) d_env false false t' + let t',cs',ef',e' = type_coerce (Expr l) d_env Guarantee false false t' (rebuild (Base(([],{t=Tfn(unit_t,t',IP_none,ef)}),Constructor,cs,ef,bounds))) expect_t in (e',t',t_env,cs@cs',nob,union_effects ef ef') | Tfn(t1,t',IP_none,e) -> @@ -470,7 +471,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Some(Base((params,t),Enum,cs,ef,bounds)) -> let t',cs,_,_ = subst params t cs ef in let t',cs',ef',e' = - type_coerce (Expr l) d_env false false t' (rebuild (cons_tag_annot t' Enum cs)) expect_t in + type_coerce (Expr l) d_env Require false false t' (rebuild (cons_tag_annot t' Enum cs)) expect_t in (e',t',t_env,cs@cs',nob,ef') | Some(Base(tp,Default,cs,ef,_)) | Some(Base(tp,Spec,cs,ef,_)) -> typ_error l ("Identifier " ^ i ^ " must be defined, not just specified, before use") @@ -492,25 +493,25 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | 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 = Base(([],t),Emp_global,cs,ef,bounds) in - let t',cs' = type_consistent (Expr l) d_env false t' expect_t' in + let t',cs' = type_consistent (Expr l) d_env Require false t' expect_t' in (rebuild tannot,t,t_env,cs@cs',bounds,ef) | Tapp("register",[TA_typ(t')]),Tuvar _ -> let ef' = add_effect (BE_aux(BE_rreg,l)) ef in let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in - let t',cs',_,e' = type_coerce (Expr l) d_env false false t' (rebuild tannot) expect_actual in + let t',cs',_,e' = type_coerce (Expr l) d_env Require false false t' (rebuild tannot) expect_actual in (e',t,t_env,cs@cs',bounds,ef') | Tapp("register",[TA_typ(t')]),_ -> let ef' = add_effect (BE_aux(BE_rreg,l)) ef in let tannot = Base(([],t),(if is_alias then Alias else External (Some i)),cs,ef',bounds) in - let t',cs',_,e' = type_coerce (Expr l) d_env false false t' (rebuild tannot) expect_actual in + let t',cs',_,e' = type_coerce (Expr l) d_env Require false false t' (rebuild tannot) expect_actual in (e',t',t_env,cs@cs',bounds,ef') | Tapp("reg",[TA_typ(t')]),_ -> let tannot = cons_bs_annot t cs bounds in - let t',cs',_,e' = type_coerce (Expr l) d_env false false t' (rebuild tannot) expect_actual in + let t',cs',_,e' = type_coerce (Expr l) d_env Require false false t' (rebuild tannot) expect_actual in (e',t',t_env,cs@cs',bounds,pure_e) | _ -> let t',cs',ef',e' = - type_coerce (Expr l) d_env false false t (rebuild (Base(([],t),tag,cs,pure_e,bounds))) expect_t in + type_coerce (Expr l) d_env Require false false t (rebuild (Base(([],t),tag,cs,pure_e,bounds))) expect_t in (e',t',t_env,cs@cs',bounds,union_effects ef ef') ) | Some NoTyp | Some Overload _ | None -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is unbound")) @@ -541,7 +542,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Tapp ("vector",[TA_nexp base;TA_nexp rise;TA_ord o;(TA_typ {t=Tid "bit"})]) -> let n = {nexp = Nconst (big_int_of_int i) } in let t = {t=Tapp("atom", [TA_nexp n;])} in - let cs = [LtEq(Expr l,n,{nexp = N2n(rise,None)})] in + let cs = [LtEq(Expr l,Guarantee,n,mk_sub {nexp = N2n(rise,None)} n_one)] in let f = match o.order with | Oinc -> "to_vec_inc" | Odec -> "to_vec_dec" | _ -> "to_vec_inc" in let internal_tannot = (l,(cons_bs_annot {t = Tapp("implicit",[TA_nexp rise])} [] b_env)) in let tannot = (l,cons_tag_annot expect_t (External (Some f)) cs) in @@ -568,7 +569,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): E_aux(E_app((Id_aux((Id f),l)), [(E_aux (E_internal_exp(tannot), tannot));simp_exp e l bit_t]),tannot),[],ef | _ -> simp_exp e l (new_t ()),[],ef)) in - let t',cs',_,e' = type_coerce (Expr l) d_env false true (get_e_typ e) e expect_t in + let t',cs',_,e' = type_coerce (Expr l) d_env Require false true (get_e_typ e) e expect_t in (e',t',t_env,cs@cs',nob,effect) | E_cast(typ,e) -> let cast_t = typ_to_t false false typ in @@ -576,14 +577,14 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let cast_t = typ_subst tp_env cast_t in let ct = {t = Toptions(cast_t,None)} in let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param ct e in - let t',cs2,ef',e' = type_coerce (Expr l) d_env true false u e' cast_t in - let t',cs3,ef'',e'' = type_coerce (Expr l) d_env false false cast_t e' expect_t in + let t',cs2,ef',e' = type_coerce (Expr l) d_env Require true false u e' cast_t in + let t',cs3,ef'',e'' = type_coerce (Expr l) d_env Guarantee false false cast_t e' expect_t in (e'',t',t_env,cs_a@cs@cs2@cs3,bounds,union_effects ef' (union_effects ef'' ef)) | E_app(id,parms) -> let i = id_to_string id in let check_parms p_typ parms = (match parms with | [] | [(E_aux (E_lit (L_aux (L_unit,_)),_))] - -> let (_,cs') = type_consistent (Expr l) d_env false unit_t p_typ in [],unit_t,cs',pure_e + -> let (_,cs') = type_consistent (Expr l) d_env Require false unit_t p_typ in [],unit_t,cs',pure_e | [parm] -> let (parm',arg_t,t_env,cs',_,ef_p) = check_exp envs imp_param p_typ parm in [parm'],arg_t,cs',ef_p | parms -> (match check_exp envs imp_param p_typ (E_aux (E_tuple parms,(l,NoTyp))) with @@ -594,9 +595,10 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (match parms with | [] | [(E_aux (E_lit (L_aux(L_unit, _)), _))] -> [],pure_e,[] | [parm] -> - let _,cs,ef,parm' = type_coerce (Expr l) d_env false false arg_t parm expect_arg_t in [parm'],ef,cs + let _,cs,ef,parm' = type_coerce (Expr l) d_env Require false false arg_t parm expect_arg_t in [parm'],ef,cs | parms -> - (match type_coerce (Expr l) d_env false false arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t with + (match type_coerce (Expr l) d_env Require false false arg_t (E_aux (E_tuple parms,(l,NoTyp))) expect_arg_t + with | (_,cs,ef,(E_aux(E_tuple parms',tannot'))) -> (parms',ef,cs) | _ -> raise (Reporting_basic.err_unreachable l "type coerce given tuple and tuple type returned non-tuple"))) in @@ -608,8 +610,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let implicit = {t= Tapp("implicit",[TA_nexp n])} in let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in E_aux(E_internal_exp((l,annot_i)),(l,simple_annot nat_t)) in - type_coerce (Expr l) - d_env false false ret (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t + type_coerce (Expr l) d_env Guarantee false false ret + (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) -> (*let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in let _ = Printf.eprintf "and expected type is %s and return type is %s\n" (t_to_string expect_t) (t_to_string ret) in*) @@ -620,11 +622,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in E_aux (E_internal_exp_user((l, annot_iu),(l,annot_i)), (l,simple_annot nat_t)) in - type_coerce (Expr l) d_env false false ret + type_coerce (Expr l) d_env Guarantee false false ret (E_aux (E_app(id,internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t | (IP_none,_) -> (*let _ = Printf.printf "no implicit length or var required\n" in*) - type_coerce (Expr l) d_env false false ret + type_coerce (Expr l) d_env Guarantee false false ret (E_aux (E_app(id, parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t in (match Envmap.apply t_env i with @@ -696,7 +698,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | _ -> typ_error l (i ^ " expected either the return type or the expected type to be a vector") in type_coerce (Expr l) d_env false false ret (E_aux (E_app(op, [internal_exp;lft;rht]),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t*) | IP_none -> - type_coerce (Expr l) d_env false false ret (E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t + type_coerce (Expr l) d_env Guarantee false false ret (E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t in (match Envmap.apply t_env i with | Some(Base(tp,Enum,cs,ef,b)) -> typ_error l ("Expected function with name " ^ i ^ " but found an enumeration identifier") @@ -783,7 +785,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): exps ([],[],[],pure_e) in let t = { t=Ttup typs } in let t',cs',ef',e' = - type_coerce (Expr l) d_env false false t (E_aux(E_tuple(exps),(l,simple_annot t))) expect_t in + type_coerce (Expr l) d_env Require false false t (E_aux(E_tuple(exps),(l,simple_annot t))) expect_t in (e',t',t_env,consts@cs',nob,union_effects ef' effect)) | E_if(cond,then_,else_) -> let (cond',_,_,c1,_,ef1) = check_exp envs imp_param bit_t cond in @@ -791,8 +793,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Tuvar _ -> let then',then_t,then_env,then_c,then_bs,then_ef = check_exp envs imp_param (new_t ()) then_ in let else',else_t,else_env,else_c,else_bs,else_ef = check_exp envs imp_param (new_t ()) else_ in - let then_t',then_c' = type_consistent (Expr l) d_env true then_t expect_t in - let else_t',else_c' = type_consistent (Expr l) d_env true else_t then_t' in + let then_t',then_c' = type_consistent (Expr l) d_env Require true then_t expect_t in + let else_t',else_c' = type_consistent (Expr l) d_env Require true else_t then_t' in let t_cs = CondCons((Expr l),c1,then_c@then_c') in let e_cs = CondCons((Expr l),[],else_c@else_c') in (E_aux(E_if(cond',then',else'),(l,simple_annot expect_t)), @@ -818,11 +820,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let new_annot,local_cs = match (aorder_to_ord order).order with | Oinc -> - (simple_annot {t=Tapp("range",[TA_nexp fb;TA_nexp {nexp=Nadd(tb,tr)}])}, - [LtEq((Expr l),{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});LtEq((Expr l),fb,tb)]) + (simple_annot {t=Tapp("range",[TA_nexp fb;TA_nexp tr])}, + [LtEq((Expr l),Guarantee ,fr,tr);LtEq((Expr l),Guarantee,fb,tb)]) | Odec -> - (simple_annot {t=Tapp("range",[TA_nexp tb; TA_nexp {nexp=Nadd(fb,fr)}])}, - [GtEq((Expr l),{nexp=Nadd(fb,fr)},{nexp=Nadd(tb,tr)});GtEq((Expr l),fb,tb)]) + (simple_annot {t=Tapp("range",[TA_nexp tb; TA_nexp fr])}, + [GtEq((Expr l),Guarantee,fr,tr);GtEq((Expr l),Guarantee,fb,tb)]) | _ -> (typ_error l "Order specification in a foreach loop must be either inc or dec, not polymorphic") in (*TODO Might want to extend bounds here for the introduced variable*) @@ -847,7 +849,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): {t = Tapp("vector",[TA_nexp {nexp=Nconst (big_int_of_int (len-1))}; TA_nexp {nexp=Nconst (big_int_of_int len)}; TA_ord {order= Odec}; TA_typ item_t])} in - let t',cs',ef',e' = type_coerce (Expr l) d_env false false t (E_aux(E_vector es,(l,simple_annot t))) expect_t in + let t',cs',ef',e' = type_coerce (Expr l) d_env Guarantee false false t + (E_aux(E_vector es,(l,simple_annot t))) expect_t in (e',t',t_env,cs@cs',nob,union_effects effect ef') | E_vector_indexed(eis,(Def_val_aux(default,(ld,annot)))) -> let item_t,base_n,rise_n = match expect_t.t with @@ -880,12 +883,13 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let (base_bound,length_bound,cs_bounds) = if fully_enumerate then ({nexp=Nconst (big_int_of_int first)},{nexp = Nconst (big_int_of_int (List.length eis))},[]) - else (base_n,rise_n,[LtEq(Expr l, base_n,{nexp = Nconst (big_int_of_int first)}); - GtEq(Expr l,rise_n,{nexp = Nconst (big_int_of_int (List.length eis))})]) in + else (base_n,rise_n,[LtEq(Expr l,Require, base_n,{nexp = Nconst (big_int_of_int first)}); + GtEq(Expr l,Require, rise_n,{nexp = Nconst (big_int_of_int (List.length eis))})]) + in let t = {t = Tapp("vector", [TA_nexp(base_bound);TA_nexp length_bound; TA_ord({order= if is_increasing then Oinc else Odec});TA_typ item_t])} in - let t',cs',ef',e' = type_coerce (Expr l) d_env false false t + let t',cs',ef',e' = type_coerce (Expr l) d_env Require false false t (E_aux (E_vector_indexed(es,default'),(l,simple_annot t))) expect_t in (e',t',t_env,cs@cs_d@cs_bounds@cs',nob,union_effects ef_d (union_effects ef' effect)) | E_vector_access(vec,i) -> @@ -902,17 +906,18 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let cs_loc = match (ord.order,d_env.default_o.order) with | (Oinc,_) -> - [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})] + [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require, mk_add min m_rise,mk_add base rise)] | (Odec,_) -> - [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})] + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)] | (_,Oinc) -> - [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})] + [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise, mk_add base rise)] | (_,Odec) -> - [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})] + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require, mk_add min m_rise, mk_sub base rise)] | _ -> typ_error l "A vector must be either increasing or decreasing to access a single element" in (*let _ = Printf.eprintf "Type checking vector access. item_t is %s and expect_t is %s\n" (t_to_string item_t) (t_to_string expect_t) in*) - let t',cs',ef',e'=type_coerce (Expr l) d_env false false item_t (E_aux(E_vector_access(vec',i'),(l,simple_annot item_t))) expect_t in + let t',cs',ef',e'=type_coerce (Expr l) d_env Guarantee false false item_t + (E_aux(E_vector_access(vec',i'),(l,simple_annot item_t))) expect_t in (e',t',t_env,cs_loc@cs_i@cs@cs',nob,union_effects ef (union_effects ef' ef_i)) | E_vector_subrange(vec,i1,i2) -> let base,rise,ord = new_n(),new_n(),new_o() in @@ -932,44 +937,44 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): match (ord.order,d_env.default_o.order) with | (Oinc,_) -> [Eq((Expr l), new_base, n1); - Eq((Expr l), new_rise, {nexp=Nadd(n2, {nexp = Nneg n1})}); - LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1); - LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2); - LtEq((Expr l),base,n1); - LtEq((Expr l),base,max1); - LtEq((Expr l),n2,{nexp=Nadd(base,rise)}); - LtEq((Expr l),max2,{nexp=Nadd(base,rise)});] + Eq((Expr l), new_rise, mk_sub n2 n1); + LtEq((Expr l),Require, min1, n1); LtEq((Expr l),Require, n1,max1); + LtEq((Expr l),Require, min2, n2); LtEq((Expr l),Require, n2,max2); + LtEq((Expr l),Require,base,n1); + LtEq((Expr l),Require,base,max1); + LtEq((Expr l),Require,n2,mk_add base rise); + LtEq((Expr l),Require,max2,mk_add base rise);] | (Odec,_) -> [Eq((Expr l), new_base, n1); - Eq((Expr l), new_rise, {nexp= Nadd({nexp=Nadd(n1, {nexp = Nneg n2})}, {nexp = Nconst one})}); - LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1); - LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2); - GtEq((Expr l),base,n1); - GtEq((Expr l),base,max1); - LtEq((Expr l),n2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})}); - LtEq((Expr l),max2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})});] + Eq((Expr l), new_rise, mk_add (mk_sub n1 n2) n_one); + LtEq((Expr l), Require, min1, n1); LtEq((Expr l),Require, n1,max1); + LtEq((Expr l), Require, min2, n2); LtEq((Expr l),Require, n2,max2); + GtEq((Expr l),Require,base,n1); + GtEq((Expr l),Require,base,max1); + LtEq((Expr l),Require,n2,mk_add (mk_sub base rise) n_one); + LtEq((Expr l),Require,max2,mk_add (mk_sub base rise) n_one);] | (_,Oinc) -> [Eq((Expr l), new_base, n1); - Eq((Expr l), new_rise, {nexp=Nadd(n2, {nexp = Nneg n1})}); - LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1); - LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2); - LtEq((Expr l),base,n1); - LtEq((Expr l),base,max1); - LtEq((Expr l),n2,{nexp=Nadd(base,rise)}); - LtEq((Expr l),max2,{nexp=Nadd(base,rise)});] + Eq((Expr l), new_rise, mk_sub n2 n1); + LtEq((Expr l),Require, min1, n1); LtEq((Expr l),Require, n1,max1); + LtEq((Expr l),Require, min2, n2); LtEq((Expr l),Require, n2,max2); + LtEq((Expr l),Require,base,n1); + LtEq((Expr l),Require,base,max1); + LtEq((Expr l),Require,n2,mk_add base rise); + LtEq((Expr l),Require,max2,mk_add base rise);] | (_,Odec) -> [Eq((Expr l), new_base, n1); - Eq((Expr l), new_rise, {nexp= Nadd({nexp=Nadd(n1, {nexp = Nneg n2})}, {nexp = Nconst one})}); - LtEq((Expr l), min1, n1); LtEq((Expr l), n1,max1); - LtEq((Expr l), min2, n2); LtEq((Expr l), n2,max2); - GtEq((Expr l),base,n1); - GtEq((Expr l),base,max1); - LtEq((Expr l),n2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})}); - LtEq((Expr l),max2,{nexp= Nadd({nexp=Nadd(base, {nexp = Nneg rise})}, {nexp = Nconst one})});] + Eq((Expr l), new_rise, mk_add (mk_sub n1 n2) n_one); + LtEq((Expr l), Require, min1, n1); LtEq((Expr l),Require, n1,max1); + LtEq((Expr l), Require, min2, n2); LtEq((Expr l),Require, n2,max2); + GtEq((Expr l),Require,base,n1); + GtEq((Expr l),Require,base,max1); + LtEq((Expr l),Require,n2,mk_add (mk_sub base rise) n_one); + LtEq((Expr l),Require,max2,mk_add (mk_sub base rise) n_one);] | _ -> typ_error l "A vector must be either increasing or decreasing to access a slice" in let nt = {t=Tapp("vector",[TA_nexp new_base;TA_nexp new_rise; TA_ord ord;TA_typ item_t])} in let (t,cs3,ef3,e') = - type_coerce (Expr l) d_env false false nt + type_coerce (Expr l) d_env Guarantee false false nt (E_aux(E_vector_subrange(vec',i1',i2'),(l,constrained_annot nt cs_loc))) expect_t in (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc,nob,(union_effects ef (union_effects ef3 (union_effects ef_i1 ef_i2)))) | E_vector_update(vec,i,e) -> @@ -986,18 +991,19 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let cs_loc = match (ord.order,d_env.default_o.order) with | (Oinc,_) -> - [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})] + [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_add base rise)] | (Odec,_) -> - [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})] + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)] | (_,Oinc) -> - [LtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,rise)})] + [LtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise, mk_add base rise)] | (_,Odec) -> - [GtEq((Expr l),base,min); LtEq((Expr l),{nexp=Nadd(min,m_rise)},{nexp=Nadd(base,{nexp=Nneg rise})})] + [GtEq((Expr l),Require,base,min); LtEq((Expr l),Require,mk_add min m_rise,mk_sub base rise)] | _ -> typ_error l "A vector must be either increasing or decreasing to change a single element" in let nt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise; TA_ord ord;TA_typ item_t])} in let (t,cs3,ef3,e') = - type_coerce (Expr l) d_env false false nt (E_aux(E_vector_update(vec',i',e'),(l,constrained_annot nt cs_loc))) expect_t in + type_coerce (Expr l) d_env Guarantee false false nt + (E_aux(E_vector_update(vec',i',e'),(l,constrained_annot nt cs_loc))) expect_t in (e',t,t_env,cs3@cs@cs_i@cs_e@cs_loc,nob,(union_effects ef (union_effects ef3 (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 @@ -1017,27 +1023,30 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | _ -> let (base_e,rise_e) = new_n(),new_n() in let (e',ti',env_e,cs_e,bs_e,ef_e) = - check_exp envs imp_param {t=Tapp("vector",[TA_nexp base_e;TA_nexp rise_e;TA_ord ord;TA_typ item_t])} e in - let cs_add = [Eq((Expr l),base_e,min1);LtEq((Expr l),rise,m_rise2)] in + check_exp envs imp_param {t=Tapp("vector",[TA_nexp base_e;TA_nexp rise_e;TA_ord ord;TA_typ item_t])} e + in + let cs_add = [Eq((Expr l),base_e,min1);LtEq((Expr l),Guarantee,rise,m_rise2)] in (e',ti',env_e,cs_e@cs_add,bs_e,ef_e) in let cs_loc = match (ord.order,d_env.default_o.order) with | (Oinc,_) -> - [LtEq((Expr l),base,min1); LtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); - LtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,rise)});] + [LtEq((Expr l),Require,base,min1); LtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + LtEq((Expr l),Require,mk_add min2 m_rise2,mk_add base rise);] | (Odec,_) -> - [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); - GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});] + [GtEq((Expr l),Require,base,mk_add min1 m_rise1); + GtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + GtEq((Expr l),Require,mk_add min2 m_rise2,mk_sub base rise);] | (_,Oinc) -> - [LtEq((Expr l),base,min1); LtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); - LtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,rise)});] + [LtEq((Expr l),Require,base,min1); LtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + LtEq((Expr l),Require,mk_add min2 m_rise2,mk_add base rise);] | (_,Odec) -> - [GtEq((Expr l),base,{nexp=Nadd(min1,m_rise1)}); GtEq((Expr l),{nexp=Nadd(min1,m_rise1)},{nexp=Nadd(min2,m_rise2)}); - GtEq((Expr l),{nexp=Nadd(min2,m_rise2)},{nexp=Nadd(base,{nexp=Nneg rise})});] + [GtEq((Expr l),Require,base,mk_add min1 m_rise1); + GtEq((Expr l),Require,mk_add min1 m_rise1,mk_add min2 m_rise2); + GtEq((Expr l),Require,mk_add min2 m_rise2,mk_sub base rise);] | _ -> 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,ef3,e') = - type_coerce (Expr l) d_env false false nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,constrained_annot nt cs_loc))) expect_t in + type_coerce (Expr l) d_env Guarantee false false nt (E_aux(E_vector_update_subrange(vec',i1',i2',e'),(l,constrained_annot nt cs_loc))) expect_t in (e',t,t_env,cs3@cs@cs_i1@cs_i2@cs_loc@cs_e,nob,(union_effects ef (union_effects ef3 (union_effects ef_i1 (union_effects ef_i2 ef_e))))) | E_vector_append(v1,v2) -> let item_t,ord = match expect_t.t with @@ -1046,14 +1055,17 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | _ -> new_t (),new_o () in let base1,rise1 = new_n(), new_n() in let base2,rise2 = new_n(),new_n() in - let (v1',t1',_,cs_1,_,ef_1) = check_exp envs imp_param {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in - let (v2',t2',_,cs_2,_,ef_2) = check_exp envs imp_param {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in + let (v1',t1',_,cs_1,_,ef_1) = + check_exp envs imp_param {t=Tapp("vector",[TA_nexp base1;TA_nexp rise1;TA_ord ord;TA_typ item_t])} v1 in + let (v2',t2',_,cs_2,_,ef_2) = + check_exp envs imp_param {t=Tapp("vector",[TA_nexp base2;TA_nexp rise2;TA_ord ord;TA_typ item_t])} v2 in let ti = {t=Tapp("vector",[TA_nexp base1;TA_nexp {nexp = Nadd(rise1,rise2)};TA_ord ord; TA_typ item_t])} in let cs_loc = match ord.order with - | Odec -> [GtEq((Expr l),base1,{nexp = Nadd(rise1,rise2)})] + | Odec -> [GtEq((Expr l),Require,base1,mk_add rise1 rise2)] | _ -> [] in let (t,cs_c,ef_c,e') = - type_coerce (Expr l) d_env false false ti (E_aux(E_vector_append(v1',v2'),(l,constrained_annot ti cs_loc))) expect_t in + type_coerce (Expr l) d_env Guarantee false false ti + (E_aux(E_vector_append(v1',v2'),(l,constrained_annot ti cs_loc))) expect_t in (e',t,t_env,cs_loc@cs_1@cs_2,nob,(union_effects ef_c (union_effects ef_1 ef_2))) | E_list(es) -> let item_t = match expect_t.t with @@ -1063,7 +1075,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): (List.fold_right (fun (e,_,_,c,_,ef) (es,cs,effect) -> (e::es),(c@cs),union_effects ef effect) (List.map (check_exp envs imp_param item_t) es) ([],[],pure_e)) in let t = {t = Tapp("list",[TA_typ item_t])} in - let t',cs',ef',e' = type_coerce (Expr l) d_env false false t (E_aux(E_list es,(l,simple_annot t))) expect_t in + let t',cs',ef',e' = type_coerce (Expr l) d_env Guarantee false false t + (E_aux(E_list es,(l,simple_annot t))) expect_t in (e',t',t_env,cs@cs',nob,union_effects ef' effect) | E_cons(ls,i) -> let item_t = match expect_t.t with @@ -1073,7 +1086,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): let (ls',t',_,cs,_,ef) = check_exp envs imp_param lt ls in let (i', ti, _,cs_i,_,ef_i) = check_exp envs imp_param item_t i in let (t',cs',ef',e') = - type_coerce (Expr l) d_env false false lt (E_aux(E_cons(ls',i'),(l,simple_annot lt))) expect_t in + type_coerce (Expr l) d_env Guarantee false false lt (E_aux(E_cons(ls',i'),(l,simple_annot lt))) expect_t in (e',t',t_env,cs@cs'@cs_i,nob,union_effects ef' (union_effects ef ef_i)) | E_record(FES_aux(FES_Fexps(fexps,_),l')) -> let u,_ = get_abbrev d_env expect_t in @@ -1184,7 +1197,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Base((params,et),tag,cs,ef,bounds) -> let et,cs,ef,_ = subst params et cs ef in let (et',c',ef',acc) = - type_coerce (Expr l) d_env false false et + type_coerce (Expr l) d_env Guarantee false false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef,bounds)))) expect_t in (acc,et',t_env,cs@c'@c_sub,nob,union_effects ef' ef_sub))) | Tid i -> @@ -1200,7 +1213,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Base((params,et),tag,cs,ef,bounds) -> let et,cs,ef,_ = subst params et cs ef in let (et',c',ef',acc) = - type_coerce (Expr l) d_env false false et + type_coerce (Expr l) d_env Guarantee false false et (E_aux(E_field(e',id),(l,Base(([],et),tag,cs,ef,bounds)))) expect_t in (acc,et',t_env,cs@c'@c_sub,nob,union_effects ef' ef_sub))) | Tuvar _ -> @@ -1216,8 +1229,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | Base((params,et),tag,cs,ef,bounds) -> let et,cs,ef,_ = subst params et cs ef in let (et',c',ef',acc) = - type_coerce (Expr l) d_env false false et (E_aux(E_field(e',id), - (l,Base(([],et),tag,cs,ef,bounds)))) expect_t in + type_coerce (Expr l) d_env Guarantee false false et + (E_aux(E_field(e',id), + (l,Base(([],et),tag,cs,ef,bounds)))) expect_t in equate_t t' {t=Tid i}; (acc,et',t_env,cs@c'@c_sub,nob,union_effects ef' ef_sub)) | records -> typ_error l ("Multiple structs contain field " ^ fi ^ ", try adding a cast to disambiguate")) @@ -1243,7 +1257,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)): | E_assign(lexp,exp) -> let (lexp',t',t_env',tag,cs,b_env',ef) = check_lexp envs imp_param true lexp in let (exp',t'',_,cs',_,ef') = check_exp envs imp_param t' exp in - let (t',c') = type_consistent (Expr l) d_env false unit_t expect_t in + let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in (*let _ = Printf.eprintf "Constraints for E_assign %s\n" (constraints_to_string (cs@cs'@c')) in*) (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],ef,nob)))),unit_t,t_env',cs@cs'@c',b_env',union_effects ef ef') | E_exit e -> @@ -1409,17 +1423,18 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * let bs = merge_bounds bounds new_bounds in (match t_actual.t,is_top with | Tapp("register",[TA_typ u]),_ -> - let t',cs = type_consistent (Expr l) d_env false ty u in + let t',cs = type_consistent (Expr l) d_env Guarantee false ty u in let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in (LEXP_aux(lexp,(l,(Base(([],t),External (Some i),cs,ef,nob)))),ty,Envmap.empty,External (Some i),[],nob,ef) | Tapp("reg",[TA_typ u]),_ -> - let t',cs = type_consistent (Expr l) d_env false ty u in + let t',cs = type_consistent (Expr l) d_env Guarantee false ty u in (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,Envmap.empty,Emp_local,[],bs,pure_e) | Tapp("vector",_),false -> (LEXP_aux(lexp,(l,(Base(([],t),Emp_local,cs,pure_e,bs)))),ty,Envmap.empty,Emp_local,[],bs,pure_e) | Tuvar _,_ -> let u' = {t=Tapp("reg",[TA_typ ty])} in - t.t <- u'.t; (*Should be equate_t*) + equate_t t u'; + (*t.t <- u'.t; (*Should be equate_t*)*) (LEXP_aux(lexp,(l,(Base((([],u'),Emp_local,cs,pure_e,bs))))),ty,Envmap.empty,Emp_local,[],bs,pure_e) | (Tfn _ ,_) -> (match tag with @@ -1447,7 +1462,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * | Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) -> let acc_t = match ord.order with | Oinc -> {t = Tapp("range",[TA_nexp base;TA_nexp rise])} - | Odec -> {t = Tapp("range",[TA_nexp {nexp = Nadd(base,{nexp=Nneg rise})};TA_nexp rise])} + | Odec -> {t = Tapp("range",[TA_nexp (mk_sub base rise);TA_nexp rise])} | _ -> typ_error l ("Assignment to one vector element requires either inc or dec order") in let (e,t',_,cs',_,ef_e) = check_exp envs imp_param acc_t acc in @@ -1482,17 +1497,17 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot))) : (tannot lexp * | _ -> base_e1,range_e1,base_e2,range_e2 in let len = new_n() in let cs_t,res_t = match ord.order with - | Oinc -> ([LtEq((Expr l),base,base_e1); - LtEq((Expr l),{nexp=Nadd(base_e1,range_e1)},{nexp=Nadd(base_e2,range_e2)}); - LtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,rise)}); - LtEq((Expr l),len, {nexp =Nadd({nexp= Nadd({nexp= Nadd(base_e2,range_e2)},{nexp= Nconst one})}, - {nexp = Nneg({nexp = Nadd(base_e1,range_e1)})})});], + | Oinc -> ([LtEq((Expr l),Require,base,base_e1); + LtEq((Expr l),Require,mk_add base_e1 range_e1, mk_add base_e2 range_e2); + LtEq((Expr l),Require,mk_add base_e1 range_e2, mk_add base rise); + LtEq((Expr l),Require,len, mk_sub (mk_add (mk_add base_e2 range_e2) n_one) + (mk_add base_e1 range_e1))], {t=Tapp("vector",[TA_nexp base_e1;TA_nexp len;TA_ord ord;TA_typ t])}) - | Odec -> ([GtEq((Expr l),base,base_e1); - GtEq((Expr l),{nexp=Nadd(base_e1,range_e1)},{nexp=Nadd(base_e2,range_e2)}); - GtEq((Expr l),{nexp=Nadd(base_e1,range_e2)},{nexp=Nadd(base,{nexp=Nneg rise})}); - LtEq((Expr l),len, {nexp =Nadd({nexp= Nadd({nexp= Nadd(base_e2,range_e2)},{nexp= Nconst one})}, - {nexp = Nneg({nexp = Nadd(base_e1,range_e1)})})});], + | Odec -> ([GtEq((Expr l),Require,base,base_e1); + GtEq((Expr l),Require,mk_add base_e1 range_e1,mk_add base_e2 range_e2); + GtEq((Expr l),Require,mk_add base_e1 range_e2,mk_sub base rise); + LtEq((Expr l),Require,len, mk_sub (mk_add (mk_add base_e2 range_e2) n_one) + (mk_add base_e1 range_e1));], {t=Tapp("vector",[TA_nexp {nexp=Nadd(base_e1,range_e1)};TA_nexp len;TA_ord ord; TA_typ t])}) | _ -> typ_error l ("Assignment to a range of vector elements requires either inc or dec order") in @@ -1715,7 +1730,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) -> (* let _ = Printf.eprintf "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,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in - let t', _ = type_consistent (Patt l) d_env false param_t t' in + let t', _ = type_consistent (Patt l) d_env Require false param_t t' in let exp',_,_,cs_e,_,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', merge_bounds b_env b_env',tp_env)) imp_param ret_t exp in @@ -1735,7 +1750,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l, (*let _ = Printf.eprintf "Function %s is in env\n" id in*) let u,constraints,eft,t_param_env_spec = subst params u constraints eft in let t_param_cs = type_param_consistent l t_param_env_spec t_param_env in - let _,cs_decs = type_consistent (Specc l) d_env false t u in + let _,cs_decs = type_consistent (Specc l) d_env Require false t u in (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %s derived constraints and %s stated and %s from environment consistency\n" id (t_to_string t) (t_to_string u) (constraints_to_string cs_decs) (constraints_to_string (constraints@c')) (constraints_to_string t_param_cs) in*) let imp_param = match u.t with | Tfn(_,_,IP_user n,_) -> Some n @@ -1839,7 +1854,7 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ = (match (t1.t,t2.t) with | (Tapp("vector",[TA_nexp b1;TA_nexp r; TA_ord {order = Oinc}; TA_typ item_t]), Tapp("vector",[TA_nexp _ ;TA_nexp r2; TA_ord {order = Oinc}; TA_typ item_t2])) -> - let _ = type_consistent (Specc l) d_env false item_t item_t2 in + let _ = type_consistent (Specc l) d_env Guarantee false item_t item_t2 in let t = {t= Tapp("register",[TA_typ {t= Tapp("vector",[TA_nexp b1; TA_nexp {nexp = Nadd(r,r2)}; TA_ord {order = Oinc}; TA_typ item_t])}])} in let tannot = Base(([],t),Alias,[],pure_e,nob) in let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, TwoReg(reg1,reg2,tannot))} in diff --git a/src/type_internal.ml b/src/type_internal.ml index b74fa8ae..989460a8 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -86,11 +86,13 @@ type constraint_origin = | Fun of Parse_ast.l | Specc of Parse_ast.l +type range_enforcement = Require | Guarantee + (* Constraints for nexps, plus the location which added the constraint *) type nexp_range = - | LtEq of constraint_origin * nexp * nexp + | LtEq of constraint_origin * range_enforcement * nexp * nexp | Eq of constraint_origin * nexp * nexp - | GtEq of constraint_origin * nexp * nexp + | GtEq of constraint_origin * range_enforcement * nexp * nexp | In of constraint_origin * string * int list | InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *) | CondCons of constraint_origin * nexp_range list * nexp_range list @@ -220,13 +222,17 @@ let tag_to_string = function | Alias -> "Alias" | Spec -> "Spec" +let enforce_to_string = function + | Require -> "require" + | Guarantee -> "guarantee" + let rec constraint_to_string = function - | LtEq (co,nexp1,nexp2) -> - "LtEq(" ^ co_to_string co ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")" + | LtEq (co,enforce,nexp1,nexp2) -> + "LtEq(" ^ co_to_string co ^ ", " ^ enforce_to_string enforce ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")" | Eq (co,nexp1,nexp2) -> "Eq(" ^ co_to_string co ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")" - | GtEq (co,nexp1,nexp2) -> - "GtEq(" ^ co_to_string co ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")" + | GtEq (co,enforce,nexp1,nexp2) -> + "GtEq(" ^ co_to_string co ^ ", " ^ enforce_to_string enforce ^ ", " ^ n_to_string nexp1 ^ ", " ^ n_to_string nexp2 ^ ")" | In(co,var,ints) -> "In of " ^ var | InS(co,n,ints) -> "InS of " ^ n_to_string n | CondCons(co,pats,exps) -> @@ -988,7 +994,7 @@ let initial_typ_env = mk_range (mk_nv "o") (mk_nv "p")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "add_vec_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "p"),mk_sub {nexp=N2n (mk_nv "m",None)} n_one)], pure_e,nob); Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); @@ -1000,21 +1006,21 @@ let initial_typ_env = mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), External (Some "add_vec_range_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "p"),mk_sub {nexp=N2n (mk_nv "m",None)} n_one)], pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "add_range_vec"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "p"),mk_sub {nexp = N2n (mk_nv "m",None)} n_one)], pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) - (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), + (mk_range (mk_nv "o") (mk_add (mk_nv "p") (mk_sub {nexp = N2n (mk_nv "m",None)} n_one))))), External (Some "add_range_vec_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "p"),mk_sub {nexp=N2n (mk_nv "m",None)} n_one)], pure_e,nob); Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t]) @@ -1048,7 +1054,7 @@ let initial_typ_env = mk_range (mk_nv "o") (mk_nv "p")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "add_vec_range_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "p"),(mk_sub {nexp=N2n (mk_nv "m",None)} n_one))], pure_e,nob); Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); @@ -1060,21 +1066,21 @@ let initial_typ_env = mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), External (Some "add_vec_range_range_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require, (mk_nv "p"),mk_sub {nexp=N2n (mk_nv "m",None)} n_one)], pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "add_range_vec_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "p"),(mk_sub {nexp = N2n (mk_nv "m",None)} n_one))], pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), External (Some "add_range_vec_range_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], + [LtEq(Specc(Parse_ast.Int("+",None)),Require,(mk_nv "p"),(mk_sub {nexp=N2n (mk_nv "m",None)} n_one))], pure_e,nob); Base(((mk_nat_params ["o";"p"]@(mk_ord_params["ord"])), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "p"); bit_t]) @@ -1097,10 +1103,7 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_sub (mk_nv "n") (mk_nv "o")) (mk_sub (mk_nv "m") (mk_nv "p"))))), - External (Some "minus"), - [GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nvar "n"},{nexp=Nvar "o"}); - GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nvar "o"})], - pure_e,nob); + External (Some "minus"),[],pure_e,nob); Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) @@ -1111,29 +1114,22 @@ let initial_typ_env = mk_range (mk_nv "o") (mk_nv "p")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "minus_vec_range_signed"), - [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + [],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), - External (Some "minus_vec_range_range_signed"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "minus_vec_range_range_signed"),[],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), - External (Some "minus_range_vec_signed"), - [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "minus_range_vec_signed"),[],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), - External (Some "minus_range_vec_range_signed"), - [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "minus_range_vec_range_signed"),[],pure_e,nob); Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) @@ -1152,10 +1148,7 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_sub (mk_nv "n") (mk_nv "o")) (mk_sub (mk_nv "m") (mk_nv "p"))))), - External (Some "minus"), - [GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nvar "n"},{nexp=Nvar "o"}); - GtEq(Specc(Parse_ast.Int("-",None)),{nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},{nexp=Nvar "o"})], - pure_e,nob); + External (Some "minus"),[],pure_e,nob); Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) @@ -1169,30 +1162,22 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), - External (Some "minus_vec_range"), - [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "minus_vec_range"),[],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), - External (Some "minus_vec_range_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "minus_vec_range_range"),[],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), - External (Some "minus_range_vec"), - [LtEq(Specc(Parse_ast.Int("-",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "minus_range_vec"),[],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p";])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m");]) (mk_range (mk_nv "o") (mk_add (mk_nv "p") {nexp = N2n (mk_nv "m",None)})))), - External (Some "minus_range_vec_range"), - [LtEq(Specc(Parse_ast.Int("+",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp=N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "minus_range_vec_range"),[],pure_e,nob); Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) @@ -1221,16 +1206,12 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))), - External (Some "mult_range_vec"), - [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "mult_range_vec"),[],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))), - External (Some "mult_vec_range"), - [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "mult_vec_range"),[],pure_e,nob); ])); ("*_s",Overload( Base(((mk_typ_params ["a";"b";"c"]), @@ -1250,16 +1231,12 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_range (mk_nv "o") (mk_nv "p"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))), - External (Some "mult_range_vec_signed"), - [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "mult_range_vec_signed"),[],pure_e,nob); Base(((mk_nat_params ["n";"m";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nadd (mk_nv "m", mk_nv "m"))))), - External (Some "mult_vec_range_signed"), - [LtEq(Specc(Parse_ast.Int("*",None)),mk_add (mk_nv "o") (mk_nv "p"),{nexp = N2n (mk_nv "m",None)})], - pure_e,nob); + External (Some "mult_vec_range_signed"),[],pure_e,nob); Base(((mk_nat_params ["n";"o";"p"])@(mk_ord_params ["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) @@ -1281,14 +1258,13 @@ let initial_typ_env = [Base(((mk_nat_params["n";"m";"o"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range n_one (mk_nv "o")]) (mk_range n_zero (mk_sub (mk_nv "o") n_one)))), - External (Some "mod"),[GtEq(Specc(Parse_ast.Int("mod",None)),(mk_nv "o"),n_one)],pure_e,nob); + External (Some "mod"),[GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one)],pure_e,nob); Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_range n_one (mk_nv "o")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "mod_vec_range"), - [GtEq(Specc(Parse_ast.Int("mod",None)),(mk_nv "o"),n_one); - LtEq(Specc(Parse_ast.Int("mod",None)),(mk_nv "o"),{nexp = N2n (mk_nv "m", None)})],pure_e,nob); + [GtEq(Specc(Parse_ast.Int("mod",None)),Require,(mk_nv "o"),n_one);],pure_e,nob); Base(((mk_nat_params["n";"m"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")]) @@ -1302,21 +1278,22 @@ let initial_typ_env = [Base(((mk_nat_params["n";"m";"o";"p";"q";"r"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "q") (mk_nv "r")))), - External (Some "quot"),[GtEq(Specc(Parse_ast.Int("quot",None)),(mk_nv "o"),n_one); - LtEq(Specc(Parse_ast.Int("quot",None)), - (mk_mult (mk_add (mk_nv "o") (mk_nv "p")) (mk_add (mk_nv "q") (mk_nv "r"))), - (mk_add (mk_nv "n") (mk_nv "m")))], + External (Some "quot"),[GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "o"),n_one); + LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee, + (mk_mult (mk_nv "p") (mk_nv "r")),(mk_nv "m"))], pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), - External (Some "quot_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e,nob); + External (Some "quot_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")], + pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")]) (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")); bit_t;bit_t]))), - External (Some "quot_overflow_vec"),[GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")], + External (Some "quot_overflow_vec"), + [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")], pure_e,nob)])); ("quot_s", Overload( @@ -1327,23 +1304,21 @@ let initial_typ_env = (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m"); mk_range (mk_nv "o") (mk_nv "p")]) (mk_range (mk_nv "q") (mk_nv "r")))), External (Some "quot_signed"), - [GtEq(Specc(Parse_ast.Int("quot",None)),(mk_nv "o"),n_one); - LtEq(Specc(Parse_ast.Int("quot",None)),(mk_mult (mk_add (mk_nv "o") (mk_nv "p")) - (mk_add (mk_nv "q") (mk_nv "r"))), - (mk_add (mk_nv "n") (mk_nv "m")))], + [GtEq(Specc(Parse_ast.Int("quot",None)),Require,(mk_nv "o"),n_one); + LtEq(Specc(Parse_ast.Int("quot",None)),Guarantee,(mk_mult (mk_nv "p") (mk_nv "r")),mk_nv "m")], pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")]) (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")))), External (Some "quot_vec_signed"), - [GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e,nob); + [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,nob); Base(((mk_nat_params["n";"m";"p";"q"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "q")]) (mk_tup [(mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")); bit_t;bit_t]))), External (Some "quot_overflow_vec_signed"), - [GtEq(Specc(Parse_ast.Int("quot",None)), mk_nv "m", mk_nv "q")],pure_e,nob); + [GtEq(Specc(Parse_ast.Int("quot",None)),Require, mk_nv "m", mk_nv "q")],pure_e,nob); ])); ("length", Base((["a",{k=K_Typ}]@(mk_nat_params["n";"m"])@(mk_ord_params["ord"]), (mk_pure_fun (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nvar "m")) @@ -1354,7 +1329,7 @@ let initial_typ_env = (mk_pure_imp (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "n") (Nvar "m")) (mk_vector {t=Tvar "a"} (Ovar "ord") (Nvar "p") (Nvar "o")) "o")), External (Some "mask"), - [GtEq(Specc(Parse_ast.Int("mask",None)), (mk_nv "m"), (mk_nv "o"))],pure_e,nob)); + [GtEq(Specc(Parse_ast.Int("mask",None)),Guarantee, (mk_nv "m"), (mk_nv "o"))],pure_e,nob)); (*TODO These should be IP_start *) ("to_vec_inc",Base(([("a",{k=K_Typ})],{t=Tfn(nat_typ,{t=Tvar "a"},IP_none,pure_e)}),External None,[],pure_e,nob)); ("to_vec_dec",Base(([("a",{k=K_Typ})],{t=Tfn(nat_typ,{t=Tvar "a"},IP_none,pure_e)}),External None,[],pure_e,nob)); @@ -1398,9 +1373,8 @@ let initial_typ_env = [Base(((mk_nat_params ["n"; "m"; "o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "lt"), - [LtEq(Specc(Parse_ast.Int("<",None)), - {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},n_one)}, - {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})], + [LtEq(Specc(Parse_ast.Int("<",None)),Guarantee, mk_add (mk_nv "n") n_one, mk_nv "o"); + LtEq(Specc(Parse_ast.Int("<",None)),Guarantee, mk_add (mk_nv "m") n_one, mk_nv "p")], pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); @@ -1415,9 +1389,9 @@ let initial_typ_env = [Base(((mk_nat_params ["n"; "m"; "o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "lt_signed"), - [LtEq(Specc(Parse_ast.Int("<_s",None)), - {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},n_one)}, - {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e,nob); + [LtEq(Specc(Parse_ast.Int("<_s",None)),Guarantee, mk_add (mk_nv "n") n_one, mk_nv "o"); + LtEq(Specc(Parse_ast.Int("<_s",None)),Guarantee, mk_add (mk_nv "m") n_one, mk_nv "p")], + pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), @@ -1431,9 +1405,9 @@ let initial_typ_env = [Base(((mk_nat_params ["n";"m";"o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "gt"), - [GtEq(Specc(Parse_ast.Int(">",None)), - {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})}, - {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},n_one)})],pure_e,nob); + [GtEq(Specc(Parse_ast.Int(">",None)),Guarantee, mk_nv "n", mk_add (mk_nv "o") n_one); + GtEq(Specc(Parse_ast.Int(">",None)),Guarantee, mk_nv "m", mk_add (mk_nv "p") n_one)], + pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), @@ -1447,9 +1421,9 @@ let initial_typ_env = [Base(((mk_nat_params ["n";"m";"o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "gt_signed"), - [GtEq(Specc(Parse_ast.Int(">",None)), - {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})}, - {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},n_one)})],pure_e,nob); + [GtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "n", mk_add (mk_nv "o") n_one); + GtEq(Specc(Parse_ast.Int(">_s",None)),Guarantee, mk_nv "m", mk_add (mk_nv "p") n_one)], + pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), @@ -1463,9 +1437,9 @@ let initial_typ_env = [Base(((mk_nat_params ["n"; "m"; "o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "lteq"), - [LtEq(Specc(Parse_ast.Int("<=",None)), - {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},n_one)}, - {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e,nob); + [LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "n",mk_nv "o"); + LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "m",mk_nv "p")], + pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), @@ -1479,9 +1453,9 @@ let initial_typ_env = [Base(((mk_nat_params ["n"; "m"; "o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "lteq_signed"), - [LtEq(Specc(Parse_ast.Int("<=",None)), - {nexp=Nadd({nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})},n_one)}, - {nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})})],pure_e,nob); + [LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "n",mk_nv "o"); + LtEq(Specc(Parse_ast.Int("<=",None)),Guarantee,mk_nv "m",mk_nv "p")], + pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@["ord",{k=K_Ord}]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), @@ -1495,9 +1469,9 @@ let initial_typ_env = [Base(((mk_nat_params ["n";"m";"o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "gteq"), - [GtEq(Specc(Parse_ast.Int(">",None)), - {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})}, - {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},n_one)})],pure_e,nob); + [GtEq(Specc(Parse_ast.Int(">=",None)),Guarantee, mk_nv "n", mk_nv "o"); + GtEq(Specc(Parse_ast.Int(">=",None)),Guarantee, mk_nv "m", mk_nv "p")], + pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), @@ -1511,9 +1485,9 @@ let initial_typ_env = [Base(((mk_nat_params ["n";"m";"o";"p"]), (mk_pure_fun (mk_tup [mk_range (mk_nv "n") (mk_nv "m");mk_range (mk_nv "o") (mk_nv "p")]) bit_t)), External (Some "gteq_signed"), - [GtEq(Specc(Parse_ast.Int(">",None)), - {nexp=Nadd({nexp=Nvar "n"},{nexp=Nvar "m"})}, - {nexp=Nadd({nexp=Nadd({nexp=Nvar "o"},{nexp=Nvar "p"})},n_one)})],pure_e,nob); + [GtEq(Specc(Parse_ast.Int(">=_s",None)),Guarantee, mk_nv "n", mk_nv "o"); + GtEq(Specc(Parse_ast.Int(">=_s",None)),Guarantee, mk_nv "m", mk_nv "p")], + pure_e,nob); Base((((mk_nat_params ["n";"o";"p"])@[("ord",{k=K_Ord})]), (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (Nvar "o") (Nvar "n"); mk_vector bit_t (Ovar "ord") (Nvar "p") (Nvar "n")]) bit_t)), @@ -1526,7 +1500,7 @@ let initial_typ_env = External (Some "ltu"),[],pure_e,nob)); (">_u",Base((["a",{k=K_Typ}],(mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "a"}]) bit_t)), External (Some "gtu"),[],pure_e,nob)); - ("is_one",Base(([],(mk_pure_fun bit_t bool_t)),External (Some "is_one"),[],pure_e,nob)); + ("is_one",Base(([],(mk_pure_fun bit_t bit_t)),External (Some "is_one"),[],pure_e,nob)); (*correct again*) mk_bitwise_op "bitwise_not" "~" 1; mk_bitwise_op "bitwise_or" "|" 2; @@ -1611,8 +1585,8 @@ 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) + | GtEq(l,enforce,n1,n2)::cs -> GtEq(l,enforce,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs) + | LtEq(l,enforce,n1,n2)::cs -> LtEq(l,enforce,n_subst t_env n1, n_subst t_env n2)::(cs_subst t_env cs) | In(l,s,ns)::cs -> let nexp = n_subst t_env {nexp=Nvar s} in (match nexp.nexp with @@ -1851,7 +1825,7 @@ let build_variable_range d_env v typ = let t_actual = match t.t with | Tabbrev(_,t) -> t | _ -> t in match t_actual.t with | Tapp("atom", [TA_nexp n]) -> Some(VR_eq(v,n)) - | Tapp("range", [TA_nexp base;TA_nexp top]) -> Some(VR_range(v,[LtEq((Patt Unknown),base,top)])) + | Tapp("range", [TA_nexp base;TA_nexp top]) -> Some(VR_range(v,[LtEq((Patt Unknown),Require,base,top)])) | Tapp("vector", [TA_nexp start; TA_nexp rise; _; _]) -> Some(VR_vec_eq(v,rise)) | Tuvar _ -> Some(VR_recheck(v,t_actual)) | _ -> None @@ -1977,7 +1951,7 @@ and conforms_to_e loosely spec actual = When considering two range type applications, will check for consistency instead of equality When considering two atom type applications, will expand into a range encompasing both when widen is true *) -let rec type_consistent_internal co d_env widen t1 cs1 t2 cs2 = +let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 = (* let _ = Printf.printf "type_consistent_internal called with %s and %s\n" (t_to_string t1) (t_to_string t2) in*) let l = get_c_loc co in let t1,cs1' = get_abbrev d_env t1 in @@ -1996,11 +1970,11 @@ let rec type_consistent_internal co d_env widen t1 cs1 t2 cs2 = | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tapp("range",[TA_nexp b2;TA_nexp r2;]) -> if (nexp_eq b1 b2)&&(nexp_eq r1 r2) then (t2,csp) - else (t1, csp@[GtEq(co,b1,b2);LtEq(co,r1,r2)]) + else (t1, csp@[GtEq(co,enforce,b1,b2);LtEq(co,enforce,r1,r2)]) | Tapp("atom",[TA_nexp a]),Tapp("range",[TA_nexp b1; TA_nexp r1]) -> - (t1, csp@[GtEq(co,a,b1);LtEq(co,a,r1)]) + (t1, csp@[GtEq(co,enforce,a,b1);LtEq(co,enforce,a,r1)]) | Tapp("range",[TA_nexp b1; TA_nexp r1]),Tapp("atom",[TA_nexp a]) -> - (t2, csp@[GtEq(co,b1,a);LtEq(co,r1,a)]) + (t2, csp@[GtEq(co,enforce,b1,a);LtEq(co,enforce,r1,a)]) | Tapp("atom",[TA_nexp a1]),Tapp("atom",[TA_nexp a2]) -> if nexp_eq a1 a2 then (t2,csp) @@ -2013,46 +1987,46 @@ let rec type_consistent_internal co d_env widen t1 cs1 t2 cs2 = else ({t=Tapp ("range",[TA_nexp a2;TA_nexp a1])},csp) | _ -> let nu1,nu2 = new_n (),new_n () in ({t=Tapp("range",[TA_nexp nu1;TA_nexp nu2])}, - csp@[LtEq(co,nu1,a1);LtEq(co,nu1,a2);LtEq(co,a1,nu2);LtEq(co,a2,nu2)])) + csp@[LtEq(co,enforce,nu1,a1);LtEq(co,enforce,nu1,a2);LtEq(co,enforce,a1,nu2);LtEq(co,enforce,a2,nu2)])) | Tapp(id1,args1), Tapp(id2,args2) -> (*let _ = Printf.printf "checking consistency of %s and %s\n" id1 id2 in*) let la1,la2 = List.length args1, List.length args2 in if id1=id2 && la1 = la2 - then (t2,csp@(List.flatten (List.map2 (type_arg_eq co d_env widen) args1 args2))) + then (t2,csp@(List.flatten (List.map2 (type_arg_eq co d_env enforce widen) args1 args2))) else eq_error l ("Type application of " ^ (t_to_string t1) ^ " and " ^ (t_to_string t2) ^ " must match") | Tfn(tin1,tout1,_,effect1),Tfn(tin2,tout2,_,effect2) -> - let (tin,cin) = type_consistent co d_env widen tin1 tin2 in - let (tout,cout) = type_consistent co d_env widen tout1 tout2 in + let (tin,cin) = type_consistent co d_env Require widen tin1 tin2 in + let (tout,cout) = type_consistent co d_env Guarantee widen tout1 tout2 in let _ = effects_eq co effect1 effect2 in (t2,csp@cin@cout) | Ttup t1s, Ttup t2s -> - (t2,csp@(List.flatten (List.map snd (List.map2 (type_consistent co d_env widen) t1s t2s)))) + (t2,csp@(List.flatten (List.map snd (List.map2 (type_consistent co d_env enforce widen) t1s t2s)))) | Tuvar _, t -> equate_t t1 t2; (t1,csp) | Tapp("range",[TA_nexp b;TA_nexp r]),Tuvar _ -> let b2,r2 = new_n (), new_n () in let t2' = {t=Tapp("range",[TA_nexp b2;TA_nexp r2])} in equate_t t2 t2'; - (t2,csp@[GtEq(co,b,b2);LtEq(co,r,r2)]) + (t2,csp@[GtEq(co,enforce,b,b2);LtEq(co,enforce,r,r2)]) | Tapp("atom",[TA_nexp a]),Tuvar _ -> let b,r = new_n (), new_n () in let t2' = {t=Tapp("range",[TA_nexp b;TA_nexp r])} in equate_t t2 t2'; - (t2,csp@[GtEq(co,a,b);LtEq(co,a,r)]) + (t2,csp@[GtEq(co,enforce,a,b);LtEq(co,enforce,a,r)]) | t,Tuvar _ -> equate_t t2 t1; (t2,csp) | _,_ -> eq_error l ("Type mismatch found " ^ (t_to_string t1) ^ " but expected a " ^ (t_to_string t2)) -and type_arg_eq co d_env widen ta1 ta2 = +and type_arg_eq co d_env enforce widen ta1 ta2 = match ta1,ta2 with - | TA_typ t1,TA_typ t2 -> snd (type_consistent co d_env widen t1 t2) + | TA_typ t1,TA_typ t2 -> snd (type_consistent co d_env enforce widen t1 t2) | TA_nexp n1,TA_nexp n2 -> if nexp_eq n1 n2 then [] else [Eq(co,n1,n2)] | TA_eft e1,TA_eft e2 -> (ignore(effects_eq co e1 e2); []) | TA_ord o1,TA_ord o2 -> (ignore(order_eq co o1 o2);[]) | _,_ -> eq_error (get_c_loc co) "Type arguments must be of the same kind" -and type_consistent co d_env widen t1 t2 = - type_consistent_internal co d_env widen t1 [] t2 [] +and type_consistent co d_env enforce widen t1 t2 = + type_consistent_internal co d_env enforce widen t1 [] t2 [] -let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = +let rec type_coerce_internal co d_env enforce is_explicit widen 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 @@ -2069,7 +2043,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = " nor " ^ (t_to_string to2) ^ " can match expected type " ^ (t_to_string t2)) | Toptions(to1,None),_ -> if is_explicit - then type_coerce_internal co d_env is_explicit widen to1 cs1 e t2 cs2 + then type_coerce_internal co d_env enforce is_explicit widen to1 cs1 e t2 cs2 else (t2,csp,pure_e,e) | _,Toptions(to1,Some to2) -> if (conforms_to_t d_env false true to1 t1_actual || conforms_to_t d_env false true to2 t1_actual) @@ -2077,7 +2051,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = 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) -> if is_explicit - then type_coerce_internal co d_env is_explicit widen t1_actual cs1 e to1 cs2 + then type_coerce_internal co d_env enforce is_explicit widen t1_actual cs1 e to1 cs2 else (t1,csp,pure_e,e) | Ttup t1s, Ttup t2s -> let tl1,tl2 = List.length t1s,List.length t2s in @@ -2086,7 +2060,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = let vars = List.map2 (fun i t -> E_aux(E_id(i),(l,Base(([],t),Emp_local,[],pure_e,nob)))) ids t1s in let (coerced_ts,cs,efs,coerced_vars,any_coerced) = List.fold_right2 (fun v (t1,t2) (ts,cs,efs,es,coerced) -> - let (t',c',ef,e') = type_coerce co d_env is_explicit widen t1 v t2 in + let (t',c',ef,e') = type_coerce co d_env enforce is_explicit widen t1 v t2 in ((t'::ts),c'@cs,union_effects ef efs,(e'::es), coerced || (v == e'))) vars (List.combine t1s t2s) ([],[],pure_e,[],false) in if (not any_coerced) then (t2,cs,pure_e,e) @@ -2107,7 +2081,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = 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 && (id1 <> "vector") - then let t',cs' = type_consistent co d_env widen t1 t2 in (t',cs',pure_e,e) + then let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,e) else (match id1,id2,is_explicit with | "vector","vector",_ -> (match args1,args2 with @@ -2123,7 +2097,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = | _,Nuvar _ -> ignore(resolve_nsubst(r2)); equate_n r2 r1; | _ -> ());*) let cs = csp@[Eq(co,r1,r2)] in - let t',cs' = type_consistent co d_env widen t1i t2i in + let t',cs' = type_consistent co d_env enforce widen t1i t2i in let tannot = Base(([],t2),Emp_local,cs@cs',pure_e,nob) in (*let _ = Printf.eprintf "looking at vector vector coerce, t1 %s, t2 %s\n" (t_to_string t1) (t_to_string t2) in*) let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e,nob))),e),(l,tannot)) in @@ -2133,11 +2107,11 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (match args1,args2 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [Eq(co,b2,n_zero);GtEq(co,r2,{nexp = Nadd({nexp=N2n(r1,None)},{nexp = Nneg n_one})})] in + let cs = [Eq(co,b2,n_zero);GtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [Eq(co,b2,n_zero);GtEq(co,r2,{nexp = Nadd({nexp=N2n(r1,None)},{nexp = Nneg n_one})})] in + let cs = [Eq(co,b2,n_zero);GtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> eq_error l "Cannot convert a vector to an range without an order" @@ -2148,11 +2122,11 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (match args1,args2 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> - let cs = [GtEq(co,b2,{nexp=N2n(r1,None)})] in + let cs = [GtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> - let cs = [GtEq(co,b2,{nexp=N2n(r1,None)})] in + let cs = [GtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Base(([],t2),External None,cs,pure_e,nob)))) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> eq_error l "Cannot convert a vector to an range without an order" @@ -2163,13 +2137,13 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (match args2,args1 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [LtEq(co,r2,{nexp=N2n(r1,None)})] in + let cs = [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2;TA_nexp r2;] -> - let cs = [LtEq(co,r2,{nexp=N2n(r1,None)})] in + let cs = [LtEq(co,Guarantee,r2,mk_sub {nexp=N2n(r1,None)} n_one)] in let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) @@ -2182,13 +2156,13 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (match args2,args1 with | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> - let cs = [LtEq(co,b2,{nexp=N2n(r1,None)})] in + let cs = [LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in let tannot = (l,Base(([],t2),External None, cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_inc",l)), [(E_aux(E_internal_exp(tannot), tannot));e]),tannot)) | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}], [TA_nexp b2] -> - let cs = [LtEq(co,b2,{nexp=N2n(r1,None)})] in + let cs = [LtEq(co,Guarantee,b2,mk_sub {nexp=N2n(r1,None)} n_one)] in let tannot = (l,Base(([],t2),External None,cs,pure_e,nob)) in (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "to_vec_dec",l)), [(E_aux(E_internal_exp(tannot), tannot)); e]),tannot)) @@ -2197,7 +2171,6 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> eq_error l "Cannot convert a range into a non-bit vector" | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded")) - | "register",_,_ -> (match args1 with | [TA_typ t] -> @@ -2206,18 +2179,18 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (*let _ = Printf.eprintf "Adding cast to remove register read\n" in*) let ef = add_effect (BE_aux (BE_rreg, l)) pure_e in let new_e = E_aux(E_cast(t_to_typ unit_t,e),(l,Base(([],t),External None,[],ef,nob))) in - let (t',cs,ef',e) = type_coerce co d_env is_explicit widen t new_e t2 in + let (t',cs,ef',e) = type_coerce co d_env Guarantee is_explicit widen t new_e t2 in (t',cs,union_effects ef ef',e) | _ -> raise (Reporting_basic.err_unreachable l "register is not properly kinded")) | _,_,_ -> - let t',cs' = type_consistent co d_env widen t1 t2 in (t',cs',pure_e,e)) + let t',cs' = type_consistent co d_env enforce widen t1 t2 in (t',cs',pure_e,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(co,r1,n_one)] in (t2,cs,pure_e,E_aux((E_vector_access (e,(E_aux(E_lit(L_aux(L_num (int_of_big_int i),l)), (l,Base(([],{t=Tapp("atom",[TA_nexp b1])}),Emp_local,cs,pure_e,nob)))))), (l,Base(([],t2),Emp_local,cs,pure_e,nob)))) | Tid("bit"),Tapp("range",[TA_nexp b1;TA_nexp r1]) -> - let t',cs'= type_consistent co d_env false {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} t2 in + let t',cs'= type_consistent co d_env enforce false {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} t2 in (t2,cs',pure_e, E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Base(([],t1),Emp_local,[],pure_e,nob))), E_aux(E_lit(L_aux(L_num 0,l)),(l,Base(([],t2),Emp_local,[],pure_e,nob)))), @@ -2227,7 +2200,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (l,Base(([],t2),Emp_local,[],pure_e,nob)));]), (l,Base(([],t2),Emp_local,[],pure_e,nob)))) | Tid("bit"),Tapp("atom",[TA_nexp b1]) -> - let t',cs'= type_consistent co d_env false t2 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in + let t',cs'= type_consistent co d_env enforce false t2 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in (t2,cs',pure_e, E_aux(E_case (e,[Pat_aux(Pat_exp(P_aux(P_lit(L_aux(L_zero,l)),(l,Base(([],t1),Emp_local,[],pure_e,nob))), E_aux(E_lit(L_aux(L_num 0,l)),(l,Base(([],t2),Emp_local,[],pure_e,nob)))), @@ -2237,13 +2210,13 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (l,Base(([],t2),Emp_local,[],pure_e,nob)));]), (l,Base(([],t2),Emp_local,[],pure_e,nob)))) | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid("bit") -> - let t',cs'= type_consistent co d_env false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} + let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in (t2,cs',pure_e,E_aux(E_if(E_aux(E_app(Id_aux(Id "is_one",l),[e]),(l,Base(([],bit_t),External None,[],pure_e,nob))), E_aux(E_lit(L_aux(L_one,l)),(l,Base(([],bit_t),Emp_local,[],pure_e,nob))), E_aux(E_lit(L_aux(L_zero,l)),(l,Base(([],bit_t),Emp_local,[],pure_e,nob)))), (l,Base(([],bit_t),Emp_local,cs',pure_e,nob)))) | Tapp("atom",[TA_nexp b1]),Tid("bit") -> - let t',cs'= type_consistent co d_env false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} + let t',cs'= type_consistent co d_env enforce false t1 {t=Tapp("range",[TA_nexp n_zero;TA_nexp n_one])} in (t2,cs',pure_e,E_aux(E_if(E_aux(E_app(Id_aux(Id "is_one",l),[e]), (l,Base(([],bool_t),External None,[],pure_e,nob))), E_aux(E_lit(L_aux(L_one,l)),(l,Base(([],bit_t),Emp_local,[],pure_e,nob))), @@ -2252,7 +2225,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = | Tapp("range",[TA_nexp b1;TA_nexp r1;]),Tid(i) -> (match Envmap.apply d_env.enum_env i with | Some(enums) -> - (t2,[GtEq(co,b1,n_zero);LtEq(co,r1,{nexp=Nconst (big_int_of_int (List.length enums))})],pure_e, + (t2,[GtEq(co,Require,b1,n_zero);LtEq(co,Require,r1,{nexp=Nconst (big_int_of_int (List.length enums))})],pure_e, 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,Base(([],t1),Emp_local,[],pure_e, nob))), @@ -2264,7 +2237,8 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = | Tapp("atom",[TA_nexp b1]),Tid(i) -> (match Envmap.apply d_env.enum_env i with | Some(enums) -> - (t2,[GtEq(co,b1,n_zero);LtEq(co,b1,{nexp=Nconst (big_int_of_int (List.length enums))})],pure_e, + (t2,[GtEq(co,Require,b1,n_zero); + LtEq(co,Require,b1,{nexp=Nconst (big_int_of_int (List.length enums))})],pure_e, 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,Base(([],t1),Emp_local,[],pure_e,nob))), @@ -2276,7 +2250,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = | Tid(i),Tapp("range",[TA_nexp b1;TA_nexp r1;]) -> (match Envmap.apply d_env.enum_env i with | Some(enums) -> - (t2,[Eq(co,b1,n_zero);GtEq(co,r1,{nexp=Nconst (big_int_of_int (List.length enums))})],pure_e, + (t2,[Eq(co,b1,n_zero);GtEq(co,Guarantee,r1,{nexp=Nconst (big_int_of_int (List.length enums))})],pure_e, E_aux(E_case(e, List.mapi (fun i a -> Pat_aux(Pat_exp(P_aux(P_id(Id_aux(Id a,l)), (l,Base(([],t1),Emp_local,[],pure_e,nob))), @@ -2285,9 +2259,10 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 = (l,Base(([],t2),Emp_local,[],pure_e, nob)))) enums), (l,Base(([],t2),Emp_local,[],pure_e,nob)))) | None -> eq_error l ("Type mismatch: " ^ (t_to_string t1) ^ " , " ^ (t_to_string t2))) - | _,_ -> let t',cs = type_consistent co d_env widen t1 t2 in (t',cs,pure_e,e) + | _,_ -> let t',cs = type_consistent co d_env enforce widen t1 t2 in (t',cs,pure_e,e) -and type_coerce co d_env is_explicit widen t1 e t2 = type_coerce_internal co d_env is_explicit widen t1 [] e t2 [];; +and type_coerce co d_env enforce is_explicit widen t1 e t2 = + type_coerce_internal co d_env enforce is_explicit widen t1 [] e t2 [];; let rec select_overload_variant d_env params_check get_all variants actual_type = match variants with @@ -2428,7 +2403,7 @@ let rec simple_constraint_check in_env cs = | None -> (check cs) | Some(c) -> c::(check cs)) | _ -> (Eq(co,n1,n2)::(check cs))) - | GtEq(co,n1,n2)::cs -> + | GtEq(co,enforce,n1,n2)::cs -> (*let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in (*let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*) @@ -2450,8 +2425,8 @@ let rec simple_constraint_check in_env cs = then (check cs) else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i) - | _ -> GtEq(co,n1',n2')::(check cs))) - | LtEq(co,n1,n2)::cs -> + | _ -> GtEq(co,enforce,n1',n2')::(check cs))) + | LtEq(co,enforce,n1,n2)::cs -> (*let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *) let n1',n2' = normalize_nexp n1,normalize_nexp n2 in (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *) @@ -2464,7 +2439,7 @@ let rec simple_constraint_check in_env cs = | _, Npos_inf | Npos_inf, Npos_inf | Nneg_inf, _ | Nneg_inf, Nneg_inf -> check cs | Npos_inf, Nconst _ -> eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires infinity to be less than " ^ (n_to_string n2')) - | _,_ -> LtEq(co,n1',n2')::(check cs)) + | _,_ -> LtEq(co,enforce,n1',n2')::(check cs)) | CondCons(co,pats,exps):: cs -> (*let _ = Printf.eprintf "Condcons check length pats %i, length exps %i\n" (List.length pats) (List.length exps) in*) let pats' = check pats in @@ -2538,13 +2513,13 @@ let tannot_merge co denv widen t_older t_newer = | Default,tag -> (match t_n.t with | Tuvar _ -> let t_o,cs_o,ef_o,_ = subst ps_o t_o cs_o ef_o in - let t,_ = type_consistent co denv false t_n t_o in + let t,_ = type_consistent co denv Guarantee false t_n t_o in Base(([],t),tag_n,cs_o,ef_o,bounds_o) | _ -> t_newer) | Emp_local, Emp_local -> (*let _ = Printf.printf "local-local case\n" in*) (*TODO Check conforms to first; if true check consistent, if false replace with t_newer *) - let t,cs_b = type_consistent co denv widen t_n t_o in + let t,cs_b = type_consistent co denv Guarantee widen t_n t_o in (*let _ = Printf.printf "types consistent\n" in*) Base(([],t),Emp_local,cs_o@cs_n@cs_b,union_effects ef_o ef_n, merge_bounds bounds_o bounds_n) | _,_ -> t_newer) diff --git a/src/type_internal.mli b/src/type_internal.mli index d43e4650..f087f7f4 100644 --- a/src/type_internal.mli +++ b/src/type_internal.mli @@ -87,11 +87,13 @@ type constraint_origin = | Fun of Parse_ast.l | Specc of Parse_ast.l +type range_enforcement = Require | Guarantee + (* Constraints for nexps, plus the location which added the constraint *) type nexp_range = - | LtEq of constraint_origin * nexp * nexp + | LtEq of constraint_origin * range_enforcement * nexp * nexp | Eq of constraint_origin * nexp * nexp - | GtEq of constraint_origin * nexp * nexp + | GtEq of constraint_origin * range_enforcement * nexp * nexp | In of constraint_origin * string * int list | InS of constraint_origin * nexp * int list (* This holds the given value for string after a substitution *) | CondCons of constraint_origin * nexp_range list * nexp_range list (* Constraints from one path from a conditional (pattern or if) and the constraints from that conditional *) @@ -102,6 +104,8 @@ val get_c_loc : constraint_origin -> Parse_ast.l val n_zero : nexp val n_one : nexp val n_two : nexp +val mk_add : nexp -> nexp -> nexp +val mk_sub : nexp -> nexp -> nexp type variable_range = | VR_eq of string * nexp @@ -215,12 +219,12 @@ val conforms_to_t : def_envs -> bool -> bool -> t -> t -> bool When widen, two atoms are used to generate a range that contains them (or is defined by them for constants; and an atom and a range may widen the range. type_consistent mutates uvars to perform unification and will raise an error if the [[t1]] and [[t2]] are inconsistent *) -val type_consistent : constraint_origin -> def_envs -> bool -> t -> t -> t * nexp_range list +val type_consistent : constraint_origin -> def_envs -> range_enforcement -> bool -> t -> t -> t * nexp_range list (* type_coerce mutates to unify variables, and will raise an exception if the first type cannot be coerced into the second and is additionally inconsistent with the second; bool specifices whether this has arisen from an implicit or explicit type coercion request *) -val type_coerce : constraint_origin -> def_envs -> bool -> bool -> t -> exp -> t -> t * nexp_range list * effect * exp +val type_coerce : constraint_origin -> def_envs -> range_enforcement -> bool -> bool -> t -> exp -> t -> t * nexp_range list * effect * exp (* Merge tannots when intersection or unioning two environments. In case of default types, defer to tannot on right When merging atoms, use bool to control widening. |