diff options
Diffstat (limited to 'test/mono/times8div8.sail')
| -rw-r--r-- | test/mono/times8div8.sail | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/test/mono/times8div8.sail b/test/mono/times8div8.sail index 1deb571f..fa8bcb20 100644 --- a/test/mono/times8div8.sail +++ b/test/mono/times8div8.sail @@ -1,24 +1,10 @@ -$include <smt.sail> -$include <flow.sail> -$include <arith.sail> default Order dec -type bits ('n : Int) = bitvector('n, dec) -val operator & = "and_bool" : (bool, bool) -> bool -val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -overload operator == = {eq_int, eq_vec} -val mult_int = {ocaml: "mult", lem: "integerMult"} : (int, int) -> int -overload operator * = {mult_range, mult_int, mult_real} -val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm) -overload operator < = {lt_atom, lt_int} +$include <prelude.sail> +$include <smt.sail> val "extz_vec" : forall 'n 'm. (atom('m),bitvector('n, dec)) -> bitvector('m, dec) effect pure val extzv : forall 'n 'm. (implicit('m), bitvector('n, dec)) -> bitvector('m, dec) effect pure function extzv(m,v) = extz_vec(m,v) -val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). - (bits('n), bits('m)) -> bits('n + 'm) -overload append = {bitvector_concat} val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure -val bitvector_length = "length" : forall 'n. bits('n) -> atom('n) -overload length = {bitvector_length} val cast ex_int : int -> {'n, true. atom('n)} function ex_int 'n = n val quotient = {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (int, int) -> int |