The Coq mailing list

[Valentin Robert <vrobert AT cs.ucsd.edu>]

Dear coq-club,

I have been looking into building on top of Coq 8.5, and for the purpose of my tools, I would like to get rich ASTs for the current hypotheses and goal of the proof in progress. What I mean by rich is, I would like to know both the low-level term (with all notations resolved), and the high-level view of it (what notations are used, and what do they map to), as well as the relations between the two.

To the extent of my investigation, I believe that:

- the PrintAST command of the new XML protocol prints AST information for Vernacular commands that were sent to the interpreter, but cannot give information about the current Gallina context ;

- the constr type has the low-level information I want ;

- the constr_expr type has part of the high-level information I want (the name of the notations), and I can query the notation printing rules to obtain their precedence and unparsing rules, which I can recover associativity information from (it is a bit tedious) ;

It seems though that the only way to recover the "notation to low-level" mapping is to use the glob_constr type, and recursively query for possible notations using Notation.uninterp_notations and pattern matching the interpretation term (a notation_constr term) with the glob_constr I have to figure out which notation matches and how much of the glob_constr is part of the notation.

Am I missing something that I could use to obtain this information much more easily?

Thanks,

- Valentin