module whileTestGears where

open import Function
open import Data.Nat
open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_)
open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality

open import utilities
open  _/\_

record Env : Set (succ Zero) where
  field
    varn : ℕ
    vari : ℕ
open Env 

whileTest : {l : Level} {t : Set l}  → (c10 : ℕ) → (Code : Env → t) → t
whileTest c10 next = next (record {varn = c10 ; vari = 0 } )

{-# 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 env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next

test1 : Env 
test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))


proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
proof1 = 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
  where
    env : Env 
    env = record {vari = 0 ; varn = c10 }
    proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) -- PostCondition
    proof2 = record {pi1 = refl ; pi2 = refl}

open import Data.Empty
open import Data.Nat.Properties


{-# TERMINATING #-} --                                                  ↓PreCondition(Invaliant)
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 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
          ∎

-- Condition to Invariant
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
      proof4 = let open ≡-Reasoning  in
          begin
            varn env + vari env
          ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
            c10 + vari env
          ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩
            c10 + 0
          ≡⟨ +-sym {c10} {0} ⟩
            c10
          ∎


proofGears : {c10 :  ℕ } → Set
proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 

-- proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
-- proofGearsMeta {c10} = {!!} -- net yet done

--
--      openended Env c  <=>  Context
--

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 } )

whileLoopP : {l : Level} {t : Set l} → Env → (next : Env → t) → (exit : Env → 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 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

record EnvP : Set (succ Zero) where
  field
     env : Env
     c10 : ℕ 
     cx :  whileTestStateP c10 (vari env) (varn env)

open EnvP

s1 : (c10 : ℕ) → EnvP
s1 c10 = record {env = record {vari = 0 ; varn = c10} ; c10 = c10 ; cx = pstate1 (record {pi1 = refl ; pi2 = refl})}

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 { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pstate2 {!!} {!!} {!!} }
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 {!!} {!!} }

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 = {!!}

proofs : (c : ℕ) (e : EnvP) → vari (env e) ≡ c10 e
proofs c e = s3 (s2 (s1 {!!}) {!!} {!!}) {!!}


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 = whileLoopP (env e) (λ e1 → loopPwithProof record e { env = e1 ; cx = {!!} } exit ) (λ env → exit {!!} ) where
    lemma :  {!!}
    lemma = {!!}

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} = {!!}