Coq XML Protocol: a likely PrintAST malfunction

Question

I am using the XML Protocol from Coq 8.6.1. When I tried the PrintAst call, I failed to get an AST, but got an "todo" instead. Is this a malfunction or did I do something wrong? How should I get an AST from a print AST call?

Here is my case: I used coqtop -toploop coqidetop -main-channel stdfds to open an ideslave process, an then input the Coq code from coq-8.6.1/theories/FSets/FSetCompat.v.

Here I use "<<<<<<<" to enclose some detailed procedures if you would like to repeat my experiment.

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

First, I input

<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>

then

<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>

then

<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>

and finally

<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>

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

At this time, I called <call val="PrintAst"><state_id val="5"/></call>, which I expect to return the AST of

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

To my disappointment, I got

<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>

By pretty printing it is

<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>

But this is merely a copy of the code! It even didn't apply a lexer... Why would this happen? Could somebody help? Thank you so much!

Answer 1

The print_ast call was never completed and it has been removed in newer Coq versions.

If you need a structured representation of Coq data I recommend Coq SerAPI which is based on automatic serialization. [Disclaimer: I am the author]

Edit: how to do that in 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

yields [after removing location info from the AST which is quite verbose]:

((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)))
    ()))

what is more, Coq and SerAPI provide these days a generic mapping system form ASTs to input buffer location.