s-exp field documentation · SerAPI

hello - pretty new serapi user here (and also new zulip user, so my apologies if I am using this wrong), so these might be slightly dumb questions. i've been playing around with sercomp and trying to understand the generated sexp -- is there any information anywhere on what all the fields of the returned expression are? i'm mostly confused about the ones that seem to be key value pairs, but further nesting in that node doesn't actually contain any data, simply the empty list. I'm working with an extremely small program and the generated expression is still pretty big, and my eventual goal is to use it to serialize fairly large coq programs. thanks !

Karl Palmskog (Dec 26 2022 at 19:26):

SerAPI uses metaprogramming to generate sexps based on Coq's internal data structures written in OCaml. So one guide might be the .ml/.mli code for the Coq version you are using (you could grep for the data constructor names). See also here for a bit more on Coq's datatypes.

Karl Palmskog (Dec 26 2022 at 19:28):

our paper also has an illustration of the various source code level datatypes as sexps

Emilio Jesús Gallego Arias (Dec 26 2022 at 23:43):

@Bhakti Shah , indeed the generated Sexp is far from nice, usually empty lists correspond to None values of the OCaml 'option` type. I think if you post an example here that would be most useful.

Bhakti Shah (Dec 27 2022 at 10:26):

@Emilio Jesús Gallego Arias Sure, here's an example.
it's not too readable in that form (for me) so I just put it into this sexp to tree generator to make looking at it a bit easier
there's a bunch of fields that I can't find anything about in the .ml file but I believe they're something to do with camlp5 (which i am also not familiar with) because they came up in the reference manual, but I'm wondering if there's an explicit description of what the autogenerated characteristics of a node are. Some of them I can infer like line_nb probably means line number, but I would obviously prefer more concrete evidence, if it exists. Hopefully that made sense - I can clarify some more if it isn't clear.

Bhakti Shah (Dec 27 2022 at 10:31):

@Karl Palmskog thanks for the info! I already looked in the .ml file but at first glance the paper looks useful, I'll give reading
that a shot and see how it goes.

Gaëtan Gilbert (Dec 27 2022 at 10:44):

Gaëtan Gilbert (Dec 27 2022 at 10:47):

coq doesn't use camlp5 but uses a vendored modified version ("gramlib")
I don't think its datatypes would show up in the sexp though

Emilio Jesús Gallego Arias (Dec 27 2022 at 10:48):

@Bhakti Shah , see https://github.com/janestreet/ppx_sexp_conv for more info on how sexp are generated. You can also access json and python in serapi, but not from sertop yet.

Note that you can pass --printer=human --omit_att to help you make sense of an expression, for your example:

(CoqAst
 ((control ()) (attrs ())
  (expr
   (VernacInductive
    Inductive_kw
    ((((false ((Id Bool2) ())) (() ()) ((CSort (UAnonymous (rigid true))))
       (Constructors
        ((false ((Id tru) (CHole () IntroAnonymous ())))
         (false ((Id fls) (CHole () IntroAnonymous ()))))))
      ()))))))

Which doesn't look so bad, and indeed, it is 1 to 1 to Coq's Ast (see vernacexpr.ml for the definition of VernacInductiv)

Emilio Jesús Gallego Arias (Dec 27 2022 at 10:49):

  | VernacInductive of inductive_kind * (inductive_expr * notation_declaration list) list

type inductive_expr =
  cumul_ident_decl with_coercion
  * inductive_params_expr * constr_expr option
  * constructor_list_or_record_decl_expr

IMHO Ast manipulation is better done in OCaml directly, due to having types. I'd be nice to generate .ts bindings for the Coq Ast, we may do so at some point.

Emilio Jesús Gallego Arias (Dec 27 2022 at 10:50):

Karl Palmskog (Dec 27 2022 at 10:56):

if you're manipulating syntax-level ASTs and want to feed that back into Coq, I'd argue it's more convenient to use a SerAPI serialized representation. Coq will figure out if something is wrong anyway.

Karl Palmskog (Dec 27 2022 at 10:58):

for example, in the Coq mutation work, our manipulation target was the Coq syntax since this is what the user sees (and mutants are, at least traditionally, supposed to be surface-level changes by programmers)

Karl Palmskog (Dec 27 2022 at 10:59):

if we had .ts support, I guess one could implement the mutation on top of a .ts mutation tool. Sexps are pretty niche in the wider PL world.

Emilio Jesús Gallego Arias (Dec 27 2022 at 11:01):

Yes, moreover it is nice to have types, otherwise maintaining such tools becomes very costly

Emilio Jesús Gallego Arias (Dec 27 2022 at 11:02):

We could have implemented the mutation tool as a small OCaml mutator, but indeed the OCaml toolchain is still not very usable, but in general, it is much faster to program like that

Karl Palmskog (Dec 27 2022 at 11:09):

one issue is that syntax ASTs contain quite a lot of implementation details when all you usually really care about is the unparseable-by-anyone-but-Coq Gallina stuff. Maybe there is a way to get small language-agnostic syntax API that can be maintained across Coq versions. As witnessed by MathComp, the surface Gallina/Vernacular language seems remarkably stable, but as you look just below the surface at say lexing, changes are considerable.

Karl Palmskog (Dec 27 2022 at 11:13):

(I think that Elpi already offers a small API for syntax, but I didn't look carefully)

Bhakti Shah (Dec 29 2022 at 10:30):

Thanks for all the pointers! I'll try a couple different things and see what works, and just look deeper into the coq and sexp source code for clarity.

Stream: SerAPI

Topic: s-exp field documentation

Bhakti Shah (Dec 26 2022 at 18:57):