changeset 36:320b765a6424

fix loopProof
author ryokka
date Fri, 13 Dec 2019 19:45:34 +0900
parents 7c739972cd26
children 2db6120a02e6
files whileTestGears.agda
diffstat 1 files changed, 11 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Fri Dec 13 19:23:15 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 13 19:45:34 2019 +0900
@@ -176,13 +176,17 @@
 loop cxt exit = whileLoopProof cxt (λ cxt → loop cxt exit ) exit
 
 
-
-loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (d : Dec (P c))
-          → Pre c → (Context → (continue : (c1 : Context) → ¬ (P c1) → Inv c1 → t)
-          → (exit : (c2 : Context) → (P c2) → Post c2  → t) → t)  → t
-loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (false because proof₁) f =
-          loopProof {!!} {!!} {!!}
-loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt (true because proof₁) f = {!!}
+{-# TERMINATING #-}
+loopProof : {l : Level} {t : Set l} {P Pre Post Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
+          → Pre c  → (exit : (c2 : Context) → (P c2) → Post c2  → t)
+          (f : Context → (exit : (c2 : Context) → (P c2) → Post c2  → t) → t) → t
+loopProof {l} {t} {P} {Pre} {Post} {Inv} cxt if pre exit f = lem cxt
+  where
+    lem : (c : Context) → t
+    lem c  with if c
+    lem c | no ¬p = f c exit
+    lem c | yes p = exit c p {!!}
+        
 
 
 proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error })