2011年05月10日

OCamlでocamldebugを使う

研究の関係上、とあるOCamlのプロジェクト――いえ、まあ、とあるもなにも、Coqだが――をいじる必要が出た。

そんなにプログラミング・・・というかプロジェクトの読み解きなどをやったことがない私は、途方にくれ・・・まではしなかった。

運がいいことに、先輩から「そういうときはデバッガで追いながら読めばいいよ」というアドバイスを受けたことがあったからだ。

さすが先輩。先達はあらまほしきことなり。


で、デバッガを使うためにいろいろ調べながらやった結果知ったこと。

いまいちまとまった情報が見当たらない気がしたので、軽くメモ代わりにでも、と思った次第。

ocamldebugはバイトコードしか対応してない

明記してる人があまりいないのではっきりと。

OCamlには二つのコンパイラ、ocamlcとocamloptがある*1

前者がバイトコード(+VM?)へのコンパイラ、後者がネイティブコードへのコンパイラ。

どちらにもオプションとして-gが存在する。

だが、この二つのコンパイラでは、-gの説明がわずかだが異なる。

前者ではdebuggerと言う単語が陽に出てくるが、後者は出てこない。

というか対応してない。

現にocamloptでコンパイルしたプログラムをocamldebugに読み込ませると「対応したバイトコードじゃない」といってくる。

早く言ってくれ。

ちなみにocamloptの-gオプションは「例外をキャッチし損ねたときにスタックトレースを出したりする」のに使われるらしい。

デバッガ用オプションではない。

ocamldebugは元のソースコードが必要

絶対必要かまでは断言できないが、まずブレイクポイントが設定できない。

多くの解説ではソースコードがある環境で、ちょこちょこっとemacsでデバッガを動かしているのでよくわからない。

私のケースでは、プロジェクトの中を見ようとしている以上、バイナリとソースコードは全然違う場所にあるし、どちらも今自分のいるフォルダにはなかったりする*2

そしてブレイクポイントを設定しようとしたら「ソースコードがないよ」なんていわれる始末だ。

最初本気で何を言っているのかわからなかった。


ocamldebugにソースコードのあるフォルダを教えるオプションは-I。

ocamldebug -I toplevel bin/coqtop.byte -coqlib .

とかすると、「toplevelというフォルダをソースコード探索の対象に含め、binフォルダのcoqtop.byteを-coqlib .というオプションをつけてデバッグする」という形になる。

ocamldebugに渡すオプションは対象のプログラムの前。後ろは全て対象のプログラムのオプション。

ついでに:dumpobj

最初はデバッガの動かし方に四苦八苦したせいで、そもそもデバッグ情報が入ってるかすら怪しく感じ始めた。

そのため、まずその情報を見てみたくなった。

調べてみたらdumpobjというものがあるとかいう。

シェルに打ち込んでもそんなコマンドはないという。

なるほど、apt程度では入らないということか?仕方ない、自分でビルドしてインストールしよう。

した結果:make installしたらocamldumpobjという名前で入っていた。

名前変えるのか!?

早く言ってくれ。

実は入ってたりしたんじゃなかろうな*3


これで読み進められ・・・るといいな、と思っている。

散文になってしまったが、以上である。

*1:誰かが作った独自実装などの話はしてないのであしからず。

*2:makeするフォルダにいる場合。

*3:Ubuntuにて確認。OCamlをインストールすると入る。

posted by chiguri at 22:28| Comment(0) | TrackBack(0) | 研究

2011年02月11日

CoqのType classでExpression problemに挑戦する その2

なぜ一度で出来なかったか?

計画性がないからさ。


さて、ではType classで先ほどの流れをもう一度作ろう。

しかし、先ほどの定義とは、様々な点で異なるので注意。

Class Exp := { Eval : nat }.
Instance EConst (n : nat) : Exp := { Eval := n }.
Instance EAdd (e1 e2 : Exp) : Exp :=
 { Eval := let (n1) := e1 in let (n2) := e2 in n2 + n1 }.

式の定義がEvalによって特徴付けられている。

つまり、式とはある種のインターフェースでしかない。

では次に、スタックマシンの定義に入る。

Require Import List.
Class Word := { Exe : list nat -> option (list nat) }.
Instance WPush (n : nat) : Word := { Exe s := Some (n :: s) }.
Instance WPlus : Word :=
 { Exe s := match s with
            | n1 :: n2 :: s' => Some (n2 + n1 :: s')
            | _ => None
            end }.
Fixpoint Execute (p : list Word) s :=
 match p with
 | nil => match s with | n :: nil => Some n | _ => None end
 | w :: p' =>
   match Exe s with
   | None => None
   | Some s' => Execute p' s'
   end
 end.

命令はExeという名前のスタックマシンの状態遷移で定義されている。

また、Executeは再び関数として定義されている。

ではコンパイラの定義に・・・といいたいところだが、ここで少しばかり問題が生じる。

コンパイラは、どうしてもEConstやEAddの引数が見えなければ作れない。

しかし、Expを扱う関数からはこれらの引数が見えない。

このままでは、作れないことになる。


これは、CoqのType classとHaskellのType classの大きな差である。

Haskellの関数定義は元々開いている。

開いている、とはここでは定義のなかにデータ型の展開を直接書かないという意味だが、これは新たなインスタンスが出来た場合でも、そのインスタンス用の関数として定義すればいいことを意味している。

簡単に言えば、どんなときに関数を定義するときでもいつでも引数が見えている、ということだ。

一方、Coqの関数定義は閉じている。

関数の定義中に引数が必要になれば、必ず型を展開するように記述しなければならないため、結果としてインターフェースだけしかないType classでは新たな関数が定義できない。

このため、CoqのType classは演算子の追加などには強いものの、関数の追加に弱いわけである*1


これを解決することが出来ないのか、と言えば一応別の策がある。

Classを継承するように使えばいいわけである。

次のコードがそんな感じのもの。

Class CompExp := { E :> Exp ; Compile : list Word }.
Instance CEConst n : CompExp := { E := EConst n ; Compile := WPush n :: nil }.

さて、新たに作ったCompile付きの式は、内部にExpを持っている。

これを使えば今までの定義も使いまわせる、というわけである。

・・・え?足し算はどこに消えたのか?

そんなに見たいのですか、そうですか・・・

私が書いたコードは、次のようになっている。

Instance CEAdd (e1 e2 : CompExp) : CompExp.
destruct e1; destruct e2; constructor.
 destruct E0; destruct E1; constructor.
  apply (plus Eval0 Eval1).
 apply (app Compile0 (app Compile1 (WPlus :: nil))).
Defined.

なぜProofモードで作っているか、と?

それはこのインスタンスの定義が何度も展開を繰り返すからだ*2


今度は証明をしなければならないが、証明はEvalの結果とCompileの結果出てくる命令列を用いなければ出来ない。

つまり、また継承である。

もう面倒なので定数までにしておく。

Class CertCompExp := { CE :> CompExp ; Verify : forall p s, Execute (Compile++p) s = Execute p (Eval :: s) }.
Instance CCEConst (n : nat) : CertCompExp := { CE := CEConst n }.
auto.
Qed.


では、通常のデータ型で難しかった演算子の追加をやってみる。

ここでは掛け算だが、いたって簡単である。

Instance EMult (e1 e2 : Exp) : Exp :=
 { Eval := let (n1) := e1 in let (n2) := e2 in n1 * n2 }.
Instance WTimes : Word :=
 { Exe s := match s with
            | n1 :: n2 :: s' => Some (n2 * n1 :: s')
            | _ => None
            end }.
Instance CEMult (e1 e2 : CompExp) : CompExp.
...

というわけで、後は足し算同様に行えば出来るわけである。

たしかに元々あるコードに何もしていないので、その意味ではうまくいっている。

関数を追加するのも、確かに元のコードには一切手を出してない

なんとも七面倒なコードであるわけだが。


HaskellのType classについて、ボイラープレートが多いという記述をmaoeさんがしていたが、Coqはその比じゃないような・・・

まあ、Coqに以前からあった要素で構築したものなので、かなり無理やりで仕方ないといえば仕方ないのだが。

今回のように検証に用いる場合に、最も困る点はそこではなくて・・・

全ての構成要素について継承で列挙しなおさないと検証にならないし、誰も全ての式について保証してくれないことである。

各インスタンスでは確かに正しいのだが、ほしい式全体は正しくそこにエンコードされたのだろうか?誰か追加したものを忘れてはいないだろうか?

そんな疑心暗鬼に陥りそうな、CoqのType classでありましたとさ。


あー長かった。

*1:もちろん見えている処理だけで定義できる関数は容易に作れる。

*2:destructが4回も呼ばれていることに注意。

posted by chiguri at 01:43| Comment(0) | TrackBack(0) | 研究

CoqのType classでExpression problemに挑戦する

Coq8.2からType classが導入された。

もともとType classはHaskellにあったものである。

よって、Expression problemもHaskellからやり始めるのが楽である。

だが、私は残念ながらHaskellの世界の住人ではないので、Haskellによる解決に関しては私がこれをやるにいたった原因であるmaoeさんの記事を参照してほしい。


HaskellのType classなんてわからん!という人のために、Expression problemに関してだけ説明*1

要は、式を計算するようなプログラムを書いて、今まで書いた部分に手を加えることなく新しい演算子を入れたり新しい処理を定義してみたい、と*2

たとえば、足し算と引き算しかない小学校一年生の世界を、小学校二年生の世界へ広げるために掛け算を加えよう、ということだ。

・・・我ながら意味がわからない例だ。


さて、さっそくCoqで書いていくのだが。

まず通常のデータ型定義のやり方でやってみる*3

Inductive Exp := EConst (n : nat) | EAdd (e1 e2 : Exp).
Fixpoint Eval e :=
 match e with
 | EConst n => n
 | EAdd e1 e2 => Eval e1 + Eval e2
 end.

これで計算する関数の定義が完了である。

しかし、これだけでは面白くない。とはいえ、文字列に変換など、Coqらしくもない*4

よって、少し回り道をして、簡単なスタックマシンの定義と、式のコードへのコンパイルを行ってみる。

用いるコードは以下の通り。

Require Import List.
Inductive Word := WPush (n : nat) | WPlus.
Fixpoint Execute p s :=
 match p with
 | nil =>
   match s with
   | n :: nil => Some n
   | _ => None
   end
 | WPush n :: p' => Execute p' (n :: s)
 | WPlus :: p' =>
   match s with
   | n1 :: n2 :: s' => Execute p' ((n2 + n1) :: s')
   | _ => None
   end
 end.

これがスタックマシン。

そしてコンパイル用の関数を定義して、それが正しいことを証明する。

Fixpoint Compile e :=
 match e with
 | EConst n => WPush n :: nil
 | EAdd e1 e2 => Compile e1 ++ Compile e2 ++ WPlus :: nil
 end.
Goal forall e, Execute (Compile e) nil = Some (Eval e).

あとはこれを証明する・・・のだが、証明については省略しておこう。

ただし、一つだけ言っておくと、実はこの補題を証明しないとうまくいかない(または非常に難しい)。

Goal forall e p s, Execute (Compile e ++ p) s = Execute p (Eval e :: s).

これで一通り終わった。


さて、これに新たな動作を定義するのはどうするか?

普通に関数を定義すればよい。証明も同様。

こちらは非常に簡単なのである。

では、これに掛け算を導入しようと考えたら、一体どこを変更すればいいだろうか?

実は、スタックマシンの命令が足りないことも考慮すると、最後の定理以外全て、である。

つまりExpression problemに対応できていないわけだ。

これを解決するのに使えるのがType classである。


さて、記事が長くなってきたので、本題のType classは次の記事に書こう。

*1:元のネタなどもmaoeさんの記事にあるので、読みたい方はそちらを。

*2:わざと少しだけ解釈を変えている。事実上はほとんど変わらないが、正確ではない。

*3:短くするために型のほとんどは省略している。気になる場合各自がCoq上でPrintしていただきたい。

*4:Coqは証明してこそCoqらしい。

posted by chiguri at 00:28| Comment(0) | TrackBack(0) | 研究

2010年04月29日

輪講用テキスト

今年の研究室輪講は、Implementing functional languagesという本(といっても本自体は絶版、リンク先からPDFがダウンロード可能)になった。

しかし、この本・・・

明らかに実装言語変えてるのに、テキストがところどころ元のまま。

というか実装言語が途中途中で変わってるわけで、気持ち悪いことこの上ない!

説明があってない!

説明がない機能をぽこぽこと使ってる!


勘弁してほしい・・・orz

そのうちTypo(うち間違いのこと)じゃなくて一貫性保持のためのエラッタとしてまとめて送るかなあ・・・

posted by chiguri at 05:02| Comment(0) | TrackBack(0) | 研究

2009年12月21日

論文を書いていた

オワタ\(^o^)/。

以上。無念なり・・・

posted by chiguri at 05:49| Comment(0) | TrackBack(0) | 研究