Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/cbc-type.tex @ 86:e437746d6038

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix lstinput
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 15:40:11 +0900
parents c0199291c58e
children f535393e4043
comparison
equal deleted inserted replaced
85:9d154c48a1f6 86:e437746d6038
16 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。 16 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。
17 例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。 17 例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。
18 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。 18 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。
19 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。 19 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。
20 20
21 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda} 21 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda.replaced}
22 % }}} 22 % }}}
23 23
24 % {{{ CodeSegment の定義 24 % {{{ CodeSegment の定義
25 \section{CodeSegment の定義} 25 \section{CodeSegment の定義}
26 次に CodeSegment を定義する。 26 次に CodeSegment を定義する。
54 最後に計算をする cs0 へと軽量継続する main を定義する。 54 最後に計算をする cs0 へと軽量継続する main を定義する。
55 例として、 a の値を 100 とし、 b の値を50としている。 55 例として、 a の値を 100 とし、 b の値を50としている。
56 56
57 cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。 57 cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。
58 58
59 \lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda} 59 \lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda.replaced}
60 60
61 正しく計算が行なえたなら値150が得られるはずである。 61 正しく計算が行なえたなら値150が得られるはずである。
62 % }}} 62 % }}}
63 63
64 % {{{ ノーマルレベル計算の実行 64 % {{{ ノーマルレベル計算の実行
79 よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。 79 よって、\verb/goto/を利用できるのは関数の末尾のみである、という制約を関数に付け加える必要がある。
80 80
81 この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。 81 この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。
82 具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。 82 具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。
83 83
84 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda} 84 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced}
85 85
86 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。 86 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。
87 本文中での CodeSegment の定義は一部を抜粋している。 87 本文中での CodeSegment の定義は一部を抜粋している。
88 実行可能な Agda のソースコードは付録に載せる。 88 実行可能な Agda のソースコードは付録に載せる。
89 89
165 そのために Meta Meta DataSegment \verb/Meta/ には制御を移す対象であるノーマルレベル CodeSegment を持つ。 165 そのために Meta Meta DataSegment \verb/Meta/ には制御を移す対象であるノーマルレベル CodeSegment を持つ。
166 値を格納する \verb/c'/ の位置は Meta DataSegment でも Meta Meta DataSegment でも構わないが、今回は Meta Meta DataSegemnt に格納するものとする。 166 値を格納する \verb/c'/ の位置は Meta DataSegment でも Meta Meta DataSegment でも構わないが、今回は Meta Meta DataSegemnt に格納するものとする。
167 それらを踏まえた上での Meta Meta DataSegment の Agda 上での定義は~\ref{src:agda-mmds}のようになる。 167 それらを踏まえた上での Meta Meta DataSegment の Agda 上での定義は~\ref{src:agda-mmds}のようになる。
168 なお、\verb/goto/ などの名前の衝突を避けるためにノーマルレベルの定義は \verb/N/ に、メタレベルの定義は \verb/M/ へと名前を付けかえている。 168 なお、\verb/goto/ などの名前の衝突を避けるためにノーマルレベルの定義は \verb/N/ に、メタレベルの定義は \verb/M/ へと名前を付けかえている。
169 169
170 \lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda} 170 \lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda.replaced}
171 171
172 定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。 172 定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。
173 より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。 173 より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。
174 \verb/gotoMeta/ や \verb/push/ で利用している \verb/liftContext/ や \verb/liftMeta/ はノーマルレベル計算をメタ計算レベルとするように型を明示的に変更するものである。 174 \verb/gotoMeta/ や \verb/push/ で利用している \verb/liftContext/ や \verb/liftMeta/ はノーマルレベル計算をメタ計算レベルとするように型を明示的に変更するものである。
175 結果的に \verb/main/ の \verb/goto/ を \verb/gotoMeta/ に置き換えることにより、c の値を計算しながら保存できる。 175 結果的に \verb/main/ の \verb/goto/ を \verb/gotoMeta/ に置き換えることにより、c の値を計算しながら保存できる。
176 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。 176 リスト~\ref{src:agda-mmcs} に示したプログラムでは、通常レベルのコードセグメントを全く変更せずにメタ計算を含む形に拡張している。
177 加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。 177 加算を行なう前の \verb/c/ の値が \verb/70/ であったとした時、計算結果 \verb/150/ は \verb/c/ に格納されるが、\verb/c'/には\verb/70/に保存されている。
178 178
179 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda} 179 \lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda.replaced}
180 180
181 なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる 181 なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる
182 % TODO: cbc と agda の diff 182 % TODO: cbc と agda の diff
183 183
184 CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。 184 CodeSegment や Meta CodeSegment などの定義が多かっため、どの処理やデータがどのレベルに属するか複雑になったため、一度図にてまとめる。
219 CbC とほぼ同様の定義ができている。 219 CbC とほぼ同様の定義ができている。
220 CbC、 Agda 共に\verb/SingleLinkedStack/ は \verb/Element/ 型の \verb/top/ を持っている。 220 CbC、 Agda 共に\verb/SingleLinkedStack/ は \verb/Element/ 型の \verb/top/ を持っている。
221 \verb/Element/ 型は値と次の \verb/Element/ を持つ。 221 \verb/Element/ 型は値と次の \verb/Element/ を持つ。
222 CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。 222 CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。
223 223
224 \lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda} 224 \lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda.replaced}
225 225
226 Agda で片方向リストを利用する DataSegment の定義をリスト~\ref{src:agda-stack-ds}に示す。 226 Agda で片方向リストを利用する DataSegment の定義をリスト~\ref{src:agda-stack-ds}に示す。
227 ノーマルレベルからアクセス可能な場所として \verb/Context/ に \verb/element/ フィールドを追加する。 227 ノーマルレベルからアクセス可能な場所として \verb/Context/ に \verb/element/ フィールドを追加する。
228 そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。 228 そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。
229 CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。 229 CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。
230 230
231 \lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda} 231 \lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda.replaced}
232 232
233 次にスタックへの操作に注目する。 233 次にスタックへの操作に注目する。
234 スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。 234 スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。
235 \verb/SingleLinkedStack/ は Meta CodeSegment であり、メタ計算を実行した後には通常の CodeSegment へと操作を移す。 235 \verb/SingleLinkedStack/ は Meta CodeSegment であり、メタ計算を実行した後には通常の CodeSegment へと操作を移す。
236 そのために \verb/next/ という名前で次のコードセグメントを保持している。 236 そのために \verb/next/ という名前で次のコードセグメントを保持している。
260 \verb/top/ が空でなければ \verb/element/ は \verb/top/ の値となる。 260 \verb/top/ が空でなければ \verb/element/ は \verb/top/ の値となる。
261 261
262 \verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。 262 \verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。
263 ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。 263 ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。
264 264
265 \lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda} 265 \lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda.replaced}
266 266
267 また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 267 また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。
268 268
269 % }}} 269 % }}}
270 270