Coq XML Protocol: вероятная неисправность PrintAST

Question

Я использую протокол XML из Coq 8.6.1. Когда я попробовал вызов PrintAst, мне не удалось получить AST, но вместо этого я получил "todo". Это неисправность или я сделал что-то не так? Как я должен получить AST от печатного вызова AST?

Вот мой случай: я использовал coqtop -toploop coqidetop -main-channel stdfds чтобы открыть процесс Ideslave, а затем введите код Coq из coq-8.6.1/theories/FSets/FSetCompat.v,

Здесь я использую "<<<<<<<" для включения некоторых подробных процедур, если вы хотите повторить мой эксперимент.

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<

Во-первых, я ввожу

<call val="Add"><pair><pair><string>(***********************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
(* &lt;O___,, *        INRIA-Rocquencourt  &amp;  LRI-CNRS-Orsay              *)
(*   \VV/  *************************************************************)
(*    //   *      This file is distributed under the terms of the      *)
(*         *       GNU Lesser General Public License Version 2.1       *)
(***********************************************************************)

(** * Compatibility functors between FSetInterface and MSetInterface. *)

Require Import FSetInterface FSetFacts MSetInterface MSetFacts.
</string><int>1</int></pair><pair><state_id val="1"/><bool val="true"/></pair></pair></call>

затем

<call val="Add"><pair><pair><string>Set Implicit Arguments.
</string><int>1</int></pair><pair><state_id val="2"/><bool val="true"/></pair></pair></call>

затем

<call val="Add"><pair><pair><string>Unset Strict Implicit.
</string><int>1</int></pair><pair><state_id val="3"/><bool val="true"/></pair></pair></call>

и наконец

<call val="Add"><pair><pair><string>
(** * From new Weak Sets to old ones *)

Module Backport_WSets
 (E:DecidableType.DecidableType)
 (M:MSetInterface.WSets with Definition E.t := E.t
                        with Definition E.eq := E.eq)
 &lt;: FSetInterface.WSfun E.
</string><int>1</int></pair><pair><state_id val="4"/><bool val="true"/></pair></pair></call>

<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<

На этот раз я позвонил <call val="PrintAst"><state_id val="5"/></call>, который я ожидаю вернуть АСТ

Module Backport_WSets
 (E:DecidableType.DecidableType)
 (M:MSetInterface.WSets with Definition E.t := E.t
                        with Definition E.eq := E.eq)
 <: FSetInterface.WSfun E.

К моему разочарованию, я получил

<value val="good"><gallina begin="42" end="228"><todo begin="42" end="228">Module&nbsp;Backport_WSets&nbsp;(E:&nbsp;DecidableType.DecidableType)
&nbsp;&nbsp;(M:&nbsp;MSetInterface.WSets&nbsp;with&nbsp;Definition&nbsp;E.t&nbsp;:=&nbsp;E.t&nbsp;with&nbsp;Definition
&nbsp;&nbsp;&nbsp;E.eq&nbsp;:=&nbsp;E.eq)&lt;:&nbsp;FSetInterface.WSfun&nbsp;E.</todo></gallina></value>

Благодаря красивой печати это

<value val="good">
    <gallina begin="42" end="228">
        <todo begin="42" end="228">Module Backport_WSets (E: DecidableType.DecidableType)
  (M: MSetInterface.WSets with Definition E.t := E.t with Definition
   E.eq := E.eq)<: FSetInterface.WSfun E.</todo>
    </gallina>
</value>

Но это всего лишь копия кода! Он даже не применил лексер... Почему это случилось? Может ли кто-нибудь помочь? Спасибо вам большое!

Answer 1

print_ast вызов не был завершен, и он был удален в новых версиях Coq.

Если вам нужно структурированное представление данных Coq, я рекомендую Coq SerAPI, основанный на автоматической сериализации. [Отказ от ответственности: я автор]

Редактировать: как это сделать в SerAPI:

echo '
(Add () "From Coq Require Import FSetInterface FSetFacts MSetInterface MSetFacts.

(** * From new Weak Sets to old ones *)

Module Backport_WSets
 (E:DecidableType.DecidableType)
 (M:MSetInterface.WSets with Definition E.t := E.t
                        with Definition E.eq := E.eq)
 <: FSetInterface.WSfun E.")
(Query () (Ast 3))
' | ./sertop.native --printer=human

Урожай [после удаления информации о местоположении из AST, которая довольно многословна]:

((CoqAst
  (VernacDefineModule ()
    (Id Backport_WSets)
    (((Id E)))
      (CMident
       (Ser_Qualid (DirPath ((Id DecidableType))) (Id DecidableType))
       DefaultInline)
     (()
      (((Id M)))
      ((CMwith
        (CMwith
         (CMident
          (Ser_Qualid (DirPath ((Id MSetInterface))) (Id WSets))))
        (CWith_Definition
         (((Id E) (Id t)))
         (CRef
          (Qualid
           ((Ser_Qualid (DirPath ((Id E))) (Id t))))
          ()))
        (CWith_Definition
         (((Id E) (Id eq)))
         (CRef
          (Qualid
           ((Ser_Qualid (DirPath ((Id E))) (Id eq))))
          ()))
        DefaultInline)))
     (Check
      (CMapply
       (CMident
        (Ser_Qualid (DirPath ((Id FSetInterface))) (Id WSfun))))
      ((v (CMident (Ser_Qualid (DirPath ()) (Id E))))
       DefaultInline)))
    ()))

Более того, в наши дни Coq и SerAPI предоставляют общую систему отображения формы AST для определения местоположения входного буфера.