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

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index d398ab52..756bb699 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,24 +1,24 @@
 open import Pervasives_extra
-open import Sail_impl_base
+(*open import Sail_impl_base*)
 open import Sail_values
 open import Prompt_monad
 open import {isabelle} `Prompt_monad_extras`
 
-val iter_aux : forall 'a 'e. integer -> (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e
+val iter_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let rec iter_aux i f xs = match xs with
   | x :: xs -> f i x >> iter_aux (i + 1) f xs
   | [] -> return ()
   end
 
-val iteri : forall 'a 'e. (integer -> 'a -> M unit 'e) -> list 'a -> M unit 'e
+val iteri : forall 'rv 'a 'e. (integer -> 'a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iteri f xs = iter_aux 0 f xs
 
-val iter : forall 'a 'e. ('a -> M unit 'e) -> list 'a -> M unit 'e
+val iter : forall 'rv 'a 'e. ('a -> monad 'rv unit 'e) -> list 'a -> monad 'rv unit 'e
 let iter f xs = iteri (fun _ x -> f x) xs
 
 
-val foreachM_inc : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e
+val foreachM_inc : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec foreachM_inc (i,stop,by) vars body =
   if (by > 0 && i <= stop) || (by < 0 && stop <= i)
   then
@@ -27,8 +27,8 @@ let rec foreachM_inc (i,stop,by) vars body =
   else return vars
 
 
-val foreachM_dec : forall 'vars 'e. (integer * integer * integer) -> 'vars ->
-                  (integer -> 'vars -> M 'vars 'e) -> M 'vars 'e
+val foreachM_dec : forall 'rv 'vars 'e. (integer * integer * integer) -> 'vars ->
+                  (integer -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec foreachM_dec (i,stop,by) vars body =
   if (by > 0 && i >= stop) || (by < 0 && stop >= i)
   then
@@ -40,21 +40,21 @@ val while_PP : forall 'vars. 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'va
 let rec while_PP vars cond body =
   if cond vars then while_PP (body vars) cond body else vars
 
-val while_PM : forall 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val while_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec while_PM vars cond body =
   if cond vars then
     body vars >>= fun vars -> while_PM vars cond body
   else return vars
 
-val while_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> 'vars) -> M 'vars 'e
+val while_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> 'vars) -> monad 'rv 'vars 'e
 let rec while_MP vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then while_MP (body vars) cond body else return vars
 
-val while_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val while_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec while_MM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then
@@ -66,21 +66,21 @@ let rec until_PP vars cond body =
   let vars = body vars in
   if (cond vars) then vars else until_PP (body vars) cond body
 
-val until_PM : forall 'vars 'e. 'vars -> ('vars -> bool) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val until_PM : forall 'rv 'vars 'e. 'vars -> ('vars -> bool) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec until_PM vars cond body =
   body vars >>= fun vars ->
   if (cond vars) then return vars else until_PM vars cond body
 
-val until_MP : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> 'vars) -> M 'vars 'e
+val until_MP : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> 'vars) -> monad 'rv 'vars 'e
 let rec until_MP vars cond body =
   let vars = body vars in
   cond vars >>= fun cond_val ->
   if cond_val then return vars else until_MP vars cond body
 
-val until_MM : forall 'vars 'e. 'vars -> ('vars -> M bool 'e) ->
-                ('vars -> M 'vars 'e) -> M 'vars 'e
+val until_MM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec until_MM vars cond body =
   body vars >>= fun vars ->
   cond vars >>= fun cond_val ->