CoqからHaskellのコードを生成する
Extraction
という機能を使うとできるらしい。Coq
で証明してHaskell
で動作させる感じなのか。
単純な方の定義
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'}}