Stream: Coq devs & plugin devs

Topic: Ltac2 API to access the constructor and fields of a record


view this post on Zulip Tej Chajed (Nov 24 2020 at 00:42):

I wrote my first Coq plugin (with a bunch of help from @Talia Ringer ), an extension of coq-record-update that removes the boilerplate of listing out the fields of a record. All the OCaml code is here: https://github.com/tchajed/coq-record-update-plugin/blob/master/src/eta_expansion.ml.

If I just had an API to get the projections for a record, I wouldn't need a plugin for this. Is this something Ltac2 could provide? I think it's just a wrapper around Recordops.lookup_projections, returning a ident option list; the rest I believe I can handle in normal Ltac2 userland.

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 01:26):

I hate to ask, but would that API still be the right one once there's (Ltac2) support for introspecting inductives?

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 01:30):

(I don't see an obvious problem, but it's not so obvious to me there are no problems)

view this post on Zulip Tej Chajed (Nov 24 2020 at 02:39):

Introspecting an inductive could solve this problem, but that's a vague feature description (am I missing some concrete proposal?). Looking up a record's projections accurately specifically requires looking at a table where they're registered that's defined in recordops.ml, so I'd expect this to be required regardless. One possibility though is that projection information is stored in some sort of Ltac2-specific descriptor about the inductive.

Ltac2 is incredibly unstable so I dislike worrying about compatibility problems before the features are even there.

view this post on Zulip Gaëtan Gilbert (Nov 24 2020 at 08:38):

aside: Option.get raises Option.IsNone not Not_found

view this post on Zulip Tej Chajed (Nov 24 2020 at 14:55):

Thanks @Gaëtan Gilbert, that's now fixed! I got confused by a different anomaly triggered by Recordops.lookup_projections.

view this post on Zulip Tej Chajed (Nov 24 2020 at 14:57):

@Pierre-Marie Pédrot I'm curious what your thoughts are on exposing Recordops.lookup_projections (or perhaps some other record-related API) in Ltac2

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 15:04):

It's part of the TODO list on a useful API for inductive types

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 15:05):

note that lookup_projections is not very well specified for non-primitive records, it could be abused in weird ways

view this post on Zulip Pierre-Marie Pédrot (Nov 24 2020 at 15:07):

nothing prevents the user to define meaningless records

view this post on Zulip Enrico Tassi (Nov 24 2020 at 16:38):

In elpi I have this API
https://github.com/LPCIC/coq-elpi/blob/5a6c5ce8c42de8e9888c3e989ea2412b37bbc7d5/coq-builtin.elpi#L689-L693
which is just sugar around Recordops.lookup_projections

view this post on Zulip Enrico Tassi (Nov 24 2020 at 16:39):

It works well for hierarchy builder

view this post on Zulip Enrico Tassi (Nov 24 2020 at 17:02):

FTR elpi has no support for primitive projections yet, but this API just works fine. It returns the projections generated by Coq at record declaration time (the only ones that are canonical as in canonical structures).


Last updated: Oct 16 2021 at 02:03 UTC