diff options
25 files changed, 162 insertions, 61 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index a759162e..edddcdd3 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -721,7 +721,9 @@ let doc_exp_lem, doc_let_lem = | E_field((E_aux(_,(l,fannot)) as fexp),id) -> let ft = typ_of_annot (l,fannot) in (match fannot with - | Some(env, (Typ_aux (Typ_id tid, _)), _) when Env.is_record tid env -> + | Some(env, (Typ_aux (Typ_id tid, _)), _) + | Some(env, (Typ_aux (Typ_app (tid, _), _)), _) + when Env.is_record tid env -> let fname = if prefix_recordtype then (string (string_of_id tid ^ "_")) ^^ doc_id_lem id diff --git a/src/rewrites.ml b/src/rewrites.ml index 9a5d8410..4378c720 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2614,7 +2614,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let typ' = Typ_aux (Typ_tup [typ_of exp;typ_of vars], gen_loc l) in E_aux (E_tuple [exp;vars],swaptyp typ' annot) in - let mk_varstup l es = + let mk_varstup l env es = let exp_to_pat (E_aux (eaux, annot) as exp) = match eaux with | E_lit lit -> P_aux (P_lit lit, annot) @@ -2624,18 +2624,31 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = ("Failed to extract pattern from expression " ^ string_of_exp exp)) in match es with | [] -> - annot_exp (E_lit (mk_lit L_unit)) (gen_loc l) Env.empty unit_typ, - annot_pat P_wild (gen_loc l) Env.empty unit_typ + annot_exp (E_lit (mk_lit L_unit)) (gen_loc l) Env.empty unit_typ, [], [] | [e] -> - let e = infer_exp (env_of e) (strip_exp e) in - e, annot_pat (P_typ (typ_of e, exp_to_pat e)) l (env_of e) (typ_of e) + let e = infer_exp env (strip_exp e) in + let typ = typ_of e in + e, [annot_pat (P_typ (typ, exp_to_pat e)) l env typ], [typ_of e] | e :: _ -> - let infer_e e = infer_exp (env_of e) (strip_exp e) in + let infer_e e = infer_exp env (strip_exp e) in let es = List.map infer_e es in let pats = List.map exp_to_pat es in let typ = tuple_typ (List.map typ_of es) in - annot_exp (E_tuple es) l (env_of e) typ, - annot_pat (P_typ (typ, annot_pat (P_tup pats) l (env_of e) typ)) l (env_of e) typ in + annot_exp (E_tuple es) l env typ, pats, List.map typ_of es in + + let add_vars_pat overwrite l env pat vartyps varpats = + let typ, pat = match pat with + | P_aux (P_typ (typ, pat), _) -> typ, pat + | pat -> pat_typ_of pat, pat in + let typs, pats = + if overwrite then vartyps, varpats + else typ :: vartyps, pat :: varpats in + match typs, pats with + | [], [] -> annot_pat P_wild l env unit_typ + | [typ], [pat] -> annot_pat (P_typ (typ, pat)) l env typ + | _, _ -> + let tup_typ = tuple_typ typs in + annot_pat (P_typ (tup_typ, annot_pat (P_tup pats) l env typ)) l env tup_typ in let rewrite (E_aux (expaux,((el,_) as annot)) as full_exp) (P_aux (_,(pl,pannot)) as pat) = let env = env_of_annot annot in @@ -2654,7 +2667,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = expects. In (Lem) pretty-printing, this turned into an anonymous function and passed to foreach*. *) let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars exp4) in - let varstuple, varspat = mk_varstup el vars in + let varstuple, varpats, vartyps = mk_varstup el env vars in let varstyp = typ_of varstuple in let exp4 = rewrite_var_updates (add_vars overwrite exp4 varstuple) in let ord_exp, lower, upper = match destruct_range (typ_of exp1), destruct_range (typ_of exp2) with @@ -2673,13 +2686,11 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let lb = annot_letbind (lvar_pat, exp1) el env lvar_typ in let body = annot_exp (E_let (lb, exp4)) el env (typ_of exp4) in let v = annot_exp (E_app (mk_id "foreach", [exp1; exp2; exp3; ord_exp; varstuple; body])) el env (typ_of body) in - let pat = - if overwrite then varspat - else annot_pat (P_tup [pat; varspat]) pl env (typ_of v) in + let pat = add_vars_pat overwrite pl env pat vartyps varpats in Added_vars (v,pat) | E_loop(loop,cond,body) -> let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars body) in - let varstuple, varspat = mk_varstup el vars in + let varstuple, varpats, vartyps = mk_varstup el env vars in let varstyp = typ_of varstuple in (* let cond = rewrite_var_updates (add_vars false cond varstuple) in *) let body = rewrite_var_updates (add_vars overwrite body varstuple) in @@ -2689,9 +2700,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | Until -> "until" in let funcl = Id_aux (Id fname,gen_loc el) in let v = E_aux (E_app (funcl,[cond;varstuple;body]), (gen_loc el, bannot)) in - let pat = - if overwrite then varspat - else annot_pat (P_tup [pat; varspat]) pl env (typ_of v) in + let pat = add_vars_pat overwrite pl env pat vartyps varpats in Added_vars (v,pat) | E_if (c,e1,e2) -> let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) @@ -2699,7 +2708,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = if vars = [] then (Same_vars (E_aux (E_if (c,rewrite_var_updates e1,rewrite_var_updates e2),annot))) else - let varstuple, varspat = mk_varstup el vars in + let varstuple, varpats, vartyps = mk_varstup el env vars in let varstyp = typ_of varstuple in let e1 = rewrite_var_updates (add_vars overwrite e1 varstuple) in let e2 = rewrite_var_updates (add_vars overwrite e2 varstuple) in @@ -2708,9 +2717,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = let typ = typ_of e1 in let eff = union_eff_exps [e1;e2] in let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in - let pat = - if overwrite then varspat - else annot_pat (P_tup [pat; varspat]) pl env (typ_of v) in + let pat = add_vars_pat overwrite pl env pat vartyps varpats in Added_vars (v,pat) | E_case (e1,ps) -> (* after rewrite_defs_letbind_effects e1 needs no rewriting *) @@ -2727,7 +2734,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = Pat_aux (Pat_when (p,g,rewrite_var_updates e),a)) ps in Same_vars (E_aux (E_case (e1,ps),annot)) else - let varstuple, varspat = mk_varstup el vars in + let varstuple, varpats, vartyps = mk_varstup el env vars in let varstyp = typ_of varstuple in let rewrite_pexp (Pat_aux (pexp, (l, _))) = match pexp with | Pat_exp (pat, exp) -> @@ -2741,9 +2748,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) = | Pat_aux ((Pat_exp (_,first)|Pat_when (_,_,first)),_) :: _ -> typ_of first | _ -> unit_typ in let v = propagate_exp_effect (annot_exp (E_case (e1, List.map rewrite_pexp ps)) pl env typ) in - let pat = - if overwrite then varspat - else annot_pat (P_tup [pat; varspat]) pl env (typ_of v) in + let pat = add_vars_pat overwrite pl env pat vartyps varpats in Added_vars (v,pat) | E_assign (lexp,vexp) -> let mk_id_pat id = match Env.lookup_id id env with diff --git a/test/lem/run_tests.sh b/test/lem/run_tests.sh new file mode 100755 index 00000000..5d435950 --- /dev/null +++ b/test/lem/run_tests.sh @@ -0,0 +1,66 @@ +#!/usr/bin/env bash +set -e + +DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +SAILDIR="$DIR/../.." +TESTSDIR="$DIR/../typecheck/pass" + +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[0;33m' +NC='\033[0m' + +rm -f $DIR/tests.xml + +pass=0 +fail=0 + +XML="" + +function green { + (( pass += 1 )) + printf "$1: ${GREEN}$2${NC}\n" + XML+=" <testcase name=\"$1\"/>\n" +} + +function yellow { + (( fail += 1 )) + printf "$1: ${YELLOW}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function red { + (( fail += 1 )) + printf "$1: ${RED}$2${NC}\n" + XML+=" <testcase name=\"$1\">\n <error message=\"$2\">$2</error>\n </testcase>\n" +} + +function finish_suite { + printf "$1: Passed ${pass} out of $(( pass + fail ))\n\n" + XML=" <testsuite name=\"$1\" tests=\"$(( pass + fail ))\" failures=\"${fail}\" timestamp=\"$(date)\">\n$XML </testsuite>\n" + printf "$XML" >> $DIR/tests.xml + XML="" + pass=0 + fail=0 +} + +printf "<testsuites>\n" >> $DIR/tests.xml + +for i in `ls $TESTSDIR/ | grep sail`; +do + if $SAILDIR/sail -lem -lem_sequential -o out $TESTSDIR/$i &>/dev/null; + then + if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib out_embed_types_sequential.lem out_embed_sequential.lem &>/dev/null; + then + green "tested $i expecting pass" "pass" + else + yellow "tested $i expecting pass" "failed to typecheck generated Lem" + fi + else + red "tested $i expecting pass" "failed to generate Lem" + fi +done + +finish_suite "Expecting pass" + +printf "</testsuites>\n" >> $DIR/tests.xml diff --git a/test/run_tests.sh b/test/run_tests.sh index fc93929f..b3224aea 100755 --- a/test/run_tests.sh +++ b/test/run_tests.sh @@ -18,6 +18,12 @@ printf "******************************************\n\n" ./test/ocaml/run_tests.sh printf "******************************************\n" +printf "* Lem tests *\n" +printf "******************************************\n\n" + +./test/lem/run_tests.sh + +printf "******************************************\n" printf "* ARM spec tests *\n" printf "******************************************\n\n" diff --git a/test/typecheck/pass/arm_FPEXC1.sail b/test/typecheck/pass/arm_FPEXC1.sail index 078beb4a..d93143f0 100644 --- a/test/typecheck/pass/arm_FPEXC1.sail +++ b/test/typecheck/pass/arm_FPEXC1.sail @@ -1,11 +1,14 @@ default Order dec -val vector_access = {ocaml: "bitvector_access_dec", lem: "bitvector_access_dec"}: forall ('n : Int). +val vector_access = {ocaml: "access", lem: "access_vec_dec"}: forall ('n : Int). (vector('n, dec, bit), int) -> bit -val vector_subrange = {ocaml: "bitvector_subrange_dec", lem: "bitvector_subrange_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"}: forall ('n : Int) ('m : Int) ('o : Int), 'm >= 'o & 'o >= 0 & 'n >= 'm + 1. (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit) +val vector_update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec"} : forall 'n 'm 'o. + (vector('n, dec, bit), atom('m), atom('o), vector('m - ('o - 1), dec, bit)) -> vector('n, dec, bit) + register _FPEXC32_EL2 : vector(32, dec, bit) val set_FPEXC32_EL2 : vector(32, dec, bit) -> unit effect {wreg} diff --git a/test/typecheck/pass/atomcase.sail b/test/typecheck/pass/atomcase.sail index 2ed00a13..4e030a60 100644 --- a/test/typecheck/pass/atomcase.sail +++ b/test/typecheck/pass/atomcase.sail @@ -2,7 +2,7 @@ default Order dec infix 4 == -val eq_atom = {ocaml: "eq_atom", lem: "eq_atom"}: forall ('n : Int) ('m : Int). +val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> bool overload operator == = {eq_atom} diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail index 4ac0fec4..66fc0025 100644 --- a/test/typecheck/pass/case_simple_constraints.sail +++ b/test/typecheck/pass/case_simple_constraints.sail @@ -1,4 +1,4 @@ -val plus = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int). +val plus = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int). (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) val minus_ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n <= -10. diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 7d125d23..178f8003 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -8,9 +8,15 @@ register x : nat register y : nat -val eq_int : (int, int) -> bool +val eq_int = {lem: "eq"} : (int, int) -> bool +val eq_vec = {lem: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool -overload operator == = {eq_int} +overload operator == = {eq_int, eq_vec} + +val "and_bool" : (bool, bool) -> bool + +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n. + (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit) type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)} diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail index 95f9a854..47b26261 100644 --- a/test/typecheck/pass/flow_gt1.sail +++ b/test/typecheck/pass/flow_gt1.sail @@ -1,9 +1,9 @@ default Order inc -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail index d644ce40..3ea9d69b 100644 --- a/test/typecheck/pass/flow_gteq1.sail +++ b/test/typecheck/pass/flow_gteq1.sail @@ -1,9 +1,9 @@ default Order inc -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail index 569ec3aa..e29424be 100644 --- a/test/typecheck/pass/flow_lt1.sail +++ b/test/typecheck/pass/flow_lt1.sail @@ -1,9 +1,9 @@ default Order inc -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail index d5b5cfd0..2c1ad667 100644 --- a/test/typecheck/pass/flow_lt2.sail +++ b/test/typecheck/pass/flow_lt2.sail @@ -1,9 +1,9 @@ default Order inc -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail index 40c09c8e..afc620b6 100644 --- a/test/typecheck/pass/flow_lt_assign.sail +++ b/test/typecheck/pass/flow_lt_assign.sail @@ -1,9 +1,9 @@ default Order inc -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail index 90c4fb17..c61f93e2 100644 --- a/test/typecheck/pass/flow_lteq1.sail +++ b/test/typecheck/pass/flow_lteq1.sail @@ -1,9 +1,9 @@ default Order inc -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val sub_range = {ocaml: "sub", lem: "sub"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). diff --git a/test/typecheck/pass/foreach_var_updates.sail b/test/typecheck/pass/foreach_var_updates.sail index 19d491d0..7813cb16 100644 --- a/test/typecheck/pass/foreach_var_updates.sail +++ b/test/typecheck/pass/foreach_var_updates.sail @@ -1,8 +1,8 @@ -val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int +val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int overload operator + = {add_int} -val sub_int = {ocaml: "sub", lem: "sub"}: (int, int) -> int +val sub_int = {ocaml: "sub", lem: "integerMinus"}: (int, int) -> int overload operator - = {sub_int} diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail index e498cded..6763922a 100644 --- a/test/typecheck/pass/nzcv.sail +++ b/test/typecheck/pass/nzcv.sail @@ -1,5 +1,8 @@ default Order dec +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. + (vector('n, dec, bit), atom('m), atom('o)) -> vector('m - ('o - 1), dec, bit) + val test : vector(4, dec, bit) -> unit function test nzcv = { diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail index e1587ebc..94b40885 100644 --- a/test/typecheck/pass/patternrefinement.sail +++ b/test/typecheck/pass/patternrefinement.sail @@ -2,8 +2,8 @@ default Order dec infix 4 == -val extz = {ocaml: "extz", lem: "extz"}: forall ('n : Int) ('m : Int) ('ord : Order). - vector('n, 'ord, bit) -> vector('m, 'ord, bit) +val extz = {ocaml: "extz", lem: "extz_vec"}: forall ('n : Int) ('m : Int) ('ord : Order). + (atom('m), vector('n, 'ord, bit)) -> vector('m, 'ord, bit) val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order) ('a : Type). vector('m, 'ord, 'a) -> atom('m) @@ -11,7 +11,7 @@ val length = {ocaml: "length", lem: "length"}: forall ('m : Int) ('ord : Order) val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order). (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool -val eq_atom = {ocaml: "eq_atom", lem: "eq_atom"}: forall ('n : Int) ('m : Int). +val eq_atom = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> bool val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool @@ -22,6 +22,6 @@ val test : forall 'n, 'n in {32, 64}. vector('n, dec, bit) -> vector(64, dec, bit) function test v = match length(v) { - 32 => extz(v), + 32 => extz(64, v), 64 => v } diff --git a/test/typecheck/pass/procstate1.sail b/test/typecheck/pass/procstate1.sail index 726f9575..1d7e15b1 100644 --- a/test/typecheck/pass/procstate1.sail +++ b/test/typecheck/pass/procstate1.sail @@ -2,7 +2,7 @@ default Order dec infix 4 == -val operator == : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool +val operator == = {lem: "eq_vec"} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool struct ProcState ('n : Int) = { N : vector('n, dec, bit), diff --git a/test/typecheck/pass/vec_pat1.sail b/test/typecheck/pass/vec_pat1.sail index 9376b2a8..6de87a8c 100644 --- a/test/typecheck/pass/vec_pat1.sail +++ b/test/typecheck/pass/vec_pat1.sail @@ -3,12 +3,17 @@ default Order inc val bv_add = {ocaml: "add_vec", lem: "add_vec"}: forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> vector('n, inc, bit) -val vector_subrange = {ocaml: "bitvector_subrange_inc", lem: "bitvector_subrange_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"}: forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. (vector('l, inc, bit), atom('m), atom('o)) -> vector('o + 1 - 'm, inc, bit) -val bitvector_concat : forall ('m : Int) ('p : Int). +val bitvector_concat = {ocaml: "append", lem: "concat_vec"} : forall ('m : Int) ('p : Int). (vector('m, inc, bit), vector('p, inc, bit)) -> vector('m + 'p, inc, bit) +val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (vector('n, inc, bit), vector('n, inc, bit)) -> bool + +infix 4 == +overload operator == = {eq_vec} + overload operator + = {bv_add} overload append = {bitvector_concat} diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail index 8a1bfae4..d2e2da47 100644 --- a/test/typecheck/pass/vector_append.sail +++ b/test/typecheck/pass/vector_append.sail @@ -1,4 +1,4 @@ -val append = "bitvector_concat" : forall ('l1 : Int) ('l2 : Int) ('o : Order), 'l1 >= 0 & 'l2 >= 0. +val append = {ocaml: "append", lem: "concat_vec"} : forall ('l1 : Int) ('l2 : Int) ('o : Order), 'l1 >= 0 & 'l2 >= 0. (vector('l1, 'o, bit), vector('l2, 'o, bit)) -> vector('l1 + 'l2, 'o, bit) default Order inc diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail index 6ce5bf90..427f8dd7 100644 --- a/test/typecheck/pass/vector_append_gen.sail +++ b/test/typecheck/pass/vector_append_gen.sail @@ -1,4 +1,4 @@ -val vector_append = "bitvector_concat": forall 'l1 'l2 ('o : Order), 'l1 >= 0 & 'l2 >= 0. +val vector_append = {ocaml: "append", lem: "concat_vec"}: forall 'l1 'l2 ('o : Order), 'l1 >= 0 & 'l2 >= 0. (vector('l1, 'o, bit), vector('l2, 'o, bit)) -> vector('l1 + 'l2, 'o, bit) default Order inc diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail index aff87df4..50a93cff 100644 --- a/test/typecheck/pass/vector_subrange_gen.sail +++ b/test/typecheck/pass/vector_subrange_gen.sail @@ -4,11 +4,13 @@ val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0. val vector_append : forall ('l1 : Int) ('l2 : Int) ('o : Order) ('a : Type), 'l1 >= 0 & 'l2 >= 0. (vector('l1, 'o, 'a), vector('l2, 'o, 'a)) -> vector('l1 + 'l2, 'o, 'a) -val vector_subrange = "bitvector_subrange_inc" : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. +val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc"} : forall ('l : Int) ('m : Int) ('o : Int), 'l >= 0 & 'm <= 'o & 'o <= 'l. (vector('l, inc, bit), atom('m), atom('o)) -> vector('o - 'm + 1, inc, bit) val sub : forall ('n : Int) ('m : Int). (atom('n), atom('m)) -> atom('n - 'm) +val "length" : forall ('n : Int). vector('n, inc, bit) -> atom('n) + default Order inc val test : forall 'n 'm, 'n >= 5. diff --git a/test/typecheck/pass/while_MP.sail b/test/typecheck/pass/while_MP.sail index 60b5fb90..32d351e8 100644 --- a/test/typecheck/pass/while_MP.sail +++ b/test/typecheck/pass/while_MP.sail @@ -1,6 +1,6 @@ default Order dec -val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int +val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int overload operator + = {add_vec_int, add_range, add_int} diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail index 39ecdb2b..c148e6da 100644 --- a/test/typecheck/pass/while_PM.sail +++ b/test/typecheck/pass/while_PM.sail @@ -7,16 +7,19 @@ val lt_int = {ocaml: "lt", lem: "lt"}: (int, int) -> bool overload operator < = {lt_range_atom, lt_int} -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int +val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int overload operator + = {add_range, add_int} -val vector_access = "bitvector_access_dec" : forall ('l : Int), 'l >= 0. +val vector_access = {ocaml: "access", lem: "access_vec_dec"} : forall ('l : Int), 'l >= 0. (vector('l, dec, bit), int) -> bit +val vector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n. + (vector('n, dec, bit), int, bit) -> vector('n, dec, bit) + register GPR00 : vector(64, dec, bit) function test b : bit -> unit = { diff --git a/test/typecheck/pass/while_PP.sail b/test/typecheck/pass/while_PP.sail index 557bf963..d982241a 100644 --- a/test/typecheck/pass/while_PP.sail +++ b/test/typecheck/pass/while_PP.sail @@ -11,10 +11,10 @@ val mult_int : (int, int) -> int overload operator * = {mult_int} -val add_range = {ocaml: "add", lem: "add"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). +val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val add_int = {ocaml: "add", lem: "add"}: (int, int) -> int +val add_int = {ocaml: "add", lem: "integerAdd"}: (int, int) -> int overload operator + = {add_range, add_int} |