Rebase state monad onto prompt monad

Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad.  Add some
Isabelle lemmas about the monad lifting.

Also drop the "_embed" and "_sequential" suffixes from names of generated
files.

1 files changed, 0 insertions, 79 deletions

diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras_embed_sequential.lem
deleted file mode 100644
index 31eea6ab..00000000
--- a/riscv/riscv_extras_embed_sequential.lem
+++ /dev/null
@@ -1,79 +0,0 @@
-open import Pervasives
-open import Pervasives_extra
-open import Sail_instr_kinds
-open import Sail_values
-open import Sail_operators_mwords
-open import State
-open import State_monad
-
-type bitvector 'a = mword 'a
-
-let MEM_fence_rw_rw () = barrier Barrier_RISCV_rw_rw
-let MEM_fence_r_rw  () = barrier Barrier_RISCV_r_rw
-let MEM_fence_r_r   () = barrier Barrier_RISCV_r_r
-let MEM_fence_rw_w  () = barrier Barrier_RISCV_rw_w
-let MEM_fence_w_w   () = barrier Barrier_RISCV_w_w
-let MEM_fence_i     () = barrier Barrier_RISCV_i
-
-val MEMea                            : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
-val MEMea_release                    : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
-val MEMea_strong_release             : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
-val MEMea_conditional                : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
-val MEMea_conditional_release        : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
-val MEMea_conditional_strong_release : forall 'r 'a 'e. Size 'a => bitvector 'a -> integer -> M 'r unit 'e
-
-let MEMea addr size                      = write_mem_ea Write_plain addr size
-let MEMea_release addr size              = write_mem_ea Write_RISCV_release addr size
-let MEMea_strong_release addr size       = write_mem_ea Write_RISCV_strong_release addr size
-let MEMea_conditional addr size          = write_mem_ea Write_RISCV_conditional addr size
-let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_release addr size
-let MEMea_conditional_strong_release addr size
-                                          = write_mem_ea Write_RISCV_conditional_strong_release addr size
-
-val write_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> M 'r unit 'e
-let write_ram addrsize size hexRAM address value =
-  write_mem_ea Write_plain address size >>
-  write_mem_val value >>= fun _ ->
-  return ()
-
-val read_ram : forall 'a 'b 'r 'e. Size 'a, Size 'b =>
-  integer -> integer -> bitvector 'a -> bitvector 'a -> M 'r (bitvector 'b) 'e
-let read_ram addrsize size hexRAM address =
-  read_mem Read_plain address size
-
-let speculate_conditional_success () = excl_result ()
-
-val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> bitvector 'a
-let get_slice_int len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bits = bits_of_int (hi + 1) n in
-  of_bits (get_bits false bits hi lo)
-
-val sign_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
-let sign_extend v len = exts_vec len v
-val zero_extend : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> integer -> bitvector 'b
-let zero_extend v len = extz_vec len v
-
-val shift_bits_right : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_right v m = shiftr v (unsigned m)
-val shift_bits_left : forall 'a 'b. Size 'a, Size 'b => bitvector 'a -> bitvector 'b -> bitvector 'a
-let shift_bits_left v m = shiftl v (unsigned m)
-
-val prerr_endline : string -> unit
-let prerr_endline _ = ()
-declare ocaml target_rep function prerr_endline = `prerr_endline`
-
-val print_string : string -> string -> unit
-let print_string msg s = prerr_endline (msg ^ s)
-
-val print_int : string -> integer -> unit
-let print_int msg i = prerr_endline (msg ^ (stringFromInteger i))
-
-val print_bits : forall 'a. Size 'a => string -> bitvector 'a -> unit
-let print_bits msg bs = prerr_endline (msg ^ (show_bitlist (bits_of bs)))
-
-val putchar : integer -> unit
-let putchar _ = ()
-declare ocaml target_rep function putchar i = (`print_char` (`char_of_int` (`Nat_big_num.to_int` i)))