# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1575935831 -32400
# Node ID dd66b94bf36510b2ef2369e29e4e3cf8eb6c8e52
# Parent  816b44e5e6740523cbc698def05fd097fa18b496
loop causes agda inifinite loop

diff -r 816b44e5e674 -r dd66b94bf365 whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 09 19:17:01 2019 +0900
+++ b/whileTestGears.agda	Tue Dec 10 08:57:11 2019 +0900
@@ -94,32 +94,91 @@
 proofGears : {c10 :  ℕ } → Set
 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
-proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
-proofGearsMeta {c10} = {!!}
+-- proofGearsMeta : {c10 :  ℕ } → whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
+-- proofGearsMeta {c10} = {!!}
+
+data whileTestState (c10 : ℕ ) : Set where
+  error : whileTestState c10
+  state1 : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10
+  state2 : (env : Env) → (varn env + vari env ≡ c10) → whileTestState c10
+  finstate : (env : Env)  → ((vari env) ≡ c10 ) → whileTestState c10
+
+whileLoopProof0 : {c10 : ℕ } → Set
+whileLoopProof0 {c10 } = Env /\ whileTestState c10 → whileLoop {!!} ( λ env → vari env ≡ c10 )  
+whileTestProof0 : {c10 : ℕ } → Set
+whileTestProof0 {c10} = Env /\ whileTestState c10 → whileTest c10 (λ env →  {!!} )
+
+proofGearsState : {c10 :  ℕ } → whileTestProof0
+proofGearsState {c10} = {!!}  where 
+  lemma1 : (env : Env ) →  vari env ≡ c10
+  lemma1 = {!!}
 
-data whileTestState : Set where
-  
-  state1 : whileTestState
-  state2 : whileTestState
-  finstate : whileTestState
+record Context : Set where
+   field 
+     c10 : ℕ
+     whileDG : Env
+     whileCond : whileTestState c10
+
+open Context
+
+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}} )
+
+{-# TERMINATING #-}
+whileLoopContext : {l : Level} {t : Set l} -> Context -> (Code : Context -> t) -> t
+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} } )  next
+
+{-# TERMINATING #-}
+whileLoopStep : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) (Code : Env -> t) -> t
+whileLoopStep env next exit with lt 0 (varn env)
+whileLoopStep env next exit | false = exit env
+whileLoopStep env next exit | true =
+    next (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) 
 
-record whileTestCondition  (c10 : ℕ)  (t : whileTestState)  : Set where
-  coinductive
-  field
-    fincase : (env : Env) → (t ≡ finstate)  → (vari env ≡ c10)
-    case1 : (env : Env)  → (t ≡ state1) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestCondition c10 state2
-    case2 : (env : Env) → (t ≡ state2)  → (varn env + vari env ≡ c10) → whileTestCondition c10 state2
+whileTestProof : {l : Level} {t : Set l} -> Context → (Code : Context -> t) -> t
+whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } where
+    out : Env 
+    out =  whileTest (c10 cxt) ( λ e → e ) 
+    init : whileTestState (c10 cxt)
+    init = state1 out record { pi1 = refl ; pi2 = refl }
 
-open whileTestCondition
+{-# 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
 
-test2 : (c10 : ℕ) → whileTestCondition c10 state1 → whileTestCondition c10 state2 
-test2 c10 cond1 = whileTest 10 (λ env  → whileLoop env (λ env1 → {!!}))
-  where    
-    whileLoopCond : (e env1 : Env) → varn env1 + vari env1 ≡ c10 → varn e + vari e ≡ c10 → whileTestCondition c10 state2
-    whileLoopCond = {!!}
-    proof3 : (env env1 : Env) → whileTestCondition c10 finstate
-    fincase (proof3 env env1) = {!!}
-    case1 (proof3 env env1 ) e ()
-    case2 (proof3 env env1 ) e ()
+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
 
--- conversion1 e {c10} (case2  (case1 cond1 ? ? ?)) {!!}
+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) {!!} 
+    ... | _ = error
+
+{-# TERMINATING #-}
+loop : {l : Level} {t : Set l} -> Context -> (exit : Context -> t) -> t
+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
+