summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/arith.sail1
-rw-r--r--lib/flow.sail11
-rw-r--r--lib/smt.sail13
-rw-r--r--lib/vector_dec.sail2
-rw-r--r--src/ocaml_backend.ml1
-rw-r--r--src/rewrites.ml8
-rw-r--r--src/sail.ml7
-rw-r--r--src/type_check.ml1
-rw-r--r--test/c/cheri_capreg.sail8
-rw-r--r--test/c/config_register.sail5
-rw-r--r--test/typecheck/pass/phantom_num.sail8
-rw-r--r--test/typecheck/pass/return_simple3.sail8
-rw-r--r--test/typecheck/pass/tautology.sail1
-rw-r--r--test/typecheck/pass/vector_subrange_gen.sail3
14 files changed, 50 insertions, 27 deletions
diff --git a/lib/arith.sail b/lib/arith.sail
index b233048e..8825ac2f 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -102,6 +102,7 @@ val abs_int = {
smt : "abs",
ocaml: "abs_int",
lem: "abs_int",
+ c: "abs_int",
coq: "Z.abs"
} : (int, int) -> int
diff --git a/lib/flow.sail b/lib/flow.sail
index cb77f5b1..e6fe7fc0 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -50,4 +50,15 @@ overload operator < = {lt_int}
overload operator >= = {gteq_int}
overload operator > = {gt_int}
+/*
+
+when we have sizeof('n) where x : int('n), we can remove that sizeof
+by rewriting it to __size(x).
+
+*/
+
+function __id forall 'n. (x: int('n)) -> int('n) = x
+
+overload __size = {__id}
+
$endif
diff --git a/lib/smt.sail b/lib/smt.sail
index 6a5a1327..d886c127 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -4,36 +4,33 @@ $define _SMT
// see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
val div = {
- smt: "div",
ocaml: "quotient",
lem: "integerDiv",
c: "tdiv_int",
coq: "ediv_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm)) // {'o, 'o == div('n, 'm). atom('o)}
+} : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
overload operator / = {div}
val mod = {
- smt: "mod",
ocaml: "modulus",
lem: "integerMod",
c: "tmod_int",
coq: "emod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm))
+} : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
overload operator % = {mod}
-val abs_atom = {
- smt : "abs",
+val abs_int = {
ocaml: "abs_int",
lem: "abs_int",
c: "abs_int",
coq: "abs_with_eq"
-} : forall 'n. atom('n) -> atom(abs('n))
+} : forall 'n. int('n) -> int(abs('n))
$ifdef TEST
-let __smt_x : atom(div(4, 2)) = div(8, 4)
+let __smt_x : int(div(4, 2)) = div(8, 4)
$endif
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 4e4bad5a..166db243 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -166,4 +166,6 @@ val signed = {
_: "sint"
} : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
+overload __size = {length}
+
$endif
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 31c3e093..3f34c422 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -128,6 +128,7 @@ let ocaml_typ_id ctx = function
| id when Id.compare id (mk_id "list") = 0 -> string "list"
| id when Id.compare id (mk_id "bit") = 0 -> string "bit"
| id when Id.compare id (mk_id "int") = 0 -> string "Big_int.num"
+ | id when Id.compare id (mk_id "implicit") = 0 -> string "Big_int.num"
| id when Id.compare id (mk_id "nat") = 0 -> string "Big_int.num"
| id when Id.compare id (mk_id "bool") = 0 -> string "bool"
| id when Id.compare id (mk_id "unit") = 0 -> string "unit"
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 19294698..4b147aee 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5147,9 +5147,6 @@ let rewrite_defs_ocaml = [
("remove_numeral_pats", rewrite_defs_remove_numeral_pats);
("exp_lift_assign", rewrite_defs_exp_lift_assign);
("top_sort_defs", top_sort_defs);
- ("constraint", rewrite_constraint);
- ("trivial_sizeof", rewrite_trivial_sizeof);
- ("sizeof", rewrite_sizeof);
("simple_types", rewrite_simple_types);
("overload_cast", rewrite_overload_cast);
(* ("separate_numbs", rewrite_defs_separate_numbs) *)
@@ -5184,10 +5181,7 @@ let rewrite_defs_interpreter = [
("rewrite_undefined", rewrite_undefined_if_gen false);
("vector_concat_assignments", rewrite_vector_concat_assignments);
("tuple_assignments", rewrite_tuple_assignments);
- ("simple_assignments", rewrite_simple_assignments);
- ("constraint", rewrite_constraint);
- ("trivial_sizeof", rewrite_trivial_sizeof);
- ("sizeof", rewrite_sizeof);
+ ("simple_assignments", rewrite_simple_assignments)
]
let rewrite_check_annot =
diff --git a/src/sail.ml b/src/sail.ml
index fdf4f5b9..c63c3d19 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -64,7 +64,7 @@ let opt_print_c = ref false
let opt_print_latex = ref false
let opt_print_coq = ref false
let opt_print_cgen = ref false
-let opt_memo_z3 = ref false
+let opt_memo_z3 = ref true
let opt_sanity = ref false
let opt_includes_c = ref ([]:string list)
let opt_libs_lem = ref ([]:string list)
@@ -202,7 +202,10 @@ let options = Arg.align ([
"<filename>:<line>:<variable> to case split for monomorphisation");
( "-memo_z3",
Arg.Set opt_memo_z3,
- " memoize calls to z3, improving performance when typechecking repeatedly");
+ " memoize calls to z3, improving performance when typechecking repeatedly (default)");
+ ( "-no_memo_z3",
+ Arg.Clear opt_memo_z3,
+ " do not memoize calls to z3");
( "-memo",
Arg.Tuple [Arg.Set opt_memo_z3; Arg.Set C_backend.opt_memo_cache],
" memoize calls to z3, and intermediate compilation results");
diff --git a/src/type_check.ml b/src/type_check.ml
index 11fed096..82286491 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -473,6 +473,7 @@ end = struct
List.fold_left (fun m (name, kinds) -> Bindings.add (mk_id name) (kinds_typq kinds) m) Bindings.empty
[ ("range", [K_int; K_int]);
("atom", [K_int]);
+ ("implicit", [K_int]);
("vector", [K_int; K_order; K_type]);
("register", [K_type]);
("bit", []);
diff --git a/test/c/cheri_capreg.sail b/test/c/cheri_capreg.sail
index e8890a4a..a9480ab6 100644
--- a/test/c/cheri_capreg.sail
+++ b/test/c/cheri_capreg.sail
@@ -13,11 +13,11 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
val zeros_0 = "zeros" : forall 'n. int('n) -> bits('n)
-val zeros : forall 'n. unit -> bits('n)
-function zeros() = zeros_0('n)
+val zeros : forall 'n. (implicit('n), unit) -> bits('n)
+function zeros(n, _) = zeros_0(n)
-val ones : forall 'n, 'n >= 0 . unit -> bits('n)
-function ones() = replicate_bits (0b1,'n)
+val ones : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n)
+function ones(n, _) = replicate_bits(0b1, n)
val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
diff --git a/test/c/config_register.sail b/test/c/config_register.sail
index f4831ca5..8b41a3f4 100644
--- a/test/c/config_register.sail
+++ b/test/c/config_register.sail
@@ -2,8 +2,9 @@ default Order dec
$include <prelude.sail>
-function zeros forall 'n. (() : unit) -> bits('n) = {
- sail_zeros('n)
+val zeros : forall 'n, 'n >= 0. (implicit('n), unit) -> bits('n)
+function zeros(n, _) = {
+ sail_zeros(n)
}
register configuration R : bits(32) = zeros()
diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail
index 96663073..6be3533f 100644
--- a/test/typecheck/pass/phantom_num.sail
+++ b/test/typecheck/pass/phantom_num.sail
@@ -1,9 +1,13 @@
+function __id forall 'n. (x: int('n)) -> int('n) = x
+
+overload __size = {__id}
+
val gt_int = {ocaml: "gt", lem: "gt"}: (int, int) -> bool
overload operator > = {gt_int}
register z : int
-val test : forall ('n : Int). unit -> unit effect {wreg}
+val test : forall ('n : Int). (implicit('n), unit) -> unit effect {wreg}
-function test () = if 'n > 3 then z = 0 else z = 1
+function test(n, _) = if 'n > 3 then z = 0 else z = 1
diff --git a/test/typecheck/pass/return_simple3.sail b/test/typecheck/pass/return_simple3.sail
index fdda96dc..5653cb51 100644
--- a/test/typecheck/pass/return_simple3.sail
+++ b/test/typecheck/pass/return_simple3.sail
@@ -1,6 +1,10 @@
-val return_test : forall ('N : Int), 'N >= 10. range(10, 'N) -> range(10, 'N)
+function __id forall 'n. (x: int('n)) -> int('n) = x
-function return_test x = {
+overload __size = {__id}
+
+val return_test : forall ('N : Int), 'N >= 10. (implicit('N), range(10, 'N)) -> range(10, 'N)
+
+function return_test(N, x) = {
return(x);
'N
}
diff --git a/test/typecheck/pass/tautology.sail b/test/typecheck/pass/tautology.sail
index f1c8bade..43c7ddc9 100644
--- a/test/typecheck/pass/tautology.sail
+++ b/test/typecheck/pass/tautology.sail
@@ -1,3 +1,4 @@
+$include <flow.sail>
type implies('p: Bool, 'q: Bool) -> Bool = not('p) | 'q
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
index 50a93cff..b82d6c8c 100644
--- a/test/typecheck/pass/vector_subrange_gen.sail
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -1,3 +1,4 @@
+
val vector_access : forall ('l : Int) ('o : Order) ('a : Type), 'l >= 0.
(vector('l, 'o, 'a), range(0, 'l - 1)) -> 'a
@@ -11,6 +12,8 @@ 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)
+overload __size = {length}
+
default Order inc
val test : forall 'n 'm, 'n >= 5.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:08:46 +0000