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

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

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

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.