%% Natural Deduction の説明をして、 Agda が命題を証明することができることを示す
%% 章? 要る。。。かどうかは微妙な気がする。 「こういう話で Agda では証明ができます。」
%% で勝手に証明して証明できたね！はありだけど読み手があんまり嬉しくないかも。
%% ソレだとやっぱり自然演繹の話しして~同型対応でちゃんとつながってるね~じゃあ
%% Agda で表現できるし証明できるねでいい感じかも

\chapter{Agda における CbC の表現}

% ツッコミどころさん
% どうするのかは書けるけどなんでAgdaなの？みたいな話が飛んでくる

前章では Agda の文法について説明した。
本章では CbC と対応して CodeGear、 DataGear、 継続を Agda で表現する。
また、 Agda で継続を記述することで得た知見を示す。

\section{Agda での CodeGear 、 DataGear 、 継続の表現}

%% 書くこと
% CodeGearとDataGearのAgda上での定義

DataGear はレコード型で表現できるため、 Agda のレコード型をそのまま利用して定義
してく。
記述は~\ref{src:agda-ds}のようになる。

\lstinputlisting[label=src:agda-ds, caption=Agda における DataGear の定義]
{src/DataSegment.agda.replaced}

CodeGear は DataGear を受け取って DataGear を返すという定義であるため、
$ I \rightarrow O $ を内包する CodeGear 型のデータ型(~\ref{src:agda-cs})を定義する。

\lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced}

CodeGear 型を定義することで、 Agda での CodeGear の本体は Agda での関数そのもの
と対応する。
% しかし、そのままだと再帰呼び出しの点で CbC との対応が失われてしまう。
% そのため、 Agda では \verb/goto/を利用できるのは関数の末尾のみという制約を設ける
% 必要がある。
% この制約さえ満たせば、

CodeGear の実行は CodeGear 型から関数本体を取り出し、レコード型を持つ値を適用す
ることに相当する。


CbC での軽量継続は

\begin{itemize}
 \item 次に実行する CodeGear を指定する
 \item CodeGear に渡す DataGear を指定する
 \item 現在実行している CodeGear から制御を指定された CodeGear へと移す
\end{itemize}

の機能を持っている。

この機能を満たす関数はソースコード\ref{src:agda-goto} として定義されている。

\lstinputlisting[label=src:agda-goto, caption=Agdaにおける goto の定義] {src/Goto.agda.replaced}

goto は CodeGear よりも一つ Level が上の Meta CodeGear にあたり、次に実行する
CodeGear 型を受け取り、Input DataGear、 Output DataGear を返す。型になっている。


\section{Agda での Stack、 Tree の実装}

ここでは Agda での Stack 、 Tree の実装を示す。

Stack の実装を以下のソースコード\ref{src:stack-impl}で示す。
実装は SingleLinkedStack という名前で定義されている。
定義されている API は push を例に残りは省略する。残りのの実装は付録に示す。 %~\

\lstinputlisting[label=src:stack-impl, caption=Agdaにおける Stack の実装] {src/AgdaStackImpl.agda.replaced}

Element は SingleLinkedStack で扱われる要素の定義で、現在のデータ datum と次のデー
タを Maybe 型という値の存在が不確かな場合の型で包み、自身で再帰的に定義している。
Maybe 型では値が存在する場合は Just 、 存在しない場合は　Nothing を返す。

SingleLinkedStack 型では、この Element の top 部分のみを定義している。

Stack に対する push 操作では stack と push する element 型の datum を受け取り、 datum
の next に現在の top を入れ、 stack の top を受け取った datum に切り替え、新しい
stack を返すというような実装をしている。

Tree の実装(以下のソースコード\ref{src:tree-impl})は RedBlackTree という名前で定義されている。
定義されている API は put 以後省略する。残りのの実装は付録に示す。 %~\

\lstinputlisting[label=src:tree-impl, caption=Agdaにおける Tree の実装] {src/AgdaTreeImpl.agda.replaced}

Node 型は key と value 、 Color と Node の rihgt 、 left の情報を持っている。
Tree を構成する末端の Node は leafNode 型で定義されている。

RedBlackTree 型は root の Node 情報と Tree に関する計算をする際に、そこまでの
Node の経路情報を保持するための nodeStack と 比較するための compare を持っている。

Tree の put 操作では tree 、 put するノードのキーと値(k1、value)を引数として受け
取り、Tree の root に Node が存在しているかどうかで場合分けしている。
Nothing が返ってきたときは RedBlackTree 型の tree 内に定義されている root に受け
取ったキーと値を新しいノードとして追加する。
Just が返ってきたときは root が存在するので、経路情報を積むために nodeStack を初
期化し、受け取ったキーと値で新たなノードを作成した後、ノードが追加されるべき位置
までキーの値を比べて新しい Tree を返すというような実装になっている。

\section{Agda における Interface の実装}

%% 書くこと
% stack の Interface部分と redBlackTree の Interface部分。
% interfaceとは?->cbcのとこに突っ込んでこっちは同様に〜で済ませたい

Agda 側でも CbC 側と同様に interface を実装した。
interface は record で列挙し、ソースコード~\ref{src:agda-interface}のように紐付けることができる。
CbC とは異なり、 Agda では型を明記する必要があるため record 内に型を記述している。

例として Agda で実装した Stack 上の interface (ソースコード\ref{src:agda-interface})を見る。
Stack の実装は SingleLinkedStack(ソースコード\ref{src:agda-single-linked-stack}) として書かれている。それを Stack 側から
interface を通して呼び出している。

ここでの interface の型は Stack の record 内にある pushStack や popStack などで、
実際に使われる Stack の操作は StackMethods にある push や popである。この push
や pop は SingleLinkedStack で実装されている。

% \lstinputlisting[label=src:agda-single-linked-stack, caption=Agda における Stack
% の実装] {src/AgdaSingleLinkedStack.agda.replaced}

\lstinputlisting[label=src:agda-interface, caption=Agda における Interface の定義] {src/AgdaInterface.agda.replaced}

interface を通すことで、実際には Stack の push では stackImpl と何らかのデータ a を取
り、 stack を変更し、継続を返す型であったのが、 pushStack では 何らかのデータ a を取り stack を変更
して継続を返す型に変わっている。

また、 Tree でも interface を記述した。

\lstinputlisting[label=src:agda-tree, caption=Tree Interface の定義]{src/AgdaTree.agda.replaced}

interface を記述することによって、データを push する際に予め決まっている引数を省
略することができた。
また、 Agda で interface を記述することで CbC 側では意識していなかった型が、明確
化された。

% 元の push では 送り先の stack を関数に書く必要があり、異なる stack に push
% する可能性があったが、 pushStack では紐付けた Stack に push することになり

\section{継続を使った Agda における Test , Debug}

Agda ではプログラムのコンパイルが通ると型の整合性が取れていることは保証できるが、必ず
しも期待した動作をするとは限らない。そのため、本研究中に書いたプログラムが正しい動
作をしているかを確認するために行なった手法を幾つか示す。

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
今回は実験中にソースコード\ref{src:agda-stack-test}のような Test を書いた。
この Test では Stack をターゲットにしていて、 Stack に1、 2の二つの$ \mathbb{N} $型のデー
タを push した後、 pop2 Interface を使って Stack に入っている 1、 2 が Stack の
定義である First in Last out の通りに 2、 1 の順で取り出せるかを確認するために作成した。

\lstinputlisting[label=src:agda-stack-test, caption=Agdaにおけるテスト]{src/AgdaStackTest.agda.replaced}

上の Test では、02 が 2つのデータを push し、 03 で 二つのデータを pop する pop2
を行っている。それらをまとめて記述したものが 04 で 2 回 push し、 2つのデータを pop する動
作が正しく行われていれば 04 は True を返し、 05 で記述された型通りに互いに等しくなる
ため 05 が refl でコンパイルが通るようになる。
今回は、 pop2 で取れた値を確認するため 03 の後に 031、 032 の二つの作成した。
032 では 03 で扱っている値が Maybe であるため、 031 のような比較をする前に値が確
実に存在していることを示す補題である。 032 を通すことで 031 では 2つの値があり、
かつ$\mathbb{N}$型である事がわかる。 031 では直接取れた値が 2、 1 の順番で入って
いるかを確認している。

この Test でエラーが出なかったことから、 Stack に1、2の二つのデータを pushする
と、 push した値が Stack 上から消えることなく push した順番に取り出せることが分
かる。


また、継続を用いて記述することで関数の Test を書くことで計算途中のデータ内部をチェックするこ
とができた。

ここでの \$ は \( \) をまとめる糖衣構文で、 \$ が書かれた一行を\(\)でくくること
ができる。
% \ref{sintax}のようなコードを
% \begin{lstlisting}[frame=lrbt,label=sintax,caption={\footnotesize 通常の継続の
%     コード}]

% \end{lstlisting}

% \begin{lstlisting}[frame=lrbt,label=sintax-sugar,caption={\footnotesize 糖衣構文
%     を用いた継続のコード}]

% \end{lstlisting}

ソースコード~\ref{src:agda-tree-debug}のように関数本体に記述してデータを返し、C-c C-n
(Compute normal form) で関数を評価すると関数で扱っているデータを見ることができる。
また、途中の計算で受ける変数名を変更し、 Return 時にその変更した変数名に変えるこ
とで、計算途中のデータの中身を確認することができる。評価結果はソースコード内にコメントで記述した。

 \lstinputlisting[label=src:agda-tree-debug, caption=Agdaにおけるテスト]{src/AgdaTreeDebug.agda.replaced}

今回、この手法を用いることで複数の関数を組み合わせた findNode 関数内に異常があるこ
とが分かった。


%getRedBlackTree の関数に

% \lstinputlisting[label=agda-Debug, caption=Agdaにおけるデバッグ]{src/AgdaTreeDebug.agda.replaced}
% Tree全然載せてないけどどうしよ。。。どこに書こうかは考えておきましょう