Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestGears.agda @ 54:3adf50622101

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 20 Dec 2019 16:13:52 +0900
parents 03235251b3a7
children 1be7bb658cf0
comparison
equal deleted inserted replaced
53:03235251b3a7 54:3adf50622101
141 whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t 141 whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
142 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where 142 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
143 env : Envc 143 env : Envc
144 env = whileTestP c10 ( λ env → env ) 144 env = whileTestP c10 ( λ env → env )
145 145
146 whileLoopPwP : {l : Level} {t : Set l} → Envc 146 whileLoopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env
147 → (next : (env : Envc ) → whileTestStateP s2 env → t) 147 → (next : (env : Envc ) → whileTestStateP s2 env → t)
148 → (exit : (env : Envc ) → whileTestStateP sf env → t) → t 148 → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
149 whileLoopPwP env next exit with <-cmp 0 (varn env) 149 whileLoopPwP env s next exit with <-cmp 0 (varn env)
150 whileLoopPwP env next exit | tri≈ ¬a b ¬c = exit env {!!} 150 whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env {!!}
151 whileLoopPwP env next exit | tri< a ¬b ¬c = 151 whileLoopPwP env s next exit | tri< a ¬b ¬c =
152 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!} 152 next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!}
153 153
154 {-# TERMINATING #-} 154 {-# TERMINATING #-}
155 loopPwP : {l : Level} {t : Set l} → Envc → (exit : (env : Envc ) → whileTestStateP sf env → t) → t 155 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
156 loopPwP env exit = whileLoopPwP env (λ env s → loopPwP env exit ) exit 156 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
157 157
158 whileTestPCallwP : (c10 : ℕ ) → Set 158 whileTestPCallwP : (c : ℕ ) → Set
159 whileTestPCallwP c10 = whileTestPwP {_} {_} c10 (λ env → loopPwP env (λ env x x1 → vari env ≡ c10 )) 159 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c ) ) where
160 conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
161 conv = {!!}
160 162
161 163
162 164
163 165
164 166
165 167
166
167