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 : @$\mathbb{N}$@
    varn : @$\mathbb{N}$@
    vari : @$\mathbb{N}$@
open Envc

whileTestP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
whileTestP c10 next = next (record {varn = c10 ; vari = 0 ; c10 = c10 } )

whileLoopP : {l : Level} {t : Set l} @$\rightarrow$@ Envc @$\rightarrow$@ (next : Envc @$\rightarrow$@ t) @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ 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} @$\rightarrow$@ Envc @$\rightarrow$@ (exit : Envc @$\rightarrow$@ t) @$\rightarrow$@ t
loopP env exit = whileLoopP env (@$\lambda$@ env @$\rightarrow$@ loopP env exit ) exit

whileTestPCall : (c10 :  @$\mathbb{N}$@ ) @$\rightarrow$@ Envc
whileTestPCall c10 = whileTestP {_} {_} c10 (@$\lambda$@ env @$\rightarrow$@ loopP env (@$\lambda$@ env @$\rightarrow$@  env))

---
open import Data.Empty
--open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)

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

open import Relation.Binary.PropositionalEquality

open _@$\wedge$@_

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

whileTestStateP : whileTestState @$\rightarrow$@ Envc @$\rightarrow$@  Set
whileTestStateP s1 env = (vari env @$\equiv$@ 0) @$\wedge$@ (varn env @$\equiv$@ c10 env)
whileTestStateP s2 env = (varn env + vari env @$\equiv$@ c10 env)
whileTestStateP sf env = (vari env @$\equiv$@ c10 env)

whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t
whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
   env : Envc
   env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env )

whileLoopPwP : {l : Level} {t : Set l}   @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env
    @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ whileTestStateP s2 env  @$\rightarrow$@ t)
    @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env  @$\rightarrow$@ t) @$\rightarrow$@ t
whileLoopPwP env s next exit with <-cmp 0 (varn env)
whileLoopPwP env s next exit | tri≈ @$\neg$@a b @$\neg$@c = exit env (lem (sym b) s)
  where
    lem : (varn env @$\equiv$@ 0) @$\rightarrow$@ (varn env + vari env @$\equiv$@ c10 env) @$\rightarrow$@ vari env @$\equiv$@ c10 env
    lem refl refl = refl
whileLoopPwP env s next exit | tri< a @$\neg$@b @$\neg$@c  = next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 }) (proof5 a)
  where
    1<0 : 1 @$\leq$@ zero @$\rightarrow$@ @$\bot$@
    1<0 ()
    proof5 : (suc zero  @$\leq$@ (varn  env))  @$\rightarrow$@ ((varn env ) - 1) + (vari env + 1) @$\equiv$@ c10 env
    proof5 (s@$\leq$@s lt) with varn  env
    proof5 (s@$\leq$@s z@$\leq$@n) | zero = @$\bot$@-elim (1<0 a)
    proof5 (s@$\leq$@s (z@$\leq$@n {n'}) ) | suc n = let open @$\equiv$@-Reasoning in
      begin
        n' + (vari env + 1)
      @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ n' + z ) ( +-sym  {vari env} {1} )  @$\rangle$@
        n' + (1 + vari env )
      @$\equiv$@@$\langle$@ sym ( +-assoc (n')  1 (vari env) ) @$\rangle$@
        (n' + 1) + vari env
      @$\equiv$@@$\langle$@ cong ( @$\lambda$@ z @$\rightarrow$@ z + vari env )  +1@$\equiv$@suc  @$\rangle$@
        (suc n' ) + vari env
      @$\equiv$@@$\langle$@@$\rangle$@
        varn env + vari env
      @$\equiv$@@$\langle$@ s  @$\rangle$@
         c10 env
      @$\blacksquare$@


whileLoopPwP' : {l : Level} {t : Set l} @$\rightarrow$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ (env : Envc ) @$\rightarrow$@ (n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env
  @$\rightarrow$@ (next : (env : Envc ) @$\rightarrow$@ (pred n @$\equiv$@ varn env) @$\rightarrow$@ whileTestStateP s2 env  @$\rightarrow$@ t)
  @$\rightarrow$@ (exit : (env : Envc ) @$\rightarrow$@ whileTestStateP sf env  @$\rightarrow$@ t) @$\rightarrow$@ 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 : @$\mathbb{N}$@ ) (output : Envc ) @$\rightarrow$@ output @$\equiv$@ whileTestP c (@$\lambda$@ e @$\rightarrow$@ e) @$\rightarrow$@ @$\top$@ implies ((vari output @$\equiv$@ 0) @$\wedge$@ (varn output @$\equiv$@ c))
whileTestPSemSound c output refl = whileTestPSem c