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.