module whileTestPrim 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 hiding ( _/\_ )

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

PrimComm : Set
PrimComm = Env → Env

Cond : Set
Cond = (Env → Bool) 

Axiom : Cond -> PrimComm -> Cond -> Set
Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true

Tautology : Cond -> Cond -> Set
Tautology pre post = ∀ (env : Env) →  (pre env)  ⇒ (post env) ≡ true

_and_ :  Cond -> Cond -> Cond
x and y =  λ env → x env ∧ y env 

neg :  Cond -> Cond 
neg x  =  λ env → not ( x env )

open import Hoare PrimComm Cond Axiom Tautology _and_ neg

---------------------------

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

simple : ℕ → Comm
simple c10 = 
    Seq ( PComm (λ env → record env {varn = c10}))
    $  PComm (λ env → record env {vari = 0})

{-# 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 : Env
test1 =  interpret ( record { vari = 0  ; varn = 0 } ) (program 10)

eval-proof : vari test1 ≡ 10
eval-proof = refl

tests : Env
tests =  interpret ( record { vari = 0  ; varn = 0 } ) (simple 10)