|
57
|
1 \chapter{Agda における Continuation based C の表現}
|
|
|
2 \label{chapter:cbc-type}
|
|
58
|
3 CbC の項を部分型を用いて Agda 上に記述していく。
|
|
|
4 DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、 Agda 上で実行できることを確認する。
|
|
|
5 また、Agda上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 上で証明していく。
|
|
|
6
|
|
|
7 \section{DataSegment の定義}
|
|
|
8 まず DataSegment から定義していく。
|
|
|
9 DataSegment はレコード型で表現できるため、Agda のレコードをそのまま利用できる。
|
|
|
10 例えは~\ref{src:goto} に示していた a と b を加算して c を出力するプログラムに必要な DataSegment を記述すると~\ref{src:agda-ds}のようになる。
|
|
|
11 cs0 は a と b の二つの Int 型の変数を利用するため、対応する ds0 は a と b のフィールドを持つ。
|
|
|
12 cs1 は計算結果を格納する c という名前の変数のみを持つので、同様にds1もcのみを持つ。
|
|
|
13
|
|
|
14 \lstinputlisting[label=src:agda-ds, caption=Agda における DataSegment の定義] {src/DataSegment.agda}
|
|
|
15
|
|
57
|
16 \section{CodeSegment の定義}
|
|
58
|
17 次に CodeSegment を定義する。
|
|
|
18 CodeSegment は DataSegment を取って DataSegment を返すものである。
|
|
|
19 よって $ I \rightarrow O $ を内包するデータ型を定義する。
|
|
|
20
|
|
|
21 レコード型の型は Set なので、Set 型を持つ変数 I と O を型変数に持ったデータ型 CodeSegment を定義する。
|
|
|
22 I は Input DataSegment の型であり、 O は Output DataSegment である。
|
|
|
23
|
|
|
24 CodeSegment 型のコンストラクタには \verb/cs/ があり、Input DataSegment を取って Output DataSegment を返す関数を取る。
|
|
|
25 具体的なデータ型の定義はリスト ~\ref{src:agda-cs} のようになる。
|
|
|
26
|
|
|
27 \lstinputlisting[label=src:agda-cs, caption= Agda における CodeSegment 型の定義] {src/CodeSegment.agda}
|
|
|
28
|
|
|
29 この CodeSegment 型を用いて CodeSegment の処理本体を記述する。
|
|
|
30
|
|
|
31 まず計算の本体となる cs0 に注目する。
|
|
|
32 cs0 は二つのInt型変数を持つ ds0 を取り、一つのInt型変数を作った上で cs1 に軽量継続を行なう。
|
|
|
33 DataSegment はレコードなので、a と b のフィールドから値を取り出した上で加算を行ない、cを持つレコードを生成する。
|
|
|
34 そのレコードを引き連れたまま cs1 へと goto する。
|
|
|
35
|
|
|
36 次に cs1 に注目する。
|
|
|
37 cs1 は値に触れず cs2 へと goto するだけである。
|
|
|
38 よって何もせずにそのまま goto する関数をコンストラクタ\verb/cs/ に渡すだけで良い。
|
|
|
39
|
|
|
40 最後に cs2 である。
|
|
|
41 cs2 はリスト~\ref{src:goto}では省略していたが、今回は計算を終了させる CodeSegment として定義する。
|
|
|
42 どの CodeSegment にも軽量継続せずに値を持ったまま計算を終了させる。
|
|
|
43 コンストラクタ \verb/cs/ には関数を与えなくては値を構成できないため、何もしない関数である id を渡している。
|
|
|
44
|
|
|
45 最後に計算をする cs0 へと軽量継続する main を定義する。
|
|
|
46 例として、 a の値を 100 とし、 b の値を50としている。
|
|
|
47 正しく計算が行なえたら値150が得られるはずである。
|
|
|
48
|
|
57
|
49 \section{ノーマルレベル計算の実行}
|
|
58
|
50 \section{MetaDataSegment の定義}
|
|
57
|
51 \section{MetaCodeSegment の定義}
|
|
|
52 \section{メタレベル計算の実行}
|
|
|
53 \section{Agda を用いたContinuation based C の検証}
|
|
|
54 \section{スタックの実装の検証}
|
