Извлечение Coq в Haskell с сохранением комментариев - PullRequest
Новая
       19

Извлечение Coq в Haskell с сохранением комментариев

7 голосов
/ 25 марта 2019

Есть ли возможность оставлять комментарии при извлечении 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, все работает отлично, кроме факта, что комментарий внутри factorial теряется: 

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

1 Ответ

5 голосов
/ 25 марта 2019

Нет, это невозможно.Чтобы проверить еще раз, вы можете видеть, что AST для внутреннего языка, который предназначен для извлечения , называемого MiniML, не имеет (по состоянию на v8.9) никаких конструкторов для комментариев.Соответствующий файл находится в репозитории Coq, plugins/extraction/miniml.ml.

...