Mercurial > hg > Papers > 2022 > soto-sigos
comparison Paper/src/agda/hoare-test.agda.replaced @ 0:14a0e409d574
ADD fast commit
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Apr 2022 23:13:44 +0900 |
| parents | |
| children | 9ec2d2ac1309 |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:14a0e409d574 |
|---|---|
| 1 module hoare-test where | |
| 2 | |
| 3 open import Data.Nat hiding (_!$\sqcup$!_) | |
| 4 open import Level renaming ( suc to succ ; zero to Zero ) | |
| 5 | |
| 6 open import Relation.Binary | |
| 7 open import Relation.Binary.PropositionalEquality | |
| 8 | |
| 9 open import Relation.Nullary hiding (proof) | |
| 10 | |
| 11 open import Data.Nat.Properties as NatProp -- <-cmp | |
| 12 | |
| 13 record Env : Set where | |
| 14 field | |
| 15 var-init-x : !$\mathbb{N}$! | |
| 16 var-init-y : !$\mathbb{N}$! | |
| 17 var-x : !$\mathbb{N}$! | |
| 18 var-y : !$\mathbb{N}$! | |
| 19 open Env | |
| 20 | |
| 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 | |
| 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} | |
| 25 | |
| 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 }) | |
| 28 | |
| 29 {-!$\#$! TERMINATING !$\#$!-} | |
| 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 | |
| 32 | |
| 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)) | |
| 35 --(record { varx = x ; vary = y }) (!$\lambda$! env !$\rightarrow$! env) | |
| 36 | |
| 37 -- ここまでplusの定義 | |
| 38 | |
| 39 -- mdg (meta code gear) | |
| 40 data mdg-state : Set where | |
| 41 s-init : mdg-state | |
| 42 s-doing : mdg-state | |
| 43 s-fin : mdg-state | |
| 44 | |
| 45 record _!$\wedge$!_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n !$\sqcup$! m) where | |
| 46 field | |
| 47 proj1 : A | |
| 48 proj2 : B | |
| 49 | |
| 50 -- mcg (meta code gear) | |
| 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) | |
| 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 | |
| 55 | |
| 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 | |
| 58 plus-init-mcg x y next = next ( plus-init x y ( !$\lambda$! env !$\rightarrow$! env ) ) record { proj1 = refl ; proj2 = refl } where | |
| 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 | |
| 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 | |
| 63 ... | zero = exit env-in (record { proj1 = refl ; proj2 = refl }) | |
| 64 | |
| 65 --plus-com-mcg | |
| 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 | |
| 68 plus-p-mcg env exit = plus-com-mcg env (!$\lambda$! env s !$\rightarrow$! plus-p-mcg env exit ) exit | |
| 69 | |
| 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)) | |
| 72 | |
| 73 test1 = plus-mcg 3 4 | |
| 74 | |
| 75 {- | |
| 76 next env ? where | |
| 77 env : Env | |
| 78 env = plus-com env-in {!!} {!!} | |
| 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)) | |
| 81 | |
| 82 | |
| 83 | |
| 84 {- | |
| 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 | |
| 87 env : Envc | |
| 88 env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env ) | |
| 89 -} | |
| 90 | |
| 91 data hoare-cond : Set where | |
| 92 p : hoare-cond | |
| 93 q : hoare-cond | |
| 94 | |
| 95 | |
| 96 {- | |
| 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 | |
| 99 continuation-hoare-triple q next = continuation-hoare-triple p | |
| 100 -} | |
| 101 | |
| 102 | |
| 103 |