# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485930435 -32400
# Node ID 5450e7ae5fa569ff438b25be716e42bce603dc00
# Parent  68bf744d726e2acc45d8bf8d85d03b5ab7472d9f
Mini fixes

diff -r 68bf744d726e -r 5450e7ae5fa5 paper/cbc-type.tex
--- a/paper/cbc-type.tex	Wed Feb 01 14:52:01 2017 +0900
+++ b/paper/cbc-type.tex	Wed Feb 01 15:27:15 2017 +0900
@@ -4,6 +4,7 @@
 DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、 Agda 上で実行できることを確認する。
 また、Agda上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 上で証明していく。
 
+% {{{ DataSegment の定義
 \section{DataSegment の定義}
 まず DataSegment から定義していく。
 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。
@@ -12,7 +13,9 @@
 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。
 
 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
+% }}}
 
+% {{{ CodeSegment の定義
 \section{CodeSegment の定義}
 次に CodeSegment を定義する。
 CodeSegment は DataSegment を取って DataSegment を返すものである。
@@ -24,7 +27,7 @@
 CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。
 具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。
 
-\lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda}
+\lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda.replaced}
 
 この CodeSegment 型を用いて CodeSegment の処理本体を記述する。
 
@@ -44,7 +47,13 @@
 
 最後に計算をする cs0 へと軽量継続する main を定義する。
 例として、 a の値を 100 とし、 b の値を50としている。
-正しく計算が行なえたら値150が得られるはずである。
+
+cs0, cs1, cs2, main をAgda で定義するとリスト~\ref{src:agda-css}のようになる。
+
+\lstinputlisting[label=src:agda-css, caption= Agda における CodeSegment の定義] {src/CodeSegments.agda}
+
+正しく計算が行なえたなら値150が得られるはずである。
+% }}}
 
 \section{ノーマルレベル計算の実行}
 \section{MetaDataSegment の定義}
diff -r 68bf744d726e -r 5450e7ae5fa5 paper/escape_agda.rb
--- a/paper/escape_agda.rb	Wed Feb 01 14:52:01 2017 +0900
+++ b/paper/escape_agda.rb	Wed Feb 01 15:27:15 2017 +0900
@@ -6,6 +6,7 @@
 
 ReplaceTable = {
   '->' => 'rightarrow',
+  '⊔'  => 'sqcup',
   '∷' => 'text{::}',
   '∙'  => 'circ',
   '≡' => 'equiv',
diff -r 68bf744d726e -r 5450e7ae5fa5 paper/src/CodeSegment.agda
--- a/paper/src/CodeSegment.agda	Wed Feb 01 14:52:01 2017 +0900
+++ b/paper/src/CodeSegment.agda	Wed Feb 01 15:27:15 2017 +0900
@@ -1,14 +1,2 @@
 data CodeSegment {l1 l2 : Level} (I : Set l1) (O : Set l2) : Set (l ⊔ l1 ⊔ l2) where
   cs : (I -> O) -> CodeSegment I O
-
-cs2 : CodeSegment ds1 ds1
-cs2 = cs id
-
-cs1 : CodeSegment ds1 ds1
-cs1 = cs (\d -> goto cs2 d)
-
-cs0 : CodeSegment ds0 ds1
-cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
-
-main : ds1
-main = goto cs0 (record {a = 100 ; b = 50})
diff -r 68bf744d726e -r 5450e7ae5fa5 paper/src/CodeSegments.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/CodeSegments.agda	Wed Feb 01 15:27:15 2017 +0900
@@ -0,0 +1,12 @@
+cs2 : CodeSegment ds1 ds1
+cs2 = cs id
+
+cs1 : CodeSegment ds1 ds1
+cs1 = cs (\d -> goto cs2 d)
+
+cs0 : CodeSegment ds0 ds1
+cs0 = cs (\d -> goto cs1 (record {c = (ds0.a d) + (ds0.b d)}))
+
+main : ds1
+main = goto cs0 (record {a = 100 ; b = 50})
+