Mercurial > hg > Members > ryokka > HoareLogic
changeset 54:3adf50622101
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 20 Dec 2019 16:13:52 +0900 |
| parents | 03235251b3a7 |
| children | 1be7bb658cf0 |
| files | whileTestGears.agda |
| diffstat | 1 files changed, 10 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/whileTestGears.agda Fri Dec 20 15:57:17 2019 +0900 +++ b/whileTestGears.agda Fri Dec 20 16:13:52 2019 +0900 @@ -143,25 +143,25 @@ env : Envc env = whileTestP c10 ( λ env → env ) -whileLoopPwP : {l : Level} {t : Set l} → Envc +whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (next : (env : Envc ) → whileTestStateP s2 env → t) → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -whileLoopPwP env next exit with <-cmp 0 (varn env) -whileLoopPwP env next exit | tri≈ ¬a b ¬c = exit env {!!} -whileLoopPwP env next exit | tri< a ¬b ¬c = +whileLoopPwP env s next exit with <-cmp 0 (varn env) +whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env {!!} +whileLoopPwP env s next exit | tri< a ¬b ¬c = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!} {-# TERMINATING #-} -loopPwP : {l : Level} {t : Set l} → Envc → (exit : (env : Envc ) → whileTestStateP sf env → t) → t -loopPwP env exit = whileLoopPwP env (λ env s → loopPwP env exit ) exit +loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t +loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit -whileTestPCallwP : (c10 : ℕ ) → Set -whileTestPCallwP c10 = whileTestPwP {_} {_} c10 (λ env → loopPwP env (λ env x x1 → vari env ≡ c10 )) +whileTestPCallwP : (c : ℕ ) → Set +whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where + conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env + conv = {!!} - -