separate decimal_string_of_bits from string_of_bits

3 files changed, 24 insertions, 0 deletions

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 186e0a09..bacf59e7 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -115,6 +115,9 @@ let int_of_vec sign v = maybe_failwith (int_of_vec_maybe sign v)
 val string_of_bits : list bitU -> string
 let string_of_bits = string_of_bv
 
+val decimal_string_of_bits : list bitU -> string
+let decimal_string_of_bits = decimal_string_of_bv
+
 val and_vec : list bitU -> list bitU -> list bitU
 val or_vec  : list bitU -> list bitU -> list bitU
 val xor_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 a7fb7c50..d47d9b40 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -120,6 +120,9 @@ let int_of_vec_fail sign w = return (int_of_vec sign w)
 val string_of_bits : forall 'a. Size 'a => mword 'a -> string
 let string_of_bits = string_of_bv
 
+val decimal_string_of_bits : forall 'a. Size 'a => mword 'a -> string
+let decimal_string_of_bits = decimal_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
 val xor_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> mword 'a
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index fd742fb1..8957f0dd 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -628,6 +628,24 @@ let exts_bv n v = exts_bits n (bits_of v)
 val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let string_of_bv v = show_bitlist (bits_of v)
 
+val int_of_bit : bitU -> integer
+let int_of_bit b =
+  match b with
+  | B0 -> 0
+  | B1 -> 1
+  | _ -> failwith "int_of_bit saw unknown"
+  end
+
+val decimal_string_of_bv : forall 'a. Bitvector 'a => 'a -> string
+let decimal_string_of_bv bv =
+  let place_values =
+    List.mapi
+      (fun i b -> (int_of_bit b) * (2 ** i))
+      (List.reverse (bits_of bv))
+  in
+  let sum = List.foldl (+) 0 place_values in
+  show sum
+
 (*** Bytes and addresses *)
 
 type memory_byte = list bitU