# HG changeset patch
# User ryokka
# Date 1577176086 -32400
# Node ID 57d5a3884898da7ae7dee67757a454d8a9018937
# Parent  fdd31b6808dba31d3dbdd5b7ac700f5f089d5386
fix whileLoopPSem

diff -r fdd31b6808db -r 57d5a3884898 whileTestGears.agda
--- a/whileTestGears.agda	Mon Dec 23 18:20:42 2019 +0900
+++ b/whileTestGears.agda	Tue Dec 24 17:28:06 2019 +0900
@@ -103,7 +103,7 @@
 --      openended Env c  <=>  Context
 --
 
-open import Relation.Nullary
+open import Relation.Nullary hiding (proof)
 open import Relation.Binary
 
 record Envc : Set (succ Zero) where
@@ -111,7 +111,7 @@
     c10 : ℕ
     varn : ℕ
     vari : ℕ
-open Envc 
+open Envc
 
 whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (Code : Envc → t) → t
 whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )
@@ -119,8 +119,16 @@
 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 }) 
+whileLoopP env next exit | tri< a ¬b ¬c =
+     next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
+
+whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
+whileLoopP' env@record { c10 = c10 ; varn = varn ; vari = zero } next exit = exit env
+whileLoopP' env@record { c10 = c10 ; varn = varn ; vari = (suc vari₁) } next exit = next (record env {varn = varn - 1 ; vari = (suc vari₁) + 1 })
+
+-- 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} → Envc → (exit : Envc → t) → t
@@ -194,27 +202,32 @@
 GearsUnitSound e0 e1 f fsem = fsem e0
 
 whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
-whileTestPSemSound c output refl = whileTestPSem c 
+whileTestPSemSound c output refl = whileTestPSem c
 
 whileLoopPSem : {l : Level} {t : Set l}   → (input : Envc ) → whileTestStateP s2 input
     → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
     → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)  → t) → t
 whileLoopPSem env s next exit with <-cmp 0 (varn env)
-whileLoopPSem env s next exit | tri≈ ¬a b ¬c = {!!}
-whileLoopPSem env s next exit | tri< a ¬b ¬c  = {!!}
+whileLoopPSem env s next exit | tri≈ ¬a b ¬c rewrite (sym b) = exit env (proof (λ z → z))
+whileLoopPSem env s next exit | tri< a ¬b ¬c  = next env (proof (λ z → z))
 
+{-# TERMINATING #-}
 loopPP : (input : Envc ) → Envc
-loopPP input with <-cmp 0 (varn input )
+loopPP input with <-cmp 0 (varn input)
 loopPP input | tri≈ ¬a b ¬c = input
-loopPP input | tri< a ¬b ¬c = {!!} -- loopPP (whileLoopP ?
+loopPP input | tri< a ¬b ¬c = loopPP (whileLoopP input (λ next → loopPP next) (λ output → output))
+
+
 -- = whileLoopP input (λ next → loopPP next ) (λ output → output )
 
 whileLoopPSemSound : (input output : Envc )
    → whileTestStateP s2 input
    →  output ≡ loopPP input
+   -- (whileLoopP input (λ tt → whileLoopP tt {!!} {!!}) {!!}) ← y-conbinater
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
-whileLoopPSemSound input output pre refl with <-cmp 0 (varn input )
-... | ttt = {!!}
+whileLoopPSemSound input output pre eq = whileLoopPSem input pre {!!} {!!} -- proof (whileLoopPwP input pre (λ e p1 p11 → {!!}) (λ e2 p2 p22 → {!!}) )
+-- with <-cmp 0 (varn input )
+-- ... | ttt = {!!}
 
 -- induction にする
 {-# TERMINATING #-}