summaryrefslogtreecommitdiff
path: root/src/gen_lib
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib')
-rw-r--r--src/gen_lib/state.lem59
-rw-r--r--src/gen_lib/state_lifting.lem27
-rw-r--r--src/gen_lib/state_monad.lem14
3 files changed, 68 insertions, 32 deletions
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 61477258..6bc304a8 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -1,33 +1,8 @@
open import Pervasives_extra
-(*open import Sail_impl_base*)
open import Sail_values
-open import Prompt_monad
-open import Prompt
open import State_monad
open import {isabelle} `State_monad_lemmas`
-(* State monad wrapper around prompt monad *)
-
-val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
- | (Done a) -> returnS a
- | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
- | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v))
- | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v))
- | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v))
- | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
- | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
- | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v))
- | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
- | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
- | (Footprint k) -> liftState ra k
- | (Barrier _ k) -> liftState ra k
- | (Print _ k) -> liftState ra k (* TODO *)
- | (Fail descr) -> failS descr
- | (Exception e) -> throwS e
-end
-
-
val iterS_aux : forall 'rv 'a 'e. integer -> (integer -> 'a -> monadS 'rv unit 'e) -> list 'a -> monadS 'rv unit 'e
let rec iterS_aux i f xs = match xs with
| x :: xs -> f i x >>$ iterS_aux (i + 1) f xs
@@ -53,6 +28,40 @@ end
declare {isabelle} termination_argument foreachS = automatic
+val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_fail = function
+ | B0 -> returnS false
+ | B1 -> returnS true
+ | BU -> failS "bool_of_bitU"
+end
+
+val bool_of_bitU_oracleS : forall 'rv 'e. bitU -> monadS 'rv bool 'e
+let bool_of_bitU_oracleS = function
+ | B0 -> returnS false
+ | B1 -> returnS true
+ | BU -> undefined_boolS ()
+end
+
+val bools_of_bits_oracleS : forall 'rv 'e. list bitU -> monadS 'rv (list bool) 'e
+let bools_of_bits_oracleS bits =
+ foreachS bits []
+ (fun b bools ->
+ bool_of_bitU_oracleS b >>$= (fun b ->
+ returnS (bools ++ [b])))
+
+val of_bits_oracleS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_oracleS bits =
+ bools_of_bits_oracleS bits >>$= (fun bs ->
+ returnS (of_bools bs))
+
+val of_bits_failS : forall 'rv 'a 'e. Bitvector 'a => list bitU -> monadS 'rv 'a 'e
+let of_bits_failS bits = maybe_failS "of_bits" (of_bits bits)
+
+val mword_oracleS : forall 'rv 'a 'e. Size 'a => unit -> monadS 'rv (mword 'a) 'e
+let mword_oracleS () =
+ bools_of_bits_oracleS (repeat [BU] (integerFromNat size)) >>$= (fun bs ->
+ returnS (wordFromBitlist bs))
+
val whileS : forall 'rv 'vars 'e. 'vars -> ('vars -> monadS 'rv bool 'e) ->
('vars -> monadS 'rv 'vars 'e) -> monadS 'rv 'vars 'e
diff --git a/src/gen_lib/state_lifting.lem b/src/gen_lib/state_lifting.lem
new file mode 100644
index 00000000..7e569a7e
--- /dev/null
+++ b/src/gen_lib/state_lifting.lem
@@ -0,0 +1,27 @@
+open import Pervasives_extra
+open import Sail_values
+open import Prompt_monad
+open import Prompt
+open import State_monad
+open import {isabelle} `State_monad_lemmas`
+
+(* State monad wrapper around prompt monad *)
+
+val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
+let rec liftState ra s = match s with
+ | (Done a) -> returnS a
+ | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+ | (Read_tag t k) -> bindS (read_tagS t) (fun v -> liftState ra (k v))
+ | (Write_memv a k) -> bindS (write_mem_bytesS a) (fun v -> liftState ra (k v))
+ | (Write_tag a t k) -> bindS (write_tagS a t) (fun v -> liftState ra (k v))
+ | (Read_reg r k) -> bindS (read_regvalS ra r) (fun v -> liftState ra (k v))
+ | (Excl_res k) -> bindS (excl_resultS ()) (fun v -> liftState ra (k v))
+ | (Undefined k) -> bindS (undefined_boolS ()) (fun v -> liftState ra (k v))
+ | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz) (liftState ra k)
+ | (Write_reg r v k) -> seqS (write_regvalS ra r v) (liftState ra k)
+ | (Footprint k) -> liftState ra k
+ | (Barrier _ k) -> liftState ra k
+ | (Print _ k) -> liftState ra k (* TODO *)
+ | (Fail descr) -> failS descr
+ | (Exception e) -> throwS e
+end
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index 8253b800..781bc129 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -94,12 +94,12 @@ let assert_expS exp msg = if exp then returnS () else failS msg
(* 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 monadSR 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
+type monadRS 'regs 'a 'r 'e = monadS 'regs 'a (either 'r 'e)
-val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadSR 'regs 'a 'r 'e
+val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e
let early_returnS r = throwS (Left r)
-val catch_early_returnS : forall 'regs 'a 'e. monadSR 'regs 'a 'a 'e -> monadS 'regs 'a 'e
+val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e
let catch_early_returnS m =
try_catchS m
(function
@@ -108,12 +108,12 @@ let catch_early_returnS m =
end)
(* Lift to monad with early return by wrapping exceptions *)
-val liftSR : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadSR 'regs 'a 'r 'e
-let liftSR m = try_catchS m (fun e -> throwS (Right e))
+val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e
+let liftRS m = try_catchS m (fun e -> throwS (Right e))
(* Catch exceptions in the presence of early returns *)
-val try_catchSR : forall 'regs 'a 'r 'e1 'e2. monadSR 'regs 'a 'r 'e1 -> ('e1 -> monadSR 'regs 'a 'r 'e2) -> monadSR 'regs 'a 'r 'e2
-let try_catchSR m h =
+val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) -> monadRS 'regs 'a 'r 'e2
+let try_catchRS m h =
try_catchS m
(function
| Left r -> throwS (Left r)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:47:44 +0000