move decode_error type back to Sail_impl_base for now

1 files changed, 42 insertions, 0 deletions

diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index bfa161c4..e932282c 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1356,3 +1356,45 @@ end
 
 type v_kind = Bitv | Bytev
 
+type decode_error = 
+  | Unsupported_instruction_error of instruction
+  | Not_an_instruction_error of opcode
+  | 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