Support bitlist representation in Sail2_string

6 files changed, 12 insertions, 16 deletions

diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
index 7e3bb28a..a8bc6431 100644
--- a/aarch64/aarch64_extras.lem
+++ b/aarch64/aarch64_extras.lem
@@ -1,9 +1,9 @@
 open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators_bitlists
-open import Prompt_monad
-open import Prompt
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_bitlists
+open import Sail2_prompt_monad
+open import Sail2_prompt
 
 type ty512
 instance (Size ty512) let size = 512 end
diff --git a/mips/mips_extras.lem b/mips/mips_extras.lem
index 4e570a6f..2e07586c 100644
--- a/mips/mips_extras.lem
+++ b/mips/mips_extras.lem
@@ -77,7 +77,6 @@ let write_ram _ size _ addr data =
 
 let read_ram _ size _ addr = MEMr addr size
 
-let string_of_bits bs = string_of_bv (bits_of bs)
 let string_of_int = show
 
 let shift_bits_left v n =
@@ -113,7 +112,7 @@ val elf_entry : unit -> integer
 let elf_entry () = 0
 declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
 
-let print_bits msg bs = prerr_endline (msg ^ (string_of_bits bs))
+let print_bits msg bs = prerr_endline (msg ^ (string_of_bv bs))
 
 val get_time_ns : unit -> integer
 let get_time_ns () = 0
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index d10dddc9..412dcfc7 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -229,7 +229,7 @@ val DecStr : int -> string
 
 val HexStr : int -> string
 
-val BitStr = {ocaml: "string_of_bits", lem: "string_of_vec"} : forall 'n. bits('n) -> string
+val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
 
 val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
 
diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 7f1bcba5..3f8b7510 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -112,8 +112,8 @@ let int_of_vec_fail sign v = maybe_fail "int_of_vec" (int_of_vec_maybe sign v)
 let int_of_vec_oracle sign v = bools_of_bits_oracle v >>= (fun v -> return (int_of_bools sign v))
 let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v)
 
-val string_of_vec : list bitU -> string
-let string_of_vec = string_of_bv
+val string_of_bits : list bitU -> string
+let string_of_bits = string_of_bv
 
 val and_vec : list bitU -> list bitU -> list bitU
 val or_vec  : list bitU -> list bitU -> list bitU
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index fe319efc..1e4d63ba 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -117,8 +117,8 @@ let int_of_vec sign w =
 let int_of_vec_maybe sign w = Just (int_of_vec sign w)
 let int_of_vec_fail sign w = return (int_of_vec sign w)
 
-val string_of_vec : forall 'a. Size 'a => mword 'a -> string
-let string_of_vec = string_of_bv
+val string_of_bits : forall 'a. Size 'a => mword 'a -> string
+let string_of_bits = string_of_bv
 
 val and_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
 val or_vec  : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index 3374d800..d0e40ad4 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -4,7 +4,7 @@ open import List_extra
 open import String
 open import String_extra
 
-open import Sail2_operators_mwords
+open import Sail2_operators
 open import Sail2_values
 
 val string_sub : string -> ii -> ii -> string
@@ -162,6 +162,3 @@ let hex_bits_32_matches_prefix s =
      else
        Nothing
   end
-
-
-let string_of_bits = string_of_vec