diff options
Diffstat (limited to 'src/gen_lib')
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 3 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 6 |
2 files changed, 6 insertions, 3 deletions
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index 9b81e233..edba83ba 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -220,6 +220,9 @@ let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate (bitU_of_bool b) n)) +val reverse_endianness : list bitU -> list bitU +let reverse_endianness v = reverse_endianness_list v + val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool val ult_vec : list bitU -> list bitU -> bool diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index ea7c11cf..e87f4b7c 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -5,9 +5,6 @@ open import Sail_operators open import Prompt_monad open import Prompt -val mword_zero : forall 'a. Size 'a => mword 'a -let mword_zero = wordFromInteger 0 - (* Specialisation of operators to machine words *) let uint v = unsignedIntegerFromWord v @@ -233,6 +230,9 @@ let duplicate_fail b n = bool_of_bitU_fail b >>= (fun b -> return (duplicate_b let duplicate_oracle b n = bool_of_bitU_oracle b >>= (fun b -> return (duplicate_bool b n)) let duplicate b n = maybe_failwith (duplicate_maybe b n) +val reverse_endianness : forall 'a. Size 'a => mword 'a -> mword 'a +let reverse_endianness v = wordFromBitlist (reverse_endianness_list (bitlistFromWord v)) + val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool |