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

1 files changed, 0 insertions, 221 deletions

diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
deleted file mode 100644
index 87c9af39..00000000
--- a/src/gen_lib/prompt_monad.lem
+++ /dev/null
@@ -1,221 +0,0 @@
-open import Pervasives_extra
-(*open import Sail_impl_base*)
-open import Sail_instr_kinds
-open import Sail_values
-
-type register_name = string
-type address = list bitU
-
-type monad 'regval 'a 'e =
-  | Done of 'a
-  (* Read a number of bytes from memory, returned in little endian order *)
-  | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
-  (* Read the tag of a memory address *)
-  | Read_tag of address * (bitU -> monad 'regval 'a 'e)
-  (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
-  (* Request the result of store-exclusive *)
-  | Excl_res of (bool -> monad 'regval 'a 'e)
-  (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal, given in little endian order *)
-  | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
-  (* Request to write the tag at given address. *)
-  | Write_tag of address * bitU * (bool -> monad 'regval 'a 'e)
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of monad 'regval 'a 'e
-  (* Request a memory barrier *)
-  | Barrier of barrier_kind * monad 'regval 'a 'e
-  (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
-  (* Request to write register *)
-  | Write_reg of register_name * 'regval * monad 'regval 'a 'e
-  | Undefined of (bool -> monad 'regval 'a 'e)
-  (* Print debugging or tracing information *)
-  | Print of string * monad 'regval 'a 'e
-  (*Result of a failed assert with possible error message to report*)
-  | Fail of string
-  (* Exception of type 'e *)
-  | Exception of 'e
-
-val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
-let return a = Done a
-
-val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
-let rec bind m f = match m with
-  | Done a -> f a
-  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
-  | Read_tag a k ->       Read_tag a       (fun v -> bind (k v) f)
-  | Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f)
-  | Write_tag a t k ->    Write_tag a t    (fun v -> bind (k v) f)
-  | Read_reg descr k ->   Read_reg descr   (fun v -> bind (k v) f)
-  | Excl_res k ->         Excl_res         (fun v -> bind (k v) f)
-  | Undefined k ->        Undefined        (fun v -> bind (k v) f)
-  | Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
-  | Footprint k ->        Footprint        (bind k f)
-  | Barrier bk k ->       Barrier bk       (bind k f)
-  | Write_reg r v k ->    Write_reg r v    (bind k f)
-  | Print msg k ->        Print msg        (bind k f)
-  | Fail descr ->         Fail descr
-  | Exception e ->        Exception e
-end
-
-val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
-let exit () = Fail "exit"
-
-val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
-let undefined_bool () = Undefined return
-
-val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
-let assert_exp exp msg = if exp then Done () else Fail msg
-
-val throw : forall 'rv 'a 'e. 'e -> monad 'rv 'a 'e
-let throw e = Exception e
-
-val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
-let rec try_catch m h = match m with
-  | Done a ->             Done a
-  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
-  | Read_tag a k ->       Read_tag a       (fun v -> try_catch (k v) h)
-  | Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h)
-  | Write_tag a t k ->    Write_tag a t    (fun v -> try_catch (k v) h)
-  | Read_reg descr k ->   Read_reg descr   (fun v -> try_catch (k v) h)
-  | Excl_res k ->         Excl_res         (fun v -> try_catch (k v) h)
-  | Undefined k ->        Undefined        (fun v -> try_catch (k v) h)
-  | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
-  | Footprint k ->        Footprint        (try_catch k h)
-  | Barrier bk k ->       Barrier bk       (try_catch k h)
-  | Write_reg r v k ->    Write_reg r v    (try_catch k h)
-  | Print msg k ->        Print msg        (try_catch k h)
-  | Fail descr ->         Fail descr
-  | Exception e ->        h e
-end
-
-(* For early return, we abuse exceptions by throwing and catching
-   the return value. The exception type is "either 'r 'e", where "Right e"
-   represents a proper exception and "Left r" an early return of value "r". *)
-type monadR 'rv 'a 'r 'e = monad 'rv 'a (either 'r 'e)
-
-val early_return : forall 'rv 'a 'r 'e. 'r -> monadR 'rv 'a 'r 'e
-let early_return r = throw (Left r)
-
-val catch_early_return : forall 'rv 'a 'e. monadR 'rv 'a 'a 'e -> monad 'rv 'a 'e
-let catch_early_return m =
-  try_catch m
-    (function
-      | Left a -> return a
-      | Right e -> throw e
-     end)
-
-(* Lift to monad with early return by wrapping exceptions *)
-val liftR : forall 'rv 'a 'r 'e. monad 'rv 'a 'e -> monadR 'rv 'a 'r 'e
-let liftR m = try_catch m (fun e -> throw (Right e))
-
-(* Catch exceptions in the presence of early returns *)
-val try_catchR : forall 'rv 'a 'r 'e1 'e2. monadR 'rv 'a 'r 'e1 -> ('e1 -> monadR 'rv 'a 'r 'e2) ->  monadR 'rv 'a 'r 'e2
-let try_catchR m h =
-  try_catch m
-    (function
-      | Left r -> throw (Left r)
-      | Right e -> h e
-     end)
-
-val maybe_fail : forall 'rv 'a 'e. string -> maybe 'a -> monad 'rv 'a 'e
-let maybe_fail msg = function
-  | Just a -> return a
-  | Nothing -> Fail msg
-end
-
-val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
-let read_mem_bytes rk addr sz =
-  Read_mem rk (bits_of addr) (nat_of_int sz) return
-
-val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
-let read_mem rk addr sz =
-  bind
-    (read_mem_bytes rk addr sz)
-    (fun bytes ->
-       maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
-
-val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
-let read_tag addr = Read_tag (bits_of addr) return
-
-val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
-let excl_result () =
-  let k successful = (return successful) in
-  Excl_res k
-
-val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
-
-val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
-let write_mem_val v = match mem_bytes_of_bits v with
-  | Just v -> Write_memv v return
-  | Nothing -> Fail "write_mem_val"
-end
-
-val write_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> bitU -> monad 'rv bool 'e
-let write_tag addr b = Write_tag (bits_of addr) b return
-
-val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
-let read_reg reg =
-  let k v =
-    match reg.of_regval v with
-      | Just v -> Done v
-      | Nothing -> Fail "read_reg: unrecognised value"
-    end
-  in
-  Read_reg reg.name k
-
-(* TODO
-val read_reg_range : forall 's 'r 'rv 'a 'e. Bitvector 'a => register_ref 's 'rv 'r -> integer -> integer -> monad 'rv 'a 'e
-let read_reg_range reg i j =
-  read_reg_aux of_bits (external_reg_slice reg (nat_of_int i,nat_of_int j))
-
-let read_reg_bit reg i =
-  read_reg_aux (fun v -> v) (external_reg_slice reg (nat_of_int i,nat_of_int i)) >>= fun v ->
-  return (extract_only_element v)
-
-let read_reg_field reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield)
-
-let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
-  return (extract_only_element v)*)
-
-let reg_deref = read_reg
-
-val write_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> 'a -> monad 'rv unit 'e
-let write_reg reg v = Write_reg reg.name (reg.regval_of v) (Done ())
-
-(* TODO
-let write_reg reg v =
-  write_reg_aux (external_reg_whole reg) v
-let write_reg_range reg i j v =
-  write_reg_aux (external_reg_slice reg (nat_of_int i,nat_of_int j)) v
-let write_reg_pos reg i v =
-  let iN = nat_of_int i in
-  write_reg_aux (external_reg_slice reg (iN,iN)) [v]
-let write_reg_bit = write_reg_pos
-let write_reg_field reg regfield v =
-  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
-let write_reg_field_bit reg regfield bit =
-  write_reg_aux (external_reg_field_whole reg regfield.field_name)
-                (Vector [bit] 0 (is_inc_of_reg reg))
-let write_reg_field_range reg regfield i j v =
-  write_reg_aux (external_reg_field_slice reg regfield.field_name (nat_of_int i,nat_of_int j)) v
-let write_reg_field_pos reg regfield i v =
-  write_reg_field_range reg regfield i i [v]
-let write_reg_field_bit = write_reg_field_pos*)
-
-val barrier : forall 'rv 'e. barrier_kind -> monad 'rv unit 'e
-let barrier bk = Barrier bk (Done ())
-
-val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
-let footprint _ = Footprint (Done ())
-
-(* Define a type synonym that also takes the register state as a type parameter,
-   in order to make switching to the state monad without changing generated
-   definitions easier, see also lib/hol/prompt_monad.lem. *)
-
-type base_monad 'regval 'regstate 'a 'e = monad 'regval 'a 'e
-type base_monadR 'regval 'regstate 'a 'r 'e = monadR 'regval 'a 'r 'e