Я использую протокол XML из Coq 8.6.1. Когда я попробовал вызов PrintAst, мне не удалось получить AST, но вместо этого я получил «todo». Это неисправность или я что-то не так сделал? Как мне получить AST из вызова print 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 *)
(* <O___,, * INRIA-Rocquencourt & 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)
<: 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>, который, как я ожидаю, вернет AST
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 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>
Красивой печатью это
<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>
Но это всего лишь копия кода! Он даже не применил лексер... Почему это произошло? Может ли кто-нибудь помочь? Большое спасибо!
