fixes, check in Shaked's sail_impl_base changes

3 files changed, 111 insertions, 14 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
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 81d84dec..cb4c0414 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1363,5 +1363,55 @@ type decode_error =
   | Internal_error of string
 
 
+let decode_error_compare e1 e2 =
+  match (e1, e2) with
+  | (Unsupported_instruction_error i1, Unsupported_instruction_error i2)
+      -> defaultCompare i1 i2
+  | (Unsupported_instruction_error _, _) -> LT
+  | (_, Unsupported_instruction_error _) -> GT
+
+  | (Not_an_instruction_error o1, Not_an_instruction_error o2) -> defaultCompare o1 o2
+  | (Not_an_instruction_error _, _) -> LT
+  | (_, Not_an_instruction_error _) -> GT
+
+  | (Internal_error s1, Internal_error s2) -> compare s1 s2
+  (* | (Internal_error _, _) -> LT *)
+  (* | (_, Internal_error _) -> GT *)
+  end
+
+let decode_error_less e1 e2       = decode_error_compare e1 e2 =  LT
+let decode_error_less_eq e1 e2    = decode_error_compare e1 e2 <> GT
+let decode_error_greater e1 e2    = decode_error_compare e1 e2 =  GT
+let decode_error_greater_eq e1 e2 = decode_error_compare e1 e2 <> LT
+
+instance (Ord decode_error)
+  let compare = decode_error_compare
+  let (<)  = decode_error_less
+  let (<=) = decode_error_less_eq
+  let (>)  = decode_error_greater
+  let (>=) = decode_error_greater_eq
+end
 
+let decode_error_equal e1 e2 = (decode_error_compare e1 e2) = EQ
+let decode_error_inequal e1 e2 = not (decode_error_equal e1 e2)
 
+instance  (Eq decode_error)
+  let (=)  = decode_error_equal
+  let (<>) = decode_error_inequal
+end
+
+
+val outcome_s_descrEqual : forall 's 'a. Eq 'a => outcome_s 's 'a -> outcome_s 's 'a -> bool
+let outcome_s_descrEqual os1 os2 = match (fst os1,fst os2) with
+  | (Read_mem  descr1 _, Read_mem  descr2 _) -> descr1 = descr2
+  | (Write_ea  descr1 _, Write_ea  descr2 _) -> descr1 = descr2
+  | (Barrier   descr1 _, Barrier   descr2 _) -> descr1 = descr2
+  | (Read_reg  descr1 _, Read_reg  descr2 _) -> descr1 = descr2
+  | (Write_reg descr1 _, Write_reg descr2 _) -> descr1 = descr2
+  | (Escape    descr1 _, Escape    descr2 _) -> descr1 = descr2
+  | (Fail      descr1,   Fail      descr2)   -> descr1 = descr2
+  | (Internal  descr1 _, Internal  descr2 _)   -> descr1 = descr2
+  | (Done a1, Done a2) -> a1 = a2
+  | (Error e1, Error e2) -> e1 = e2
+  | (Footprint _, Footprint _) -> true
+end
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 244a7263..184d2a39 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2799,10 +2799,12 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
                           arrow;
                           doc_id_lem_ctor cid])
                   ar) ^/^
-                 ((separate space)
-                    [pipe;underscore;arrow;string "failwith";
-                     string_lit (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;
-                                         space;string "unexpected value"])]) ^/^
+                 let failmessage =
+                    (string_lit
+                       (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;space;string "unexpected value. ";]))
+                    ^^
+                      (string " ^ Interp.debug_print_value v") in
+                  ((separate space) [pipe;string "v";arrow;string "failwith";parens failmessage]) ^/^
                  string "end") in
          let toInterpValuePP =
            (prefix 2 1)
@@ -2863,17 +2865,39 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
              (separate space [string "let";fromInterpValueF;equals;string "function"])
              (
                ((separate_map (break 1))
-                  (fun cid ->
+                  (fun (cid) ->
                     (separate space)
                       [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
-                       arrow;
-                       doc_id_lem_ctor cid])
-                  enums) ^/^
-                 ((separate space)
-                    [pipe;underscore;arrow;string "failwith";
-                     string_lit (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;
-                                         space;string "unexpected value"])]) ^/^
-                 string "end") in
+                       arrow;doc_id_lem_ctor cid]
+                  )
+                  enums
+               ) ^/^
+                 (
+                   (align
+                      ((prefix 3 1)
+                         (separate space [pipe;string ("SI.V_lit (SIA.L_aux (SIA.L_num n) _)");arrow])
+                         (separate space [string "match";parens(string "natFromInteger n");string "with"] ^/^
+                            (
+                              ((separate_map (break 1))
+                                 (fun (cid,number) ->
+                                   (separate space)
+                                     [pipe;string (string_of_int number);arrow;doc_id_lem_ctor cid]
+                                 )
+                                 (List.combine enums (nats ((List.length enums) - 1)))
+                              ) ^/^ string "end"
+                            )
+                         )
+                      )
+                   )
+                 )
+                 ^/^
+                   let failmessage =
+                     (string_lit
+                        (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;space;string "unexpected value. ";]))
+                     ^^
+                       (string " ^ Interp.debug_print_value v") in
+                   ((separate space) [pipe;string "v";arrow;string "failwith";parens failmessage]) ^/^
+                     string "end") in
          let toInterpValuePP =
            (prefix 2 1)
              (separate space [string "let";toInterpValueF;equals;string "function"])