この記事は Theorem Prover Advent Calendar 2014 の5日目の記事です。

昨日は notogawa さんの ブラウザ上でAgdaを試せるサイトを作ってみた でした。Try Agda、前に見せていただいたときよりかなり綺麗になっててビビりました。自分の ProveEverywhere はやるやる言いながら放置なので、ダメですね…

Verlang と Coq の Extraction について

さて、本題ですが、Coq には Extraction という、Coq のコードを別の言語に変換する機能があり、この機能によってコードを検証済みの部品として実際のプログラムに使えるようになっています。標準では OCaml, Haskell, Scheme への変換が可能になっています。

この記事では、Verlang という、Coq の Extraction 対象に Erlang のコア言語である Core Erlang を加えるパッチ (つまり Coq2Erlang 的なもの) について紹介したいと思います。

Core Erlang について

Core Erlang は Erlang のコアとなる部分を抽出したシンプルな言語です。言語仕様の現在のバージョンは2004年に書かれたものです。

Erlang 標準の erl コマンドで Erlang から Core Erlang に、Core Erlang から beam にコンパイルできます。

% erl
Erlang/OTP 17 [erts-6.2] [source] [64-bit] [smp:4:4] [async-threads:10] [hipe] [kernel-poll:false] [dtrace]

Eshell V6.2  (abort with ^G)
1> c(hoge, to_core). %% hoge.erl を Core Erlang にコンパイル (hoge.core ができる)
ok
2> c(hoge, from_core). %% hoge.core を beam 形式にコンパイル (hoge.beam ができる)
{ok,hoge}

詳しく知りたい方はここにある Language Specification や Introduction を読んで欲しいのですが、ちょっとだけサンプルコードを見てみます。

下のサンプルコードはリストの map (: (A -> B) -> list A -> list B) の定義です。

module 'map' ['map'/2] attributes []

'map'/2 = fun (F, L) ->
  case L of
    [] when 'true' -> []
    [H | T] when 'true' -> [apply F(H) | apply 'map'/2(F, T)]
  end

end

Erlang を知らなくてもなんとなく雰囲気でわかると思います (Erlang では変数は大文字始まり、'map'/2 は map は引数を2個取る関数という意味、[H | T] は H :: T (cons) のことです)。だいたい Erlang と同じですが、以下のような違いがあります。

• モジュールとエクスポートの書き方が異なる
• トップレベルのパターンマッチは書けない
• モジュール内の関数呼び出しは apply をつける
  • apply 'map'/2(F, T) は call 'map':'map'/2(F, T) と書くこともできて、モジュールを明示しなければならない場合はこのように call で書きます。
• アトムは必ずシングルクオートで囲む
• パターンの後の when は必ずつける

言語としてはこれ以外にも、メッセージを受け取る際に使う receive や、例外処理のtry ... catch などがあります。

Verlang について

Verlang というのは、はじめにも書いたように Coq の Extraction 対象に Core Erlang を加えるようなパッチです。パッチをあてる対象は Coq8.4pl2 になっています。

ここで説明する Verlang のバージョンは 2014/12/05 現在の HEAD である 12ca9a0e57 です。

また、これ以降では Verlang パッチをあてた Coq のことも Verlang と言うことにします。

Verlang Vagrant box と Verlang のインストール

Vagrant Cloud に Verlang と Erlang がインストールされた box を上げているので簡単に試せます。(Docker コンテナも作ろうと思ったけど作ってない)

$ vagrant init amutake/verlang
$ vagrant up
$ vagrant ssh
...
$ coqc -v
The Coq Proof Assistant, version 8.4pl2 (December 2014)
compiled on Dec 04 2014 17:03:59 with OCaml 3.12.1
$ erl -version
Erlang (SMP,ASYNC_THREADS) (BEAM) emulator version 6.2

手元で試したい方は、

$ git clone git://github.com/tcarstens/verlang.git
$ cd verlang
$ wget https://coq.inria.fr/distrib/8.4pl2/files/coq-8.4pl2.tar.gz
$ tar xf coq-8.4pl2.tar.gz
$ patch -u -p1 -d coq-8.4pl2 < src/verlang.patch
$ cd coq-8.4pl2
$ ./configure -prefix ../ # mac を使っていて gcc が Clang になっている場合は configure を編集して -fno-defer-pop を消す
$ make world
$ make install

で、/path/to/verlang/bin に Core Erlang に抽出できるようになった coqc コマンドなどができます。

Arch Linux を使っている人はリポジトリの中に PKGBUILD ファイルがあるのでそれを使うと簡単に入れられるみたいです。

使ってみる

基本的には OCaml や Haskell などへの Extraction と同様に、

Extraction Language CoreErlang.

でターゲットを Core Erlang に変えて、

Extraction hoge.
Recursive Extraction foo bar.
Extraction "hoge.core" hoge.

とかします。

Core Erlang のサンプルコードと比較するために map を Extract してみようと思います。

map.v

Fixpoint map {A B} (f : A -> B) (l : list A) : list B :=
  match l with
    | [] => []
    | h :: t => f h :: map f t
  end.

Extraction Language CoreErlang.
Extraction "map.core" map.

coqc map.v とすると、map.core と map.hrl が出てきます。.core は Core Erlang のファイルで、.hrl は Erlang のヘッダーファイルみたいです。hrl の方は Verlang はまだサポートしていないみたいです。

map.core

module 'Coq.Init.Datatypes' [  ] attributes [ ]

end

module 'map' [ 'map'/2 ] attributes [ ]
'map'/2 = fun (_f, _l) ->
  case _l of
    [] when 'true' ->
        []
    [_t|_h] when 'true' ->
        [apply _f (_t)|call 'map':'map'
            ( _f
            , _h
            )]
  end
end

map.core を見てみると上のようになっていました。Core Erlang のサンプルコードとほとんど同じです。アンダースコア始まりでも変数として使えるみたいです。カリー化された関数はカリー化されていない関数になるみたいです。

さて、これをコンパイルするのですが、このままコンパイルしようとしても失敗してしまいます。
コンパイルできるようにするには map.core を編集してモジュールの定義をいじらなければいけません。
具体的には、

• モジュールを一つにする
• モジュール名 (module の後に続く atom) をファイルの名前と同じにする
• 関数定義の中に出てくるモジュール名を適切なものに変える

をします。特に3番目を忘れるとコンパイル時にはエラーが出ずに実行時にエラーが出るので注意してください。

編集後の map.core はこうなります。

map.core

module 'map' [ 'map'/2 ] attributes [ ]
'map'/2 = fun (_f, _l) ->
  case _l of
    [] when 'true' ->
        []
    [_t|_h] when 'true' ->
        [apply _f (_t)|call 'map':'map'
            ( _f
            , _h
            )]
  end
end

これを Erlang でコンパイルして使ってみます。

$ erl
1> c(map, from_core).
{ok,map}
2> map:map(fun (X) -> X + 1 end, [1,2,3]).
[2,3,4]

使えました。

他の例

自分で型を定義して使ってみます。

型を Extract

適当に mylist という型を作ってみます。

type.v

Inductive mylist (A : Set) : Set :=
| my_nil : mylist A
| my_cons : A -> mylist A -> mylist A.

Arguments my_nil {A}.
Arguments my_cons {A} _ _.

Extraction Language CoreErlang.
Extraction "type.core" mylist.

coqc type.v してみます。

type.core

module 'type' [  ] attributes [ ]

end

出てきません。型宣言は出てこないようです。

値を Extract

次に適当に値を作ってそれを Extract してみます。

type2.v

Inductive mylist (A : Set) : Set :=
| my_nil : mylist A
| my_cons : A -> mylist A -> mylist A.

Arguments my_nil {A}.
Arguments my_cons {A} _ _.

Definition nats := my_cons 0 (my_cons 1 (my_cons 2 my_nil)).

Extraction Language CoreErlang.
Extraction "type2.core" nats.

type2.core

module 'Coq.Init.Datatypes' [  ] attributes [ ]

end

module 'type2' [  ] attributes [ ]

end

これも出てきません。Erlang ではトップレベルには関数しか書けない (はず。間違ってたらすみません) からでしょうか。

関数を Extract

unit をとって mylist nat を返すような関数にしてみます。

type3.v

Inductive mylist (A : Set) : Set :=
| my_nil : mylist A
| my_cons : A -> mylist A -> mylist A.

Arguments my_nil {A}.
Arguments my_cons {A} _ _.

Definition nats (_ : unit) := my_cons 0 (my_cons 1 (my_cons 2 my_nil)).

Extraction Language CoreErlang.
Extraction "type3.core" nats.

type3.core

module 'Coq.Init.Datatypes' [  ] attributes [ ]

end

module 'type3' [ 'nats'/1 ] attributes [ ]
'nats'/1 = fun (_x) ->
  { 'My_cons'
  , 'O'
  , { 'My_cons'
  , {'S', 'O'}
  , { 'My_cons'
  , {'S', {'S', 'O'}}
  , 'My_nil'
  }
  }
  }
end

出てきました。

インデントをきちんとさせるとこんなかんじ。

type3.core

module 'type3' [ 'nats'/1 ] attributes [ ]
'nats'/1 = fun (_x) ->
  { 'My_cons'
  , 'O'
  , { 'My_cons'
    , {'S', 'O'}
    , { 'My_cons'
      , {'S', {'S', 'O'}}
      , 'My_nil'
      }
    }
  }
end

コンストラクタがあるときは、{'My_cons', {'My_cons', ...}} のようにコンストラクタ名のアトムがはじめにくるタプルになるようです。(Erlang では {a, b, c, ...} はタプル)

メッセージパッシング

Erlang はアクターモデルに基づいたメッセージパッシング方式の並行計算ができることが特徴なので、並行プログラムを生成したくなります。メッセージを受け取るために receive という、キューからメッセージを受け取ってパターンマッチを行う文法があるのですが、Verlang は receive に対応しているのかしていないのかわからないという感じです。README にはできるっぽいことが書いてありますが...

実際に receive を作っている部分である coreerlang.v の L246-L264 を見ると、match .. with の中に apply でもって 'receive_fin'/2 というのが使われていると receive になるっぽいです。

つまり

match receive_fin delay default with
  | ... => ...
  | ... => ...

のように書くと、

receive
    ... -> ...
    ... -> ...
    after delay -> default

となるのですが、receive_fin というアトムをどう作ればいいかわかりませんでした。Axiom や別の関数にすると apply ではなく call が使われてしまい、引数にすると _receive_fin になってしまいます。

ちょっと Verlang を改造すれば簡単にできそうですが、できれば改造しないで receive を生成したいので、方法がわかったらまた書きたいと思います。

Verlang のパッチ

Verlang (というか Extraction 対象を増やす場合全般) は Coq にパッチをあててコンパイルするようになっています。実際にパッチをあてて変更している箇所を見ていきたいと思います。
Verlang は 8.4pl2 を対象にしているのでこの説明でも Coq8.4pl2 で説明します。現在の Coq とは異なっているところがけっこうあるので気をつけてください。

src/verlang.patch がパッチのファイルです。これを見ればだいたい何をやっているかわかります。

• ide/coq_lex.mll#L104
  • CoqIDE の字句解析器に CoreErlang というトークンを追加している？
• plugins/extraction/common.ml
  • L312-314
    • CoreErlang 用に識別子の変換規則を追加
  • L554-L560
    • (pp_coreerlang_gen の定義) 生成規則に則って実際に Core Erlang のコードを出力するところ？(自信なし)
  • L588
    • 言語で場合分けをして pp_language_gen するところに Core Erlang の pp_coreerlang_gen を追加
  • L617
    • 文字型の名前
• plugins/extraction/coreerlang.ml, plugins/extraction/coreerlang.mli
  • Core Erlang コードの生成規則 (メイン)
• plugins/extraction/extract_env.ml#L382
  • Core Erlang の language_descr (後述) を追加
• plugins/extraction/extraction_plugin.mllib
  • Extract するモジュールの追加？
• plugins/extraction/g_extraction.ml4#L46,L53
  • lang 型と文字列の相互変換に CoreErlang を追加
• plugins/extraction/table.ml#L537, plugins/extraction/table.mli#L136
  • lang 型に CoreErlang を追加

一番重要なのが extract_env.ml で使われていて coreerlang.ml で定義されている coreerlang_descr で、これは language_descr というレコード型の値なのですが、この language_descr の値が MiniML から各言語への生成規則になっているようです。MiniML というのは ML のサブセットのような言語で、Extraction する際はこの言語を経由して対象の言語に変換されます。

(* plugins/extraction/miniml.mli の最後 *)

type language_descr = {
  keywords : Idset.t; (* 予約語リスト *)

  (* Concerning the source file *)
  file_suffix : string; (* 言語の拡張子 *)
  preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; (* コードの最初に書くべきもの (モジュール名とかインポートとか) *)
  pp_struct : ml_structure -> std_ppcmds; (* モジュールの中身の MiniML からの出力規則 *)

  (* Concerning a possible interface file *)
  sig_suffix : string option; (* ヘッダーファイルの拡張子 (.mli とか) *)
  sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; (* ヘッダーファイルの最初に書くべきもの *)
  pp_sig : ml_signature -> std_ppcmds; (* ヘッダーファイルの出力 *)

  (* for an isolated declaration print *)
  pp_decl : ml_decl -> std_ppcmds; (* 宣言の出力規則？ *)

}

language_descr を作る以外は簡単そうなので、新しく Extraction 先を追加したい場合は頑張って language_descr の値を作ればいいということになります。

coreerlang.v の実装

最後に、src/extractor に定義されている Coq コードを見ていきたいと思います。

src/extractor にあるものは、coreerlang.v 以外はほとんど対応する OCaml の各シグネチャに一致するように作られたものです。

Verlang	対応するもの
OurString.v	Str モジュール
PP.v	lib/pp.mli
MiniML.v	plugins/extraction/miniml.mli

coreerlang.ml は coreerlang.v から変換されたもので、他の言語のファイル (plugins/extraction/ocaml.ml, plugins/extraction/haskell.ml など) と同じように使うので、名前とシグネチャを一致させることが重要になります。

で、MiniML から Core Erlang の AST に変換する部分が書いてある coreerlang.v の解読と説明までしようと思っていたのですが、時間がもうギリギリなのでまたあとでということにしたいと思います。すみません。

まとめ

• Verlang という Coq から Core Erlang に Extract できるようにするものを触ってみました。
• 抽出後のコードについて簡単に見てみました。
• Verlang ではどのように作っているかを中途半端ですが調べてみました。

明日6日目の担当は chiguri さんです。よろしくお願いします！