module whileTest where

open import Data.Nat
open import Data.Bool hiding (_≟_)
open import Data.Product
open import Relation.Nullary
open import Relation.Binary
open import SET


record Env : Set where
  field
    varn : ℕ
    vari : ℕ
open Env

neg : (Env → Bool) → (Env → Bool)
neg x e = not (x e)

and : (Env → Bool) → (Env → Bool)  → (Env → Bool)
and x y e = (x e) ∧ (y e)

enveq : (Env → Bool) → (Env → Bool) → Set
enveq x y = {!!}

sem : (Env → Bool) → Pred Env
sem x y = {!!}

tautValid : (b1 b2 : Env → Bool) -> enveq b1 b2 ->
                 (s : Env) -> sem b1 s -> sem b2 s
tautValid = {!!}

respNeg : (b : Env → Bool) -> (s : Env) ->
               Iff (sem (neg b) s) (¬ sem b s)
respNeg = {!!}               

respAnd : (b1 b2 : Env → Bool) -> (s : Env) ->
               Iff (sem (and b1 b2) s)
                   ((sem b1 s) ×  (sem b2 s))
respAnd = {!!}

PrimSemComm : ∀ {l} -> (Env → Env) -> Rel Env l
PrimSemComm = {!!}

Axiom :( Env → Bool) -> (Env → Env) -> (Env → Bool) -> Set
Axiom = {!!}

axiomValid : ∀ {l} -> (bPre : Env → Bool ) -> (pcm : (Env → Env)) -> (bPost : Env → Bool) ->
                  (ax : Axiom bPre pcm bPost) -> (s1 s2 : Env) ->
                  sem bPre s1 -> PrimSemComm {l} pcm s1 s2 -> sem bPost s2
axiomValid = {!!}

open import Hoare (Env → Bool) (Env → Env) neg and enveq Env sem  tautValid
                  respNeg respAnd PrimSemComm Axiom axiomValid

lt : ℕ → ℕ → Bool
lt x y with x <? y
lt x y | yes p = true
lt x y | no ¬p = false

_-_ : ℕ → ℕ → ℕ
x - zero = x
zero - (suc _) = zero
(suc x) - (suc y) = x - y

_==_ : ℕ → ℕ → Bool
x == y with x ≟ y
(x == y) | yes p = true
(x == y) | no ¬p = false


program : Comm
program = 
    Seq ( PComm (λ env → record env {varn = 10}))
    (Seq ( PComm (λ env → record env {vari = 0}))
    (While (λ env → lt 0 (varn env) )
      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
        (PComm (λ env → record env {varn = ((varn env) - 1)} )))))

{-# TERMINATING #-}
interpret : Env → Comm → Env
interpret env Skip = env
interpret env Abort = env
interpret env (PComm  x) = x env
interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
interpret env (If x then else) with x env
... | true = interpret env then
... | false = interpret env else
interpret env (While x comm) with x env
... | true = interpret (interpret env comm) (While x comm)
... | false = env

test1 = interpret (record {vari = 0 ; varn = 0}) program

initCond : Env → Bool
initCond _ = true

termCond : Env → Bool
termCond env = (vari env) == 10


proof1 : HTProof initCond program termCond
proof1 = {!!}