--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/hoare-test.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,103 @@
+module hoare-test where
+
+open import Data.Nat hiding (_!$\sqcup$!_)
+open import Level renaming ( suc to succ ; zero to Zero )
+
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+
+open import Relation.Nullary hiding (proof)
+
+open import Data.Nat.Properties as NatProp -- <-cmp
+
+record Env : Set where
+  field
+    var-init-x : !$\mathbb{N}$!
+    var-init-y : !$\mathbb{N}$!
+    var-x : !$\mathbb{N}$!
+    var-y : !$\mathbb{N}$!
+open Env
+
+plus-com : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
+plus-com env next exit with var-y env
+... | zero  = exit record env{var-x = var-x env ; var-y = zero}
+... | suc y = next record env{var-x = suc (var-x env) ; var-y = y}
+
+plus-init : {l : Level} {t : Set l} !$\rightarrow$! ( x y : !$\mathbb{N}$! ) !$\rightarrow$! (next : Env !$\rightarrow$! t) !$\rightarrow$! t
+plus-init x y next = next (record { var-init-x = x ; var-init-y = y ; var-x = x ; var-y = y })
+
+{-!$\#$! TERMINATING !$\#$!-}
+plus-p : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t
+plus-p env exit = plus-com env ( !$\lambda$! env !$\rightarrow$! plus-p env exit ) exit
+
+plus : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! Env
+plus x y = plus-init x y (!$\lambda$! env !$\rightarrow$!  plus-p env (!$\lambda$! env !$\rightarrow$! env))
+--(record { varx = x ; vary = y }) (!$\lambda$! env !$\rightarrow$! env)
+
+-- ここまでplusの定義
+
+-- mdg (meta code gear)
+data mdg-state : Set where
+  s-init  : mdg-state
+  s-doing : mdg-state
+  s-fin   : mdg-state
+
+record  _!$\wedge$!_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n !$\sqcup$! m) where
+   field
+      proj1 : A
+      proj2 : B
+
+-- mcg (meta code gear)
+plus-mdg : mdg-state !$\rightarrow$! Env !$\rightarrow$! Set
+plus-mdg s-init  env = (var-x env !$\equiv$! var-init-x env) !$\wedge$! (var-y env !$\equiv$! var-init-y env)
+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
+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
+
+-- 実行のwrapperを作って、そこでmcgが適切に選ばれて接続をしたい。多分できる気がする。
+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
+plus-init-mcg x y next = next ( plus-init x y ( !$\lambda$! env !$\rightarrow$! env ) ) record { proj1 = refl ; proj2 = refl } where
+
+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
+plus-com-mcg env-in next exit with (var-y env-in)
+... | suc y = next ( plus-com env-in ( !$\lambda$! env !$\rightarrow$! env ) ( !$\lambda$! env !$\rightarrow$! env ) ) (record { proj1 = refl ; proj2 = refl }) where
+... | zero = exit env-in (record { proj1 = refl ; proj2 = refl })
+
+--plus-com-mcg
+{-!$\#$! TERMINATING !$\#$!-}
+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
+plus-p-mcg env exit = plus-com-mcg env (!$\lambda$! env s !$\rightarrow$! plus-p-mcg env exit ) exit
+
+plus-mcg : (x y : !$\mathbb{N}$!) !$\rightarrow$! Env
+plus-mcg x y = plus-init-mcg x y (!$\lambda$! env s !$\rightarrow$! plus-p-mcg env (!$\lambda$! env s !$\rightarrow$! env))
+
+test1 = plus-mcg 3 4
+
+{-
+next env ? where
+   env : Env
+   env = plus-com env-in {!!} {!!}
+-}
+--plus-mdg s-init (plus-p record env{var-x = var-init-x env ; var-y = var-init-y env} (!$\lambda$! env !$\rightarrow$! env))
+
+
+
+{-
+whileTestPwP  : {l : Level} {t : Set l} !$\rightarrow$! (c10 : !$\mathbb{N}$!) !$\rightarrow$! ((env : Envc ) !$\rightarrow$! whileTestStateP s1 env !$\rightarrow$! t) !$\rightarrow$! t
+whileTestPwP c10 next = next env record { pi1 = refl ; pi2 = refl } where
+   env : Envc
+   env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )
+-}
+
+data hoare-cond : Set where
+  p : hoare-cond
+  q : hoare-cond
+
+
+{-
+continuation-hoare-triple : {l : Level} {t : Set l} !$\rightarrow$! hoare-cond !$\rightarrow$! (next : Env !$\rightarrow$! t) Set
+continuation-hoare-triple p next = continuation-hoare-triple q
+continuation-hoare-triple q next = continuation-hoare-triple p
+-}
+
+
+