# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1575937154 -32400
# Node ID 600b4e914071a8e56f01b043a74e218a32680b11
# Parent  dd66b94bf36510b2ef2369e29e4e3cf8eb6c8e52
fix loop

diff -r dd66b94bf365 -r 600b4e914071 whileTestGears.agda
--- a/whileTestGears.agda	Tue Dec 10 08:57:11 2019 +0900
+++ b/whileTestGears.agda	Tue Dec 10 09:19:14 2019 +0900
@@ -147,38 +147,32 @@
 
 {-# TERMINATING #-}
 whileLoopProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) (Code : Context -> t) -> t
-whileLoopProof cxt next exit = next record cxt { whileDG = out ; whileCond = postCond }  where
-    out : Env 
-    out =  whileLoopStep (whileDG cxt) ( λ e → e ) {!!}
-    postCond : whileTestState (c10 cxt) 
-    postCond with whileCond cxt
-    ... | state2 e inv = state2 out {!!} where
-       proof3 : {!!} 
-       proof3 = {!!}
-    ... | _ = error
+whileLoopProof cxt next exit = whileLoopStep (whileDG cxt)
+    ( λ env → next record cxt { whileDG = env ; whileCond = nextCond env } )  
+    ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env } )   where
+        nextCond : Env → whileTestState (c10 cxt)
+        nextCond nenv with whileCond cxt
+        ... | state2 e inv = state2 (whileDG cxt) {!!}
+        ... | _ = error
+        exitCond : Env → whileTestState (c10 cxt)
+        exitCond nenv with whileCond cxt
+        ... | state2 e inv = finstate (whileDG cxt) {!!}
+        ... | _ = error
 
 whileConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
 whileConvProof cxt next = next record cxt { whileCond = postCond } where
     postCond : whileTestState (c10 cxt)
     postCond with whileCond cxt
-    ... | state1 e inv = state2 (whileDG cxt) {!!} 
-    ... | _ = error
-
-whileFinConvProof : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
-whileFinConvProof cxt next = next record cxt { whileCond = postCond } where
-    postCond : whileTestState (c10 cxt)
-    postCond with whileCond cxt
-    ... | state2 e inv = finstate (whileDG cxt) {!!} 
+    ... | state1 e inv = state2 (whileDG cxt) {!!}
     ... | _ = error
 
 {-# TERMINATING #-}
 loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t
-loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit) exit
+loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
 
 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })
     $ λ cxt → whileConvProof cxt 
     $ λ cxt → loop cxt 
-    $ λ cxt → whileFinConvProof cxt
     $ λ cxt → vari (whileDG cxt) ≡ c10 cxt
-proofWhileGear cxt = refl
+proofWhileGear cxt = {!!}