module whileTestPrim where

open import Function
open import Data.Nat
open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ )
open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality

open import utilities hiding ( _@$\wedge$@_ )

record Env : Set where
  field
    varn : @$\mathbb{N}$@
    vari : @$\mathbb{N}$@
open Env

PrimComm : Set
PrimComm = Env @$\rightarrow$@ Env

Cond : Set
Cond = (Env @$\rightarrow$@ Bool)

Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set
Axiom pre comm post = @$\forall$@ (env : Env) @$\rightarrow$@  (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true

Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set
Tautology pre post = @$\forall$@ (env : Env) @$\rightarrow$@  (pre env)  @$\Rightarrow$@ (post env) @$\equiv$@ true

_and_ :  Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond
x and y =  @$\lambda$@ env @$\rightarrow$@ x env @$\wedge$@ y env

neg :  Cond @$\rightarrow$@ Cond
neg x  =  @$\lambda$@ env @$\rightarrow$@ not ( x env )

open import Hoare PrimComm Cond Axiom Tautology _and_ neg

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

program : @$\mathbb{N}$@ @$\rightarrow$@ Comm
program c10 =
    Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
    $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}))
    $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) )
      (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} ))
        $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} ))

simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm
simple c10 =
    Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
    $  PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})

{-@$\#$@ TERMINATING @$\#$@-}
interpret : Env @$\rightarrow$@ Comm @$\rightarrow$@ 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)


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