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 = {!!}
 
 
 
 
 
 
-
-