--- a/paper/agda.tex	Thu Feb 09 15:36:52 2017 +0900
+++ b/paper/agda.tex	Thu Feb 09 15:40:11 2017 +0900
@@ -22,7 +22,7 @@
 トップレベルのモジュールはファイル名と同一となる。
 例えば \verb/AgdaBasics.agda/ を作成する時のモジュール名はリスト~\ref{src:agda-module}のように定義する。
 
-\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda}
+\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda.replaced}
 
 Agda における型指定は $:$ を用いて行なう。
 例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。
@@ -35,7 +35,7 @@
 Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。
 Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。
 
-\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}
+\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda.replaced}
 
 
 関数の定義は Haskell に近い。
@@ -45,13 +45,13 @@
 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A -> B/ のように書ける。
 Bool 変数 \verb/x/ を取って true を返す関数 \verb/f/はリスト~\ref{src:agda-function}のようになる。
 
-\lstinputlisting[label=src/agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda}
+\lstinputlisting[label=src/agda-function, caption=Agda における関数定義] {src/AgdaFunction.agda.replaced}
 
 引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
 例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
 
-\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
+\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}
 
 パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
 例えば、Bool 型を受け取る関数で \verb/true/ の時の挙動のみを書くことはできない。
@@ -59,14 +59,14 @@
 例えばリスト~\ref{src:agda-pattern}の not は x には true しか入ることは無い。
 なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
 
-\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
+\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda.replaced}
 
 関数にはリテラルが存在し、関数名を定義せずともその場で生成することができる。
 これをラムダ式と呼び、\verb/\arg1 arg2 -> function body/ のように書く。
 例えば Bool 型の引数 \verb/b/ を取って not を適用する \verb/not-apply/ をラムダ式で書くとリスト~\ref{src:agda-lambda}のようになる。
 関数 \verb/not-apply/ をラムダ式を使わずに定義すると \verb/not-apply-2/ になるが、この二つの関数は同一の動作をする。
 
-\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda}
+\lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ式] {src/AgdaLambda.agda.replaced}
 
 Agda では特定の関数内のみで利用する関数を \verb/where/ 句で記述できる。
 これは関数内部の冗長な記述を省略するのに活用できる。
@@ -75,14 +75,14 @@
 これは \verb/f'/ と同様の動作をする。
 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
 
-\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda}
+\lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}
 
 
 データ型のコンストラクタには自分自身の型を引数に取ることもできる(リスト~\ref{src:agda-nat})。
 自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
 例えば0 は \verb/zero/ であり、1 は \verb/suc zero/に、3は \verb/suc (suc (suc zero))/ に対応する。
 
-\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}
+\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced}
 
 自然数に対する演算は再帰関数として定義できる。
 例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。
@@ -96,7 +96,7 @@
 左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
 もし \verb/suc n/ のまま自分自身へと再帰した場合、Agda は警告を出す。
 
-\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
+\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda.replaced}
 
 次に依存型について見ていく。
 依存型で最も基本的なものは関数型である。
@@ -106,7 +106,7 @@
 ここで B の中で x を扱っても良い。
 例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。
 
-\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}
+\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda.replaced}
 
 この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
 実際に関数 \verb/identitiy/ を Nat へ適用した例が \verb/identitiy-zero/ である。
@@ -121,7 +121,7 @@
 なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる(\verb/id'/ 関数)。
 適用する場合も \verb/{}/でくくり、\verb/id-true/のように使用する。
 
-\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}
+\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda.replaced}
 
 Agda には C における構造体に相当するレコード型も存在する。
 定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
@@ -129,14 +129,14 @@
 レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
 複数の値を列挙する際は \verb/;/ で区切る。
 
-\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}
+\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced}
 
 構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。
 なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。
 また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。
 Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。
 
-\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}
+\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda.replaced}
 
 Agda における部分型のように振る舞う機能として Instance Arguments が存在する。
 これはとあるデータ型が、ある型と名前を持つ関数を持つことを保証する機能であり、Haskell における型クラスや Java におけるインターフェースに相当する。
@@ -144,12 +144,12 @@
 例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。
 具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。
 
-\lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda}
+\lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda.replaced}
 
 ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
 型Nat が Eq の上位型であることを記述するとリスト~\ref{src:agda-instance}のようになる。
 
-\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}
+\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda.replaced}
 
 これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。
 例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。
@@ -175,7 +175,7 @@
 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open/ キーワードを使うことで展開できる。
 モジュールをインポートする例をリスト~\ref{src:agda-import}に示す。
 
-\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda}
+\lstinputlisting[label=src:agda-import, caption=Agdaにおけるモジュールのインポート] {src/AgdaImport.agda.replaced}
 
 また、モジュールには値を渡すことができる。
 そのようなモジュールは Parameterized Module と呼ばれ、渡された値はそのモジュール内部で一貫して扱える。
@@ -183,7 +183,7 @@
 そのモジュールは引数に型Aと二項演算子 \verb/</を取り、ソートする関数を提供する。
 \verb/Sort/モジュールを \verb/Nat/ と \verb/Bool/ で利用した例がリスト~\ref{src:agda-parameterized-module}である。
 
-\lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda}
+\lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda.replaced}
 
 % }}}
 
@@ -450,7 +450,7 @@
 
 なお、直積型は型Aを持つフィールド\verb/fst/と型Bを持つフィールド\verb/snd/を持つレコード型と考えても良い。
 
-\lstinputlisting[label=src:agda-product, caption=Agda における直積型] {src/AgdaProduct.agda}
+\lstinputlisting[label=src:agda-product, caption=Agda における直積型] {src/AgdaProduct.agda.replaced}
 
 三段論法の証明は 「1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ で dead にする」形であった。
 
@@ -486,7 +486,7 @@
 
 Agda で自然数型 Nat を定義するとリスト \ref{src:agda-nat-2} のようになる。
 
-\lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda}
+\lstinputlisting[label=src:agda-nat-2, caption=Agda における自然数型 Nat の定義] {src/Nat.agda.replaced}
 
 自然数型 Nat は2つのコンストラクタを持つ。
 
@@ -506,7 +506,7 @@
 
 次に加算を定義する(リスト\ref{src:agda-nat-add})。
 
-\lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda}
+\lstinputlisting[label=src:agda-nat-add, caption=Agdaにおける自然数型に対する加算の定義] {src/NatAdd.agda.replaced}
 
 加算は中置関数 \verb/_+_/ として定義する。
 2つの Nat を取り、Natを返す。
@@ -525,7 +525,7 @@
 
 実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:agda-three-plus-one})。
 
-\lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda}
+\lstinputlisting[label=src:agda-three-plus-one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/ThreePlusOne.agda.replaced}
 
 3+1 という関数を定義し、その型として証明すべき式を記述し、証明を関数の定義として定義する。
 証明する式は \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ である。
@@ -549,7 +549,7 @@
 
 ではこれから nat の加法の交換法則を証明していく(リスト\ref{src:agda-nat-add-sym})。
 
-\lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda}
+\lstinputlisting[label=src:agda-nat-add-sym, caption= Agda における加法の交換法則の証明] {src/NatAddSym.agda.replaced}
 
 証明する式は $ n + m \equiv m + n $ である。
 n と m は Nat であるため、それぞれがコンストラクタ O か S により構成される。

Binary file paper/atton-master.pdf has changed

--- 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 の動作するソースコードは付録に載せる。