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 (Cxt : Set) : Set (succ Zero) where
  field
    varn : ℕ
    vari : ℕ
    cx : Cxt
open Env  

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

{-# TERMINATING #-}
whileLoop : {l : Level} {t : Set l} {Cxt : Set} {c : Cxt } → Env Cxt → (Code : Env Cxt → 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 : {Cxt : Set }  → (c : Cxt) → Env Cxt 
test1 c = whileTest c 10 (λ env → whileLoop env (λ env1 → env1 ))


proof1 : {Cxt : Set } (c : Cxt ) → whileTest c 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
proof1 c = refl

--                                                                              ↓PostCondition
whileTest' : {l : Level} {t : Set l} {Cxt : Set}  →  {c : Cxt} → {c10 :  ℕ } → (Code : (env : Env Cxt )  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t
whileTest' {_} {_} {Cxt} {c} {c10} next = next env proof2
  where
    env : Env Cxt 
    env = record {vari = 0 ; varn = c10 ; cx = c }
    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} {Cxt : Set} {c : Cxt } → (env : Env Cxt ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env Cxt  → 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 = {!!}
      -- 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 Invaliant
conversion1 : {l : Level} {t : Set l } {Cxt : Set} {c : Cxt } → (env : Env Cxt ) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
               → (Code : (env1 : Env Cxt ) → (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 :  ℕ } → { Cxt : Set } → (c : Cxt ) → Set
proofGears {c10} c = whileTest' {_} {_} {_} {c} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 

record Context (e : Set ) : Set (succ Zero)

data whileTestState {Cxt : Set } (c10 : ℕ ) (env : Env Cxt ) : Set  where
  error : whileTestState c10 env
  state1 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → whileTestState c10 env
  state2 : (varn env + vari env ≡ c10) → whileTestState c10 env
  finstate : ((vari env) ≡ c10 ) → whileTestState c10 env

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

record Context e where
   field 
     c10 : ℕ
     whileDG : Env e
     whileCond : whileTestState c10 whileDG

open Context

open import Relation.Nullary
open import Relation.Binary

--
-- transparency of condition
--

whileCondP : Env {!!} → Set
whileCondP env = varn env > 0

whileDec : (cxt : Context) → Dec (whileCondP (whileDG cxt))
whileDec cxt = {!!}

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

{-# 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 (whileDG cxt) {varn = (varn (whileDG cxt)) - 1 ; vari = (vari (whileDG cxt)) + 1} ; whileCond = state2 (proof cxt) } )  next
      where
        proof : (cxt : Context) → (varn (whileDG cxt) - 1) + (vari (whileDG cxt) + 1) ≡ c10 cxt
        proof cxt = {!!} 

{-# TERMINATING #-}
whileLoopStep : {l : Level} {t : Set l} → Env {!!} → (next : (e : Env {!!} ) → t) (exit : (e : Env {!!} ) → t) → t
whileLoopStep env next exit with <-cmp 0 (varn env)
whileLoopStep env next exit | tri≈ _ eq _ = exit env 
whileLoopStep env next exit | tri< gt ¬eq _  = next record env {varn = (varn env) - 1 ; vari = (vari env) + 1} 
whileLoopStep env next exit | tri> _ _ c  = ⊥-elim (m<n⇒n≢0 {varn env} {0} c refl) 

whileTestProof : {l : Level} {t : Set l} → Context → (Code : (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt) ) → t) → t
whileTestProof cxt next = next record cxt { whileDG = out ; whileCond = init } i!=n where
    out : Env {!!} 
    out =  whileTest {!!} (c10 cxt) ( λ e → e ) 
    init : whileTestState (c10 cxt) out
    init = state1 record { pi1 = refl ; pi2 = refl }
    i!=n : ¬ vari out ≡ varn out
    i!=n eq = {!!}

{-# TERMINATING #-}
whileLoopProof : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt) 
    → (continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
whileLoopProof cxt i!=n next exit = whileLoopStep (whileDG cxt)
    ( λ env → next record cxt { whileDG = env ; whileCond = {!!} } {!!} ) 
    ( λ env → exit record cxt { whileDG = env ; whileCond = exitCond env {!!} } {!!} )   where
        proof5 : (e : Env {!!} ) → varn e + vari e ≡ c10 cxt →  0 ≡ varn e → vari e ≡ c10 cxt
        proof5 record { varn = .0 ; vari = vari } refl refl = refl
        exitCond : (e : Env {!!} ) → 0 ≡ varn e → whileTestState (c10 cxt) e
        exitCond nenv eq1 with whileCond cxt | inspect whileDG cxt
        ... | state2 cond | record { eq = eq2 } = finstate ( proof5 nenv {!!} eq1 )
        ... | _ | _ = error

whileConvProof : {l : Level} {t : Set l} → (cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt))
    → ((cxt : Context ) → ¬ (vari (whileDG cxt) ≡ varn (whileDG cxt)) → t) → t
whileConvProof cxt i!=n next = next record cxt { whileCond = postCond } i!=n where
    proof4 : (e : Env {!!} ) → (vari e ≡ 0) /\ (varn e ≡ c10 cxt)  → varn e + vari e ≡ c10 cxt
    proof4 env p1 = let open ≡-Reasoning  in
          begin
            varn env + vari env
          ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩
            c10 cxt + vari env
          ≡⟨ cong ( λ n → c10 cxt + n ) (pi1 p1 ) ⟩
            c10 cxt + 0
          ≡⟨ +-sym {c10 cxt} {0} ⟩
            c10 cxt 
          ∎
    postCond : whileTestState (c10 cxt) (whileDG cxt)
    postCond with whileCond cxt
    ... | state1 cond = state2 (proof4 (whileDG cxt) cond )
    ... | _ = error

{-# TERMINATING #-}
loop : {l : Level} {t : Set l} → (cxt : Context ) → whileCondP (whileDG cxt) 
    → (exit : (cxt : Context ) → ¬ whileCondP (whileDG cxt)  → t) → t
loop cxt i!=n exit = whileLoopProof cxt i!=n (λ cxt → loop cxt {!!} {!!} exit ) {!!}


{-# TERMINATING #-}
loopProof : {l : Level} {t : Set l} {P Inv : Context → Set } → (c : Context) → (if : (c : Context) → Dec (P c))
          → ( (cont : (c2 : Context) → (P c2) → t) → (exit : (c2 : Context) → ¬ (P c2) → t) → t )
          → t
loopProof {l} {t} {P} {Inv} cxt if f = {!!}
  where
    lem : (c : Context) → t
    lem c with if c
    lem c | no ¬p = {!!} -- f c (λ c1 _ → lem c1 )
    lem c | yes p = {!!}
        
whileLoopProof' : {l : Level} {t : Set l} 
    → (cxt : Context ) → ( continue : (cxt : Context ) → whileCondP (whileDG cxt)  → t) (exit : Context → ¬ whileCondP (whileDG cxt)  → t) → t
whileLoopProof' = {!!}

proofWhileGear : (c : ℕ) (cxt : Context) → whileTestProof (record cxt { c10 = c ; whileCond = error }) 
    $ λ cxt i!=n → whileConvProof cxt i!=n
    $ λ cxt i+n=c10 → loopProof cxt whileDec {!!} -- whileLoopProof'
    $ λ cxt _ → {!!} 
proofWhileGear c cxt = {!!}