Backport fixes to SMT generation from poly_mapping branch

2 files changed, 28 insertions, 3 deletions

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index c9892e4c..15daa545 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -38,6 +38,9 @@ let sign_extend bits len = exts_bits len bits
 val zeros : integer -> list bitU
 let zeros len = repeat [B0] len
 
+val ones : integer -> list bitU
+let ones len = repeat [B1] len
+
 val vector_truncate : list bitU -> integer -> list bitU
 let vector_truncate bs len = extz_bv len bs
 
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index f657803f..69bf0852 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -423,6 +423,26 @@ let char_of_nibble = function
   | _ -> Nothing
   end
 
+let nibble_of_char = function
+  | #'0' -> Just (B0, B0, B0, B0)
+  | #'1' -> Just (B0, B0, B0, B1)
+  | #'2' -> Just (B0, B0, B1, B0)
+  | #'3' -> Just (B0, B0, B1, B1)
+  | #'4' -> Just (B0, B1, B0, B0)
+  | #'5' -> Just (B0, B1, B0, B1)
+  | #'6' -> Just (B0, B1, B1, B0)
+  | #'7' -> Just (B0, B1, B1, B1)
+  | #'8' -> Just (B1, B0, B0, B0)
+  | #'9' -> Just (B1, B0, B0, B1)
+  | #'A' -> Just (B1, B0, B1, B0)
+  | #'B' -> Just (B1, B0, B1, B1)
+  | #'C' -> Just (B1, B1, B0, B0)
+  | #'D' -> Just (B1, B1, B0, B1)
+  | #'E' -> Just (B1, B1, B1, B0)
+  | #'F' -> Just (B1, B1, B1, B1)
+  | _ -> Nothing
+  end
+
 let rec hexstring_of_bits bs = match bs with
   | b1 :: b2 :: b3 :: b4 :: bs ->
      let n = char_of_nibble (b1, b2, b3, b4) in
@@ -436,12 +456,14 @@ let rec hexstring_of_bits bs = match bs with
   end
 declare {isabelle; hol} termination_argument hexstring_of_bits = automatic
 
-let show_bitlist bs =
+let show_bitlist_prefix c bs =
   match hexstring_of_bits bs with
-  | Just s -> toString (#'0' :: #'x' :: s)
-  | Nothing -> toString (#'0' :: #'b' :: map bitU_char bs)
+  | Just s -> toString (c :: #'x' :: s)
+  | Nothing -> toString (c :: #'b' :: map bitU_char bs)
   end
 
+let show_bitlist bs = show_bitlist_prefix #'0' bs
+
 (*** List operations *)
 
 let inline (^^) = append_list