diff options
| author | Alasdair Armstrong | 2019-02-12 18:18:05 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-02-12 18:18:05 +0000 |
| commit | 24fc989891ad266eae642815646294279e2485ca (patch) | |
| tree | d533fc26b5980d1144ee4d7849d3dd0f2a1b0e95 /lib/hol | |
| parent | b847a472a1f853d783d1af5f8eb033b97f33be5b (diff) | |
| parent | 974494b1dda38c1ee5c1502cc6e448e67a7374ac (diff) | |
Merge remote-tracking branch 'origin/asl_flow2' into sail2
Diffstat (limited to 'lib/hol')
| -rw-r--r-- | lib/hol/sail2_prompt.lem | 3 | ||||
| -rw-r--r-- | lib/hol/sail2_prompt_monad.lem | 12 |
2 files changed, 10 insertions, 5 deletions
diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem index 674d4e34..3107d3a5 100644 --- a/lib/hol/sail2_prompt.lem +++ b/lib/hol/sail2_prompt.lem @@ -4,12 +4,13 @@ open import Sail2_state let inline undefined_bool = undefined_boolS let inline bool_of_bitU_nondet = bool_of_bitU_nondetS -let inline bool_of_bitU_fail = bool_of_bitU_fail +let inline bool_of_bitU_fail = Sail2_state.bool_of_bitU_fail 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_nondet = mword_nondetS let inline reg_deref = read_regS +let inline choose msg xs = chooseS xs let inline internal_pick = internal_pickS let inline foreachM = foreachS diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem index 3af931a5..ade12347 100644 --- a/lib/hol/sail2_prompt_monad.lem +++ b/lib/hol/sail2_prompt_monad.lem @@ -22,6 +22,8 @@ let inline bind = bindS let inline (>>=) = (>>$=) let inline (>>) = (>>$) +let inline choose_bool msg = choose_boolS () +let inline undefined_bool = undefined_boolS let inline exit = exitS let inline throw = throwS @@ -34,16 +36,18 @@ let inline try_catchR = try_catchRS let inline maybe_fail = maybe_failS +let inline read_memt_bytes = read_memt_bytesS let inline read_mem_bytes = read_mem_bytesS let inline read_reg = read_regS let inline reg_deref = read_regS +let inline read_memt = read_memtS let inline read_mem = read_memS -let inline read_tag = read_tagS let inline excl_result = excl_resultS let inline write_reg = write_regS -let inline write_tag = write_tagS -let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz) -let inline write_mem_val = write_mem_valS +let inline write_mem_ea wk addr sz = return () +let inline write_memt = write_memtS +let inline write_mem = write_memS let barrier _ = return () +let footprint _ = return () let inline assert_exp = assert_expS |