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/sail_values.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/sail_values.lem')
| -rw-r--r-- | src/gen_lib/sail_values.lem | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index fce595e0..edb8da88 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -622,6 +622,7 @@ type register_ref 'regstate 'regval 'a = of_regval : 'regval -> maybe 'a; regval_of : 'a -> 'regval |> +(* Register accessors: pair of functions for reading and writing register values *) type register_accessors 'regstate 'regval = ((string -> 'regstate -> maybe 'regval) * (string -> 'regval -> 'regstate -> maybe 'regstate)) |