Coq XML 协议：可能是 PrintAST 故障

Question

我正在使用来自 Coq 8.6.1 的 XML 协议。当我尝试调用 PrintAst 时，我未能获得 AST，而是获得了 "todo"。这是故障还是我做错了什么？我应该如何从打印 AST 调用中获取 AST？

这是我的案例：我使用 coqtop -toploop coqidetop -main-channel stdfds 打开一个 ideslave 进程，然后输入 coq-8.6.1/theories/FSets/FSetCompat.v.

的 Coq 代码

如果你想重复我的实验，我在这里用“<<<<<<<”来附上一些详细的过程。

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

首先，我输入

<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>，我希望return得到

的AST

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.

令我失望的是，我得到了

<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 到输入缓冲区位置。

Coq XML 协议：可能是 PrintAST 故障

Coq XML Protocol: a likely PrintAST malfunction

xml

coq

coq-tactic

coqide

coq-extraction