2012年1月22日日曜日

coq2scalaをさわってみた

http://proofcafe.org/wiki/Coq2Scala を試してみました。

インストールはhgでソースコードとってきて、
./configure
make world
make install
でおk。

Extraction Language Scala. が使えちゃうCoqがインストールされます。

使ってみた

とりあえず自然数と足し算を定義してみます。


吐き出されたScalaのコード。


Notationは無視される?
パラメータとらない場合はcase object使って欲しいかも・・・・
あとインデントも付くとうれしい。

ClassとInstanceを使ってみる

Monoidを定義してみた。

私はtraitとimplicit parameterでかっこ良く変換されるのかな!?と期待。


結果は・・・・・


(´・ω・`)ショボーン
明示的にインスタンスを渡して関数を得る感じですね。
まぁ、まだまだ開発途中なのでこれからどうなるかはわかりません。

最後に証明付きコード


proof-editing mode楽しいです。
ScalaでPDDの時代が来るかもですね。

0 件のコメント:

コメントを投稿