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.

2 files changed, 30 insertions, 30 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index aeba80ef..52bc150b 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -3,7 +3,7 @@ SAIL_DIR ?= $(realpath ..)
 
 export SAIL_DIR
 
-all: riscv Riscv_embed_sequential.thy
+all: riscv Riscv.thy
 
 check: $(SAIL_SRCS) main.sail
 	$(SAIL_DIR)/sail $^
@@ -14,28 +14,28 @@ riscv: $(SAIL_SRCS) main.sail
 riscv_duopod_ocaml: prelude.sail riscv_duopod.sail
 	$(SAIL_DIR)/sail -ocaml -o $@ $^
 
-riscv_duopod_embed_sequential.lem: prelude.sail riscv_duopod.sail
-	$(SAIL_DIR)/sail -lem -lem_sequential -lem_mwords -lem_lib Riscv_extras_embed -o riscv_duopod $^
-Riscv_duopod_embed_sequential.thy: riscv_duopod_embed_sequential.lem riscv_extras_embed_sequential.lem
+riscv_duopod.lem: prelude.sail riscv_duopod.sail
+	$(SAIL_DIR)/sail -lem -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^
+Riscv_duopod.thy: riscv_duopod.lem riscv_extras.lem
 	lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
-		riscv_extras_embed_sequential.lem \
-		riscv_duopod_embed_types_sequential.lem \
-		riscv_duopod_embed_sequential.lem
+		riscv_extras.lem \
+		riscv_duopod_types.lem \
+		riscv_duopod.lem
 
-riscv_duopod: riscv_duopod_ocaml Riscv_duopod_embed_sequential.thy
+riscv_duopod: riscv_duopod_ocaml Riscv_duopod.thy
 
-Riscv_embed_sequential.thy: riscv_embed_sequential.lem riscv_extras_embed_sequential.lem
+Riscv.thy: riscv.lem riscv_extras.lem
 	lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
-		riscv_extras_embed_sequential.lem \
-		riscv_embed_types_sequential.lem \
-		riscv_embed_sequential.lem
+		riscv_extras.lem \
+		riscv_types.lem \
+		riscv.lem
 
-riscv_embed_sequential.lem: $(SAIL_SRCS)
-	$(SAIL_DIR)/sail -lem -o riscv -lem_sequential -lem_mwords -lem_lib Riscv_extras_embed $^
+riscv.lem: $(SAIL_SRCS)
+	$(SAIL_DIR)/sail -lem -o riscv -lem_mwords -lem_lib Riscv_extras $^
 
 clean:
 	-rm -rf riscv _sbuild
-	-rm -f riscv_embed_sequential.lem riscv_embed_types_sequential.lem
-	-rm -f Riscv_embed_sequential.thy Riscv_embed_types_sequential.thy \
-		Riscv_extras_embed_sequential.thy
-	-rm -f Riscv_duopod_embed_sequential.thy Riscv_duopod_embed_types_sequential.thy riscv_duopod_embed_sequential.lem riscv_duopod_embed_types_sequential.lem
+	-rm -f riscv.lem riscv_types.lem
+	-rm -f Riscv.thy Riscv_types.thy \
+		Riscv_extras.thy
+	-rm -f Riscv_duopod.thy Riscv_duopod_types.thy riscv_duopod.lem riscv_duopod_types.lem
diff --git a/riscv/riscv_extras_embed_sequential.lem b/riscv/riscv_extras.lem
index 31eea6ab..49499445 100644
--- a/riscv/riscv_extras_embed_sequential.lem
+++ b/riscv/riscv_extras.lem
@@ -3,8 +3,8 @@ 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
+open import Prompt_monad
+open import Prompt
 
 type bitvector 'a = mword 'a
 
@@ -15,12 +15,12 @@ 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
+val MEMea                            : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_release                    : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_strong_release             : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional                : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional_release        : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e
+val MEMea_conditional_strong_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv 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
@@ -30,15 +30,15 @@ let MEMea_conditional_release addr size  = write_mem_ea Write_RISCV_conditional_
 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
+val write_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
+  integer -> integer -> bitvector 'a -> bitvector 'a -> bitvector 'b -> monad 'rv 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
+val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
+  integer -> integer -> bitvector 'a -> bitvector 'a -> monad 'rv (bitvector 'b) 'e
 let read_ram addrsize size hexRAM address =
   read_mem Read_plain address size