diff options
Diffstat (limited to 'src/gen_lib/sail_operators.lem')
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 78aab65e..0c5da675 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -194,36 +194,6 @@ let neq_bv l r = not (eq_bv l r) let inline neq_mword l r = (l <> r) -val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r)) -let ulteq_bv l r = (eq_bv l r) || (ult_bv l r) -let ugt_bv l r = not (ulteq_bv l r) -let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r) - -val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let slt_bv l r = - match (most_significant l, most_significant r) with - | (B0, B0) -> ult_bv l r - | (B0, B1) -> false - | (B1, B0) -> true - | (B1, B1) -> - let l' = add_one_bit_ignore_overflow (bits_of l) in - let r' = add_one_bit_ignore_overflow (bits_of r) in - ugt_bv l' r' - | (BU, BU) -> ult_bv l r - | (BU, _) -> true - | (_, BU) -> false - end -let slteq_bv l r = (eq_bv l r) || (slt_bv l r) -let sgt_bv l r = not (slteq_bv l r) -let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r) - -val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool -let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r) - -val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool -let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r) - val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a let get_slice_int_bv len n lo = let hi = lo + len - 1 in |