Merge remote-tracking branch 'origin/experiments' into interactive

1 files changed, 74 insertions, 18 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 98ac2522..231b9c8e 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -156,6 +156,9 @@ let inline (|.) x y = bitwise_or_bit (x,y)
 val (+.) : bitU -> bitU -> bitU
 let inline (+.) x y = bitwise_xor_bit (x,y)
 
+
+(*** Bit lists ***)
+
 val to_bin_aux : natural -> list bitU
 let rec to_bin_aux x =
   if x = 0 then []
@@ -175,14 +178,36 @@ let of_bin bits =
       (0,0) bits in
   sum
 
-val bitlist_to_integer : list bitU -> integer
-let bitlist_to_integer bs = integerFromNatural (of_bin bs)
+let bitwise_not_bitlist = List.map bitwise_not_bit
 
-val pad_zero : list bitU -> integer -> list bitU
-let rec pad_zero bits n =
-  if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
+val bitlist_to_unsigned : list bitU -> integer
+let bitlist_to_unsigned bs = integerFromNatural (of_bin bs)
 
-let bitwise_not_bitlist = List.map bitwise_not_bit
+val bitlist_to_signed : list bitU -> integer
+let bitlist_to_signed bits =
+  match bits with
+  | B1 :: _ -> 0 - (1 + (bitlist_to_unsigned (bitwise_not_bitlist bits)))
+  | B0 :: _ -> bitlist_to_unsigned bits
+  | BU :: _ -> failwith "bitlist_to_signed applied to list with undefined bits"
+  | [] -> failwith "bitlist_to_signed applied to empty list"
+  end
+
+val pad_bitlist : bitU -> list bitU -> integer -> list bitU
+let rec pad_bitlist b bits n =
+  if n <= 0 then bits else pad_bitlist b (b :: bits) (n - 1)
+
+let ext_bl pad (len, bits) =
+  let longer = len - (integerFromNat (List.length bits)) in
+  if longer < 0 then drop (natFromInteger (abs (longer))) bits
+  else pad_bitlist pad bits longer
+
+let extz_bl (len, bits) = ext_bl B0 (len, bits)
+let exts_bl (len, bits) =
+  match bits with
+  | BU :: _ -> failwith "exts_bl: undefined bit"
+  | B1 :: _ -> ext_bl B1 (len, bits)
+  | _ -> ext_bl B0 (len, bits)
+  end
 
 let rec add_one_bit_ignore_overflow_aux bits = match bits with
   | [] -> []
@@ -194,19 +219,50 @@ end
 let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
 
-let bits_of_nat ((len : integer),(n : natural)) =
-  let bits = to_bin n in
-  let len_bits = integerFromNat (List.length bits) in
-  let longer = len - len_bits in
-  if longer < 0 then drop (natFromInteger (abs (longer))) bits
-  else pad_zero bits longer
+let int_to_bin n =
+  let bits_abs = B0 :: to_bin (naturalFromInteger (abs n)) in
+  if n >= (0 : integer) then bits_abs
+  else add_one_bit_ignore_overflow (bitwise_not_bitlist bits_abs)
+
+let bits_of_nat ((len : integer),(n : natural)) = extz_bl (len, to_bin n)
+let bits_of_int ((len : integer),(n : integer)) = exts_bl (len, int_to_bin n)
+
+let nibble_of_bits = function
+  | (B0, B0, B0, B0) -> Just #'0'
+  | (B0, B0, B0, B1) -> Just #'1'
+  | (B0, B0, B1, B0) -> Just #'2'
+  | (B0, B0, B1, B1) -> Just #'3'
+  | (B0, B1, B0, B0) -> Just #'4'
+  | (B0, B1, B0, B1) -> Just #'5'
+  | (B0, B1, B1, B0) -> Just #'6'
+  | (B0, B1, B1, B1) -> Just #'7'
+  | (B1, B0, B0, B0) -> Just #'8'
+  | (B1, B0, B0, B1) -> Just #'9'
+  | (B1, B0, B1, B0) -> Just #'A'
+  | (B1, B0, B1, B1) -> Just #'B'
+  | (B1, B1, B0, B0) -> Just #'C'
+  | (B1, B1, B0, B1) -> Just #'D'
+  | (B1, B1, B1, B0) -> Just #'E'
+  | (B1, B1, B1, B1) -> Just #'F'
+  | _ -> Nothing
+  end
 
-let bits_of_int ((len : integer),(n : integer)) =
-  let bits = bits_of_nat (len, naturalFromInteger (abs n)) in
-  if n > (0 : integer)
-  then bits
-  else (add_one_bit_ignore_overflow (bitwise_not_bitlist bits))
+let rec hexstring_of_bits bs = match bs with
+  | b1 :: b2 :: b3 :: b4 :: bs ->
+     let n = nibble_of_bits (b1, b2, b3, b4) in
+     let s = hexstring_of_bits bs in
+     match (n, s) with
+     | (Just n, Just s) -> Just (n :: s)
+     | _ -> Nothing
+     end
+  | _ -> Nothing
+  end
 
+let show_bitlist bs =
+  match hexstring_of_bits bs with
+  | Just s -> toString (#'0' :: #'x' :: s)
+  | Nothing -> show bs
+  end
 
 (*** Vectors *)
 
@@ -348,7 +404,7 @@ end
 instance forall 'a. BitU 'a => (Bitvector (list 'a))
   let bits_of v = List.map to_bitU v
   let of_bits v = List.map of_bitU v
-  let unsigned v = bitlist_to_integer (List.map to_bitU v)
+  let unsigned v = bitlist_to_unsigned (List.map to_bitU v)
   let get_bit is_inc start v n = to_bitU (access_aux is_inc start v n)
   let set_bit is_inc start v n b = update_aux is_inc start v n n [of_bitU b]
   let get_bits is_inc start v i j = List.map to_bitU (slice_aux is_inc start v i j)