CODEWITHSUNDEEP
haskellcommentscoq
OrenIshShalom
OrenIshShalom

Reputation: 7162

Extracting Coq to Haskell while keeping comments

Is there anyway to keep comments while extracting Coq to Haskell? Ideally, I would like to have machine generated Haskell files untouched by humans, and so the motivation of extracting comments is clear. However, I couldn't find how to do it, and I wonder if this is at all possible (?). Here is an example Coq file:

(*************)
(* factorial *)
(*************)
Fixpoint factorial (n : nat) : nat :=
  match n with
  | 0 => 1
  | 1 => 1 (* this case is redundant *)
  | S n' => (mult n (factorial n'))
  end.

Compute (factorial 7).

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

(***************************)
(* Extract to Haskell file *)
(***************************)
Extraction "/home/oren/Downloads/RPRP/output.hs" factorial.

And when I extract it to Haskell everything works fine other than the fact that the comment inside factorial is lost:

$ coqc ./input.v > /dev/null
$ cat ./output.hs
module Output where

import qualified Prelude

data Nat =
   O
 | S Nat

add :: Nat -> Nat -> Nat
add n m =
  case n of {
   O -> m;
   S p -> S (add p m)}

mul :: Nat -> Nat -> Nat
mul n m =
  case n of {
   O -> O;
   S p -> add m (mul p m)}

factorial :: Nat -> Nat
factorial n =
  case n of {
   O -> S O;
   S n' ->
    case n' of {
     O -> S O;
     S _ -> mul n (factorial n')}}

Upvotes: 6

Views: 173

Answers (1)

Antal Spector-Zabusky
Antal Spector-Zabusky

Reputation: 36622

No, this isn't possible. To double-check, you can see that the AST for the internal language that extraction targets, called MiniML, doesn't (as of v8.9) have any constructors for comments. The relevant file is in the Coq repository, plugins/extraction/miniml.ml.

Upvotes: 6

Related Questions