--- a/Paper/src/agda/hoare-test.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/agda/hoare-test.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -1,6 +1,6 @@
 module hoare-test where
 
-open import Data.Nat hiding (_@$\sqcup$@_)
+open import Data.Nat hiding (_!$\sqcup$!_)
 open import Level renaming ( suc to succ ; zero to Zero )
 
 open import Relation.Binary
@@ -12,27 +12,27 @@
 
 record Env : Set where
   field
-    var-init-x : @$\mathbb{N}$@
-    var-init-y : @$\mathbb{N}$@
-    var-x : @$\mathbb{N}$@
-    var-y : @$\mathbb{N}$@
+    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 : {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 : {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
+{-!$\#$! 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 : !$\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の定義
 
@@ -42,33 +42,33 @@
   s-doing : mdg-state
   s-fin   : mdg-state
 
-record  _@$\wedge$@_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
+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
+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-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 : {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
+... | 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
+{-!$\#$! 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))
+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
 
@@ -77,15 +77,15 @@
    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))
+--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  : {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 )
+   env = whileTestP c10 ( !$\lambda$! env !$\rightarrow$! env )
 -}
 
 data hoare-cond : Set where
@@ -94,7 +94,7 @@
 
 
 {-
-continuation-hoare-triple : {l : Level} {t : Set l} @$\rightarrow$@ hoare-cond @$\rightarrow$@ (next : Env @$\rightarrow$@ t) Set
+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
 -}