# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1576825037 -32400
# Node ID 03235251b3a70ba2ce3ff1dfe8e0e518c422db1d
# Parent  0bde332e121598dfb00f3bea44c93232b0276842
discrete state

diff -r 0bde332e1215 -r 03235251b3a7 whileTestGears.agda
--- a/whileTestGears.agda	Thu Dec 19 15:48:11 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 20 15:57:17 2019 +0900
@@ -105,81 +105,63 @@
 open import Relation.Nullary
 open import Relation.Binary
 
-whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Env → t) → t
-whileTestP c10 next = next (record {varn = c10 ; vari = 0 } )
+record Envc : Set (succ Zero) where
+  field
+    c10 : ℕ
+    varn : ℕ
+    vari : ℕ
+open Envc 
 
-whileLoopP : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → t) → t
+whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t
+whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
+
+whileLoopP : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
 whileLoopP env next exit with <-cmp 0 (varn env)
 whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
 whileLoopP env next exit | tri< a ¬b ¬c = 
      next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) 
 
 {-# TERMINATING #-}
-loopP : {l : Level} {t : Set l} → Env → (exit : Env → t) → t
+loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
 loopP env exit = whileLoopP env (λ env → loopP env exit ) exit
 
-whileTestPCall : {c10 :  ℕ } → Set
-whileTestPCall {c10} = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  ( vari env ≡ c10 )))
-
-data whileTestStateP (c10 i n : ℕ ) : Set where
-  pstate1 : (i ≡ 0) /\ (n ≡ c10) → whileTestStateP c10 i n    -- n ≡ c10
-  pstate2 : (0 ≤ n) → (n ≤ c10) → (n + i ≡ c10)        → whileTestStateP c10 i n    -- 0 < n < c10
-  pfinstate : (n ≡ 0 ) → (i ≡ c10 )         → whileTestStateP c10 i n    -- n ≡ 0
+whileTestPCall : (c10 :  ℕ ) → Envc
+whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  env))
 
-record EnvP : Set (succ Zero) where
-  field
-     env : Env
-     c10 : ℕ 
-     cx :  whileTestStateP c10 (vari env) (varn env)
+data whileTestState  : Set where
+  s1 : whileTestState
+  s2 : whileTestState
+  sf : whileTestState
 
-open EnvP
-
-s1 : (c10 : ℕ) → EnvP
-s1 c10 = record {env = record {vari = 0 ; varn = c10} ; c10 = c10 ; cx = pstate1 (record {pi1 = refl ; pi2 = refl})}
+whileTestStateP : whileTestState → Envc →  Set 
+whileTestStateP s1 env = (vari env ≡ 0) /\ (varn env ≡ c10 env) 
+whileTestStateP s2 env = (varn env + vari env ≡ c10 env) 
+whileTestStateP sf env = (vari env ≡ c10 env) 
 
-s2 : (e : EnvP) → varn (env e) > 0 → varn (env e) < c10 e → EnvP
-s2 e n>0 n<c10 with <-cmp 0 (varn (env e))
-s2 e n>0 n<c10 | tri< a ¬b ¬c =
-     record e { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; cx = pstate2 {!!} {!!} {!!} } where
-        s2-1 : 0 ≤ (varn (env e) - 1)
-        s2-1 = {!!}
-s2 e n>0 n<c10 | tri≈ ¬a b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pfinstate {!!} {!!} }
+whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc ) → whileTestStateP s1 env → t) → t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+   env : Envc
+   env = whileTestP c10 ( λ env → env )
 
-s3 : (e : EnvP) → varn (env e) ≡ 0 → vari (env e) ≡ c10 e
-s3 record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl = {!!}
-
-s1ors2 : (e : EnvP) → EnvP
-s1ors2 e = {!!}
+whileLoopPwP : {l : Level} {t : Set l} → Envc
+    → (next : (env : Envc ) → whileTestStateP s2 env  → t)
+    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
+whileLoopPwP env next exit with <-cmp 0 (varn env)
+whileLoopPwP env next exit | tri≈ ¬a b ¬c = exit env {!!}
+whileLoopPwP env next exit | tri< a ¬b ¬c =
+     next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) {!!}
 
-proofs : (c : ℕ) → (λ e → vari (env e) ≡ c10 e ) (s2 {!!} {!!} {!!})
-proofs c = {!!} -- s3 (s2 ({!!}) {!!} {!!}) {!!}
+{-# TERMINATING #-}
+loopPwP : {l : Level} {t : Set l} → Envc → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
+loopPwP env exit = whileLoopPwP env (λ env s → loopPwP env exit ) exit
 
-s3' : (e : EnvP) → varn (env e) ≡ 0 → (ℕ → EnvP → vari (env e) ≡ c10 e) → vari (env e) ≡ c10 e
-s3' record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl proof = {!!}
+whileTestPCallwP : (c10 :  ℕ ) → Set
+whileTestPCallwP c10 = whileTestPwP {_} {_} c10 (λ env → loopPwP env (λ env x x1 → vari env ≡ c10 )) 
 
 
 
-whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t
-whileTestPwithProof {l} {t} c10 next = next record { env = env1 ; c10 = c10 ; cx = cx1 } where
-    env1 : Env
-    env1 = whileTestP c10 ( λ e → e )
-    cx1 : whileTestStateP c10 (vari env1) (varn env1)
-    cx1 = pstate1 record { pi1 = refl ; pi2 = refl }
 
-{-# TERMINATING #-}
-loopPwithProof : {l : Level} {t : Set l} → (e : EnvP ) → (exit : (e : EnvP ) → t ) → t
-loopPwithProof e exit with  <-cmp 0 (varn (env e)) | whileLoopP (env e) (λ e1 → pstate2 {!!} {!!} {!!} ) ( λ env → pfinstate {!!} {!!} )
-loopPwithProof e exit | tri≈ ¬a b ¬c | tt = loopPwithProof {!!} {!!}
-loopPwithProof e exit | tri< a ¬b ¬c | tt = exit {!!}
-
-ConvP : (e : EnvP) → EnvP
-ConvP = {!!}
-
-whileTestPProof : {c :  ℕ } → Set
-whileTestPProof {c} = whileTestPwithProof  c
-    $ λ e → loopPwithProof e (λ e eq → vari (env e) ≡ c10 e ) (ConvP e )
-
-whileTestPProofMeta : {c10 :  ℕ } →  whileTestPProof {c10}
-whileTestPProofMeta {c10} = {!!}
 
 
+
+