1 files changed, 168 insertions, 0 deletions
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
new file mode 100644
index 00000000..45733caa
--- /dev/null
+++ b/src/gen_lib/prompt_monad.lem
@@ -0,0 +1,168 @@
+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)