summaryrefslogtreecommitdiff
path: root/src/gen_lib/prompt.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib/prompt.lem')
-rw-r--r--src/gen_lib/prompt.lem168
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:08:05 +0000