# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576372706 -32400
# Node ID 107cd3825e6116e19b21aa590e10d67983431bbe
# Parent  a9cac7960e81e1d5d489e6c3178bdb86b88bab57
...

diff -r a9cac7960e81 -r 107cd3825e61 whileTestGears.agda
--- a/whileTestGears.agda	Sat Dec 14 21:27:49 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 15 10:18:26 2019 +0900
@@ -100,6 +100,10 @@
   state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
   finstate : ((vari env) ≡ c10 ) → whileTestState c10 env
 
+--
+--      openended Env  <=>  Context
+--
+
 record Context : Set where
    field 
      c10 : ℕ
@@ -108,6 +112,19 @@
 
 open Context
 
+open import Relation.Nullary
+open import Relation.Binary
+
+--
+-- transparency of condition
+--
+
+whileCondP : Env → Set
+whileCondP env = varn env > 0
+
+whileDec : (cxt : Context) → Dec (whileCondP (whileDG cxt))
+whileDec cxt = {!!}
+
 whileTestContext : {l : Level} {t : Set l} → Context → (Code : Context → t) → t
 whileTestContext cxt next = next (record cxt { whileDG = record (whileDG cxt) {varn = c10 cxt ; vari = 0} ; whileCond = {!!} } )
 
@@ -121,15 +138,11 @@
         proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
         proof cxt = {!!} 
 
-open import Relation.Nullary
-open import Relation.Binary
-
-
 {-# TERMINATING #-}
-whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → 1 ≤ varn e → t) (exit : (e : Env) → 0 ≡ varn e  → t) → t
+whileLoopStep : {l : Level} {t : Set l} → Env → (next : (e : Env ) → t) (exit : (e : Env) → t) → t
 whileLoopStep env next exit with <-cmp 0 (varn env)
-whileLoopStep env next exit | tri≈ _ eq _ = exit env eq
-whileLoopStep env next exit | tri< gt ¬eq _  = next env gt
+whileLoopStep env next exit | tri≈ _ eq _ = exit env 
+whileLoopStep env next exit | tri< gt ¬eq _  = next record {varn = (varn env) - 1 ; vari = (vari env) + 1} 
 whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) 
 
 whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t
@@ -142,11 +155,11 @@
     i!=n eq = {!!}
 
 {-# TERMINATING #-}
-whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )
-    → (continue : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) (exit : Context → (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) → t
+whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt) 
+    → (continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
 whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt)
-    ( λ env lt → next record cxt { whileDG = env ; whileCond = {!!} } {!!} ) 
-    ( λ env eq → exit record cxt { whileDG = env ; whileCond = exitCond env eq } {!!} )   where
+    ( λ env → next record cxt { whileDG = env ; whileCond = {!!} } {!!} ) 
+    ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env {!!} } {!!} )   where
         proof5 : (e : Env ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
         proof5 record { varn = .0 ; vari = vari } refl refl = refl
         exitCond : (e : Env ) → 0 ≡ varn e → whileTestState (c10 cxt) e
@@ -173,27 +186,29 @@
     ... | state1 cond = state2 (proof4 (whileDG cxt) cond )
     ... | _ = error
 
--- {-# TERMINATING #-}
--- loop : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) )
---    → (exit : (cxt : Context ) → (vari (whileDG cxt) ≡ varn (whileDG cxt) )  → t) → t
--- loop cxt i!=n exit = whileLoopProof cxt i!=n (λ cxt → loop cxt {!!} {!!} exit ) {!!}
+{-# TERMINATING #-}
+loop : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt) 
+    → (exit : (cxt : Context ) → ¬ whileCondP (whileDG cxt)  → t) → t
+loop cxt i!=n exit = whileLoopProof cxt i!=n (λ cxt → loop cxt {!!} {!!} exit ) {!!}
 
 
 {-# TERMINATING #-}
 loopProof : {l : Level} {t : Set l} {P Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
-           → Inv c → (exit : (c2 : Context) → (P c2) → Inv c2  → t)
-          (f : Context → (exitn : (c2 : Context) → (P c2) → Inv c2  → t) → t) → t
-loopProof {l} {t} {P} {Inv} cxt if inv exit f = lem cxt inv
+          → ( (cont : (c2 : Context) → (P c2) → t) → (exit : (c2 : Context) → ¬ (P c2) → t) → t )
+          → t
+loopProof {l} {t} {P} {Inv} cxt if f = {!!}
   where
-    lem : (c : Context) → Inv c → t
-    lem c inv with if c
-    lem c inv | no ¬p = f c (λ c1 inv1 exit1 → lem c1 exit1 )
-    lem c inv | yes p = exit c p inv
+    lem : (c : Context) → t
+    lem c with if c
+    lem c | no ¬p = {!!} -- f c (λ c1 _ → lem c1 )
+    lem c | yes p = {!!}
         
+whileLoopProof' : {l : Level} {t : Set l} → (cxt : Context ) 
+    → (continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
+whileLoopProof' = ?
 
-
-proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) {!!}
-    $ λ cxt i!=n → whileConvProof cxt {!!}
-    $ λ cxt i+n=c10 → loopProof cxt {!!} {!!} ( whileLoopStep (whileDG cxt) {!!} {!!} )
-    $ λ cxt _ → vari (whileDG cxt) ≡ c10 cxt
+proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 
+    $ λ cxt i!=n → whileConvProof cxt i!=n
+    $ λ cxt i+n=c10 → loopProof cxt whileDec ?
+    $ λ cxt _ → ? 
 proofWhileGear c cxt = {!!}