diff options
| author | Brian Campbell | 2019-10-24 14:33:57 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-10-24 14:33:57 +0100 |
| commit | 0e2b220ec96cd29471bba9f46a132427bc4b1ac4 (patch) | |
| tree | 812a5a44d3014cde683dc4128f252e2e7910209a /lib/coq/Sail2_state.v | |
| parent | 73475b844cb09f06c78d8f8a426e9de0eeffc367 (diff) | |
Coq: use `abstract` to separate out proofs from definitions
- requires fixpoint definitions containing proofs to be processed in proof
mode (due to a bug in Coq), so change libraries and pretty printing to
do that
- adjust some lemmas to avoid extra evars
Diffstat (limited to 'lib/coq/Sail2_state.v')
| -rw-r--r-- | lib/coq/Sail2_state.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index 7a25cbe9..618ca3a5 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -114,13 +114,15 @@ let rec untilS vars cond body s = if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s *) -Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E := +Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E. +exact ( if Z_ge_dec limit 0 then cond vars >>$= fun cond_val => if cond_val then - body vars >>$= fun vars => whileST' (limit - 1) vars cond body (_limit_reduces acc) + body vars >>$= fun vars => whileST' _ _ _ (limit - 1) vars cond body (_limit_reduces acc) else returnS vars - else failS "Termination limit reached". + else failS "Termination limit reached"). +Defined. Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := let limit := measure vars in @@ -128,12 +130,14 @@ Definition whileST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV b (*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*) -Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E := +Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E. +exact ( if Z_ge_dec limit 0 then body vars >>$= fun vars => cond vars >>$= fun cond_val => - if cond_val then returnS vars else untilST' (limit - 1) vars cond body (_limit_reduces acc) - else failS "Termination limit reached". + if cond_val then returnS vars else untilST' _ _ _ (limit - 1) vars cond body (_limit_reduces acc) + else failS "Termination limit reached"). +Defined. Definition untilST {RV Vars E} (vars : Vars) measure (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E := let limit := measure vars in |