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?
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.
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.