Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/whileTestPrim.agda @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 module whileTestPrim where
2
3 open import Function
4 open import Data.Nat
5 open import Data.Bool hiding ( _≟_ )
6 open import Level renaming ( suc to succ ; zero to Zero )
7 open import Relation.Nullary using (¬_; Dec; yes; no)
8 open import Relation.Binary.PropositionalEquality
9
10 open import utilities hiding ( _/\_ )
11
12 record Env : Set where
13 field
14 varn : ℕ
15 vari : ℕ
16 open Env
17
18 PrimComm : Set
19 PrimComm = Env → Env
20
21 Cond : Set
22 Cond = (Env → Bool)
23
24 Axiom : Cond -> PrimComm -> Cond -> Set
25 Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true
26
27 Tautology : Cond -> Cond -> Set
28 Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true
29
30 _and_ : Cond -> Cond -> Cond
31 x and y = λ env → x env ∧ y env
32
33 neg : Cond -> Cond
34 neg x = λ env → not ( x env )
35
36 open import Hoare PrimComm Cond Axiom Tautology _and_ neg
37
38 ---------------------------
39
40 program : ℕ → Comm
41 program c10 =
42 Seq ( PComm (λ env → record env {varn = c10}))
43 $ Seq ( PComm (λ env → record env {vari = 0}))
44 $ While (λ env → lt zero (varn env ) )
45 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
46 $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
47
48 simple : ℕ → Comm
49 simple c10 =
50 Seq ( PComm (λ env → record env {varn = c10}))
51 $ PComm (λ env → record env {vari = 0})
52
53 {-# TERMINATING #-}
54 interpret : Env → Comm → Env
55 interpret env Skip = env
56 interpret env Abort = env
57 interpret env (PComm x) = x env
58 interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
59 interpret env (If x then else) with x env
60 ... | true = interpret env then
61 ... | false = interpret env else
62 interpret env (While x comm) with x env
63 ... | true = interpret (interpret env comm) (While x comm)
64 ... | false = env
65
66 test1 : Env
67 test1 = interpret ( record { vari = 0 ; varn = 0 } ) (program 10)
68
69
70 tests : Env
71 tests = interpret ( record { vari = 0 ; varn = 0 } ) (simple 10)