diff options
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 65ae87c2..3886f919 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -110,7 +110,7 @@ type address = Address of list byte (* of length 8 *) * integer type opcode = Opcode of list byte (* of length 4 *) (** typeclass instantiations *) - + let ~{ocaml} bitCompare (b1:bit) (b2:bit) = match (b1,b2) with | (Bitc_zero, Bitc_zero) -> EQ @@ -214,6 +214,36 @@ instance (Ord byte) let (>=) = byteGreaterEq end + + + + +let ~{ocaml} opcodeCompare (Opcode o1) (Opcode o2) = + compare o1 o2 +let {ocaml} opcodeCompare = defaultCompare + +let ~{ocaml} opcodeLess b1 b2 = opcodeCompare b1 b2 = LT +let ~{ocaml} opcodeLessEq b1 b2 = opcodeCompare b1 b2 <> GT +let ~{ocaml} opcodeGreater b1 b2 = opcodeCompare b1 b2 = GT +let ~{ocaml} opcodeGreaterEq b1 b2 = opcodeCompare b1 b2 <> LT + +let inline {ocaml} opcodeLess = defaultLess +let inline {ocaml} opcodeLessEq = defaultLessEq +let inline {ocaml} opcodeGreater = defaultGreater +let inline {ocaml} opcodeGreaterEq = defaultGreaterEq + +instance (Ord opcode) + let compare = opcodeCompare + let (<) = opcodeLess + let (<=) = opcodeLessEq + let (>) = opcodeGreater + let (>=) = opcodeGreaterEq +end + + + + + let addressCompare (Address b1 i1) (Address b2 i2) = compare i1 i2 (* this cannot be defaultCompare for OCaml because addresses contain big ints *) |