rename all lem support files to sail2_foo to avoid conflict with sail1 in rmem

11 files changed, 40 insertions, 29 deletions

diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/sail2_deep_shallow_convert.lem
index 7fea0409..b963e537 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/sail2_deep_shallow_convert.lem
@@ -1,8 +1,8 @@
 open import Pervasives_extra
-open import Sail_impl_base
-open import Interp
-open import Interp_ast
-open import Sail_values
+open import Sail2_impl_base
+open import Sail2_interp
+open import Sail2_interp_ast
+open import Sail2_values
 
 
 class (ToFromInterpValue 'a)
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail2_operators.lem
index 0c5da675..547160d3 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail2_operators.lem
@@ -1,6 +1,6 @@
 open import Pervasives_extra
 open import Machine_word
-open import Sail_values
+open import Sail2_values
 
 (*** Bit vector operations *)
 
diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 19e9b519..7f1bcba5 100644
--- a/src/gen_lib/sail_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -1,9 +1,9 @@
 open import Pervasives_extra
 open import Machine_word
-open import Sail_values
-open import Sail_operators
-open import Prompt_monad
-open import Prompt
+open import Sail2_values
+open import Sail2_operators
+open import Sail2_prompt_monad
+open import Sail2_prompt
 
 (* Specialisation of operators to bit lists *)
 
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index 22d5b246..fe319efc 100644
--- a/src/gen_lib/sail_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -1,9 +1,9 @@
 open import Pervasives_extra
 open import Machine_word
-open import Sail_values
-open import Sail_operators
-open import Prompt_monad
-open import Prompt
+open import Sail2_values
+open import Sail2_operators
+open import Sail2_prompt_monad
+open import Sail2_prompt
 
 (* Specialisation of operators to machine words *)
 
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/sail2_prompt.lem
index 830f2350..434df843 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/sail2_prompt.lem
@@ -1,7 +1,7 @@
 open import Pervasives_extra
 (*open import Sail_impl_base*)
-open import Sail_values
-open import Prompt_monad
+open import Sail2_values
+open import Sail2_prompt_monad
 open import {isabelle} `Prompt_monad_lemmas`
 
 val (>>=) : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 87c9af39..745589e2 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -1,7 +1,7 @@
 open import Pervasives_extra
 (*open import Sail_impl_base*)
-open import Sail_instr_kinds
-open import Sail_values
+open import Sail2_instr_kinds
+open import Sail2_values
 
 type register_name = string
 type address = list bitU
diff --git a/src/gen_lib/state.lem b/src/gen_lib/sail2_state.lem
index f69f59c1..82ac35d8 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/sail2_state.lem
@@ -1,7 +1,7 @@
 open import Pervasives_extra
-open import Sail_values
-open import State_monad
-open import {isabelle} `State_monad_lemmas`
+open import Sail2_values
+open import Sail2_state_monad
+open import {isabelle} `Sail2_state_monad_lemmas`
 
 val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
 let rec iterS_aux i f xs = match xs with
diff --git a/src/gen_lib/state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 7e569a7e..039343e2 100644
--- a/src/gen_lib/state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -1,9 +1,9 @@
 open import Pervasives_extra
-open import Sail_values
-open import Prompt_monad
-open import Prompt
-open import State_monad
-open import {isabelle} `State_monad_lemmas`
+open import Sail2_values
+open import Sail2_prompt_monad
+open import Sail2_prompt
+open import Sail2_state_monad
+open import {isabelle} `Sail2_state_monad_lemmas`
 
 (* State monad wrapper around prompt monad *)
 
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 89021890..f207699f 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -1,6 +1,6 @@
 open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
+open import Sail2_instr_kinds
+open import Sail2_values
 
 (* 'a is result type *)
 
diff --git a/src/gen_lib/sail_string.lem b/src/gen_lib/sail2_string.lem
index 07b39ddc..329da942 100644
--- a/src/gen_lib/sail_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -4,8 +4,8 @@ open import List_extra
 open import String
 open import String_extra
 
-open import Sail_operators_mwords
-open import Sail_values
+open import Sail2_operators_mwords
+open import Sail2_values
 
 val string_sub : string -> ii -> ii -> string
 let string_sub str start len =
@@ -116,6 +116,17 @@ let hex_bits_13_matches_prefix s =
        Nothing
   end
 
+let hex_bits_16_matches_prefix s =
+  match maybe_int_of_prefix s with
+  | Nothing -> Nothing
+  | Just (n, len) ->
+     if 0 <= n && n < 65536 then
+       Just ((of_int 16 n, len))
+     else
+       Nothing
+  end
+
+
 let hex_bits_20_matches_prefix s =
   match maybe_int_of_prefix s with
   | Nothing -> Nothing
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail2_values.lem
index 0f384cab..0f384cab 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail2_values.lem