--- a/paper/agda.tex	Fri Feb 03 14:49:58 2017 +0900
+++ b/paper/agda.tex	Fri Feb 03 16:34:30 2017 +0900
@@ -433,6 +433,8 @@
 
 \lstinputlisting[label=src:agda-parameterized-module, caption=Agda における Parameterized Module] {src/AgdaParameterizedModule.agda}
 
+% TODO: where 句の説明
+
 % }}}
 
 % {{{ Reasoning

Binary file paper/atton-master.pdf has changed

--- a/paper/atton-master.tex	Fri Feb 03 14:49:58 2017 +0900
+++ b/paper/atton-master.tex	Fri Feb 03 16:34:30 2017 +0900
@@ -114,11 +114,10 @@
 \mainmatter
 
 %chapters
-\input{introduction.tex}
-
-\input{cbc.tex}
-\input{type.tex}
-\input{agda.tex}
+% \input{introduction.tex}
+% \input{cbc.tex}
+% \input{type.tex}
+% \input{agda.tex}
 \input{cbc-type.tex}
 
 \chapter{まとめ}

--- a/paper/cbc-type.tex	Fri Feb 03 14:49:58 2017 +0900
+++ b/paper/cbc-type.tex	Fri Feb 03 16:34:30 2017 +0900
@@ -182,27 +182,81 @@
 
 % }}}
 
+% {{{ Agda を用いた Continuation based C の検証
+
 \section{Agda を用いた Continuation based C の検証}
 Agda において CbC の CodeSegment と DataSegment を定義することができた。
 実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
 
-ここでは赤黒木の実装に用いられているスタックの性質について注目する。
-この時のスタックはポインタを利用した片方向リストを用いる。
+ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。
+この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。
 
-CbC における構造体 \verb/stack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。
+CbC における DataSegment \verb/SingleLinkedStack/ の定義はリスト~\ref{src:cbc-stack}のようになっている。
 
 \lstinputlisting[label=src:cbc-stack, caption=CbC における構造体 stack の定義] {src/stack.h}
 
-Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。
-CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定して、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。
+次に Agda における \verb/SingleLinkedStack/の定義について触れるが、Agda にはポインタが無いため、メモリ確保や\verb/NULL/の定義は存在しない。
+CbC におけるメモリ確保部分はノーマルレベルには出現しないと仮定し、\verb/NULL/の表現にはAgda の標準ライブラリに存在する \verb/Data.Maybe/ を用いる。
 
 \verb/Data.Maybe/ の \verb/maybe/ 型は、コンストラクタを二つ持つ。
-片方のコンストラクタ \verb/just/ は値を持つ。
-これは計算を行なうことができる値であり、ポインタの先に値があることに対応している。
-一方のコンストラツア \verb/nothing/ は値を持たない。
+片方のコンストラクタ \verb/just/ は値を持ったデータであり、ポインタの先に値があることに対応している。
+一方のコンストラクタ \verb/nothing/ は値を持たない。
 これは値が存在せず、ポインタの先が確保されていない(\verb/NULL/ ポインタである)ことを表現できる。
 
 \lstinputlisting[label=src:agda-maybe, caption=Agda における Maybe の定義] {src/Maybe.agda.replaced}
 
+Maybe を用いて片方向リストを Agda 上に定義するとリスト~\ref{src:agda-stack}のようになる。
+CbC とほぼ同様の定義ができている。
+CbC、 Agda 共に\verb/SingleLinkedStack/ は \verb/Element/ 型の \verb/top/ を持っている。
+\verb/Element/ 型は値と次の \verb/Element/ を持つ。
+CbC ではポインタで表現していた部分が Agda では Maybe で表現されているが、\verb/Element/ 型の持つ情報は変わっていない。
+
+\lstinputlisting[label=src:agda-stack, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaStack.agda}
+
+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=agda-stack-ds, caption=スタックを利用するための DataSegment の定義] {src/AgdaStackDS.agda}
+
+次にスタックへの操作に注目する。
+スタックへと値を積む \verb/pushSingleLinkedStack/ と値を取り出す \verb/popSingleLinkedStack/ の CbC 実装をリスト~\ref{src:cbc-push-pop}に示す。
+\verb/SingleLinkedStack/ は Meta CodeSegment であり、メタ計算を実行した後には通常の CodeSegment へと操作を移す。
+そのために \verb/next/ という名前で次のコードセグメントを保持している。
+具体的な \verb/next/ はコンパイル時にしか分からないため、\verb/.../ 構文を用いて不定としている。
+
+\verb/pushSingleLinkedStack/ は \verb/element/ を新しく確保し、値を入れた後に \verb/next/ へと繋げ、 \verb/top/ を更新して軽量継続する。
+\verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。
+値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。
+
+\lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c}
+
+次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。
+同様に \verb/pushSingleLinkedStack/ と \verb/popSingleLinkedStack/ を定義している。
+\verb/pushsinglelinkedstack/ では、スタックの値を更新したのちにノーマルレベルの CodeSegment である \verb/n/ を \verb/exec/ している。
+なお、 \verb/liftMeta/ はノーマルレベルの計算をメタレベルとする関数である。
+
+実際に値を追加する部分は where 句に定義された関数 \verb/push/ である。
+これはスタックへと積む値が空であれば追加を行なわず、値がある時は新たに element を作成して top を更新している。
+本来の CbC の実装では空かチェックはしていないが、値が空であるかに関わらずにスタックに積んでいるために挙動は同じである。
+
+次に \verb/popSingleLinkedStack/ に注目する。
+こちらも操作後に \verb/nextCS/ へと継続を移すようになっている。
+
+実際に値を取り出す操作はノーマルレベルからアクセスできる \verb/element/ の値の確定と、アクセスできない \verb/stack/ の更新である。
+
+\verb/element/については、 \verb/top/ が空なら取り出した後の値は無いので \verb/element/ は \verb/nothing/ である。
+\verb/top/ が空でなければ \verb/element/ は \verb/top/ の値となる。
+
+\verb/stack/ は空なら空のままであり、\verb/top/ に値があればその先頭を捨てる。
+ここで、\verb/pop/ の実装はスタックが空であっても、例外を送出したり停止したりせずに処理を続行できることが分かる。
+
+\lstinputlisting[label=src:agda-push-pop, caption=Agda における片方向リストを用いたスタックの定義] {src/AgdaPushPop.agda}
+
+また、この章で取り上げた CbC と Agda の動作するソースコードは付録に載せる。 % TODO
+
+% }}}
+
 
 \section{スタックの実装の検証}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaPushPop.agda	Fri Feb 03 16:34:30 2017 +0900
@@ -0,0 +1,28 @@
+pushSingleLinkedStack : Meta -> Meta
+pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
+  where
+    n = Meta.nextCS m
+    s = Meta.stack  m
+    e = Context.element (Meta.context m)
+    push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
+    push s nothing  = s
+    push s (just x) = record {top = just (cons x (top s))}
+
+popSingleLinkedStack : Meta -> Meta
+popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
+  where
+    n = Meta.nextCS m
+    con  = Meta.context m
+    elem : Meta -> Maybe A
+    elem record {stack = record { top = (just (cons x _)) }} = just x
+    elem record {stack = record { top = nothing           }} = nothing
+    st : Meta -> SingleLinkedStack A
+    st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
+    st record {stack = record { top = nothing           }} = record {top = nothing}
+
+
+pushSingleLinkedStackCS : M.CodeSegment Meta Meta
+pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
+
+popSingleLinkedStackCS : M.CodeSegment Meta Meta
+popSingleLinkedStackCS = M.cs popSingleLinkedStack

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaStack.agda	Fri Feb 03 16:34:30 2017 +0900
@@ -0,0 +1,13 @@
+data Element (a : Set) : Set where
+  cons : a -> Maybe (Element a) -> Element a
+
+datum : {a : Set} -> Element a -> a
+datum (cons a _) = a
+
+next : {a : Set} -> Element a -> Maybe (Element a)
+next (cons _ n) = n
+
+record SingleLinkedStack (a : Set) : Set where
+  field
+    top : Maybe (Element a)
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaStackDS.agda	Fri Feb 03 16:34:30 2017 +0900
@@ -0,0 +1,17 @@
+record Context : Set where
+  field
+    -- fields for stack
+    element : Maybe A
+
+
+open import subtype Context as N
+
+record Meta  : Set₁ where
+  field
+    -- context as set of data segments
+    context : Context
+    stack   : SingleLinkedStack A
+    nextCS  : N.CodeSegment Context Context
+
+open import subtype Meta as M
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/Maybe.agda	Fri Feb 03 16:34:30 2017 +0900
@@ -0,0 +1,3 @@
+data Maybe {a} (A : Set a) : Set a where
+  just    : (x : A) -> Maybe A
+  nothing : Maybe A

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/singleLinkedStack.c	Fri Feb 03 16:34:30 2017 +0900
@@ -0,0 +1,18 @@
+__code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) {
+    Element* element = new Element();
+    element->next = stack->top;
+    element->data = data;
+    stack->top = element;
+    goto next(...);
+}
+
+__code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) {
+    if (stack->top) {
+        data = stack->top->data;
+        stack->top = stack->top->next;
+    } else {
+        data = NULL;
+    }
+    goto next(data, ...);
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/stack.h	Fri Feb 03 16:34:30 2017 +0900
@@ -0,0 +1,7 @@
+struct SingleLinkedStack {
+    struct Element* top;
+} SingleLinkedStack;
+struct Element {
+    union Data* data;
+    struct Element* next;
+} Element;