diff options
| author | Thomas Bauereiss | 2018-03-05 12:13:16 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-03-05 15:44:58 +0000 |
| commit | 21bb415d3c148361033576af6093f72f49d92866 (patch) | |
| tree | 53d87a289a6b089c4da9644a16e43086f17c05b3 /src/gen_lib/state_monad.lem | |
| parent | ea2ff78cf675298df64e8ebacca7156b68f3c5c8 (diff) | |
Add support for undefined bit oracle to Lem shallow embedding
Add an Undefined outcome to the prompt monad that asks the environment for a
Boolean value. For the state monad, add fields for a random generator and a
seed (currently of type nat) to the state.
Diffstat (limited to 'src/gen_lib/state_monad.lem')
| -rw-r--r-- | src/gen_lib/state_monad.lem | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem index 8ff39d62..26179244 100644 --- a/src/gen_lib/state_monad.lem +++ b/src/gen_lib/state_monad.lem @@ -13,15 +13,20 @@ type sequential_state 'regs = memstate : memstate; tagstate : tagstate; write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool|> + last_exclusive_operation_was_load : bool; + (* Random bool generator for use as an undefined bit oracle *) + next_bool : nat -> (bool * nat); + seed : nat |> -val init_state : forall 'regs. 'regs -> sequential_state 'regs -let init_state regs = +val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs +let init_state regs o s = <| regstate = regs; memstate = Map.empty; tagstate = Map.empty; write_ea = Nothing; - last_exclusive_operation_was_load = false |> + last_exclusive_operation_was_load = false; + next_bool = o; + seed = s |> type ex 'e = | Failure of string @@ -63,6 +68,12 @@ let updateS f = (fun s -> returnS () (f s)) val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e let failS msg s = [(Ex (Failure msg), s)] +val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e +let undefined_boolS () = + readS (fun s -> s.next_bool (s.seed)) >>$= (fun (b, seed) -> + updateS (fun s -> <| s with seed = seed |>) >>$ + returnS b) + val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e let exitS () = failS "exit" |