Fix Lem generation for CHERI-MIPS and Aarch64

- Update Lem bindings and extras files
- Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's
  (used for cap_size in the CHERI spec)
- Add Lem and Isabelle Makefile targets for CHERI

1 files changed, 3 insertions, 3 deletions

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