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.