Split base definitions of Lem monads and further built-ins (e.g. loop combinators)

Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators.  These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.

1 files changed, 2 insertions, 166 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 5019c2f7..d398ab52 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -1,172 +1,8 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
-
-type M 'a 'e = outcome 'a 'e
-
-val return : forall 'a 'e. 'a -> M 'a 'e
-let return a = Done a
-
-val bind : forall 'a 'b 'e. M 'a 'e -> ('a -> M 'b 'e) -> M 'b 'e
-let rec bind m f = match m with
-  | Done a ->              f a
-  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (bind o f,opt))
-  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (bind o f,opt))
-  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (bind o f,opt))
-  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (bind o f,opt))
-  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (bind o f,opt))
-  | Escape descr ->        Escape descr
-  | Fail descr ->          Fail descr
-  | Error descr ->         Error descr
-  | Exception e ->         Exception e
-  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (bind o f ,opt))
-end
-
-let inline (>>=) = bind
-val (>>) : forall 'b 'e. M unit 'e -> M 'b 'e -> M 'b 'e
-let inline (>>) m n = m >>= fun (_ : unit) -> n
-
-val exit : forall 'a 'e. unit -> M 'a 'e
-let exit () = Fail Nothing
-
-val assert_exp : forall 'e. bool -> string -> M unit 'e
-let assert_exp exp msg = if exp then Done () else Fail (Just msg)
-
-val throw : forall 'a 'e. 'e -> M 'a 'e
-let throw e = Exception e
-
-val try_catch : forall 'a 'e1 'e2. M 'a 'e1 -> ('e1 -> M 'a 'e2) ->  M 'a 'e2
-let rec try_catch m h = match m with
-  | Done a ->              Done a
-  | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Read_reg descr k ->    Read_reg descr   (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Write_memv descr k ->  Write_memv descr (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Excl_res k ->          Excl_res         (fun v -> let (o,opt) = k v in (try_catch o h,opt))
-  | Write_ea descr o_s ->  Write_ea descr   (let (o,opt) = o_s in (try_catch o h,opt))
-  | Barrier descr o_s ->   Barrier descr    (let (o,opt) = o_s in (try_catch o h,opt))
-  | Footprint o_s ->       Footprint        (let (o,opt) = o_s in (try_catch o h,opt))
-  | Write_reg descr o_s -> Write_reg descr  (let (o,opt) = o_s in (try_catch o h,opt))
-  | Escape descr ->        Escape descr
-  | Fail descr ->          Fail descr
-  | Error descr ->         Error descr
-  | Exception e ->         h e
-  | Internal descr o_s ->  Internal descr   (let (o,opt) = o_s in (try_catch o h ,opt))
-end
-
-(* For early return, we abuse exceptions by throwing and catching
-   the return value. The exception type is "either 'r 'e", where "Right e"
-   represents a proper exception and "Left r" an early return of value "r". *)
-type MR 'a 'r 'e = M 'a (either 'r 'e)
-
-val early_return : forall 'a 'r 'e. 'r -> MR 'a 'r 'e
-let early_return r = throw (Left r)
-
-val catch_early_return : forall 'a 'e. MR 'a 'a 'e -> M 'a 'e
-let catch_early_return m =
-  try_catch m
-    (function
-      | Left a -> return a
-      | Right e -> throw e
-     end)
-
-(* Lift to monad with early return by wrapping exceptions *)
-val liftR : forall 'a 'r 'e. M 'a 'e -> MR 'a 'r 'e
-let liftR m = try_catch m (fun e -> throw (Right e))
-
-(* Catch exceptions in the presence of early returns *)
-val try_catchR : forall 'a 'r 'e1 'e2. MR 'a 'r 'e1 -> ('e1 -> MR 'a 'r 'e2) ->  MR 'a 'r 'e2
-let try_catchR m h =
-  try_catch m
-    (function
-      | Left r -> throw (Left r)
-      | Right e -> h e
-     end)
-
-
-val read_mem : forall 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> M 'b 'e
-let read_mem rk addr sz =
-  let addr = address_lifted_of_bitv (bits_of addr) in
-  let sz = natFromInteger sz in
-  let k memory_value =
-    let bitv = of_bits (internal_mem_value memory_value) in
-    (Done bitv,Nothing) in
-  Read_mem (rk,addr,sz) k
-
-val excl_result : forall 'e. unit -> M bool 'e
-let excl_result () =
-  let k successful = (return successful,Nothing) in
-  Excl_res k
-
-val write_mem_ea : forall 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> M unit 'e
-let write_mem_ea wk addr sz =
-  let addr = address_lifted_of_bitv (bits_of addr) in
-  let sz = natFromInteger sz in
-  Write_ea (wk,addr,sz) (Done (),Nothing)
-
-val write_mem_val : forall 'a 'e. Bitvector 'a => 'a -> M bool 'e
-let write_mem_val v =
-  let v = external_mem_value (bits_of v) in
-  let k successful = (return successful,Nothing) in
-  Write_memv v k
-
-val read_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> M 'a 'e
-let read_reg_aux reg = 
-  let k reg_value =
-    let v = of_bits (internal_reg_value reg_value) in
-    (Done v,Nothing) in
-  Read_reg reg k
-
-let read_reg reg =
-  read_reg_aux (external_reg_whole reg)
-let read_reg_range reg i j =
-  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
-let read_reg_bit reg i =
-  read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
-  return (extract_only_element v)
-let read_reg_field reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield.field_name)
-let read_reg_bitfield reg regfield =
-  read_reg_aux (external_reg_field_whole reg regfield.field_name) >>= fun v ->
-  return (extract_only_element v)
-
-let reg_deref = read_reg
-
-val write_reg_aux : forall 'a 'e. Bitvector 'a => reg_name -> 'a -> M unit 'e
-let write_reg_aux reg_name v =
-  let regval = external_reg_value reg_name (bits_of v) in
-  Write_reg (reg_name,regval) (Done (), Nothing)
-
-let write_reg reg v =
-  write_reg_aux (external_reg_whole reg) v
-let write_reg_range reg i j v =
-  write_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j)) v
-let write_reg_pos reg i v =
-  let iN = natFromInteger i in
-  write_reg_aux (external_reg_slice reg (iN,iN)) [v]
-let write_reg_bit = write_reg_pos
-let write_reg_field reg regfield v =
-  write_reg_aux (external_reg_field_whole reg regfield.field_name) v
-(*let write_reg_field_bit reg regfield bit =
-  write_reg_aux (external_reg_field_whole reg regfield.field_name)
-                (Vector [bit] 0 (is_inc_of_reg reg))*)
-let write_reg_field_range reg regfield i j v =
-  write_reg_aux (external_reg_field_slice reg regfield.field_name (natFromInteger i,natFromInteger j)) v
-let write_reg_field_pos reg regfield i v =
-  write_reg_field_range reg regfield i i [v]
-let write_reg_field_bit = write_reg_field_pos
-
-let write_reg_ref (reg, v) = write_reg reg v
-
-val barrier : forall 'e. barrier_kind -> M unit 'e
-let barrier bk = Barrier bk (Done (), Nothing)
-
-
-val footprint : forall 'e. M unit 'e
-let footprint = Footprint (Done (),Nothing)
-
+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
 let rec iter_aux i f xs = match xs with