1 files changed, 38 insertions, 0 deletions
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 69bf0852..7bd950d7 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -464,6 +464,44 @@ let show_bitlist_prefix c bs =
 
 let show_bitlist bs = show_bitlist_prefix #'0' bs
 
+val hex_char : natural -> char
+
+let hex_char n =
+  match n with
+  | 0 -> #'0'
+  | 1 -> #'1'
+  | 2 -> #'2'
+  | 3 -> #'3'
+  | 4 -> #'4'
+  | 5 -> #'5'
+  | 6 -> #'6'
+  | 7 -> #'7'
+  | 8 -> #'8'
+  | 9 -> #'9'
+  | 10 -> #'A'
+  | 11 -> #'B'
+  | 12 -> #'C'
+  | 13 -> #'D'
+  | 14 -> #'E'
+  | 15 -> #'F'
+  | _ -> failwith "hex_char: not a hexadecimal digit"
+  end
+
+val hex_str_aux : natural -> list char -> list char
+
+let rec hex_str_aux n acc =
+  if n = 0 then acc else
+  hex_str_aux (n div 16) (hex_char (n mod 16) :: acc)
+
+declare {isabelle} termination_argument hex_str_aux = automatic
+
+val hex_str : integer -> string
+
+let hex_str i =
+  if i < 0 then failwith "hex_str: negative" else
+  if i = 0 then "0x0" else
+  "0x" ^ toString (hex_str_aux (naturalFromInteger (abs i)) [])
+
 (*** List operations *)
 
 let inline (^^) = append_list