module hoare-while where

open import Data.Nat
open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary

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

whileTestP : {l : Level} {t : Set l} → (c10 : ℕ) → (next : 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 (varn env)
... | zero = exit env
... | suc n = exit (record env { varn = n ; vari = (suc n) })


{-# TERMINATING #-}
loopP : {l : Level} {t : Set l} → Envc → (exit : Envc → t) → t
loopP env exit = whileLoopP env (λ env → loopP env exit ) exit

whileTestPCall : (c10 :  ℕ ) → Envc
whileTestPCall c10 = whileTestP {_} {_} c10 (λ env → loopP env (λ env →  env))

---
open import Data.Empty
--open import Relation.Nullary using (¬_; Dec; yes; no)

--open import Agda.Builtin.Unit
open import utilities

open import Relation.Binary.PropositionalEquality

open _/\_

data whileTestState  : Set where
  s1 : whileTestState
  s2 : whileTestState
  sf : whileTestState

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)

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 )

whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
    → (next : (env : Envc ) → whileTestStateP s2 env  → t)
    → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
whileLoopPwP env s next exit with <-cmp 0 (varn env)
whileLoopPwP env s next exit | tri≈ ¬a b ¬c = exit env (lem (sym b) s)
  where
    lem : (varn env ≡ 0) → (varn env + vari env ≡ c10 env) → vari env ≡ c10 env
    lem refl refl = refl
whileLoopPwP env s next exit | tri< a ¬b ¬c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
  where
    1<0 : 1 ≤ zero → ⊥
    1<0 ()
    proof5 : (suc zero  ≤ (varn  env))  → ((varn env ) - 1) + (vari env + 1) ≡ c10 env
    proof5 (s≤s lt) with varn  env
    proof5 (s≤s z≤n) | zero = ⊥-elim (1<0 a)
    proof5 (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
      ≡⟨ s  ⟩
         c10 env
      ∎


whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc ) → (n ≡ varn env) → whileTestStateP s2 env
  → (next : (env : Envc ) → (pred n ≡ varn env) → whileTestStateP s2 env  → t)
  → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
whileLoopPwP' zero env refl refl next exit = exit env refl
whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env))



whileTestPSemSound : (c : ℕ ) (output : Envc ) → output ≡ whileTestP c (λ e → e) → ⊤ implies ((vari output ≡ 0) /\ (varn output ≡ c))
whileTestPSemSound c output refl = whileTestPSem c