fixes, check in Shaked's sail_impl_base changes

1 files changed, 24 insertions, 1 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index f2de189f..9deda11c 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -9,6 +9,15 @@ type nn = natural
 type bitU = O | I | Undef
 
 
+let showBitU = function
+  | O -> "O"
+  | I -> "I"
+  | Undef -> "Undef"
+end
+
+instance (Show bitU)
+  let show = showBitU
+end
 
 (* element list * start * has increasing direction *)
 type vector 'a = Vector of list 'a * integer * bool
@@ -20,6 +29,14 @@ let rec nth xs (n : integer) =
   end
 
 
+let showVector (Vector elems start inc) =
+  "Vector " ^ show elems ^ " " ^ show start ^ " " ^ show inc
+
+instance forall 'a. Show 'a => (Show (vector 'a))
+  let show = showVector
+end
+
+
 let get_dir (Vector _ _ ord) = ord
 let get_start (Vector _ s _) = s
 let length (Vector bs _ _) = integerFromNat (length bs)
@@ -655,7 +672,13 @@ let byte_lifteds_of_bitv (Vector bits length is_inc) =
 
 val address_lifted_of_bitv : vector bitU -> address_lifted
 let address_lifted_of_bitv v =
-  Address_lifted (byte_lifteds_of_bitv v) Nothing
+  let byte_lifteds = byte_lifteds_of_bitv v in
+  let maybe_address_integer =
+    match (maybe_all (List.map byte_of_byte_lifted byte_lifteds)) with
+    | Just bs -> Just (integer_of_byte_list bs)
+    | _ -> Nothing
+    end in
+  Address_lifted byte_lifteds maybe_address_integer
 
 
 val bitvFromRegisterValue : register_value -> vector bitU