Извлечение Coq в Haskell - PullRequest
Новая
       24

Извлечение Coq в Haskell

6 голосов
/ 18 марта 2019

Я экспериментирую с механизмом извлечения Coq для Haskell. Я написал наивный предикат для простых чисел в Coq, вот он: 

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith.PeanoNat.

(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
  match m,n with
  | 0,_ => false
  | 1,_ => false
  | _,0 => false
  | _,1 => false
  | S m',S n' => (orb ((mult m n) =? p) (helper' p m' n))
  end.

(**********)
(* helper *)
(**********)
Fixpoint helper (p m : nat) : bool :=
  match m with
  | 0 => false
  | S m' => (orb ((mult m m) =? p) (orb (helper' p m' m) (helper p m')))
  end.

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

Compute (isPrime 220).

(*****************)
(* isPrimeHelper *)
(*****************)
Extraction Language Haskell.

(*****************)
(* isPrimeHelper *)
(*****************)
Extraction "/home/oren/GIT/CoqIt/Primes.hs" isPrime helper helper'.

И после извлечения кода на Haskell я написал простой драйвер для его тестирования. Я столкнулся с двумя проблемами:

  1. Coq экспортировал свой собственный Bool вместо использования встроенного в Haskell логического типа.
  2. Coq также использовал свой nat, поэтому я не могу спросить isPrime 6, и мне нужно использовать S (S (...)). 
module Main( main ) where    
import Primes    
main = do
    if ((isPrime (
        Primes.S (
        Primes.S (
        Primes.S (
        Primes.S (
        Primes.S (
        Primes.S ( O ))))))))
        ==
        Primes.True)
    then
        print "Prime"
    else
        print "Non Prime"

Ответы [ 2 ]

8 голосов
/ 19 марта 2019

По поводу вашего первого пункта - попробуйте добавить 

Require Import ExtrHaskellBasic.

к вашему источнику Coq. Он указывает, что извлечение должно использовать определения прелюдии Haskell для некоторых основных типов. Документация может быть найдена здесь . Также есть аналогичный модуль для строк .

0 голосов
/ 19 марта 2019

Я публикую полное решение здесь, чтобы сделать это сообщение автономным.Надеюсь, что другие могут использовать его. 

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.Arith.PeanoNat.

(************)
(* helper'' *)
(************)
Fixpoint helper' (p m n : nat) : bool :=
  match m,n with
  | 0,_ => false
  | 1,_ => false
  | _,0 => false
  | _,1 => false
  | S m',S n' => (orb ((mult m n) =? p) (helper' p m' n))
  end.

(**********)
(* helper *)
(**********)
Fixpoint helper (p m : nat) : bool :=
  match m with
  | 0 => false
  | S m' => (orb ((mult m m) =? p) (orb (helper' p m' m) (helper p m')))
  end.

(***********)
(* isPrime *)
(***********)
Fixpoint isPrime (p : nat) : bool :=
  match p with
  | 0 => false
  | 1 => false
  | S p' => (negb (helper p p'))
  end.

Compute (isPrime 220).

(********************************)
(* Extraction Language: Haskell *)
(********************************)
Extraction Language Haskell.

(***************************)
(* Use Haskell basic types *)
(***************************)
Require Import ExtrHaskellBasic.

(****************************************)
(* Use Haskell support for Nat handling *)
(****************************************)
Require Import ExtrHaskellNatNum.
Extract Inductive Datatypes.nat => "Prelude.Integer" ["0" "succ"]
"(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/GIT/CoqIt/Primes.hs" isPrime helper helper'.

А вот драйвер: 

module Main( main ) where

import Primes
import Prelude

main = do
    if ((isPrime 220) == True)
    then
        print "Prime"
    else
        print "Non Prime"

Интересно упомянуть огромную разницу во времени между медленным Compute (isPrime 220) Coq и скомпилированным Haskell (и оптимизирован!) супер быстрая версия (is Prime 220).

...