diff options
| -rw-r--r-- | aarch64_small/prelude.sail | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail index f97c84a6..55d7c653 100644 --- a/aarch64_small/prelude.sail +++ b/aarch64_small/prelude.sail @@ -20,7 +20,7 @@ $include <flow.sail> $include <arith.sail> $include <option.sail> $include <vector_dec.sail> - +$include <regfp.sail> infix 7 >> infix 7 << @@ -104,16 +104,16 @@ function neq_anything (x, y) = not_bool(x == y) overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} -val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. +val add_int = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n), int) -> bits('n) overload operator + = {add_int, add_vec, add_vec_int} -val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. +val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", - lem: "integerMinus", coq: "sub_nat", c: "sub_nat"} + interpreter: "sub_nat", lem: "integerMinus", coq: "sub_nat", c: "sub_nat"} : (nat, nat) -> nat val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) @@ -124,9 +124,9 @@ overload operator - = {sub_int, sub_vec, sub_vec_int} /* function reg_index x = unsigned(x) */ -val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : +val quotient_nat = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : forall 'M 'N, 'M >= 0 & 'N >= 0. (int('M), int('N)) -> int(div('M,'N)) -val quotient = {ocaml: "quotient", lem: "integerDiv"} : +val quotient = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : forall 'M 'N. (int('M), int('N)) -> int(div('M,'N)) overload quot = {quotient_nat, quotient} @@ -142,13 +142,13 @@ function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int +val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int overload operator ^ = {xor_vec, int_power, concat_str} val mask : forall 'l 'm, 'l >= 0 & 'm >= 0. (implicit('l), bits('m)) -> bits('l) - +function mask(len, bv) = sail_mask(len, bv) overload operator % = {emod_int} overload operator / = {ediv_int} @@ -165,4 +165,4 @@ function error(message) = { type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. int('O)} -val appendL : forall ('a:Type). (list('a),list('a)) -> list('a) +val appendL = {ocaml: "append", interpreter: "append_list", lem: "append_list"} : forall ('a:Type). (list('a),list('a)) -> list('a) |