Add wrappers around Lem operators using bitvector type class

Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.

2 files changed, 18 insertions, 8 deletions

diff --git a/aarch64/aarch64_extras_embed_sequential.lem b/aarch64/aarch64_extras_embed_sequential.lem
index a9e2e9e3..4f9e0fe3 100644
--- a/aarch64/aarch64_extras_embed_sequential.lem
+++ b/aarch64/aarch64_extras_embed_sequential.lem
@@ -1,10 +1,9 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
-open import Sail_operators
+open import Sail_operators_bitlists
 open import State
 
-
 type ty2048
 instance (Size ty2048) let size = 2048 end
 declare isabelle target_rep type ty2048 = `2048`
@@ -20,12 +19,16 @@ val putchar : integer -> unit
 let putchar _ = ()
 declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))
 
-let inline uint = unsigned
-let inline sint = signed
+val uint : list bitU -> integer
+let uint = unsigned
+val sint : list bitU -> integer
+let sint = signed
 
+val slice : list bitU -> integer -> integer -> list bitU
 let slice v lo len =
   subrange_vec_dec v (lo + len - 1) lo
 
+val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
 let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
   update_subrange_vec_dec out (n + slice_len - 1) n v
 
@@ -35,8 +38,10 @@ let get_slice_int_bl len n lo =
   let bits = bits_of_int (hi + 1) n in
   get_bits false bits hi lo
 
+val get_slice_int : integer -> integer -> integer -> list bitU
 let get_slice_int len n lo = of_bits (get_slice_int_bl len n lo)
 
+val set_slice_int : integer -> integer -> integer -> list bitU -> integer
 let set_slice_int len n lo v =
   let hi = lo + len - 1 in
   let bits = bitlist_of_int n in
@@ -48,7 +53,9 @@ let ext_slice signed v i j =
   let len = length v in
   let bits = get_bits false (bits_of v) i j in
   of_bits (if signed then exts_bits len bits else extz_bits len bits)
+val exts_slice : list bitU -> integer -> integer -> list bitU
 let exts_slice v i j = ext_slice true v i j
+val extz_slice : list bitU -> integer -> integer -> list bitU
 let extz_slice v i j = ext_slice false v i j
 
 val shr_int : ii -> ii -> ii
@@ -90,6 +97,7 @@ let hexstring_to_bits s =
   | _ -> failwith "hexstring_to_bits called with unexpected string"
   end
 
+val hex_slice : string -> integer -> integer -> list bitU
 let hex_slice v len lo =
   let hi = len + lo - 1 in
   let bits = extz_bits (len + lo) (hexstring_to_bits v) in
@@ -101,7 +109,9 @@ let undefined_string () = ""
 let undefined_unit () = ()
 let undefined_int () = (0:ii)
 let undefined_bool () = false
+val undefined_vector : forall 'a. integer -> 'a -> list 'a
 let undefined_vector len u = repeat [u] len
+val undefined_bitvector : integer -> list bitU
 let undefined_bitvector len = duplicate B0 len
 let undefined_bits len = undefined_bitvector len
 let undefined_bit () = B0
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 8851b7aa..a09209d6 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -87,17 +87,17 @@ function neq_anything (x, y) = not_bool(x == y)
 
 overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
 
-val builtin_and_vec = {ocaml: "and_vec", lem: "Sail_operators.and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_and_vec = {ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val and_vec = {lem: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function and_vec (xs, ys) = builtin_and_vec(xs, ys)
 
 overload operator & = {and_bool, and_vec}
 
-val builtin_or_vec = {ocaml: "or_vec", lem: "Sail_operators.or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val builtin_or_vec = {ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
 
-val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
+val or_vec = {lem: "or_vec"}: forall 'n. (bits('n), bits('n)) -> bits('n)
 
 function or_vec (xs, ys) = builtin_or_vec(xs, ys)