Extracting Coq to Haskell while keeping comments

Question

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')}}

Answer 1

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.