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, 2 insertions, 2 deletions

diff --git a/lib/isabelle/State_monad_extras.thy b/lib/isabelle/State_monad_extras.thy
index c9522f58..cf042a02 100644
--- a/lib/isabelle/State_monad_extras.thy
+++ b/lib/isabelle/State_monad_extras.thy
@@ -7,8 +7,8 @@ lemma bind_ext_cong[fundef_cong]:
     and f: "\<And>a s'. (Value a, s') \<in> set (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
   shows "(bind m1 f1) s = (bind m2 f2) s"
 proof -
-  have "List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f1 a s' | (Exception0 e, s') \<Rightarrow> [(Exception0 e, s')]) (m2 s)) =
-        List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f2 a s' | (Exception0 e, s') \<Rightarrow> [(Exception0 e, s')]) (m2 s))"
+  have "List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f1 a s' | (Exception e, s') \<Rightarrow> [(Exception e, s')]) (m2 s)) =
+        List.concat (map (\<lambda>x. case x of (Value a, s') \<Rightarrow> f2 a s' | (Exception e, s') \<Rightarrow> [(Exception e, s')]) (m2 s))"
     using f by (intro arg_cong[where f = List.concat]) (auto intro: map_ext split: result.splits)
   then show ?thesis using m by (auto simp: bind_def)
 qed