diff options
| author | Thomas Bauereiss | 2018-06-22 19:03:02 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-07-09 14:38:51 +0100 |
| commit | edc2be164fcf53c333796e55b93f94bf6c9ed152 (patch) | |
| tree | e1ac424b8d6ee3ca7a5264bd7067c06fba283c9d /lib/hol/prompt.lem | |
| parent | a6770dbaf3231a8a8050cea588eb186ab8b36a77 (diff) | |
Simplify treating of undefined_bool in Lem library
Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state. The previous behaviour can be
implemented as Sail code, if desired.
Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.
Diffstat (limited to 'lib/hol/prompt.lem')
| -rw-r--r-- | lib/hol/prompt.lem | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/hol/prompt.lem b/lib/hol/prompt.lem index edbd3752..3597fa06 100644 --- a/lib/hol/prompt.lem +++ b/lib/hol/prompt.lem @@ -3,12 +3,12 @@ open import State_monad open import State let inline undefined_bool = undefined_boolS -let inline bool_of_bitU_oracle = bool_of_bitU_oracleS +let inline bool_of_bitU_nondet = bool_of_bitU_nondetS let inline bool_of_bitU_fail = bool_of_bitU_fail -let inline bools_of_bits_oracle = bools_of_bits_oracleS -let inline of_bits_oracle = of_bits_oracleS +let inline bools_of_bits_nondet = bools_of_bits_nondetS +let inline of_bits_nondet = of_bits_nondetS let inline of_bits_fail = of_bits_failS -let inline mword_oracle = mword_oracleS +let inline mword_nondet = mword_nondetS let inline reg_deref = read_regS let inline foreachM = foreachS |