Add lean support for hex_str

Add lean support for hex_str_upper

Add handling of negative integers for hex_str and hex_str_upper

Remove hex_str_negative from skip_selftests

This runs the Sail unit test pertaining to hex_str.

Fix capitalized 0X -> 0x for toHexUpper

Fix toHexUpper so as not to capitalize the 'x'

lib/string.sail

@@ -67,9 +67,9 @@ val dec_str = pure {
   lean: "Int.repr",
   _: "dec_str"} : int -> string
 
-val hex_str = pure "hex_str" : int -> string
+val hex_str = pure { lean: "Int.toHex", _: "hex_str" } : int -> string
 
-val hex_str_upper = pure "hex_str_upper" : int -> string
+val hex_str_upper = pure { lean: "Int.toHexUpper", _: "hex_str_upper"} : int -> string
 
 val bits_str = pure {
    lean: "BitVec.toFormatted",

src/sail_lean_backend/Sail/Sail.lean

@@ -454,6 +454,14 @@ def iterate {α : Sort u} (op : α → α) : Nat → α → α
   | 0, a => a
   | Nat.succ k, a => iterate op k (op a)
 
+def toHex (n : Nat) : String :=
+  have nbv : BitVec (Nat.log2 n + 1) := BitVec.ofNat _ n
+  "0x" ++ nbv.toHex
+
+def toHexUpper (n : Nat) : String :=
+  have nbv : BitVec (Nat.log2 n + 1) := BitVec.ofNat _ n
+  "0x" ++ nbv.toHex.toUpper
+
 end Nat
 
 namespace Int
@@ -470,6 +478,17 @@ def shiftr (a : Int) (n : Int) : Int :=
   | Int.ofNat n => Sail.Nat.iterate (fun x => x / 2) n a
   | Int.negSucc n => Sail.Nat.iterate (fun x => x * 2) (n+1) a
 
+
+def toHex (i : Int) : String :=
+  match i with
+  | Int.ofNat n => Nat.toHex n
+  | Int.negSucc n => "-" ++ Nat.toHex (n+1)
+
+def toHexUpper (i : Int) : String :=
+  match i with
+  | Int.ofNat n => Nat.toHexUpper n
+  | Int.negSucc n => "-" ++ Nat.toHexUpper (n+1)
+
 end Int
 
 def get_slice_int (len n lo : Nat) : BitVec len :=

test/lean/extern.expected.lean

@@ -265,6 +265,12 @@ def extern_concat_str (_ : Unit) : String :=
 def extern_n_leading_spaces (_ : Unit) : Nat :=
   (String.leadingSpaces "   Belated Hello world!")
 
+def extern_hex_str (_ : Unit) : String :=
+  (Int.toHex 123)
+
+def extern_hex_str_upper (_ : Unit) : String :=
+  (Int.toHexUpper 123)
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/extern.sail

@@ -169,3 +169,12 @@ function extern_n_leading_spaces() -> nat = {
   return n_leading_spaces("   Belated Hello world!")
 }
 
+/* Testing vector.sail */
+
+function extern_hex_str() -> string = {
+  return hex_str(123)
+}
+
+function extern_hex_str_upper() -> string = {
+  return hex_str_upper(123)
+}

test/lean/run_tests.py

@@ -62,7 +62,6 @@
     'list_torture',
     'option_nest',
     'string_literal_type',
-    'hex_str_negative',
     'cheri_capreg',
     'loop_exception',
     'issue429',