The Coq mailing list

[e AT x80.org (Emilio Jesús Gallego Arias)]

Hi Talia,

Talia Ringer 
<tringer AT cs.washington.edu>
 writes:

> For a project I'm working on, I need to be able to get ASTs for Coq terms.
> So far I'm aware of a few options:
>
>    - JSON extraction in 8.5, which does not work for us because we also
>    need information in Prop
>    - A Peacoq plugin which we are trying to get working
>    - The XML protocol, which I know nothing about (is this useful?) but see
>    referenced in old Coq-club threads
>    - template-coq, which is neat but does not fit our needs
>
> I'm wondering if anyone knows of any other parsers that produce ASTs for
> Coq terms, including Props, preferably as s-expressions (or something
> similarly versatile).

I am replying quite late and indeed we have discussed about this
elsewhere, but I am replying here anyways for completeness.

Another potentially useful ─ but quite experimental approach ─ is
coq-serapi [1]

Indeed, coq-serapi has been designed for the particular purpose of
exporting Coq AST and protocols in a format suitable for mechanical
manipulation.

The project may not seem very active these days, but this is for we are
busy trying to incorporate into Coq 8.7 some changes that will make
SerAPI work much better.

To process a Coq file in SerAPI, you'd usually do:

(StmAdd () $FILE_CONTENTS)

This will parse and load a whole file, assigning "State IDs" to each
sentence.

Then, you could query for the AST of state sid:

(Query () (Ast sid))

for a particular definition:

(Query () (Definition "id"))

goals, etc... We'd be glad to take issues or questions on GitHub.

Best,
Emilio

[1] https://github.com/ejgallego/coq-serapi