diff options
| author | Alasdair Armstrong | 2018-07-24 18:09:18 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-07-24 18:09:18 +0100 |
| commit | 6b4f407ad34ca7d4d8a89a5a4d401ac80c7413b0 (patch) | |
| tree | ed09b22b7ea4ca20fbcc89b761f1955caea85041 /src/gen_lib/sail2_state_monad.lem | |
| parent | dafb09e7c26840dce3d522fef3cf359729ca5b61 (diff) | |
| parent | 8114501b7b956ee4a98fa8599c7efee62fc19206 (diff) | |
Merge remote-tracking branch 'origin/sail2' into c_fixes
Diffstat (limited to 'src/gen_lib/sail2_state_monad.lem')
| -rw-r--r-- | src/gen_lib/sail2_state_monad.lem | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem index f207699f..30b296cc 100644 --- a/src/gen_lib/sail2_state_monad.lem +++ b/src/gen_lib/sail2_state_monad.lem @@ -13,20 +13,15 @@ type sequential_state 'regs = memstate : memstate; tagstate : tagstate; write_ea : maybe (write_kind * integer * integer); - last_exclusive_operation_was_load : bool; - (* Random bool generator for use as an undefined bit oracle *) - next_bool : nat -> (bool * nat); - seed : nat |> + last_exclusive_operation_was_load : bool |> -val init_state : forall 'regs. 'regs -> (nat -> (bool* nat)) -> nat -> sequential_state 'regs -let init_state regs o s = +val init_state : forall 'regs. 'regs -> sequential_state 'regs +let init_state regs = <| regstate = regs; memstate = Map.empty; tagstate = Map.empty; write_ea = Nothing; - last_exclusive_operation_was_load = false; - next_bool = o; - seed = s |> + last_exclusive_operation_was_load = false |> type ex 'e = | Failure of string @@ -69,10 +64,7 @@ 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) +let undefined_boolS () = chooseS {false; true} val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e let exitS () = failS "exit" |