fetburner.core

コアダンプ

CoqからSMLへ

CoqにはExtractionという機能があり、Coqで書かれたソースコードから対応する他の言語のソースコードを出力する事ができます。今回はそのExtractionをStandard MLに対応させた事について書こうと思います。

僕の通う大学にはStandard MLを使うプログラミング演習Bという講義があり、発展課題として、与えられた小さな処理系を改造するものとSMLまたはOCamlで自分の役に立つソフトウェアを書くものがありました。

始めCoqのExtractionを用いて証明されたSMLのサブセットを書いて前者に充てるつもりでしたが、標準でExtractionはStandard MLに対応しておらず、てっきり名古屋あたりの人かどこかの大学の人が作っていると思ったら手つかずの状態だったので、ExtractionをSMLに対応させる事で後者に充てる事にしました。*1

原理

CoqのExtractionで出力できる言語は標準でOCamlHaskellSchemeの三つがあります。 他にも非公式ではRuby等に対応させたものがありますが、この様にいくつもの言語に出力できるのには理由がありまして、CoqからExtractionで他言語のコードを出力する際一度MiniMLというMLのサブセットの様な中間言語に変換しているため、ML系の言語なら適当にプリントする部分を書くだけで対応させる事ができるのです。 その上、同じML系の言語であるOCamlへのExtractionは標準で対応しているため、MiniMLからOCamlへ変換する部分のコードを改造してSMLに対応するようにしました。

苦労した点としてはSMLのfunは引数を1つ以上取らなければならない事が挙げられます。 このため、OCamlでは何も考えずにlet recと書いておけば良い所でも引数の数で場合分けする必要がありました。 あとはレコードをExtractionした際に出力される

(** val left : ('a1, 'a2) pair -> 'a1 **)

let left x = x.left

の様なコードは、#が付いていないSMLでは型注釈を付ける必要がある事ぐらいでしょうか。

インストールの方法

肝心の成果物はhttps://github.com/fetburner/Coq2SMLで公開しています。 多分通常のCoqをインストールする場合と同じ手順でインストールできると思います。

使い方

上の改造されたCoqをインストールすると、

Extraction Language Sml.

というコマンドが使えるようになります。 これを実行すると、以降ExtractionでSMLのソースコードが出力されます。

例えばCoqで二分木を平坦化する関数の素朴な実装と高速な実装を書いて、両者が同じ事を確かめてからSMLのソースコードを出力したい場合以下の様に書きます。

Require Import List Arith Program.

(* 二分木 *)
Inductive tree (A : Type) : Type :=
  | leaf : A -> tree A
  | node : tree A -> tree A -> tree A.

(* 愚直な実装 *)
Fixpoint slow_dfs {A} (t : tree A) :=
  match t with
  | leaf x => [x]
  | node l r => slow_dfs l ++ slow_dfs r
  end.

(* 高速な実装 *)
Fixpoint dfs_aux {A} (acc : list A) (t : tree A) :=
  match t with
  | leaf x => x :: acc
  | node l r => dfs_aux (dfs_aux acc r) l
  end.
Definition dfs {A} (t : tree A) := dfs_aux [] t.

(* 補題 *)
Lemma dfs_aux_fact : forall A (l : list A) (t : tree A),
  dfs_aux l t = dfs_aux nil t ++ l.
Proof.
  intros A l t.
  generalize dependent l.
  induction t; intros l.
    reflexivity.

    simpl.
    rewrite -> IHt1.
    rewrite -> IHt2.
    rewrite app_assoc.
    congruence.
Qed.

(* 愚直な実装と高速な実装で同じ値を返す事の証明 *)
Theorem dfs_valid : forall A (t : tree A), dfs t = slow_dfs t.
Proof.
  unfold dfs.
  intros A t.
  induction t.
    reflexivity.

    simpl.
    rewrite -> dfs_aux_fact.
    congruence.
Qed.

Extraction Language Sml.
Extract Inductive list => "list" ["[]" "(::)"].
Extract Constant app => "(fn x => fn y => x @ y)". 
Extraction "dfs.sml" slow_dfs dfs.

このとき、以下の様なソースコードが出力されます。

(** val app : 'a1 list -> 'a1 list -> 'a1 list **)

val app = (fn x => fn y => x @ y)

datatype 'a tree =
  Leaf of 'a
| Node of 'a tree * 'a tree

(** val slow_dfs : 'a1 tree -> 'a1 list **)

fun slow_dfs t =
  case t of
    Leaf x => x::[]
  | Node (l, r) => app (slow_dfs l) (slow_dfs r)

(** val dfs_aux : 'a1 list -> 'a1 tree -> 'a1 list **)

fun dfs_aux acc t =
  case t of
    Leaf x => x::acc
  | Node (l, r) => dfs_aux (dfs_aux acc r) l

(** val dfs : 'a1 tree -> 'a1 list **)

fun dfs t =
  dfs_aux [] t

現在モジュールには対応していませんが、気が向いたら実装するかもしれません。 バグや要望があればissue等で連絡して頂ければ対応します。

*1:CoqはOCamlで書かれているので問題は無いという理屈