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.

0 files changed, 0 insertions, 0 deletions