Stream: SerAPI

Topic: Documentation about AST returned by sercomp --mode=sexp


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 14:39):

then have SerAPI serialize your summarized datatype

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Nov 14 2022 at 15:20):

both approaches have a problem in terms of plugins tho :/

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 05:03 UTC