Lean: Fix bitvector printing

rems-project · Feb 17, 2025 · 73678dc · 73678dc
1 parent be5a801
commit 73678dc
Show file tree

Hide file tree

Showing 27 changed files with 31 additions and 32 deletions.
diff --git a/lib/string.sail b/lib/string.sail
@@ -72,7 +72,7 @@ val hex_str = pure "hex_str" : int -> string
 val hex_str_upper = pure "hex_str_upper" : int -> string
 
 val bits_str = pure {
-   lean: "BitVec.string_of_bits",
+   lean: "BitVec.toFormatted",
    _: "string_of_bits"} : forall 'n. bitvector('n, dec) -> string
 
 val concat_str_bits : forall 'n. (string, bitvector('n, dec)) -> string

diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
@@ -44,11 +44,14 @@ def append' (x : BitVec n) (y : BitVec m) {mn}
     (hmn : mn = n + m := by (conv => rhs; dsimp); try rfl) : BitVec mn :=
   hmn ▸ x.append y
 
-def string_of_bits {w : Nat} (x : BitVec w) : String :=
+def toBin {w : Nat} (x : BitVec w) : String :=
+  List.asString (List.map (fun c => if c then '1' else '0') (List.ofFn (BitVec.getMsb' x)))
+
+def toFormatted {w : Nat} (x : BitVec w) : String :=
   if (length x % 4) == 0 then
     s!"0x{String.toUpper (BitVec.toHex x)}"
   else
-    s!"0b{toString x}"
+    s!"0b{BitVec.toBin x}"
 
 instance : Coe (BitVec (1 * n)) (BitVec n) where
   coe x := x.cast (by simp)
@@ -309,7 +312,7 @@ def print_int_effect (str : String) (n : Int) : PreSailM RegisterType c ue Unit
   print_effect s!"{str}{n}\n"
 
 def print_bits_effect {w : Nat} (str : String) (x : BitVec w) : PreSailM RegisterType c ue Unit :=
-  print_effect s!"{str}{BitVec.string_of_bits x}\n"
+  print_effect s!"{str}{BitVec.toFormatted x}\n"
 
 def print_endline_effect (str : String) : PreSailM RegisterType c ue Unit :=
   print_effect s!"{str}\n"

diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean
@@ -575,7 +575,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/append.expected.lean b/test/lean/append.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean
@@ -97,7 +97,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/enum.expected.lean b/test/lean/enum.expected.lean
@@ -89,7 +89,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/errors.expected.lean b/test/lean/errors.expected.lean
@@ -95,7 +95,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/extern_bitvec.expected.lean b/test/lean/extern_bitvec.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/implicit.expected.lean b/test/lean/implicit.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean
@@ -99,7 +99,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/let.expected.lean b/test/lean/let.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/loop.expected.lean b/test/lean/loop.expected.lean
@@ -95,7 +95,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/mapping.expected.lean b/test/lean/mapping.expected.lean
@@ -89,7 +89,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean
@@ -104,7 +104,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/match_bv.expected.lean b/test/lean/match_bv.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/option.expected.lean b/test/lean/option.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/range.expected.lean b/test/lean/range.expected.lean
@@ -84,7 +84,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/register_vector.expected.lean b/test/lean/register_vector.expected.lean
@@ -159,7 +159,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/registers.expected.lean b/test/lean/registers.expected.lean
@@ -113,7 +113,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/riscv_duopod.expected.lean b/test/lean/riscv_duopod.expected.lean
@@ -121,7 +121,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/run_tests.py b/test/lean/run_tests.py
@@ -31,15 +31,13 @@
     'pow2_var',
     'large_bitvector',
     'exn_hello_world',
-    'struct',
     'poly_union_rev',
     'match_bind',
     'rev_bits_in_byte',
     'foreach_none',
     'all_even_vector_length',
     'outcome_impl',
     'lib_valid_hex_bits',
-    'string_of_bits2',
     'tuple_conversion',
     'pow2',
     'primop',
@@ -63,7 +61,6 @@
     'rv_format2',
     'try_return',
     'bitvector_update2',
-    'poly_mapping2',
     'real',
     'inc_tests',
     'poly_outcome',
@@ -98,7 +95,6 @@
     'nexp_simp_euclidian',
     'config_register_ones',
     'toplevel_tyvar',
-    'pattern_concat_nest',
     'ediv',
     'ediv_from_tdiv',
     'int_struct',

diff --git a/test/lean/struct.expected.lean b/test/lean/struct.expected.lean
@@ -101,7 +101,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/struct_of_enum.expected.lean b/test/lean/struct_of_enum.expected.lean
@@ -93,7 +93,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/typedef.expected.lean b/test/lean/typedef.expected.lean
@@ -92,7 +92,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=

diff --git a/test/lean/typquant.expected.lean b/test/lean/typquant.expected.lean
@@ -90,7 +90,7 @@ def is_some (opt : (Option k_a)) : Bool :=
 
 /-- Type quantifiers: k_n : Int -/
 def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
-  (HAppend.hAppend str (BitVec.string_of_bits x))
+  (HAppend.hAppend str (BitVec.toFormatted x))
 
 /-- Type quantifiers: x : Int -/
 def concat_str_dec (str : String) (x : Int) : String :=