Daniel Hilst Selli (Nov 14 2022 at 13:10): Daniel Hilst Selli (Nov 14 2022 at 13:10):Hi
I'm using sercomp to serialize a file, I have a big sexp tree. Is there any documentation on the returned AST? I'm particularly interested in the structure of each node. If there is no documentation maybe there is a grammar file from where this tree is generated. I want to take this tree as input and generate a much simpler tree with requires, modules, functions, type etc
Emilio Jesús Gallego Arias (Nov 14 2022 at 14:37):Hi @Daniel Hilst Selli , the Sexp tree is generated automatically from the OCaml datatypes
Emilio Jesús Gallego Arias (Nov 14 2022 at 14:38):so you can have a look at the https://github.com/coq/coq/blob/master/vernac/vernacexpr.ml file
Emilio Jesús Gallego Arias (Nov 14 2022 at 14:38):Actually to do what you would like to do, the most efficient path for you is to write such a summarization function in OCaml
Emilio Jesús Gallego Arias (Nov 14 2022 at 14:39):then have SerAPI serialize your summarized datatype
Daniel Hilst Selli (Nov 14 2022 at 15:08):Thanks for the link!
About the summarization function, can I ask SerAPI to serialize a file and get the AST and input it in my function this is what you mean? I never tried to use it from ocaml I will try it
Emilio Jesús Gallego Arias (Nov 14 2022 at 15:19):I mean you could either process SerAPI's output, or write an OCaml function that does the serialization
Emilio Jesús Gallego Arias (Nov 14 2022 at 15:20):the latter is easier to maintain, for example there is a fucntion that extracts identifiers from Coq's AST with type Vernacexpr.vernac_expr -> Id.t list
Emilio Jesús Gallego Arias (Nov 14 2022 at 15:20):both approaches have a problem in terms of plugins tho :/
Emilio Jesús Gallego Arias (Nov 14 2022 at 15:21):Coq's Ast can be extended by plugins, so in general it is hard to be complete, but if you can tolerate approximations (that is to say, your output type is a lattice with some reasonable properties) you'd be good
Daniel Hilst Selli (Nov 14 2022 at 16:03):I think plugins will not be a problem because I'm mostly interested in functions (their types) and modules (so I know the FQN of a function at a given node), also lemma types. I will not use function or lemma bodies. I will try the OCaml approach, thank you!
Last updated: May 31 2023 at 02:31 UTC