Есть ли возможность сохранять комментарии при извлечении Coq в Haskell?? В идеале я хотел бы, чтобы файлы Haskell, сгенерированные машиной, не были затронуты людьми, поэтому мотивация извлечения комментариев ясна. Однако я не смог найти, как это сделать, и мне интересно, возможно ли это вообще (?). Вот пример файла 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')}}
Нет, это невозможно. Чтобы проверить еще раз, вы можете увидеть, что AST для внутреннего языка, на который нацелено извлечение, называемый MiniML, не имеет (начиная с версии 8.9) каких-либо конструкторов для комментариев. Соответствующий файл находится в репозитории Coq, plugins/extraction/miniml.ml
.
Это может быть не всегда возможно — рассмотрите комментарий
(* -} *)
. Будет ли это преобразовано в{- -} -}
?