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
Hi @Daniel Hilst Selli , the Sexp tree is generated automatically from the OCaml datatypes
so you can have a look at the https://github.com/coq/coq/blob/master/vernac/vernacexpr.ml file
Actually to do what you would like to do, the most efficient path for you is to write such a summarization function in OCaml
then have SerAPI serialize your summarized datatype
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
I mean you could either process SerAPI's output, or write an OCaml function that does the serialization
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
both approaches have a problem in terms of plugins tho :/
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
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: Feb 06 2023 at 05:03 UTC