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

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

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

前章では Agda の文法について説明した。
本章では CbC 

\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 型から関数本体を取り出し、
レコード型を持つ値を適用することに相当する。

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

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

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

例として Agda で実装した Stack 上のinterface を見る。
ここでの interface の型は Stack の record 内にある pushStack や popStack などで、 実際に使われる Stack の操作は StackMethods にある push や popである。

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

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

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 の
FILO の定義通り 2、 1 の順で取り出せるかを確認するために作成した。

\lstinputlisting[label=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 の順番で入って
いるかを確認している。

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

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

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

評価結果はソースコード内にコメントで記述した。
今回、この手法を用いることで複数関数を組み合わせた findNode 関数内に異常があるこ
とが分かった。


%getRedBlackTree の関数に

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%