|
1
|
1 module whileTestPrim where
|
|
|
2
|
|
|
3 open import Function
|
|
|
4 open import Data.Nat
|
|
|
5 open import Data.Bool hiding ( _@$\stackrel{?}{=}$@_ )
|
|
|
6 open import Level renaming ( suc to succ ; zero to Zero )
|
|
|
7 open import Relation.Nullary using (@$\neg$@_; Dec; yes; no)
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9
|
|
|
10 open import utilities hiding ( _@$\wedge$@_ )
|
|
|
11
|
|
|
12 record Env : Set where
|
|
|
13 field
|
|
|
14 varn : @$\mathbb{N}$@
|
|
|
15 vari : @$\mathbb{N}$@
|
|
|
16 open Env
|
|
|
17
|
|
|
18 PrimComm : Set
|
|
|
19 PrimComm = Env @$\rightarrow$@ Env
|
|
|
20
|
|
|
21 Cond : Set
|
|
|
22 Cond = (Env @$\rightarrow$@ Bool)
|
|
|
23
|
|
|
24 Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set
|
|
|
25 Axiom pre comm post = @$\forall$@ (env : Env) @$\rightarrow$@ (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true
|
|
|
26
|
|
|
27 Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set
|
|
|
28 Tautology pre post = @$\forall$@ (env : Env) @$\rightarrow$@ (pre env) @$\Rightarrow$@ (post env) @$\equiv$@ true
|
|
|
29
|
|
|
30 _and_ : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Cond
|
|
|
31 x and y = @$\lambda$@ env @$\rightarrow$@ x env @$\wedge$@ y env
|
|
|
32
|
|
|
33 neg : Cond @$\rightarrow$@ Cond
|
|
|
34 neg x = @$\lambda$@ env @$\rightarrow$@ not ( x env )
|
|
|
35
|
|
|
36 open import Hoare PrimComm Cond Axiom Tautology _and_ neg
|
|
|
37
|
|
|
38 ---------------------------
|
|
|
39
|
|
|
40 program : @$\mathbb{N}$@ @$\rightarrow$@ Comm
|
|
|
41 program c10 =
|
|
|
42 Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
|
|
|
43 $ Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0}))
|
|
|
44 $ While (@$\lambda$@ env @$\rightarrow$@ lt zero (varn env ) )
|
|
|
45 (Seq (PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = ((vari env) + 1)} ))
|
|
|
46 $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = ((varn env) - 1)} ))
|
|
|
47
|
|
|
48 simple : @$\mathbb{N}$@ @$\rightarrow$@ Comm
|
|
|
49 simple c10 =
|
|
|
50 Seq ( PComm (@$\lambda$@ env @$\rightarrow$@ record env {varn = c10}))
|
|
|
51 $ PComm (@$\lambda$@ env @$\rightarrow$@ record env {vari = 0})
|
|
|
52
|
|
|
53 {-@$\#$@ TERMINATING @$\#$@-}
|
|
|
54 interpret : Env @$\rightarrow$@ Comm @$\rightarrow$@ 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)
|
