\chapter{Continuation based C と Agda} 
\label{c:cbc_agda}
現在 CbC では検証用の上位言語として Agda を利用しており、
Agda では CbC のプログラムをメタ計算を含む形で記述することができる。

先行研究\cite{atton-master} では CbC と Agda を対応させるための型付けが行われているが、
ここでは、その型付けは使わず、前段階である Agda での記述のみで説明を行う。

本章では当研究室で推奨している単位での検証を行うために、
Agda で DataGear、 CodeGear を表現し、
これらの単位を用いた検証を行う事ができることを示す。

\section{DataGear、 CodeGear と Agdaの対応}
Agda での DataGear は Agda で使うことのできるすべてのデータに対応する。
また、Agda での記述はメタ計算として扱われるので、
Context を通すことなくそのまま扱う。

CodeGear は DataGear を受け取って処理を行い DataGear を返す。
また、CodeGear 間の移動は継続を用いて行われる。
継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、
次の CodeGear へ継続を行うものであった。

これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当し、
継続渡し(Continuation Passing Style) で書かれた Agda の関数と対応する。
継続は不定の型 (\verb/t/) を返す関数で表される。
継続先は次に実行する関数の型を引数として受け取り不定の型\verb/t/を返す関数として記述され、
CodeGear 自体も同じ型 \verb/t/ を返す関数となる。

\coderef{agda-cg} は Agda で記述した加算を行う CodeGear の例である。

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

\verb/plus 10 20/ を評価すると \verb/next/ に 30 が入力されていることがわかる。


\section{Meta Gears の表現}
\label{s:meta-gears}
通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。
Meta DataGear はメタ計算で使われる DataGear で、実行するメタ計算によって異なる。
検証での Meta DataGear は、 DataGear が持つ同値関係や、大小関係などの関係を表す DataGear がそれに当たると考えられる。
Agda 上では Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。
\coderef{agda-mdg} は While Program での制約条件をまとめたものである。

\lstinputlisting[label=agda-mdg, caption= Agda における Meta DataGear] {src/agda-mdg.agda.replaced}

ここでは \verb/whileTestState/ で Meta DataGear を識別するためのデータを分け、
\verb/whileTestStateP/ でそれぞれの Meta DataGear を返している。
ここでは \verb/(vari env ≡ 0) /\ (varn env ≡ c10 env)/ などのデータを Meta DataGear として扱う。


Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。
Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返す CodeGear である。

メタ計算で検証を行う際の Meta CodeGear は Agda で記述した CodeGear の検証そのものである。
例として \coderef{agda-mcg} を示す。

\lstinputlisting[label=agda-mcg, caption= Agda における Meta CodeGear] {src/agda-mcg.agda.replaced}

\verb/whileTestPwP/ は Meta CodeGear の例である。
ここでは Meta DataGear に \verb/mdg/ という名前をつけてある。
この Meta CodeGear では次の CodeGear に mdg を渡しており、
CodeGear 内で Meta DataGear の性質が正しいことを検証して次の CodeGear に遷移することがわかる。

Meta CodeGear はMeta DataGear を含んだ形で記述される。