Is there any way to get span information for the hypotheses and goal when querying their ASTs? It makes sense that the
loc object is empty since the hypotheses and goal were not written in the document but I wonder if it's possible to get the info somehow. Thanks!
HI @Axel Marmet , unfortunately this is not possible today, this is due the way Coq's printer work.
Let me summarize the situation:
Constr.t ---[detype + externalization]----> Ast.t where
Ast.t is the Coq's AST, note that kernel terms have no notion of location, as they are mainly computational objects
CoqAst.t to a "box layout"
Pp.t, this is already accessible from SerAPI
Format module is used to render to text, but for example jsCoq renders
Pp.t to HTML
So indeed, as you can see, you are looking at the data generated at step 2, however, textual locations don't appear until step 4 as the provenance of the objects is not from a text document
Imagine this case
(App (Ref "f") [arg1;...;argn])
the printing routine could split the application in two lines to fit it in the window, depending on the size of the display port
so @Axel Marmet , the way I'd address your question is maybe trying to understand a bit more what you are trying to do
we have some alternative output formats in the works, maybe it could work for you
Last updated: Feb 22 2024 at 04:02 UTC