summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/_tags2
-rw-r--r--src/initial_check.ml3
-rw-r--r--src/lem_interp/pretty_interp.ml2
-rw-r--r--src/lexer.mll2
-rw-r--r--src/parser.mly6
-rw-r--r--src/pre_lexer.mll8
-rw-r--r--src/pretty_print.ml16
-rw-r--r--src/process_file.ml3
-rw-r--r--src/rewriter.ml28
-rw-r--r--src/type_check.ml245
-rw-r--r--src/type_internal.ml68
-rw-r--r--src/type_internal.mli1
12 files changed, 220 insertions, 164 deletions
diff --git a/src/_tags b/src/_tags
index f188b454..334566bd 100644
--- a/src/_tags
+++ b/src/_tags
@@ -8,4 +8,4 @@ true: -traverse, debug
<test/*> and not <test/*.cmxa>: use_nums, use_lem, use_str
# disable partial match and unused variable warnings
-<**/*.ml>: warn_p, warn_y
+<**/*.ml>: warn_y
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 47810801..07fe01fd 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -20,6 +20,7 @@ let rec kind_to_string kind = match kind.k with
| K_Ord -> "Order"
| K_Efct -> "Effect"
| K_infer -> "Infer"
+ | K_Val -> "Val"
| K_Lam (kinds,kind) -> "Lam ... -> " ^ (kind_to_string kind)
@@ -234,6 +235,8 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effect =
| Parse_ast.BE_wreg -> BE_wreg
| Parse_ast.BE_rmem -> BE_rmem
| Parse_ast.BE_wmem -> BE_wmem
+ | Parse_ast.BE_wmv -> BE_wmv
+ | Parse_ast.BE_eamem -> BE_eamem
| Parse_ast.BE_depend -> BE_depend
| Parse_ast.BE_undef -> BE_undef
| Parse_ast.BE_unspec -> BE_unspec
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 76e696f9..3703940a 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -81,6 +81,8 @@ let doc_effect (BE_aux (e,_)) =
| BE_wreg -> "wreg"
| BE_rmem -> "rmem"
| BE_wmem -> "wmem"
+ | BE_wmv -> "wmv"
+ | BE_eamem -> "eamem"
| BE_barr -> "barr"
| BE_depend -> "depend"
| BE_undef -> "undef"
diff --git a/src/lexer.mll b/src/lexer.mll
index 2f07eeb9..cab2e3be 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -117,6 +117,8 @@ let kw_table =
("wreg", (fun x -> Wreg));
("rmem", (fun x -> Rmem));
("wmem", (fun x -> Wmem));
+ ("wmv", (fun x -> Wmv));
+ ("eamem", (fun x -> Eamem));
("undef", (fun x -> Undef));
("unspec", (fun x -> Unspec));
("nondet", (fun x -> Nondet));
diff --git a/src/parser.mly b/src/parser.mly
index eb2ba153..733bb83c 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -135,7 +135,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
%token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order
%token Pure Rec Register Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef
%token Undefined Union With Val
-%token Barr Depend Rreg Wreg Rmem Wmem Undef Unspec Nondet
+%token Barr Depend Rreg Wreg Rmem Wmem Wmv Eamem Undef Unspec Nondet
/* Avoid shift/reduce conflict - see right_atomic_exp rule */
@@ -316,6 +316,10 @@ effect:
{ efl BE_rmem }
| Wmem
{ efl BE_wmem }
+ | Wmv
+ { efl BE_wmv }
+ | Eamem
+ { efl BE_eamem }
| Undef
{ efl BE_undef }
| Unspec
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index b8869812..8987c0fd 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -146,7 +146,7 @@ rule token = parse
(M.find i kw_table) ()
else
Id(r i) }
- | tyvar_start startident ident* as i { Other }
+ | tyvar_start startident ident* { Other }
| "&" oper_char+ | "@" oper_char+ | "^" oper_char+ | "/" oper_char+ | "=" oper_char+ |
"!" oper_char+ | ">" oper_char+ | "<" oper_char+ | "+" oper_char+ | "*" oper_char+ |
"~" oper_char+ | "&&" oper_char+ | "^^" oper_char+| "::" oper_char+| "=/=" oper_char+ |
@@ -158,9 +158,9 @@ rule token = parse
">_ui" oper_char+ | "<=_s" oper_char+ | "<=_si" oper_char+ | "<=_u" oper_char+ | "<=_ui" oper_char+ |
"<_s" oper_char+ | "<_si" oper_char+ | "<_u" oper_char+ | "<_ui" oper_char+ | "**_s" oper_char+ |
"**_si" oper_char+ | "*_u" oper_char+ | "*_ui" oper_char+ | "2^" oper_char+ { Other }
- | digit+ as i { Other }
- | "0b" (binarydigit+ as i) { Other }
- | "0x" (hexdigit+ as i) { Other }
+ | digit+ { Other }
+ | "0b" (binarydigit+) { Other }
+ | "0x" (hexdigit+) { Other }
| '"' { let _ = string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf in Other }
| eof { Eof }
| _ as c { raise (LexError(
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index c56293ad..182c1929 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -142,6 +142,8 @@ and pp_format_base_effect_lem (BE_aux(e,l)) =
| BE_wreg -> "BE_wreg"
| BE_rmem -> "BE_rmem"
| BE_wmem -> "BE_wmem"
+ | BE_wmv -> "BE_wmv"
+ | BE_eamem -> "BE_eamem"
| BE_barr -> "BE_barr"
| BE_depend -> "BE_depend"
| BE_undef -> "BE_undef"
@@ -265,6 +267,7 @@ and pp_format_n n =
| Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")"
| Nneg_inf -> "(Ne_unary Ne_inf)"
| Npow _ -> "power_not_implemented"
+ | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)"
and pp_format_e e =
"(Effect_aux " ^
(match e.effect with
@@ -440,6 +443,7 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
| _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const"))
| _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit"))
| E_internal_cast ((_, Overload (_,_, _)), _) | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Found internal cast or exp with overload")
+ | E_internal_exp_user _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_exp_user"))
in
print_e ppf e
@@ -641,6 +645,8 @@ let doc_effect (BE_aux (e,_)) =
| BE_wreg -> "wreg"
| BE_rmem -> "rmem"
| BE_wmem -> "wmem"
+ | BE_wmv -> "wmv"
+ | BE_eamem -> "eamem"
| BE_barr -> "barr"
| BE_depend -> "depend"
| BE_undef -> "undef"
@@ -932,7 +938,11 @@ let doc_exp, doc_let =
| E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) ->
utf8string
("0b" ^
- (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst) exps ""))
+ (List.fold_right (fun (E_aux( e,_)) rst ->
+ (match e with
+ | E_lit(L_aux(l, _)) ->
+ ((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst)
+ | _ -> assert false)) exps ""))
| _ -> default_print ()))
| E_vector_indexed (iexps, (Def_val_aux (default,_))) ->
let default_string =
@@ -996,9 +1006,7 @@ let doc_exp, doc_let =
| Nvar v -> utf8string v
| _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const"))
| _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t)))
-
- (* XXX missing case
- AAA internal_cast should never have an overload, if it's been seen it's a bug *)
+ | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away"))
| E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false
and let_exp (LB_aux(lb,_)) = match lb with
diff --git a/src/process_file.ml b/src/process_file.ml
index 3b10aef8..c36f9381 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -97,7 +97,8 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty;
Type_internal.default_o =
{Type_internal.order = (match o with | (Ast.Ord_aux(Ast.Ord_inc,_)) -> Type_internal.Oinc
- | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec)};} in
+ | (Ast.Ord_aux(Ast.Ord_dec,_)) -> Type_internal.Odec
+ | _ -> Type_internal.Oinc)};} in
Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs
let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 93908eee..7999c3b4 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -40,7 +40,8 @@ let rec rewrite_nexp_to_exp program_vars l nexp =
But, for now I need to permit this to make power.sail compile, and most errors are in trap
or vectors *)
(*let _ = Printf.eprintf "unbound variable here %s\n" v in*)
- E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ)) in
+ E_aux (E_id (Id_aux (Id v,l)),(l,simple_annot typ))
+ | _ -> raise (Reporting_basic.err_unreachable l ("rewrite_nexp given n that can't be rewritten: " ^ (n_to_string nexp))) in
match program_vars with
| None -> actual_rewrite_n nexp
| Some program_vars ->
@@ -113,7 +114,6 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
| E_internal_cast ((_,casted_annot),exp) ->
let new_exp = rewrite_exp exp in
(match casted_annot,exp with
- | NoTyp,_ | Overload _,_ -> new_exp
| Base((_,t),_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_))) ->
(match t.t,exp_t.t with
(*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*)
@@ -122,18 +122,19 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
(match n1.nexp with
| Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp))
| Nadd _ | Nsub _ -> (match o1.order with
- | Oinc -> new_exp
| Odec ->
if nexp_one_more_than nw1 n1
then rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Unknown)), Unknown), new_exp))
- else new_exp)
+ else new_exp
+ | _ -> new_exp)
| _ -> new_exp)
- | _ -> new_exp))
+ | _ -> new_exp)
+ | _ -> new_exp)
| E_internal_exp (l,impl) ->
(match impl with
| Base((_,t),_,_,_,bounds) ->
(*let _ = Printf.eprintf "Rewriting internal expression, with type %s\n" (t_to_string t) in*)
- match t.t with
+ (match t.t with
(*Old case; should possibly be removed*)
| Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
| Tapp("vector", [_;TA_nexp r;_;_]) ->
@@ -147,19 +148,27 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
let nexps = expand_nexp i in
(match (match_to_program_vars nexps bounds) with
| [] -> rewrite_nexp_to_exp None l i
- | map -> rewrite_nexp_to_exp (Some map) l i))
+ | map -> rewrite_nexp_to_exp (Some map) l i)
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ ("Internal_exp given unexpected types " ^ (t_to_string t))))
+ | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot")))
| E_internal_exp_user ((l,user_spec),(_,impl)) ->
(match (user_spec,impl) with
| (Base((_,tu),_,_,_,_), Base((_,ti),_,_,_,bounds)) ->
(*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" (t_to_string tu) (t_to_string ti) in*)
- match (tu.t,ti.t) with
+ (match (tu.t,ti.t) with
| (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) ->
(*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
let nexps = expand_nexp i in
(match (match_to_program_vars nexps bounds) with
| [] -> rewrite_nexp_to_exp None l i
(*add u to program_vars env; for now it will work out properly by accident*)
- | map -> rewrite_nexp_to_exp (Some map) l i))
+ | map -> rewrite_nexp_to_exp (Some map) l i)
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti))))
+ | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot")))
and rewrite_let (LB_aux(letbind,(l,annot))) = match letbind with
| LB_val_explicit (typschm, pat,exp) ->
@@ -187,6 +196,7 @@ let rewrite_def d = match d with
| DEF_type _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ -> d
| DEF_fundef fdef -> DEF_fundef (rewrite_fun fdef)
| DEF_val letbind -> DEF_val (rewrite_let letbind)
+ | DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
let rewrite_defs (Defs defs) =
let rec rewrite ds = match ds with
diff --git a/src/type_check.ml b/src/type_check.ml
index f1b44395..0c6cbf46 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -146,7 +146,8 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env,tp_env)) as env) qis : (t_para
| K_Typ -> TA_typ {t = Tvar i}
| K_Nat -> TA_nexp { nexp = Nvar i}
| K_Ord -> TA_ord { order = Ovar i}
- | K_Efct -> TA_eft { effect = Evar i} in
+ | K_Efct -> TA_eft { effect = Evar i}
+ | _ -> raise (Reporting_basic.err_unreachable l'' "illegal kind allowed") in
((i,k)::ids,targ::typarms,cs)
| None -> raise (Reporting_basic.err_unreachable l'' "Unkinded id without default after initial check"))
| KOpt_kind(kind,Kid_aux((Var i),l'')) ->
@@ -155,7 +156,9 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env,tp_env)) as env) qis : (t_para
| K_Typ -> TA_typ {t = Tvar i}
| K_Nat -> TA_nexp { nexp = Nvar i}
| K_Ord -> TA_ord { order = Ovar i}
- | K_Efct -> TA_eft { effect = Evar i} in
+ | K_Efct -> TA_eft { effect = Evar i}
+ | K_Lam _ -> typ_error l'' "kind -> kind not permitted here"
+ | _ -> raise (Reporting_basic.err_unreachable l'' "Kind either infer or internal here") 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*)
@@ -227,7 +230,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
TA_ord d_env.default_o;TA_typ{t = Tid"bit"}])},lit
| L_string s -> {t = Tid "string"},lit
| L_undef -> typ_error l' "Cannot pattern match on undefined") in
-(* let _ = Printf.eprintf "checking pattern literal. expected type is %s. t is %s\n" (t_to_string expect_t) (t_to_string t) in*)
+ (*let _ = Printf.eprintf "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 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)
@@ -315,7 +318,9 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
let tup = {t = Ttup(List.map (fun (t,_,_,_) -> t) typ_pats)} in
let ft = {t = Tfn(tup,t, IP_none,pure_e) } in
let (ft_subst,cs,_,_) = subst vs false t cs pure_e in
- let subst_rtyp,subst_typs = match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups in
+ let subst_rtyp,subst_typs =
+ match ft_subst.t with | Tfn({t=Ttup tups},rt,_,_) -> rt,tups
+ | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec gave a non function type") in
let pat_checks =
List.map2 (fun (_,id,l,pat) styp ->
let (pat,env,constraints,new_bounds,u) = check_pattern envs emp_tag styp pat in
@@ -327,7 +332,8 @@ 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',cs' = type_consistent (Patt l) d_env Guarantee false ft_subst expect_t in
- (P_aux((P_record(pats',false)),(l,cons_tag_annot t' emp_tag (cs@cs'))),env,constraints@cs',bounds,t')))
+ (P_aux((P_record(pats',false)),(l,cons_tag_annot t' emp_tag (cs@cs'))),env,constraints@cs',bounds,t')
+ | _ -> raise (Reporting_basic.err_unreachable l "fields_to_rec returned a non Base tannot")))
| P_vector pats ->
let (item_t, base, rise, ord) = match expect_actual.t with
| Tapp("vector",[TA_nexp b;TA_nexp r;TA_ord o;TA_typ i]) -> (i,b,r,o)
@@ -711,15 +717,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
in
let check_result ret imp tag cs ef lft rht =
match imp with
- (*| IP_length _ ->
- let internal_exp = match expect_t.t,ret.t with
- | Tapp("vector",_),_ ->
- E_aux (E_internal_exp (l,simple_annot expect_t), (l, simple_annot nat_t))
- | _,Tapp("vector",_) ->
- E_aux (E_internal_exp (l,simple_annot ret), (l,simple_annot nat_t))
- | _ -> 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 ->
+ | _ -> (*implicit isn't allowed at the moment on any infix functions *)
type_coerce (Expr l) d_env Require false false b_env ret
(E_aux (E_app_infix(lft,op,rht),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
in
@@ -874,7 +872,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
| (Odec,_) | (Ouvar _,Odec) | (Ovar _,Odec) ->
{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
+ TA_ord {order= Odec}; TA_typ item_t])}
+ | _ -> raise (Reporting_basic.err_unreachable l "Default order was neither inc or dec") in
let t',cs',ef',e' = type_coerce (Expr l) d_env Guarantee false false b_env t
(E_aux(E_vector es,(l,simple_annot t))) expect_t in
(e',t',t_env,cs@cs',nob,union_effects effect ef')
@@ -886,7 +885,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let is_increasing = first <= last in
let es,cs,effect,contains_skip,_ = (List.fold_right
(fun ((i,e),c,ef) (es,cs,effect,skips,prev) ->
- (*let _ = Printf.printf "Checking increasing %b %i %i\n" is_increasing prev i in*)
+ (*let _ = Printf.eprintf "Checking increasing %b %i %i\n" is_increasing prev i in*)
let (esn, csn, efn) = (((i,e)::es), (c@cs), union_effects ef effect) in
if (is_increasing && prev > i)
then (esn,csn,efn,(((prev-i) > 1) || skips),i)
@@ -950,59 +949,44 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
(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
- let new_base,new_rise = new_n(),new_n() in
- let n1,min1,max1 = new_n(), new_n(),new_n() in
- let n2,min2,max2 = new_n(), new_n(),new_n() in
- let base_e,rise_e,ord_e,item_t = match expect_t.t with
- | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> base_n,rise_n,ord_n,item_t
- | _ -> new_n(),new_n(),new_o(),new_t() in
- let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ item_t])} in
- let (vec',t',_,cs,_,ef) = check_exp envs imp_param vt vec in
- let i1t = {t=Tapp("atom",[TA_nexp n1])} in
+ (*let _ = Printf.eprintf "checking e_vector_subrange: expect_t is %s\n" (t_to_string expect_t) in*)
+ let base,length,ord = new_n(),new_n(),new_o() in
+ let new_length = new_n() in
+ let n1_size = new_n() in
+ let n2_size = new_n() in
+ let item_t = match expect_t.t with
+ | Tapp("vector",[TA_nexp base_n;TA_nexp rise_n; TA_ord ord_n; TA_typ item_t]) -> item_t
+ | _ -> new_t() in
+ let vt = {t=Tapp("vector",[TA_nexp base;TA_nexp length;TA_ord ord;TA_typ item_t])} in
+ let (vec',vt',_,cs,_,ef) = check_exp envs imp_param vt vec in
+ let i1t = {t=Tapp("atom",[TA_nexp n1_size])} in
let (i1', ti1, _,cs_i1,_,ef_i1) = check_exp envs imp_param i1t i1 in
- let i2t = {t=Tapp("atom",[TA_nexp n2])} in
+ let i2t = {t=Tapp("atom",[TA_nexp n2_size])} in
let (i2', ti2, _,cs_i2,_,ef_i2) = check_exp envs imp_param i2t i2 in
let cs_loc =
match (ord.order,d_env.default_o.order) with
| (Oinc,_) ->
- [Eq((Expr l), new_base, n1);
- 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);]
+ [LtEq((Expr l), Require, base, n1_size);
+ LtEq((Expr l), Require, n1_size, n2_size);
+ LtEq((Expr l), Require, n2_size, mk_sub (mk_add base length) n_one);
+ Eq((Expr l), new_length, mk_add (mk_sub n2_size n1_size) n_one)]
| (Odec,_) ->
- [Eq((Expr l), new_base, n1);
- 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);]
+ [GtEq((Expr l), Require, base, n1_size);
+ GtEq((Expr l), Require, n1_size, n2_size);
+ GtEq((Expr l), Require, n2_size, mk_add (mk_sub base length) n_one);
+ Eq((Expr l), new_length, mk_add (mk_sub n1_size n2_size) n_one)]
| (_,Oinc) ->
- [Eq((Expr l), new_base, n1);
- 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);]
+ [LtEq((Expr l), Require, base, n1_size);
+ LtEq((Expr l), Require, n1_size, n2_size);
+ LtEq((Expr l), Require, n2_size, mk_sub (mk_add base length) n_one);
+ Eq((Expr l), new_length, mk_add (mk_sub n2_size n1_size) n_one)]
| (_,Odec) ->
- [Eq((Expr l), new_base, n1);
- 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);]
+ [GtEq((Expr l), Require, base, n1_size);
+ GtEq((Expr l), Require, n1_size, n2_size);
+ GtEq((Expr l), Require, n2_size, mk_add (mk_sub base length) n_one);
+ Eq((Expr l), new_length, mk_add (mk_sub n1_size n2_size) 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 nt = {t = Tapp("vector", [TA_nexp n1_size; TA_nexp new_length; TA_ord ord; TA_typ item_t]) } in
let (t,cs3,ef3,e') =
type_coerce (Expr l) d_env Require false false b_env nt
(E_aux(E_vector_subrange(vec',i1',i2'),(l,constrained_annot nt cs_loc))) expect_t in
@@ -1134,7 +1118,6 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
(match u_actual.t with
| Tid(n) | Tapp(n,_)->
(match lookup_record_typ n d_env.rec_env with
- | None -> typ_error l ("Expected a value of type " ^ n ^ " but found a struct")
| Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
let (ts,cs,eft,subst_env) = subst params false t cs eft in
if (List.length fexps = List.length fields)
@@ -1143,18 +1126,19 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in
(e',t',t_env,cs@cons@cs',nob,union_effects ef ef')
else typ_error l ("Expected a struct of type " ^ n ^ ", which should have " ^ string_of_int (List.length fields) ^ " fields")
- | Some(i,Register,tannot,fields) -> typ_error l ("Expected a value with register type, found a struct"))
+ | Some(i,Register,tannot,fields) -> typ_error l ("Expected a value with register type, found a struct")
+ | _ -> typ_error l ("Expected a value of type " ^ n ^ " but found a struct"))
| Tuvar _ ->
let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in
(match lookup_record_fields field_names d_env.rec_env with
- | None -> typ_error l "No struct type matches the set of fields given"
| Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
let (ts,cs,eft,subst_env) = subst params false t cs eft in
let fexps,cons,ef = List.fold_right (field_walker r subst_env bounds tag i) fexps ([],[],pure_e) in
let e = E_aux(E_record(FES_aux(FES_Fexps(fexps,false),l')),(l,simple_annot ts)) in
let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in
(e',t',t_env,cs@cons@cs',nob,union_effects ef ef')
- | Some(i,Register,tannot,fields) -> typ_error l "Expected a value with register type, found a struct")
+ | Some(i,Register,tannot,fields) -> typ_error l "Expected a value with register type, found a struct"
+ | _ -> typ_error l "No struct type matches the set of fields given")
| _ -> 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')) ->
let (e',t',_,c,_,ef) = check_exp envs imp_param expect_t exp in
@@ -1170,7 +1154,6 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
(match t'.t with
| Tid i | Tabbrev(_, {t=Tid i}) | Tapp(i,_) ->
(match lookup_record_typ i d_env.rec_env with
- | None -> typ_error l ("Expected a struct for this update, instead found an expression with type " ^ i)
| Some((i,Register,tannot,fields)) -> typ_error l "Expected a struct for this update, instead found a register"
| Some(((i,Record,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
if (List.length fexps <= List.length fields)
@@ -1180,7 +1163,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let e = E_aux(E_record_update(e',FES_aux(FES_Fexps(fexps,false),l')), (l,simple_annot ts)) in
let (t',cs',ef',e') = type_coerce (Expr l) d_env Guarantee false false b_env ts e expect_t in
(e',t',t_env,cs@cons@cs',nob,union_effects ef ef')
- else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes"))
+ else typ_error l ("Expected fields from struct " ^ i ^ ", given more fields than struct includes")
+ | _ ->
+ typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i))
| Tuvar _ ->
let field_names = List.map (fun (FE_aux(FE_Fexp(id,exp),(l,annot))) -> id_to_string id) fexps in
(match lookup_possible_records field_names d_env.rec_env with
@@ -1200,8 +1185,6 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
(match t'.t with
| Tabbrev({t=Tid i}, _) | Tabbrev({t=Tapp(i,_)},_) | Tid i | Tapp(i,_) ->
(match lookup_record_typ i d_env.rec_env with
- | None ->
- typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i)
| Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
let (ts,cs,eft,subst_env) = subst params false t cs eft in
(match lookup_field_type fi r with
@@ -1212,7 +1195,9 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
let (et',c',ef',acc) =
type_coerce (Expr l) d_env Require false false b_env ft
(E_aux(E_field(e',id),(l,Base(([],ft),tag,cs,eft,bounds)))) expect_t in
- (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub)))
+ (acc,et',t_env,cs@c'@c_sub@cs_sub',nob,union_effects ef' ef_sub))
+ | _ ->
+ typ_error l ("Expected a struct or register for this access, instead found an expression with type " ^ i))
| Tuvar _ ->
(match lookup_possible_records [fi] d_env.rec_env with
| [] -> typ_error l ("No struct or register has a field " ^ fi)
@@ -1252,12 +1237,12 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
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 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 ->
let (e',t',_,_,_,_) = check_exp envs imp_param (new_t ()) e in
(E_aux (E_exit e',(l,(simple_annot expect_t))),expect_t,t_env,[],nob,pure_e)
- | E_internal_cast _ | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
+ | E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ ->
+ raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
and check_block envs imp_param expect_t exps:((tannot exp) list * tannot * nexp_range list * t * effect) =
let Env(d_env,t_env,b_env,tp_env) = envs in
@@ -1313,7 +1298,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
(LEXP_aux(lexp,(l,(Base(([],t'),Alias,[],ef,nob)))), t, false, Envmap.empty, External (Some reg),[],nob,ef)
| Some(TwoReg(reg1,reg2, (Base(([],t'),_,_,_,_)))) ->
let u = match t.t with
- | Tapp("register", [TA_typ u]) -> u in
+ | Tapp("register", [TA_typ u]) -> u
+ | _ -> raise (Reporting_basic.err_unreachable l "TwoReg didn't contain a register type") in
(LEXP_aux(lexp,(l,Base(([],t'),Alias,[],ef,nob))), u, false, Envmap.empty, External None,[],nob,ef)
| _ -> assert false)
| Some(Base((parms,t),tag,cs,_,b)) ->
@@ -1369,8 +1355,9 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
(match ef'.effect with
| Eset effects ->
let mem_write = List.exists (fun (BE_aux(b,_)) -> match b with | BE_wmem -> true | _ -> false) effects in
+ let memv_write = List.exists (fun (BE_aux(b,_)) -> match b with |BE_wmv -> true | _ -> false) effects in
let reg_write = List.exists (fun (BE_aux(b,_)) -> match b with | BE_wreg -> true | _ -> false) effects in
- if (mem_write || reg_write)
+ if (mem_write || memv_write || reg_write)
then
let app,cs_a = get_abbrev d_env apps in
let out,cs_o = get_abbrev d_env out in
@@ -1406,8 +1393,8 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
let ef_all = union_effects ef ef_e in
(LEXP_aux(LEXP_memory(id,[e]),(l,Base(([],out),tag,cs_call,ef,nob))),
app,false,Envmap.empty,tag,cs_call@cs_e,nob,ef_all))
- else typ_error l ("Assignments require functions with a wmem or wreg effect")
- | _ -> typ_error l ("Assignments require functions with a wmem or wreg effect"))
+ else typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect")
+ | _ -> typ_error l ("Assignments require functions with a wmem, wmv, or wreg effect"))
| _ -> typ_error l ("Assignments require a function here, found " ^ i ^ " which has type " ^ (t_to_string t)))
| _ -> typ_error l ("Unbound identifier " ^ i))
| LEXP_cast(typ,id) ->
@@ -1485,55 +1472,49 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
typ_error l "Assignment expected a vector with a known order, try adding an annotation."
| _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t)))
| LEXP_vector_range(vec,e1,e2)->
- let (vec',item_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
- let item_t,cs = get_abbrev d_env item_t in
- let item_actual = match item_t.t with | Tabbrev(_,t) -> t | _ -> item_t in
- let item_actual,add_reg_write,reg_still_required,cs =
- match item_actual.t with
+ let (vec',vec_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
+ let vec_t,cs = get_abbrev d_env vec_t in
+ let vec_actual = match vec_t.t with | Tabbrev(_,t) -> t | _ -> vec_t in
+ let vec_actual,add_reg_write,reg_still_required,cs =
+ match vec_actual.t with
| Tapp("register",[TA_typ t]) ->
(match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,true,false,cs@cs')
| Tapp("reg",[TA_typ t]) ->
(match get_abbrev d_env t with | {t=Tabbrev(_,t)},cs' | t,cs' -> t,false,false,cs@cs')
- | _ -> item_actual,false,true,cs in
- (match item_actual.t with
+ | _ -> vec_actual,false,true,cs in
+ (match vec_actual.t with
| Tapp("vector",[TA_nexp base;TA_nexp rise;TA_ord ord;TA_typ t]) ->
- let base_e1,range_e1,base_e2,range_e2 = new_n(),new_n(),new_n(),new_n() in
- let base_t = {t=Tapp("range",[TA_nexp base_e1;TA_nexp range_e1])} in
- let range_t = {t=Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])} in
- let (e1',base_t',_,cs1,_,ef_e) = check_exp envs imp_param base_t e1 in
- let (e2',range_t',_,cs2,_,ef_e') = check_exp envs imp_param range_t e2 in
- let base_e1,range_e1,base_e2,range_e2 = match base_t'.t,range_t'.t with
- | (Tapp("range",[TA_nexp base_e1;TA_nexp range_e1]),
- Tapp("range",[TA_nexp base_e2;TA_nexp range_e2])) -> base_e1,range_e1,base_e2,range_e2
- | _ -> base_e1,range_e1,base_e2,range_e2 in
- let len = new_n() in
+ let size_e1,size_e2 = new_n(),new_n() in
+ let e1_t = {t=Tapp("atom",[TA_nexp size_e1])} in
+ let e2_t = {t=Tapp("atom",[TA_nexp size_e2])} in
+ let (e1',e1_t',_,cs1,_,ef_e) = check_exp envs imp_param e1_t e1 in
+ let (e2',e2_t',_,cs2,_,ef_e') = check_exp envs imp_param e2_t e2 in
+ let len = new_n() in
let needs_reg = match t.t with
| Tapp("reg",_) -> false
| Tapp("register",_) -> false
| _ -> true in
let cs_t,res_t = match ord.order with
- | 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),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])})
+ | Oinc -> ([LtEq((Expr l),Require,base,size_e1);
+ LtEq((Expr l),Require,size_e1, size_e2);
+ LtEq((Expr l),Require,size_e2, rise);
+ Eq((Expr l),len, mk_add (mk_sub size_e2 size_e1) n_one)],
+ {t=Tapp("vector",[TA_nexp size_e1;TA_nexp len;TA_ord ord;TA_typ t])})
+ | Odec -> ([GtEq((Expr l),Require,base,size_e1);
+ GtEq((Expr l),Require,size_e1,size_e2);
+ GtEq((Expr l),Require,size_e2,mk_sub base rise);
+ Eq((Expr l),len, mk_add (mk_sub size_e1 size_e2) n_one)],
+ {t=Tapp("vector",[TA_nexp size_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
let cs = cs_t@cs@cs1@cs2 in
let ef = union_effects ef (union_effects ef_e ef_e') in
if is_top && reg_required && reg_still_required && needs_reg
then typ_error l "Assignment requires a register or a non-parameter, non-letbound local identifier"
- else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],item_t),tag,cs,ef,nob))),res_t,reg_required&&reg_still_required && needs_reg
- ,env,tag,cs,bounds,ef)
+ else (LEXP_aux(LEXP_vector_range(vec',e1',e2'),(l,Base(([],res_t),tag,cs,ef,nob))),
+ res_t,reg_required&&reg_still_required && needs_reg,env,tag,cs,bounds,ef)
| Tuvar _ -> typ_error l "Assignement to a range of elements requires a vector with a known order, try adding an annotation."
- | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string item_t)))
+ | _ -> typ_error l ("Assignment expected vector, found assignment to type " ^ (t_to_string vec_t)))
| LEXP_field(vec,id)->
let (vec',item_t,reg_required,env,tag,csi,bounds,ef) = check_lexp envs imp_param false vec in
let vec_t = match vec' with
@@ -1543,8 +1524,6 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
(match vec_t.t with
| Tid i | Tabbrev({t=Tid i},_) | Tabbrev({t=Tapp(i,_)},_) | Tapp(i,_)->
(match lookup_record_typ i d_env.rec_env with
- | None ->
- typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i)
| Some(((i,rec_kind,(Base((params,t),tag,cs,eft,bounds)),fields) as r)) ->
let (ts,cs,eft,subst_env) = subst params false t cs eft in
(match lookup_field_type fi r with
@@ -1552,7 +1531,9 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
| Some t ->
let ft = typ_subst subst_env false t in
let (_,cs_sub') = type_consistent (Expr l) d_env Guarantee false ts vec_t in
- (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],ft),tag,csi@cs,eft,nob)))),ft,false,env,tag,csi@cs@cs_sub',bounds,ef)))
+ (LEXP_aux(LEXP_field(vec',id),(l,(Base(([],ft),tag,csi@cs,eft,nob)))),ft,false,env,tag,csi@cs@cs_sub',bounds,ef))
+ | _ ->
+ typ_error l ("Expected a register or struct for this update, instead found an expression with type " ^ i))
| _ -> typ_error l ("Expected a register binding here, found " ^ (t_to_string item_t)))
and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) : tannot letbind * tannot emap * nexp_range list * bounds_env * effect =
@@ -1723,23 +1704,25 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
let is_rec = match recopt with
| Rec_aux(Rec_nonrec,_) -> false
| Rec_aux(Rec_rec,_) -> true in
- let Some(id) = List.fold_right
- (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' ->
- match id' with
- | Some(id') -> if id' = id_to_string id then Some(id')
- else typ_error l ("Function declaration expects all definitions to have the same name, "
- ^ id_to_string id ^ " differs from other definitions of " ^ id')
- | None -> Some(id_to_string id)) funcls None in
+ let id = match (List.fold_right
+ (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' ->
+ match id' with
+ | Some(id') -> if id' = id_to_string id then Some(id')
+ else typ_error l ("Function declaration expects all definitions to have the same name, "
+ ^ id_to_string id ^ " differs from other definitions of " ^ id')
+ | None -> Some(id_to_string id)) funcls None) with
+ | Some id -> id
+ | None -> raise (Reporting_basic.err_unreachable l "funcl list might be empty") in
let in_env = Envmap.apply t_env id in
- let typ_params = match in_env with
- | Some(Base( (params,u),Spec,constraints,eft,_)) -> params
- | None -> [] in
+ let (typ_params,has_spec) = match in_env with
+ | Some(Base( (params,u),Spec,constraints,eft,_)) -> params,true
+ | _ -> [],false in
let ret_t,param_t,tannot,t_param_env = match tannotopt with
| 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 false false typ in
- (*TODO add check that ids == typ_params*)
- let t,constraints,_,t_param_env = subst typ_params true t constraints pure_e in
+ (*TODO add check that ids == typ_params when has_spec*)
+ let t,constraints,_,t_param_env = subst (if has_spec then typ_params else ids) true t constraints pure_e in
let p_t = new_t () in
let ef = new_e () in
t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef,nob),t_param_env in
@@ -1753,7 +1736,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
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
(*let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
- let _ = Printf.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) in*)
+ let _ = Printf.eprintf "constraints were pattern: %s\n expression: %s\n" (constraints_to_string cs_p) (constraints_to_string cs_e) in*)
let cs = [CondCons(Fun l,cs_p,cs_e)] in
(FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef,nob)))),(cs,ef))) funcls) in
let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) =
@@ -1832,13 +1815,13 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
let tannot = Base(([],et),Alias,[],pure_e,nob) in
let d_env = {d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
(AL_aux(AL_subreg(reg_a,subreg),(l,tannot)),tannot,d_env)))
- | _ -> let _ = Printf.eprintf "%s\n" (t_to_string reg_t) in assert false)
+ | _ -> typ_error l ("Expected a register with fields, given " ^ (t_to_string reg_t)))
| AL_bit(reg_a,bit) ->
let (reg,reg_a,reg_t,t) = check_reg reg_a in
let (E_aux(bit,(le,eannot)),_,_,_,_,_) = check_exp envs None (new_t ()) bit in
(match t.t with
| Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
- match (base.nexp,len.nexp,order.order, bit) with
+ (match (base.nexp,len.nexp,order.order, bit) with
| (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll))) ->
if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k
then let tannot = Base(([],item_t),Alias,[],pure_e,nob) in
@@ -1846,14 +1829,15 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
{d_env with alias_env = Envmap.insert (d_env.alias_env) (alias, (OneReg(reg,tannot)))} in
(AL_aux(AL_bit(reg_a,(E_aux(bit,(le,eannot)))), (l,tannot)), tannot,d_env)
else typ_error ll ("Alias bit lookup must be in the range of the vector in the register")
- | _ -> assert false)
+ | _ -> typ_error l ("Alias bit lookup must have a constant index"))
+ | _ -> typ_error l ("Alias bit lookup must refer to a register with type vector, found " ^ (t_to_string t)))
| AL_slice(reg_a,sl1,sl2) ->
let (reg,reg_a,reg_t,t) = check_reg reg_a in
let (E_aux(sl1,(le1,eannot1)),_,_,_,_,_) = check_exp envs None (new_t ()) sl1 in
let (E_aux(sl2,(le2,eannot2)),_,_,_,_,_) = check_exp envs None (new_t ()) sl2 in
(match t.t with
| Tapp("vector",[TA_nexp base;TA_nexp len;TA_ord order;TA_typ item_t]) ->
- match (base.nexp,len.nexp,order.order, sl1,sl2) with
+ (match (base.nexp,len.nexp,order.order, sl1,sl2) with
| (Nconst i,Nconst j,Oinc, E_lit (L_aux((L_num k), ll)),E_lit (L_aux((L_num k2), ll2))) ->
if (int_of_big_int i) <= k && ((int_of_big_int i) + (int_of_big_int j)) >= k2 && k < k2
then let t = {t = Tapp("vector",[TA_nexp (int_to_nexp k);TA_nexp (int_to_nexp ((k2-k) +1));
@@ -1864,7 +1848,8 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
(AL_aux(AL_slice(reg_a,(E_aux(sl1,(le1,eannot1))),(E_aux(sl2,(le2,eannot2)))),
(l,tannot)), tannot,d_env)
else typ_error ll ("Alias slices must be in the range of the vector in the register")
- | _ -> assert false)
+ | _ -> typ_error l ("Alias slices must have constant slices"))
+ | _ -> typ_error l ("Alias slices must point to a register with a vector type: found " ^ (t_to_string t)))
| AL_concat(reg1_a,reg2_a) ->
let (reg1,reg1_a,reg_t,t1) = check_reg reg1_a in
let (reg2,reg2_a,reg_t,t2) = check_reg reg2_a in
@@ -1875,7 +1860,9 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
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
- (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env))
+ (AL_aux (AL_concat(reg1_a,reg2_a), (l,tannot)), tannot, d_env)
+ | _ -> typ_error l
+ ("Alias concatentaion must connect two registers with vector type, found " ^ t_to_string t1 ^ " and " ^ t_to_string t2))
(*val check_def : envs -> tannot def -> (tannot def) envs_out*)
let check_def envs def =
diff --git a/src/type_internal.ml b/src/type_internal.ml
index b1a7ec9f..af1d31c7 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -97,6 +97,7 @@ type nexp_range =
| 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 *)
+ | Predicate of constraint_origin * nexp_range (* This will treat the inner constraint as holding in positive condcons positions*)
| CondCons of constraint_origin * nexp_range list * nexp_range list
| BranchCons of constraint_origin * nexp_range list
@@ -162,10 +163,10 @@ let get_c_loc = function
let debug_mode = ref true;;
let co_to_string = function
- | Patt l -> "Pattern "
- | Expr l -> "Expression "
- | Fun l -> "Function def "
- | Specc l -> "Specification "
+ | Patt l -> "Pattern " (*^ Reporting_basic.loc_to_string l *)
+ | Expr l -> "Expression " (*^ Reporting_basic.loc_to_string l *)
+ | Fun l -> "Function def " (*^ Reporting_basic.loc_to_string l *)
+ | Specc l -> "Specification " (*^ Reporting_basic.loc_to_string l *)
let rec t_to_string t =
match t.t with
@@ -194,6 +195,7 @@ and n_to_string n =
| Nconst i -> string_of_big_int i
| Npos_inf -> "infinity"
| Nneg_inf -> "-infinity"
+ | Ninexact -> "infinity - infinity"
| Nadd(n1,n2) -> "("^ (n_to_string n1) ^ " + " ^ (n_to_string n2) ^")"
| Nsub(n1,n2) -> "("^ (n_to_string n1) ^ " - " ^ (n_to_string n2) ^ ")"
| Nmult(n1,n2) -> "(" ^ (n_to_string n1) ^ " * " ^ (n_to_string n2) ^ ")"
@@ -208,8 +210,11 @@ and ef_to_string (Ast.BE_aux(b,l)) =
| Ast.BE_wreg -> "wreg"
| Ast.BE_rmem -> "rmem"
| Ast.BE_wmem -> "wmem"
+ | Ast.BE_wmv -> "wmv"
+ | Ast.BE_eamem -> "eamem"
| Ast.BE_barr -> "barr"
| Ast.BE_undef -> "undef"
+ | Ast.BE_depend -> "depend"
| Ast.BE_unspec-> "unspec"
| Ast.BE_nondet-> "nondet"
and efs_to_string es =
@@ -253,6 +258,7 @@ let rec constraint_to_string = function
"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
+ | Predicate(co,cs) -> "Pred(" ^ co_to_string co ^ ", " ^ constraint_to_string cs ^ ")"
| CondCons(co,pats,exps) ->
"CondCons(" ^ co_to_string co ^ ", [" ^ constraints_to_string pats ^ "], [" ^ constraints_to_string exps ^ "])"
| BranchCons(co,consts) ->
@@ -372,6 +378,8 @@ let rec compare_nexps n1 n2 =
(match compare_nexps n1 n2 with
| 0 -> compare_nexps n12 n22
| a -> a)
+ | Nsub _ , _ -> -1
+ | _ , Nsub _ -> 1
| Npow(n1,_),Npow(n2,_)-> compare_nexps n1 n2
| Npow _ , _ -> -1
| _ , Npow _ -> 1
@@ -383,6 +391,9 @@ let rec compare_nexps n1 n2 =
| Nneg _ , _ -> -1
| _ , Nneg _ -> 1
| Npos_inf , Npos_inf -> 0
+ | Npos_inf , _ -> -1
+ | _ , Npos_inf -> 1
+ | Ninexact , Ninexact -> 0
let rec pow_i i n =
@@ -394,7 +405,7 @@ let two_pow = pow_i 2
(* predicate to determine if pushing a constant in for addition or multiplication could change the form *)
let rec contains_const n =
match n.nexp with
- | Nvar _ | Nuvar _ | Npow _ | N2n _ | Npos_inf | Nneg_inf -> false
+ | Nvar _ | Nuvar _ | Npow _ | N2n _ | Npos_inf | Nneg_inf | Ninexact -> false
| Nconst _ -> true
| Nneg n -> contains_const n
| Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (contains_const n1) || (contains_const n2)
@@ -446,7 +457,7 @@ let negate n = match n.nexp with
let rec normalize_nexp n =
(*let _ = Printf.eprintf "Working on normalizing %s\n" (n_to_string n) in *)
match n.nexp with
- | Nconst _ | Nvar _ | Nuvar _ | Npos_inf | Nneg_inf -> n
+ | Nconst _ | Nvar _ | Nuvar _ | Npos_inf | Nneg_inf | Ninexact -> n
| Nneg n ->
let n',to_recur,add_neg = (match n.nexp with
| Nconst i -> negate n,false,false
@@ -579,8 +590,13 @@ let rec normalize_nexp n =
let n1',n2' = normalize_nexp n1, normalize_nexp n2 in
(match n1'.nexp,n2'.nexp with
| Nneg_inf,Nneg_inf -> {nexp = Npos_inf}
+ | Npos_inf, Nconst i | Nconst i, Npos_inf ->
+ if eq_big_int i zero then n_zero else {nexp = Npos_inf}
+ | Nneg_inf, Nconst i | Nconst i, Nneg_inf ->
+ if eq_big_int i zero then n_zero else {nexp = Nneg_inf}
| Nneg_inf, _ | _, Nneg_inf -> {nexp = Nneg_inf} (*TODO write a is_negative predicate*)
| Npos_inf, _ | _, Npos_inf -> {nexp = Npos_inf}
+ | Ninexact, _ | _, Ninexact -> {nexp = Ninexact}
| Nconst i1, Nconst i2 -> mk_c (mult_big_int i1 i2)
| Nconst i1, N2n(n,Some i2) | N2n(n,Some i2),Nconst i1 ->
if eq_big_int i1 two
@@ -650,6 +666,8 @@ let rec normalize_nexp n =
| _ -> mk_mult n2' n1')
| _ -> mk_mult (normalize_nexp (mk_mult n1' n21)) n22)
| Nmult _ ,Nmult(n21,n22) -> mk_mult (mk_mult n21 n1') (mk_mult n22 n1')
+ | Nsub _, _ | _, Nsub _ ->
+ let _ = Printf.eprintf "nsub case still around %s\n" (n_to_string n) in assert false
| Nneg _,_ | _,Nneg _ ->
let _ = Printf.eprintf "neg case still around %s\n" (n_to_string n) in assert false
(* If things are normal, neg should be gone. *)
@@ -852,7 +870,7 @@ and occurs_in_nexp n_box nuvar : bool =
let rec reduce_n_unifications n =
(*let _ = Printf.eprintf "reduce_n_unifications %s\n" (n_to_string n) in*)
(match n.nexp with
- | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> ()
+ | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact-> ()
| N2n(n1,_) | Npow(n1,_) | Nneg n1 -> reduce_n_unifications n1
| Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> reduce_n_unifications n1; reduce_n_unifications n2
| Nuvar nu ->
@@ -884,7 +902,7 @@ let equate_n (n_box : nexp) (n : nexp) : bool =
| Some({nexp = Nuvar(u)}) -> set_bottom_nsubst swap u new_bot
| Some(n_new) ->
if swap
- then set_bottom_nsubst false (match new_bot.nexp with | Nuvar u -> u) n_new
+ then set_bottom_nsubst false (match new_bot.nexp with | Nuvar u -> u | _ -> assert false) n_new
else if nexp_eq n_new new_bot then true
else false in
match n_box.nexp,n.nexp with
@@ -1004,6 +1022,11 @@ let rec contains_nuvar n cs = match cs with
(match contains_nuvar n b_cs with
| [] -> contains_nuvar n cs
| b -> BranchCons(so,b)::contains_nuvar n cs)
+ | (Predicate(so,c) as co)::cs ->
+ (match contains_nuvar n [c] with
+ | [] -> contains_nuvar n cs
+ | [c] -> co::contains_nuvar n cs
+ | _ -> assert false)
| _::cs -> contains_nuvar n cs
let rec refine_guarantees max_lt min_gt id cs =
@@ -1790,7 +1813,7 @@ and n_subst s_env n =
| Some(TA_nexp n1) -> n1
| _ -> mk_nv i)
| Nuvar _ -> new_n()
- | Nconst _ | Npos_inf | Nneg_inf -> n
+ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> n
| N2n(n1,None) -> mk_2n (n_subst s_env n1)
| N2n(n1,Some(i)) -> n
| Npow(n1,i) -> mk_pow (n_subst s_env n1) i
@@ -1826,6 +1849,7 @@ let rec cs_subst t_env cs =
| _ -> ());
InS(l,nexp,ns)::(cs_subst t_env cs)
| InS(l,n,ns)::cs -> InS(l,n_subst t_env n,ns)::(cs_subst t_env cs)
+ | Predicate(l, c)::cs -> Predicate(l, List.hd(cs_subst t_env [c]))::(cs_subst t_env cs)
| CondCons(l,cs_p,cs_e)::cs -> CondCons(l,cs_subst t_env cs_p,cs_subst t_env cs_e)::(cs_subst t_env cs)
| BranchCons(l,bs)::cs -> BranchCons(l,cs_subst t_env bs)::(cs_subst t_env cs)
@@ -1888,7 +1912,7 @@ and ta_remove_unifications s_env ta =
and n_remove_unifications s_env n =
(*let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in*)
match n.nexp with
- | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> s_env
+ | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> s_env
| Nuvar nu ->
let n' = match nu.nsubst with
| None -> n
@@ -1952,6 +1976,7 @@ and n_to_nexp n =
| Nconst i -> Nexp_constant (int_of_big_int i) (*TODO: Push more bigint around*)
| Npos_inf -> Nexp_constant max_int (*TODO: Not right*)
| Nneg_inf -> Nexp_constant min_int (* see above *)
+ | Ninexact -> Nexp_constant min_int (*and above*)
| 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)
| Nsub(n1,n2) -> Nexp_minus(n_to_nexp n1,n_to_nexp n2)
@@ -2021,6 +2046,12 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
| (BE_wmem,BE_wmem) -> 0
| (BE_wmem,_) -> -1
| (_,BE_wmem) -> 1
+ | (BE_wmv,BE_wmv) -> 0
+ | (BE_wmv, _ ) -> -1
+ | (_,BE_wmv) -> 1
+ | (BE_eamem,BE_eamem) -> 0
+ | (BE_eamem,_) -> -1
+ | (_,BE_eamem) -> 1
| (BE_barr,BE_barr) -> 0
| (BE_barr,_) -> 1
| (_,BE_barr) -> -1
@@ -2031,6 +2062,9 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
| (BE_unspec,_) -> -1
| (_,BE_unspec) -> 1
| (BE_nondet,BE_nondet) -> 0
+ | (BE_nondet,_) -> -1
+ | (_,BE_nondet) -> 1
+ | (BE_depend,BE_depend) -> 0
let effect_sort = List.sort compare_effect
@@ -2128,7 +2162,7 @@ let merge_bounds b1 b2 =
match compare_variable_range b1 b2 with
| -1 -> b1::(merge b1s (b2::b2s))
| 1 -> b2::(merge (b1::b1s) b2s)
- | 0 -> (match b1,b2 with
+ | _ -> (match b1,b2 with
| VR_eq(v,n1),VR_eq(_,n2) ->
if nexp_eq n1 n2 then b1 else VR_range(v,[Eq((Patt Unknown),n1,n2)])
| VR_eq(v,n),VR_range(_,ranges) |
@@ -2182,7 +2216,7 @@ and conforms_to_ta d_env loosely within_coercion spec actual =
| TA_eft s, TA_eft a -> conforms_to_e loosely s a
| _ -> false
and conforms_to_n loosely within_coercion op spec actual =
-(* let _ = Printf.printf "conforms_to_n called, evaluated loosely? %b, with coercion? %b with %s and %s\n"
+(* let _ = Printf.eprintf "conforms_to_n called, evaluated loosely? %b, with coercion? %b with %s and %s\n"
loosely within_coercion (n_to_string spec) (n_to_string actual) in*)
match (spec.nexp,actual.nexp,loosely,within_coercion) with
| (Nconst si,Nconst ai,_,_) -> op si ai
@@ -2236,9 +2270,13 @@ let rec type_consistent_internal co d_env enforce widen t1 cs1 t2 cs2 =
if i1 < i2
then ({t= Tapp("range",[TA_nexp a1;TA_nexp a2])},csp)
else ({t=Tapp ("range",[TA_nexp a2;TA_nexp a1])},csp)
+ (*| Nconst _, Nuvar _ | Nuvar _, Nconst _->
+ (t1, csp@[Eq(co,a1,a2)])*) (*TODO This is the correct constraint. However, without the proper support for In checks actually working, this will cause specs to not build*)
| _ -> let nu1,nu2 = new_n (),new_n () in
({t=Tapp("range",[TA_nexp nu1;TA_nexp nu2])},
csp@[LtEq(co,enforce,nu1,a1);LtEq(co,enforce,nu1,a2);LtEq(co,enforce,a1,nu2);LtEq(co,enforce,a2,nu2)]))
+ | Tapp("vector",[TA_nexp _; TA_nexp l1; ord; ty1]),Tapp("vector",[TA_nexp _; TA_nexp l2; ord2; ty2]) ->
+ (t2, Eq(co,l1,l2)::((type_arg_eq co d_env enforce widen ord ord2)@(type_arg_eq co d_env enforce widen ty1 ty2)))
| Tapp(id1,args1), Tapp(id2,args2) ->
(*let _ = Printf.eprintf "checking consistency of %s and %s\n" id1 id2 in*)
let la1,la2 = List.length args1, List.length args2 in
@@ -2543,7 +2581,7 @@ let rec in_constraint_env = function
let rec contains_var nu n =
match n.nexp with
| Nvar _ | Nuvar _ -> nexp_eq_check nu n
- | Nconst _ | Npos_inf | Nneg_inf -> false
+ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> false
| Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> contains_var nu n1 || contains_var nu n2
| Nneg n | N2n(n,_) | Npow(n,_) -> contains_var nu n
@@ -2557,7 +2595,7 @@ let rec contains_in_vars in_env n =
let rec subst_nuvars nu nc n =
match n.nexp with
- | Nconst _ | Nvar _ | Npos_inf | Nneg_inf -> n
+ | Nconst _ | Nvar _ | Npos_inf | Nneg_inf | Ninexact -> n
| Nuvar _ -> if nexp_eq_check nu n then nc else n
| Nmult(n1,n2) -> {nexp=Nmult(subst_nuvars nu nc n1,subst_nuvars nu nc n2)}
| Nadd(n1,n2) -> {nexp=Nadd(subst_nuvars nu nc n1,subst_nuvars nu nc n2)}
@@ -2568,7 +2606,7 @@ let rec subst_nuvars nu nc n =
let rec get_nuvars n =
match n.nexp with
- | Nconst _ | Nvar _ | Npos_inf | Nneg_inf -> []
+ | Nconst _ | Nvar _ | Npos_inf | Nneg_inf | Ninexact-> []
| Nuvar _ -> [n]
| Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (get_nuvars n1)@(get_nuvars n2)
| Nneg n | N2n(n,_) | Npow(n,_) -> get_nuvars n
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 7e786779..af2b99e0 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -97,6 +97,7 @@ type nexp_range =
| 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 *)
+ | Predicate of constraint_origin * nexp_range (* This will treat the inner constraint as holding in positive condcons positions : must be one of LtEq, Eq, or GtEq*)
| 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 *)
| BranchCons of constraint_origin * nexp_range list (* CondCons constraints from all branches of a conditional; list should be all CondCons *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-01 01:26:59 +0000