comparison paper/cbc-type.tex @ 71:b0cfef1cd89f

Add sample source
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 06 Feb 2017 10:15:16 +0900
parents ec6799ca9d42
children fd984cfd5425
comparison
equal deleted inserted replaced
70:4b8a75618f36 71:b0cfef1cd89f
55 正しく計算が行なえたなら値150が得られるはずである。 55 正しく計算が行なえたなら値150が得られるはずである。
56 % }}} 56 % }}}
57 57
58 % {{{ ノーマルレベル計算の実行 58 % {{{ ノーマルレベル計算の実行
59 \section{ノーマルレベル計算の実行} 59 \section{ノーマルレベル計算の実行}
60 \label{section:normal-level-exec}
60 プログラムを実行することは \verb/goto/ を定義することと同義である。 61 プログラムを実行することは \verb/goto/ を定義することと同義である。
61 軽量継続\verb/goto/ の性質としては 62 軽量継続\verb/goto/ の性質としては
62 63
63 \begin{itemize} 64 \begin{itemize}
64 \item 次に実行する CodeSegment を指定する 65 \item 次に実行する CodeSegment を指定する
76 77
77 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda} 78 \lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}
78 79
79 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。 80 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。
80 本文中での CodeSegment の定義は一部を抜粋している。 81 本文中での CodeSegment の定義は一部を抜粋している。
81 実行可能な Agda のソースコードは付録に載せる。% TODO: Appendix 82 実行可能な Agda のソースコードは付録に載せる。
82 83
83 % }}} 84 % }}}
84 85
85 % {{{ Meta DataSegment の定義 86 % {{{ Meta DataSegment の定義
86 87