Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/agda/hoare-test.agda.replaced @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INIT rbt.agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 07 Nov 2021 00:51:16 +0900
parents 9176dff8f38a
children
comparison
equal deleted inserted replaced
4:72667e8198e2 5:339fb67b4375
1 module hoare-test where 1 module hoare-test where
2 2
3 open import Data.Nat hiding (_@$\sqcup$@_) 3 open import Data.Nat hiding (_!$\sqcup$!_)
4 open import Level renaming ( suc to succ ; zero to Zero ) 4 open import Level renaming ( suc to succ ; zero to Zero )
5 5
6 open import Relation.Binary 6 open import Relation.Binary
7 open import Relation.Binary.PropositionalEquality 7 open import Relation.Binary.PropositionalEquality
8 8
10 10
11 open import Data.Nat.Properties as NatProp -- <-cmp 11 open import Data.Nat.Properties as NatProp -- <-cmp
12 12
13 record Env : Set where 13 record Env : Set where
14 field 14 field
15 var-init-x : @$\mathbb{N}$@ 15 var-init-x : !$\mathbb{N}$!
16 var-init-y : @$\mathbb{N}$@ 16 var-init-y : !$\mathbb{N}$!
17 var-x : @$\mathbb{N}$@ 17 var-x : !$\mathbb{N}$!
18 var-y : @$\mathbb{N}$@ 18 var-y : !$\mathbb{N}$!
19 open Env 19 open Env
20 20
21 plus-com : {l : Level} {t : Set l} @$\rightarrow$@ Env @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t 21 plus-com : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
22 plus-com env next exit with var-y env 22 plus-com env next exit with var-y env
23 ... | zero = exit record env{var-x = var-x env ; var-y = zero} 23 ... | zero = exit record env{var-x = var-x env ; var-y = zero}
24 ... | suc y = next record env{var-x = suc (var-x env) ; var-y = y} 24 ... | suc y = next record env{var-x = suc (var-x env) ; var-y = y}
25 25
26 plus-init : {l : Level} {t : Set l} @$\rightarrow$@ ( x y : @$\mathbb{N}$@ ) @$\rightarrow$@ (next : Env @$\rightarrow$@ t) @$\rightarrow$@ t 26 plus-init : {l : Level} {t : Set l} !$\rightarrow$! ( x y : !$\mathbb{N}$! ) !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! t
27 plus-init x y next = next (record { var-init-x = x ; var-init-y = y ; var-x = x ; var-y = y }) 27 plus-init x y next = next (record { var-init-x = x ; var-init-y = y ; var-x = x ; var-y = y })
28 28
29 {-@$\#$@ TERMINATING @$\#$@-} 29 {-!$\#$! TERMINATING !$\#$!-}
30 plus-p : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : Env @$\rightarrow$@ t) @$\rightarrow$@ t 30 plus-p : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
31 plus-p env exit = plus-com env ( @$\lambda$@ env @$\rightarrow$@ plus-p env exit ) exit 31 plus-p env exit = plus-com env ( !$\lambda$! env !$\rightarrow$! plus-p env exit ) exit
32 32
33 plus : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Env 33 plus : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Env
34 plus x y = plus-init x y (@$\lambda$@ env @$\rightarrow$@ plus-p env (@$\lambda$@ env @$\rightarrow$@ env)) 34 plus x y = plus-init x y (!$\lambda$! env !$\rightarrow$! plus-p env (!$\lambda$! env !$\rightarrow$! env))
35 --(record { varx = x ; vary = y }) (@$\lambda$@ env @$\rightarrow$@ env) 35 --(record { varx = x ; vary = y }) (!$\lambda$! env !$\rightarrow$! env)
36 36
37 -- ここまでplusの定義 37 -- ここまでplusの定義
38 38
39 -- mdg (meta code gear) 39 -- mdg (meta code gear)
40 data mdg-state : Set where 40 data mdg-state : Set where
41 s-init : mdg-state 41 s-init : mdg-state
42 s-doing : mdg-state 42 s-doing : mdg-state
43 s-fin : mdg-state 43 s-fin : mdg-state
44 44
45 record _@$\wedge$@_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where 45 record _!$\wedge$!_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n !$\sqcup$! m) where
46 field 46 field
47 proj1 : A 47 proj1 : A
48 proj2 : B 48 proj2 : B
49 49
50 -- mcg (meta code gear) 50 -- mcg (meta code gear)
51 plus-mdg : mdg-state @$\rightarrow$@ Env @$\rightarrow$@ Set 51 plus-mdg : mdg-state !$\rightarrow$! Env !$\rightarrow$! Set
52 plus-mdg s-init env = (var-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-y env @$\equiv$@ var-init-y env) 52 plus-mdg s-init env = (var-x env !$\equiv$! var-init-x env) !$\wedge$! (var-y env !$\equiv$! var-init-y env)
53 plus-mdg s-doing env = (var-init-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-init-y env @$\equiv$@ var-init-y env) -- よくないmdg 53 plus-mdg s-doing env = (var-init-x env !$\equiv$! var-init-x env) !$\wedge$! (var-init-y env !$\equiv$! var-init-y env) -- よくないmdg
54 plus-mdg s-fin env = (var-init-x env @$\equiv$@ var-init-x env) @$\wedge$@ (var-init-y env @$\equiv$@ var-init-y env) -- よくないmdg 54 plus-mdg s-fin env = (var-init-x env !$\equiv$! var-init-x env) !$\wedge$! (var-init-y env !$\equiv$! var-init-y env) -- よくないmdg
55 55
56 -- 実行のwrapperを作って、そこでmcgが適切に選ばれて接続をしたい。多分できる気がする。 56 -- 実行のwrapperを作って、そこでmcgが適切に選ばれて接続をしたい。多分できる気がする。
57 plus-init-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (x y : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Env ) @$\rightarrow$@ plus-mdg s-init env @$\rightarrow$@ t) @$\rightarrow$@ t 57 plus-init-mcg : {l : Level} {t : Set l} !$\rightarrow$! (x y : !$\mathbb{N}$!) !$\rightarrow$! ((env : Env ) !$\rightarrow$! plus-mdg s-init env !$\rightarrow$! t) !$\rightarrow$! t
58 plus-init-mcg x y next = next ( plus-init x y ( @$\lambda$@ env @$\rightarrow$@ env ) ) record { proj1 = refl ; proj2 = refl } where 58 plus-init-mcg x y next = next ( plus-init x y ( !$\lambda$! env !$\rightarrow$! env ) ) record { proj1 = refl ; proj2 = refl } where
59 59
60 plus-com-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env ) @$\rightarrow$@ (next : (env : Env ) @$\rightarrow$@ plus-mdg s-doing env @$\rightarrow$@ t) @$\rightarrow$@ (exit : (env : Env ) @$\rightarrow$@ plus-mdg s-fin env @$\rightarrow$@ t) @$\rightarrow$@ t 60 plus-com-mcg : {l : Level} {t : Set l} !$\rightarrow$! (env : Env ) !$\rightarrow$! (next : (env : Env ) !$\rightarrow$! plus-mdg s-doing env !$\rightarrow$! t) !$\rightarrow$! (exit : (env : Env ) !$\rightarrow$! plus-mdg s-fin env !$\rightarrow$! t) !$\rightarrow$! t
61 plus-com-mcg env-in next exit with (var-y env-in) 61 plus-com-mcg env-in next exit with (var-y env-in)
62 ... | suc y = next ( plus-com env-in ( @$\lambda$@ env @$\rightarrow$@ env ) ( @$\lambda$@ env @$\rightarrow$@ env ) ) (record { proj1 = refl ; proj2 = refl }) where 62 ... | suc y = next ( plus-com env-in ( !$\lambda$! env !$\rightarrow$! env ) ( !$\lambda$! env !$\rightarrow$! env ) ) (record { proj1 = refl ; proj2 = refl }) where
63 ... | zero = exit env-in (record { proj1 = refl ; proj2 = refl }) 63 ... | zero = exit env-in (record { proj1 = refl ; proj2 = refl })
64 64
65 --plus-com-mcg 65 --plus-com-mcg
66 {-@$\#$@ TERMINATING @$\#$@-} 66 {-!$\#$! TERMINATING !$\#$!-}
67 plus-p-mcg : {l : Level} {t : Set l} @$\rightarrow$@ (env : Env) @$\rightarrow$@ (exit : (env : Env ) @$\rightarrow$@ plus-mdg s-fin env @$\rightarrow$@ t) @$\rightarrow$@ t 67 plus-p-mcg : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : (env : Env ) !$\rightarrow$! plus-mdg s-fin env !$\rightarrow$! t) !$\rightarrow$! t
68 plus-p-mcg env exit = plus-com-mcg env (@$\lambda$@ env s @$\rightarrow$@ plus-p-mcg env exit ) exit 68 plus-p-mcg env exit = plus-com-mcg env (!$\lambda$! env s !$\rightarrow$! plus-p-mcg env exit ) exit
69 69
70 plus-mcg : (x y : @$\mathbb{N}$@) @$\rightarrow$@ Env 70 plus-mcg : (x y : !$\mathbb{N}$!) !$\rightarrow$! Env
71 plus-mcg x y = plus-init-mcg x y (@$\lambda$@ env s @$\rightarrow$@ plus-p-mcg env (@$\lambda$@ env s @$\rightarrow$@ env)) 71 plus-mcg x y = plus-init-mcg x y (!$\lambda$! env s !$\rightarrow$! plus-p-mcg env (!$\lambda$! env s !$\rightarrow$! env))
72 72
73 test1 = plus-mcg 3 4 73 test1 = plus-mcg 3 4
74 74
75 {- 75 {-
76 next env ? where 76 next env ? where
77 env : Env 77 env : Env
78 env = plus-com env-in {!!} {!!} 78 env = plus-com env-in {!!} {!!}
79 -} 79 -}
80 --plus-mdg s-init (plus-p record env{var-x = var-init-x env ; var-y = var-init-y env} (@$\lambda$@ env @$\rightarrow$@ env)) 80 --plus-mdg s-init (plus-p record env{var-x = var-init-x env ; var-y = var-init-y env} (!$\lambda$! env !$\rightarrow$! env))
81 81
82 82
83 83
84 {- 84 {-
85 whileTestPwP : {l : Level} {t : Set l} @$\rightarrow$@ (c10 : @$\mathbb{N}$@) @$\rightarrow$@ ((env : Envc ) @$\rightarrow$@ whileTestStateP s1 env @$\rightarrow$@ t) @$\rightarrow$@ t 85 whileTestPwP : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! ((env : Envc ) !$\rightarrow$! whileTestStateP s1 env !$\rightarrow$! t) !$\rightarrow$! t
86 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where 86 whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
87 env : Envc 87 env : Envc
88 env = whileTestP c10 ( @$\lambda$@ env @$\rightarrow$@ env ) 88 env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )
89 -} 89 -}
90 90
91 data hoare-cond : Set where 91 data hoare-cond : Set where
92 p : hoare-cond 92 p : hoare-cond
93 q : hoare-cond 93 q : hoare-cond
94 94
95 95
96 {- 96 {-
97 continuation-hoare-triple : {l : Level} {t : Set l} @$\rightarrow$@ hoare-cond @$\rightarrow$@ (next : Env @$\rightarrow$@ t) Set 97 continuation-hoare-triple : {l : Level} {t : Set l} !$\rightarrow$! hoare-cond !$\rightarrow$! (next : Env !$\rightarrow$! t) Set
98 continuation-hoare-triple p next = continuation-hoare-triple q 98 continuation-hoare-triple p next = continuation-hoare-triple q
99 continuation-hoare-triple q next = continuation-hoare-triple p 99 continuation-hoare-triple q next = continuation-hoare-triple p
100 -} 100 -}
101 101
102 102