Is there a way to extract ASTs from the Coq compiler?

Developing plugins
1

I’m interested in analyzing the ASTs that the Coq compiler generates while it compiles. Is there any way to extract these by default, or will I have to go digging around in the compiler source?

1 Like
2

There are multiple ways to work with ASTs without resorting to ML plugins:

  • SerAPI/coq-lsp provide sexp/json variants of the AST (AFAIU), usable from any (?) language
  • MetaCoq/TemplateCoq provides access to Coq kernel ASTs from within Coq, as an inductive type (very bare bones de Bruijn encoding of variables)
  • Coq-Elpi provides higher level access to the AST from an embedded lambda-prolog interpreter in Coq, using lambda-prolog’s binding support to deal with variables.
1 Like
3

Note indeed that as @mattam82 points out there are 2 ASTs in Coq:

  • kernel-level Ast (not extensible, low-level, used mainly by tactics)
  • parsing-level Ast (extensible, high-level, represents Coq’s input almost exactly)

Of the 3 systems, SerAPI provides access to both kernel and parsing-level AST, while elpi and metacoq do work with kernel terms. Thus, YMMV.