\section{Continuation based C と Agda}
本章では CbC に対応した Agda を記述する際の手法を説明する。

\subsection{GearsAgda 形式で書く agda}
Agdaでは関数の再帰呼び出しが可能であるが、CbCでは値が 帰って来ない。そのためAgda
で実装を行う際には再帰呼び出しを行わないようにする。
code \ref{agda-cg}が例となるコードである。

\lstinputlisting[caption= Agdaでの CodeGear の例, label=agda-cg, firstline=6]{src/agda/cbc-agda.agda.replaced}

1行目で Data Gear の定義を行っている。
今回は 2つの数値の足し算を行うコードを実装するため、
varx と vary の二つの自然数を持つ。

7行目の plus-com が受け取っている値を定義している。
Env と next と exit を受け取っている。

next と next は Env → t となっているが、
これは Env を受け取って不定の型 (t) を返すという意味である。
これで 次の関数遷移先を取れるようにしている。


9行目から10行目では入ってきた varx で場合分けを行っており、varx が zero ならそのまま vary を返し、次の遷移先へ、
varx が zero 以外なら varx から1を引いて、vary に 1 を足して遷移する。

13行目でxがzero以外の値であった場合の遷移先を指定している。
ここでは自身である plus-p をループするように指定した。
CbCでは再起処理を実装することはできないが、自己呼び出しを行うことはできるので、
それに合ったようにAgdaでも実装を行なう。

17行目が実際に値を入れる部分で、
Exitが実行の終了になるようにしている。

前述した加算を行うコードと比較すると、不定の型 (t) により継続を行なっている部分が見える。
これがAgdaで表現された CodeGear となり、本論では Gears Agda と呼ぶ

\subsection{agda による Meta Gears}
通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
今回はその Meta Gears をAgdaによる検証の為に用いる。

\begin{itemize}
\item Meta DataGear \mbox{}\\
  Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
  これを用いることで、仕様となる制約条件を記述することができる。

\item Meta CodeGear\mbox{}\\
  Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear
  である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返
  す CodeGear である。故に、Meta CodeGear は Agda で記述した CodeGear の検証そのものである
\end{itemize}