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

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: May 31 2023 at 02:31 UTC