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

diff -r 107cd3825e61 -r 8813f26da3b7 whileTestGears.agda
--- a/whileTestGears.agda	Sun Dec 15 10:18:26 2019 +0900
+++ b/whileTestGears.agda	Sun Dec 15 12:29:13 2019 +0900
@@ -10,35 +10,36 @@
 open import utilities
 open  _/\_
 
-record Env  : Set where
+record Env : Set (succ Zero) where
   field
     varn : ℕ
     vari : ℕ
-open Env
+    cx : Set
+open Env 
 
-whileTest : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
-whileTest c10 next = next (record {varn = c10 ; vari = 0} )
+whileTest : {l : Level} {t : Set l} (c : Set ) → (c10 : ℕ) → (Code : Env → t) → t
+whileTest c c10 next = next (record {varn = c10 ; vari = 0 ; cx = c} )
 
 {-# TERMINATING #-}
 whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
 whileLoop env next with lt 0 (varn env)
 whileLoop env next | false = next env
 whileLoop env next | true =
-    whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
+    whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
 
-test1 : Env
-test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))
+test1 : (c : Set ) → Env 
+test1 c = whileTest c 10 (λ env → whileLoop env (λ env1 → env1 ))
 
 
-proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
-proof1 = refl
+proof1 : (c : Set ) → whileTest c 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
+proof1 c = refl
 
 --                                                                              ↓PostCondition
-whileTest' : {l : Level} {t : Set l}  → {c10 :  ℕ } → (Code : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
-whileTest' {_} {_} {c10} next = next env proof2
+whileTest' : {l : Level} {t : Set l}  →  {c : Set} → {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
+whileTest' {_} {_} {c} {c10} next = next env proof2
   where
-    env : Env
-    env = record {vari = 0 ; varn = c10}
+    env : Env 
+    env = record {vari = 0 ; varn = c10 ; cx = c }
     proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
     proof2 = record {pi1 = refl ; pi2 = refl}
 
@@ -47,35 +48,36 @@
 
 
 {-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
-whileLoop' : {l : Level} {t : Set l} → (env : Env) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env → t) → t
+whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env  → t) → t
 whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
 whileLoop' env proof next | no p = next env 
 whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next
     where
-      env1 = record {varn = (varn  env) - 1 ; vari = (vari env) + 1}
+      env1 = record env {varn = (varn  env) - 1 ; vari = (vari env) + 1}
       1<0 : 1 ≤ zero → ⊥
       1<0 ()
       proof3 : (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
-      proof3 (s≤s lt) with varn  env
-      proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
-      proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
-          begin
-             n' + (vari env + 1) 
-          ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
-             n' + (1 + vari env ) 
-          ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
-             (n' + 1) + vari env 
-          ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
-             (suc n' ) + vari env 
-          ≡⟨⟩
-             varn env + vari env
-          ≡⟨ proof  ⟩
-             c10
-          ∎
+      proof3 = {!!}
+      -- proof3 (s≤s lt) with varn  env
+      -- proof3 (s≤s z≤n) | zero = ⊥-elim (1<0 p)
+      -- proof3 (s≤s (z≤n {n'}) ) | suc n =  let open ≡-Reasoning  in
+      --     begin
+      --        n' + (vari env + 1) 
+      --     ≡⟨ cong ( λ z → n' + z ) ( +-sym  {vari env} {1} )  ⟩
+      --        n' + (1 + vari env ) 
+      --     ≡⟨ sym ( +-assoc (n')  1 (vari env) ) ⟩
+      --        (n' + 1) + vari env 
+      --     ≡⟨ cong ( λ z → z + vari env )  +1≡suc  ⟩
+      --        (suc n' ) + vari env 
+      --     ≡⟨⟩
+      --        varn env + vari env
+      --     ≡⟨ proof  ⟩
+      --        c10
+      --     ∎
 
 -- Condition to Invaliant
-conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
-               → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t
+conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
+               → (Code : (env1 : Env ) → (varn env1 + vari env1 ≡ c10) → t) → t
 conversion1 env {c10} p1 next = next env proof4
    where
       proof4 : varn env + vari env ≡ c10
@@ -91,8 +93,8 @@
           ∎
 
 
-proofGears : {c10 :  ℕ } → Set
-proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+proofGears : {c10 :  ℕ } → Set → Set
+proofGears {c10} c = whileTest' {_} {_} {c} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
 data whileTestState (c10 : ℕ ) (env : Env ) : Set where
   error : whileTestState c10 env
@@ -101,13 +103,13 @@
   finstate : ((vari env) ≡ c10 ) → whileTestState c10 env
 
 --
---      openended Env  <=>  Context
+--      openended Env c  <=>  Context
 --
 
-record Context : Set where
+record Context : Set (succ Zero) where
    field 
      c10 : ℕ
-     whileDG : Env
+     whileDG : Env 
      whileCond : whileTestState c10 whileDG
 
 open Context
@@ -133,7 +135,7 @@
 whileLoopContext cxt next with lt 0 (varn (whileDG cxt) )
 whileLoopContext cxt next | false = next cxt
 whileLoopContext cxt next | true =
-    whileLoopContext (record cxt { whileDG = record {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = state2 (proof cxt) } )  next
+    whileLoopContext (record cxt { whileDG = record (whileDG cxt) {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = state2 (proof cxt) } )  next
       where
         proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
         proof cxt = {!!} 
@@ -142,13 +144,13 @@
 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 
-whileLoopStep env next exit | tri< gt ¬eq _  = next record {varn = (varn env) - 1 ; vari = (vari env) + 1} 
+whileLoopStep env next exit | tri< gt ¬eq _  = next record env {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
 whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } i!=n where
     out : Env 
-    out =  whileTest (c10 cxt) ( λ e → e ) 
+    out =  whileTest {!!} (c10 cxt) ( λ e → e ) 
     init : whileTestState (c10 cxt) out
     init = state1 record { pi1 = refl ; pi2 = refl }
     i!=n : ¬ vari out ≡ varn out
@@ -203,12 +205,12 @@
     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' = ?
+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 i!=n
-    $ λ cxt i+n=c10 → loopProof cxt whileDec ?
-    $ λ cxt _ → ? 
+    $ λ cxt i+n=c10 → loopProof cxt whileDec {!!} -- whileLoopProof'
+    $ λ cxt _ → {!!} 
 proofWhileGear c cxt = {!!}