Stream: SerAPI

Topic: Get span information of goals

Axel Marmet (Nov 02 2021 at 15:59):

Hello,

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!

Emilio Jesús Gallego Arias (Nov 03 2021 at 15:47):

HI @Axel Marmet , unfortunately this is not possible today, this is due the way Coq's printer work.

Let me summarize the situation:

• goals are stored as kernel terms
• then, printing does 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
• then, the printer maps CoqAst.t to a "box layout" Pp.t, this is already accessible from SerAPI
• if you want, OCaml's 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

Emilio Jesús Gallego Arias (Nov 03 2021 at 15:49):

Imagine this case (App (Ref "f") [arg1;...;argn])

Emilio Jesús Gallego Arias (Nov 03 2021 at 15:49):

the printing routine could split the application in two lines to fit it in the window, depending on the size of the display port

Emilio Jesús Gallego Arias (Nov 03 2021 at 15:49):

so @Axel Marmet , the way I'd address your question is maybe trying to understand a bit more what you are trying to do

Emilio Jesús Gallego Arias (Nov 03 2021 at 15:51):

we have some alternative output formats in the works, maybe it could work for you

Last updated: Jun 10 2023 at 06:31 UTC