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)