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.