# HG changeset patch
# User ryokka
# Date 1578748189 -32400
# Node ID 77798ab0e660255c1b7efa2c0a8d02f546aee6ba
# Parent  cf5e6afbeb7c9f35d40dda358e2015096ec43ce6
Wrote Loop Convertion LoopHelper

diff -r cf5e6afbeb7c -r 77798ab0e660 whileTestGears.agda
--- a/whileTestGears.agda	Mon Jan 06 16:02:31 2020 +0900
+++ b/whileTestGears.agda	Sat Jan 11 22:09:49 2020 +0900
@@ -204,32 +204,28 @@
 loopPwP' zero env refl refl exit = exit env refl
 loopPwP' (suc n) env refl refl exit  = whileLoopPwP' (suc n) env refl refl (λ env x y → loopPwP' n env x y exit) exit
 
+
+loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n) → (seq : whileTestStateP s2 env) → loopPwP' n env (sym eq) seq λ env₁ x → (vari env₁ ≡ c10 env₁)
+loopHelper zero env eq refl rewrite eq = refl
+loopHelper (suc n) env eq refl rewrite eq = loopHelper n (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) }) refl (+-suc n (vari env))
+
+
 --  all codtions are correctly connected and required condtion is proved in the continuation
 --      use required condition as t in (env → t) → t
+--
 whileTestPCallwP : (c :  ℕ ) → Set
-whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c )  ) where
+whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c10 env )  ) where
    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
    conv e record { pi1 = refl ; pi2 = refl } = +zero
 
-test : whileTestPCallwP 100
-test = refl
-
--- pt : (c : ℕ) → whileTestPCallwP c
--- pt c with <-cmp 0 c
--- ... | tri≈ ¬a b ¬c = refl
--- ... | tri< a ¬b ¬c = refl
 
 whileTestPCallwP' : (c :  ℕ ) → Set
-whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c )  ) where
+whileTestPCallwP' c = whileTestPwP {_} {_} c (λ env s → loopPwP' (varn env) env refl (conv env s) ( λ env s → vari env ≡ c10 env )  ) where
   conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
   conv e record { pi1 = refl ; pi2 = refl } = +zero
 
-
-{-- Nat だとできるけど 300 あたりから処理に時間がかかる --}
-test' : whileTestPCallwP' 100
-test' = refl
-
-
+helperCallwP : (c : ℕ) → whileTestPCallwP' c
+helperCallwP c = whileTestPwP {_} {_} c (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
 
 --
 -- Using imply relation to make soundness explicit
@@ -297,5 +293,5 @@
 
 
 
-whileTestSound : {l : Level} (c : ℕ) → (output : Envc) → ⊤ →  whileTestStateP sf output
-whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top = implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!}) (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileTestP c (λ e → e)) refl) top))
+-- whileTestSound : {l : Level} (c : ℕ) → (output : Envc) → ⊤ →  whileTestStateP sf output
+-- whileTestSound {l} c record { c10 = c10 ; varn = varn ; vari = vari } top = implies2p (whileLoopPSemSound {l} (record { c10 = c ; varn = c ; vari = zero }) (record { c10 = c10 ; varn = c ; vari = vari}) (+zero) {!!}) (implies2p (whileConvPSemSound {l} (record { c10 = c ; varn = c ; vari = zero })) (implies2p (whileTestPSemSound c (whileTestP c (λ e → e)) refl) top))