# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1486090781 -32400
# Node ID 6d8825f3b05172675d3374b87179de072a6f5f34
# Parent  a40033d3e10f5ddb230d683b8a09d649b4c9c3cd
Add example of meta code segment execution

diff -r a40033d3e10f -r 6d8825f3b051 paper/atton-master.pdf
Binary file paper/atton-master.pdf has changed
diff -r a40033d3e10f -r 6d8825f3b051 paper/cbc-type.tex
--- a/paper/cbc-type.tex	Fri Feb 03 10:29:28 2017 +0900
+++ b/paper/cbc-type.tex	Fri Feb 03 11:59:41 2017 +0900
@@ -138,6 +138,46 @@
 
 % }}}
 
+% {{{ メタレベル計算の実行
+
 \section{メタレベル計算の実行}
+Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。
+
+実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。
+メタレベル実行ではそれを Meta CodeSegment と Meta DataSegment を扱えるように拡張する。
+Meta DataSegment は Parameterized Module の引数 \verb/Context/ に相当するため、Meta CodeSegment は Context を取って Context を返す CodeSegment となる。
+軽量継続 \verb/goto/ と区別するために名前を \verb/exec/ とするリスト~\ref{src:agda-exec}のように定義できる。
+行なっていることは Meta CodeSegment の本体部分に Meta DataSegment を渡す、という \verb/goto/ と変わらないが、\verb/set/ と \verb/get/ を用いることで上位型である任意の DataSegment を実行する CodeSegment も Meta CodeSegment として一様に実行できる。
+
+\lstinputlisting[label=src:agda-exec, caption=Agda におけるメタレベル実行の定義] {src/Exec.agda.replaced}
+
+実行例として、リスト~\ref{src:goto} に示していた a と b の値を加算して c に代入するプログラムを考える。
+実行する際に c の値を \verb/c'/ に保存してから加算ようなメタ計算を考える。
+c の値を \verb/c'/ に保存するタイミングは軽量継続時にユーザが指定する。
+よって軽量継続を行なうのと同等の情報を保持してなくてはならない。
+そのために Meta Meta DataSegment \verb/Meta/ には制御を移す対象であるノーマルレベル CodeSegment を持つ。
+値を格納する \verb/c'/ の位置は Meta DataSegment でも Meta Meta DataSegment でも構わないが、今回は Meta Meta DataSegemnt に格納するものとする。
+それらを踏まえた上での Meta Meta DataSegment の Agda 上での定義は~\ref{src:agda-mmds}のようになる。
+なお、\verb/goto/ などの名前の衝突を避けるためにノーマルレベルの定義は \verb/N/ に、メタレベルの定義は \verb/M/ へと名前を付けかえている。
+
+\lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda}
+
+定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。
+より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。
+\verb/gotoMeta/ や \verb/push/ で利用している \verb/liftContext/ や \verb/liftMeta/ はノーマルレベル計算をメタ計算レベルとするように型を明示的に変更するものである。
+結果的に \verb/main/ の \verb/goto/ を \verb/gotoMeta/ に置き換えることにより、c の値を計算しながら保存できる。
+リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。
+加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。
+
+\lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda}
+
+メタの階層構造を表すと図のようになる。
+Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。
+
+
+% TODO: メタの階層構造の図
+
+% }}}
+
 \section{Agda を用いたContinuation based C の検証}
 \section{スタックの実装の検証}
diff -r a40033d3e10f -r 6d8825f3b051 paper/src/Exec.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/Exec.agda	Fri Feb 03 11:59:41 2017 +0900
@@ -0,0 +1,5 @@
+exec : {l1 l2 : Level} {I : Set l1} {O : Set l2}
+       {{_ : DataSegment I}} {{_ : DataSegment O}}
+       -> CodeSegment I O -> Context -> Context
+exec {l} {{i}} {{o}}  (cs b) c = set o c (b (get i c))
+
diff -r a40033d3e10f -r 6d8825f3b051 paper/src/MetaMetaCodeSegment.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/MetaMetaCodeSegment.agda	Fri Feb 03 11:59:41 2017 +0900
@@ -0,0 +1,30 @@
+...
+-- meta level
+liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
+liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
+
+liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
+liftMeta (N.cs f) = M.cs f
+
+gotoMeta : {I O : Set} {{_ : N.DataSegment I}} {{_ : N.DataSegment O}} -> M.CodeSegment Meta Meta -> N.CodeSegment I O -> Meta -> Meta
+gotoMeta mCode code m = M.exec mCode (record m {next = (liftContext code)})
+
+push : M.CodeSegment Meta Meta
+push = M.cs (\m -> M.exec (liftMeta (Meta.next m)) (record m {c' = Context.c (Meta.context m)}))
+
+-- normal level
+
+cs2 : N.CodeSegment ds1 ds1
+cs2 = N.cs id
+
+cs1 : N.CodeSegment ds1 ds1
+cs1 = N.cs (\d -> N.goto cs2 d)
+
+cs0 : N.CodeSegment ds0 ds1
+cs0 = N.cs (\d -> N.goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+-- meta level (with extended normal)
+main : Meta
+main = gotoMeta push cs0 (record {context = (record {a = 100 ; b = 50 ; c = 70}) ; c' = 0 ; next = (N.cs id)})
+-- record {context = record {a = 100 ; b = 50 ; c = 150} ; c' = 70 ; next = (N.cs id)}
+
diff -r a40033d3e10f -r 6d8825f3b051 paper/src/MetaMetaDataSegment.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/MetaMetaDataSegment.agda	Fri Feb 03 11:59:41 2017 +0900
@@ -0,0 +1,11 @@
+...
+open import subtype Context as N
+
+record Meta : Set where
+  field
+    context : Context
+    c'      : Int
+    next    : N.CodeSegment Context Context
+
+open import subtype Meta as M
+...