changeset 31:600b4e914071

fix loop
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 10 Dec 2019 09:19:14 +0900
parents dd66b94bf365
children bf7c7bd69e35
files whileTestGears.agda
diffstat 1 files changed, 14 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- 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 = {!!}