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

19 files changed, 79 insertions, 64 deletions

diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index 989ee1cb..60f5dde9 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -1,10 +1,10 @@
 open import Pervasives
 open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators_mwords
-open import Prompt_monad
-open import Prompt
+open import Sail2_instr_kinds
+open import Sail2_values
+open import Sail2_operators_mwords
+open import Sail2_prompt_monad
+open import Sail2_prompt
 
 type bitvector 'a = mword 'a
 
diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 96513d7f..27d4d5a2 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -124,14 +124,14 @@ let ijump ?loc:(l=Parse_ast.Unknown) cval label =
 (**************************************************************************)
 
 let string_of_value = function
-  | V_bits bs -> Sail_values.show_bitlist bs ^ "ul"
+  | V_bits bs -> Sail2_values.show_bitlist bs ^ "ul"
   | V_int i -> Big_int.to_string i ^ "l"
   | V_bool true -> "true"
   | V_bool false -> "false"
   | V_null -> "NULL"
   | V_unit -> "UNIT"
-  | V_bit Sail_values.B0 -> "0ul"
-  | V_bit Sail_values.B1 -> "1ul"
+  | V_bit Sail2_values.B0 -> "0ul"
+  | V_bit Sail2_values.B1 -> "1ul"
   | V_string str -> "\"" ^ str ^ "\""
   | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
   | _ -> failwith "Cannot convert value to string"
diff --git a/src/c_backend.ml b/src/c_backend.ml
index 06e92f3a..7d586e9a 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -861,7 +861,7 @@ let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp m
 (**************************************************************************)
 
 let hex_char =
-  let open Sail_values in
+  let open Sail2_values in
   function
   | '0' -> [B0; B0; B0; B0]
   | '1' -> [B0; B0; B0; B1]
@@ -887,7 +887,7 @@ let literal_to_fragment (L_aux (l_aux, _) as lit) =
      Some (F_lit (V_int n))
   | L_hex str when String.length str <= 16 ->
      let padding = 16 - String.length str in
-     let padding = Util.list_init padding (fun _ -> Sail_values.B0) in
+     let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in
      let content = Util.string_to_list str |> List.map hex_char |> List.concat in
      Some (F_lit (V_bits (padding @ content)))
   | L_unit -> Some (F_lit V_unit)
@@ -924,8 +924,8 @@ let rec is_bitvector = function
   | _ :: _ -> false
 
 let rec value_of_aval_bit = function
-  | AV_lit (L_aux (L_zero, _), _) -> Sail_values.B0
-  | AV_lit (L_aux (L_one, _), _) -> Sail_values.B1
+  | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0
+  | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1
   | _ -> assert false
 
 let rec c_aval ctx = function
@@ -1004,13 +1004,13 @@ let analyze_primop' ctx env l id args typ =
      AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", start)), typ))
 
   | "undefined_bit", _ ->
-     AE_val (AV_C_fragment (F_lit (V_bit Sail_values.B0), typ))
+     AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ))
 
   | "undefined_vector", [AV_C_fragment (len, _); _] ->
      begin match destruct_vector ctx.tc_env typ with
      | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
           when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
-       AE_val (AV_C_fragment (F_lit (V_bit Sail_values.B0), typ))
+       AE_val (AV_C_fragment (F_lit (V_bit Sail2_values.B0), typ))
      | _ -> no_change
      end
 
@@ -1190,8 +1190,8 @@ let rec compile_aval ctx = function
      (F_id gs, CT_mpz),
      [iclear CT_mpz gs]
 
-  | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail_values.B0), CT_bit), []
-  | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail_values.B1), CT_bit), []
+  | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), []
+  | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), []
 
   | AV_lit (L_aux (L_true, _), _) -> [], (F_lit (V_bool true), CT_bool), []
   | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), []
@@ -1285,18 +1285,18 @@ let rec compile_aval ctx = function
      in
      let gs = gensym () in
      let ctyp = CT_uint64 (len, direction) in
-     let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail_values.B0) @ [Sail_values.B1] @ Util.list_init i (fun _ -> Sail_values.B0)) in
+     let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in
      let aval_mask i aval =
        let setup, cval, cleanup = compile_aval ctx aval in
        match cval with
-       | (F_lit (V_bit Sail_values.B0), _) -> []
-       | (F_lit (V_bit Sail_values.B1), _) ->
+       | (F_lit (V_bit Sail2_values.B0), _) -> []
+       | (F_lit (V_bit Sail2_values.B1), _) ->
           [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)]
        | _ ->
           setup @ [iif cval [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup
      in
      [idecl ctyp gs;
-      icopy (CL_id gs) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail_values.B0))), ctyp)]
+      icopy (CL_id gs) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)]
      @ List.concat (List.mapi aval_mask (List.rev avals)),
      (F_id gs, ctyp),
      []
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
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail2_impl_base.lem
index 39ba0b5c..f1cd9f2a 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail2_impl_base.lem
@@ -49,7 +49,7 @@
 (*========================================================================*)
 
 open import Pervasives_extra
-open import Sail_instr_kinds
+open import Sail2_instr_kinds
 
 
 class ( EnumerationType 'a ) 
diff --git a/src/lem_interp/sail_instr_kinds.lem b/src/lem_interp/sail2_instr_kinds.lem
index d8a2c0c0..d8a2c0c0 100644
--- a/src/lem_interp/sail_instr_kinds.lem
+++ b/src/lem_interp/sail2_instr_kinds.lem
diff --git a/src/process_file.ml b/src/process_file.ml
index 710655c4..5ceb2a5c 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -279,17 +279,17 @@ let output_lem filename libs defs =
   let generated_line = generated_line filename in
   (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *)
   let types_module = (filename ^ "_types") in
-  let monad_modules = ["Prompt_monad"; "Prompt"] in
+  let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"] in
   let operators_module =
     if !Pretty_print_lem.opt_mwords
-    then "Sail_operators_mwords"
-    else "Sail_operators_bitlists" in
+    then "Sail2_operators_mwords"
+    else "Sail2_operators_bitlists" in
   (* let libs = List.map (fun lib -> lib ^ seq_suffix) libs in *)
   let base_imports = [
       "Pervasives_extra";
-      "Sail_instr_kinds";
-      "Sail_values";
-      "Sail_string";
+      "Sail2_instr_kinds";
+      "Sail2_values";
+      "Sail2_string";
       operators_module
     ] @ monad_modules
   in
@@ -298,8 +298,8 @@ let output_lem filename libs defs =
     separate hardline [
       string ("theory " ^ isa_thy_name);
       string  "  imports";
-      string  "    Sail.Sail_values_lemmas";
-      string  "    Sail.State_lemmas";
+      string  "    Sail.Sail2_values_lemmas";
+      string  "    Sail.Sail2_state_lemmas";
       string ("    " ^ String.capitalize filename);
       string  "begin";
       string  "";
@@ -326,11 +326,11 @@ let output_lem filename libs defs =
 let output_coq filename libs defs =
   let generated_line = generated_line filename in
   let types_module = (filename ^ "_types") in
-  let monad_modules = ["Prompt_monad"; "Prompt"; "State"] in
-  let operators_module = "Sail_operators_mwords" in
+  let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in
+  let operators_module = "Sail2_operators_mwords" in
   let base_imports = [
-      "Sail_instr_kinds";
-      "Sail_values";
+      "Sail2_instr_kinds";
+      "Sail2_values";
       operators_module
     ] @ monad_modules
   in
diff --git a/src/type_check.ml b/src/type_check.ml
index be8f477f..9aaf233c 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2724,13 +2724,17 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
           begin
             try
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, mapping_typ) ^ " for pattern " ^ string_of_typ typ));
+
               let unifiers, _, _ (* FIXME! *) = unify l env typ2 typ in
-              typ_debug (lazy (string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)));
+
+              typ_debug (lazy ("unifiers: " ^ string_of_list ", " (fun (kid, uvar) -> string_of_kid kid ^ " => " ^ string_of_uvar uvar) (KBindings.bindings unifiers)));
+
               let arg_typ' = subst_unifiers unifiers typ1 in
               let quants' = List.fold_left (fun qs (kid, uvar) -> instantiate_quants qs kid uvar) quants (KBindings.bindings unifiers) in
               if (match quants' with [] -> false | _ -> true)
               then typ_error l ("Quantifiers " ^ string_of_list ", " string_of_quant_item quants' ^ " not resolved in pattern " ^ string_of_pat pat)
               else ();
+
               let ret_typ' = subst_unifiers unifiers typ2 in
               let tpats, env, guards =
                 try List.fold_left2 bind_tuple_pat ([], env, []) pats (untuple arg_typ') with
diff --git a/src/value2.lem b/src/value2.lem
index 09d74520..d14dd87d 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -52,7 +52,7 @@ open import Pervasives
 open import Assert_extra
 open Map
 
-open import Sail_values
+open import Sail2_values
 
 type vl =
   | V_vector of list vl