--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/whileTestPrim.agda	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,71 @@
+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)
+
+
+tests : Env
+tests =  interpret ( record { vari = 0  ; varn = 0 } ) (simple 10)