diff options
| author | Brian Campbell | 2019-09-16 13:27:02 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-09-19 17:03:06 +0100 |
| commit | 79f3f95d6b9b589867560ee9be267df5866afadd (patch) | |
| tree | 38e09c8aed3dd36d7b658fd1467ff85c6042ffb8 /lib/coq/Sail2_state_monad.v | |
| parent | 4e1724e9c8856e38fd9683c018a43a434bf53565 (diff) | |
Expand Coq Hoare logic and congruence rules to more operators
Also tweak the informative and/or boolean definitions so that they use
the same proofs in both monads.
Diffstat (limited to 'lib/coq/Sail2_state_monad.v')
| -rw-r--r-- | lib/coq/Sail2_state_monad.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v index 552fa68e..bf5c5916 100644 --- a/lib/coq/Sail2_state_monad.v +++ b/lib/coq/Sail2_state_monad.v @@ -108,6 +108,9 @@ fun s => Definition assert_expS {Regs E} (exp : bool) (msg : string) : monadS Regs unit E := if exp then returnS tt else failS msg. +Definition assert_expS' {Regs E} (exp : bool) (msg : string) : monadS Regs (exp = true) E := + if exp return monadS Regs (exp = true) E then returnS eq_refl else failS msg. + (* For early return, we abuse exceptions by throwing and catching the return value. The exception type is "either 'r 'e", where "Right e" represents a proper exception and "Left r" an early return of value "r". *) |