aarch64_small: fix interpreter primops in prelude

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)