What is it, naokirin?

Coq to OCamlで便利な標準ライブラリ(型変換)

先日Coqの関数をOCamlのコードとして出力してみました。

サンプルとしては

(* ret_num.v *)
Definition ret_num (n : nat) : nat := n.

Extraction "ret_num.ml" ret_num.

coqc ret_num.v

して

(* ret_num.ml *)

type nat =
| O
| S of nat

(** val ret_num : nat -> nat **)

let ret_num n =
  n

ができるんですが、これだとOCamlでは使いづらすぎます。(nat型ではなく、できればint型で扱いたいところ)。

で調べてみると、Coqのコード側で型がちゃんと変換されるように書くことができるらしいのです。
今回であれば

Extract Inductive nat => int [ "0" "succ" ]
 "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

をret_num.vに追加することで、Coqのnat型をOcamlコードを出力する際にはint型として出力できます。

(** val ret_num : int -> int **)

let ret_num n =
  n


ところで、その他いろいろと型の扱いが違うCoqとOCamlなのですが、いちいちありふれた型についてこの変換のコードを書くのも面倒です。
そこで自力でモジュールなりを作れないかと思ったのですが、流石に始めたばかりのCoqで右も左もわからない状況では無理。Webを見てみるとCoqBaseというのがあったらしいことが判明。でもこれ今はそのままでは使えないみたいです。ビルドができません。

でいろいろ読みあさってみると、ななななんと!Coq8.2, 8.3あたりのChange logにこんな記述が!

Files ExtrOcaml*.v in plugins/extraction try to provide a library of common
extraction commands: mapping of basics types toward Ocaml's counterparts,
conversions from/to int and big_int, or even complete mapping of nat,Z,N
to int or big_int, or mapping of ascii to char and string to char list
(in this case recognition of ascii constants is hard-wired in the extraction).

なんだあるじゃないですか!

標準に私の望んでた機能はフツーに入ったみたいです。ただ情報としてはあんまり表に出回ってない?

先ほどのであれば、

Require Import ExtrOcamlNatInt.

を一行追加することでExtract Inductive 〜.なんて書かなくともnat型からint型に自動的に変換してくれます。(実際にはExtrOcamlNatInt内で全く同じことをしています。)

OCamlの変換関連の便利ライブラリはhttp://coq.inria.fr/stdlib/index_library_E.htmlのExtrOcaml*がそれです。ただの型変換が欲しい場合はリンク先で

Extract Inductive bool => bool [ true false ].

のように書いてある、=>の右と左の対応を見ればだいたいわかると思います。(あとはライブラリ名から推測)

ただ自分で作った型の場合は自力での変換も必要なので、Extract Inductive や Extract Constantといったものも覚えておくと便利だと思います。
以上メモ書きでした。