Mercurial > hg > Papers > 2018 > nozomi-master
comparison paper/cbc-type.tex @ 63:6d8825f3b051
Add example of meta code segment execution
| author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Feb 2017 11:59:41 +0900 |
| parents | a40033d3e10f |
| children | 10a550bf7e4a |
comparison
equal
deleted
inserted
replaced
| 62:a40033d3e10f | 63:6d8825f3b051 |
|---|---|
| 136 | 136 |
| 137 \lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced} | 137 \lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced} |
| 138 | 138 |
| 139 % }}} | 139 % }}} |
| 140 | 140 |
| 141 % {{{ メタレベル計算の実行 | |
| 142 | |
| 141 \section{メタレベル計算の実行} | 143 \section{メタレベル計算の実行} |
| 144 Meta DataSegment と Meta CodeSegment の定義を行なったので、残るは実行である。 | |
| 145 | |
| 146 実行はノーマルレベルにおいては軽量継続 \verb/goto/ を定義することによって表せた。 | |
| 147 メタレベル実行ではそれを Meta CodeSegment と Meta DataSegment を扱えるように拡張する。 | |
| 148 Meta DataSegment は Parameterized Module の引数 \verb/Context/ に相当するため、Meta CodeSegment は Context を取って Context を返す CodeSegment となる。 | |
| 149 軽量継続 \verb/goto/ と区別するために名前を \verb/exec/ とするリスト~\ref{src:agda-exec}のように定義できる。 | |
| 150 行なっていることは Meta CodeSegment の本体部分に Meta DataSegment を渡す、という \verb/goto/ と変わらないが、\verb/set/ と \verb/get/ を用いることで上位型である任意の DataSegment を実行する CodeSegment も Meta CodeSegment として一様に実行できる。 | |
| 151 | |
| 152 \lstinputlisting[label=src:agda-exec, caption=Agda におけるメタレベル実行の定義] {src/Exec.agda.replaced} | |
| 153 | |
| 154 実行例として、リスト~\ref{src:goto} に示していた a と b の値を加算して c に代入するプログラムを考える。 | |
| 155 実行する際に c の値を \verb/c'/ に保存してから加算ようなメタ計算を考える。 | |
| 156 c の値を \verb/c'/ に保存するタイミングは軽量継続時にユーザが指定する。 | |
| 157 よって軽量継続を行なうのと同等の情報を保持してなくてはならない。 | |
| 158 そのために Meta Meta DataSegment \verb/Meta/ には制御を移す対象であるノーマルレベル CodeSegment を持つ。 | |
| 159 値を格納する \verb/c'/ の位置は Meta DataSegment でも Meta Meta DataSegment でも構わないが、今回は Meta Meta DataSegemnt に格納するものとする。 | |
| 160 それらを踏まえた上での Meta Meta DataSegment の Agda 上での定義は~\ref{src:agda-mmds}のようになる。 | |
| 161 なお、\verb/goto/ などの名前の衝突を避けるためにノーマルレベルの定義は \verb/N/ に、メタレベルの定義は \verb/M/ へと名前を付けかえている。 | |
| 162 | |
| 163 \lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda} | |
| 164 | |
| 165 定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。 | |
| 166 より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。 | |
| 167 \verb/gotoMeta/ や \verb/push/ で利用している \verb/liftContext/ や \verb/liftMeta/ はノーマルレベル計算をメタ計算レベルとするように型を明示的に変更するものである。 | |
| 168 結果的に \verb/main/ の \verb/goto/ を \verb/gotoMeta/ に置き換えることにより、c の値を計算しながら保存できる。 | |
| 169 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。 | |
| 170 加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。 | |
| 171 | |
| 172 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda} | |
| 173 | |
| 174 メタの階層構造を表すと図のようになる。 | |
| 175 Meta DataSegment を含む任意の DataSegment は Meta DataSegment になりえるので、この階層構造は任意の段数定義することが可能である。 | |
| 176 | |
| 177 | |
| 178 % TODO: メタの階層構造の図 | |
| 179 | |
| 180 % }}} | |
| 181 | |
| 142 \section{Agda を用いたContinuation based C の検証} | 182 \section{Agda を用いたContinuation based C の検証} |
| 143 \section{スタックの実装の検証} | 183 \section{スタックの実装の検証} |