IT練習ノート

IT関連で調べたこと(実際は嵌ったこと)を書いています。

CoqからHaskellのコードを生成する

Extractionという機能を使うとできるらしい。Coqで証明してHaskellで動作させる感じなのか。

coq.inria.fr

単純な方の定義

Inductive FBB : Type :=
  | Foo
  | Bar
  | Buzz.

Require Extraction.
Extraction Language Haskell.
Extraction "C:\work\FBB.hs" FBB.
module FBB where

import qualified Prelude

data FBB =
   Foo
 | Bar
 | Buzz

偶数判定は以下のように変換される。

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.
module Evneb where

import qualified Prelude

data Bool =
   True
 | False

data Nat =
   O
 | S Nat

evenb :: Nat -> Bool
evenb n =
  case n of {
   O -> True;
   S n0 -> case n0 of {
            O -> False;
            S n' -> evenb n'}}