在保留评论的同时将 Coq 提取到 Haskell答案

【问题标题】：Extracting Coq to Haskell while keeping comments在保留评论的同时将 Coq 提取到 Haskell
【发布时间】：2019-03-26 03:35:09
【问题描述】：

在将 Coq 提取到 Haskell 时是否有保留 cmets？理想情况下，我希望机器生成的 Haskell 文件不受人类影响，因此提取 cmets 的动机很明确。但是，我找不到该怎么做，我想知道这是否可能（？）。这是一个示例 Coq 文件：

(*************)
(* 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.

当我将它提取到 Haskell 时，除了阶乘中的注释丢失之外，一切正常：

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

【问题讨论】：

这可能并不总是可行的——请考虑评论(* -} *)。那会被转换成{- -} -}吗？

标签： haskell comments coq

【解决方案1】：

不，这是不可能的。仔细检查一下，您可以看到名为 MiniML 的 the AST for the internal language that extraction targets（从 v8.9 开始）没有任何 cmets 构造函数。相关文件位于 Coq 存储库中，plugins/extraction/miniml.ml。

【讨论】：