### view whileTestPrim.agda @ 50:2edb44c5bf52

author ryokka Wed, 18 Dec 2019 20:08:58 +0900 e668962ac31a
line wrap: on
line source
```
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)

```