--- a/paper/cbc-type.tex	Thu Feb 09 15:36:52 2017 +0900
+++ b/paper/cbc-type.tex	Thu Feb 09 15:40:11 2017 +0900
@@ -18,7 +18,7 @@
 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。
 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。
 
-\lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
+\lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda.replaced}
 % }}}
 
 % {{{ CodeSegment の定義
@@ -56,7 +56,7 @@
 
 cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。
 
-\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda}
+\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda.replaced}
 
 正しく計算が行なえたなら値150が得られるはずである。
 % }}}
@@ -81,7 +81,7 @@
 この制約さえ満たせば、CodeSegment の実行は CodeSegment 型から関数本体を取り出し、レコード型を持つ値を適用することに相当する。
 具体的に \verb/goto/ を関数として適用するとリスト~\ref{src:agda-goto}のようになる。
 
-\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda}
+\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced}
 
 この \verb/goto/ の定義を用いることで main などの関数が評価できるようになり、値150が得られる。
 本文中での CodeSegment の定義は一部を抜粋している。
@@ -167,7 +167,7 @@
 それらを踏まえた上での 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}
+\lstinputlisting[label=src:agda-mmds, caption=Agda における Meta Meta DataSegment の定義例] {src/MetaMetaDataSegment.agda.replaced}
 
 定義した \verb/Meta/ を利用して、c を \verb/c'/に保存するメタ計算 \verb/push/ を定義する。
 より構文が CbC に似るように \verb/gotoMeta/ を糖衣構文的に定義する。
@@ -176,7 +176,7 @@
 リスト~\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}
+\lstinputlisting[label=src:agda-mmcs, caption=Agda における Meta Meta CodeSegment の定義と実行例] {src/MetaMetaCodeSegment.agda.replaced}
 
 なお、CbC におけるメタ計算を含む軽量継続\verb/goto meta/とAgda におけるメタ計算実行の比較はリスト~\ref{src:goto-meta}のようになる
 % TODO: cbc と agda の diff
@@ -221,14 +221,14 @@
 \verb/Element/ 型は値と次の \verb/Element/ を持つ。
 CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。
 
-\lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda}
+\lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda.replaced}
 
 Agda で片方向リストを利用する DataSegment の定義をリスト~\ref{src:agda-stack-ds}に示す。
 ノーマルレベルからアクセス可能な場所として \verb/Context/ に \verb/element/ フィールドを追加する。
 そしてノーマルレベルからアクセスできないよう分離した Meta Meta DataSegment である \verb/Meta/ にスタックの本体を格納する。
 CbC における実装では \verb/.../ で不定であった \verb/next/ も、agda ではメタレベルのコードセグメント \verb/nextCS/ となり、きちんと型付けされている。
 
-\lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda}
+\lstinputlisting[label=src:agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda.replaced}
 
 次にスタックへの操作に注目する。
 スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。
@@ -262,7 +262,7 @@
 \verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。
 ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。
 
-\lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda}
+\lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda.replaced}
 
 また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。