Re-engineer prompt monad of Lem shallow embedding

- Use simplified monad type (e.g., without the with_aux constructors that are
  not needed by the shallow embedding).
- Add support for registers with arbitrary types (e.g., records, enumerations,
  vectors of vectors). Instead of using bit lists as the common representation
  of register values at the monad interface, use a register_value type that is
  generated per spec as a union of all register types that occur in the spec.
  Conversion functions between register_value and concrete types are generated.
- Use the same representation of register references as the state monad, in
  preparation of rebasing the state monad onto the prompt monad.
- Split out those types from sail_impl_base.lem that are used by the shallow
  embedding into a new module sail_instr_kinds.lem, and import that.  Removing
  the dependency on Sail_impl_base from the shallow embedding avoids name clashes
  between the different monad types.

Not yet done:
- Support for reading/writing register slices.  Currently, a rewriting pass
  pushes register slices in l-expressions to the right-hand side, turning a
  write to a register slice into a read-modify-write.  For interfacing with the
  concurreny model, we will want to be more precise than that (in particular
  since some specs represent register files as big single registers containing a
  vector of bitvectors).
- Lemmas about the conversion functions to/from register_value should be
  generated automatically.

1 files changed, 3 insertions, 3 deletions

diff --git a/lib/isabelle/Makefile b/lib/isabelle/Makefile
index 84af5d75..50e6d471 100644
--- a/lib/isabelle/Makefile
+++ b/lib/isabelle/Makefile
@@ -1,4 +1,4 @@
-THYS = Sail_impl_base.thy Sail_values.thy Sail_operators.thy \
+THYS = Sail_instr_kinds.thy Sail_values.thy Sail_operators.thy \
   Sail_operators_mwords.thy Sail_operators_bitlists.thy \
   State_monad.thy State.thy Prompt_monad.thy Prompt.thy
 EXTRA_THYS = State_monad_extras.thy Prompt_monad_extras.thy
@@ -14,10 +14,10 @@ heap-img: $(THYS) $(EXTRA_THYS) ROOT
 	@echo '*** and add the isabelle binary to your PATH.'
 	isabelle build -b Sail
 
-Sail_impl_base.thy: ../../src/lem_interp/sail_impl_base.lem
+Sail_instr_kinds.thy: ../../src/lem_interp/sail_instr_kinds.lem
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
-Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_impl_base.thy
+Sail_values.thy: ../../src/gen_lib/sail_values.lem Sail_instr_kinds.thy
 	lem -isa -outdir . -lib ../../src/lem_interp -lib ../../src/gen_lib $<
 
 Sail_operators.thy: ../../src/gen_lib/sail_operators.lem Sail_values.thy