Tej Chajed (Nov 24 2020 at 00:42): 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.
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?
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)
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.
Gaëtan Gilbert (Nov 24 2020 at 08:38):aside: Option.get raises Option.IsNone not Not_found
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.
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
Pierre-Marie Pédrot (Nov 24 2020 at 15:04):It's part of the TODO list on a useful API for inductive types
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
Pierre-Marie Pédrot (Nov 24 2020 at 15:07):nothing prevents the user to define meaningless records
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
Enrico Tassi (Nov 24 2020 at 16:39):It works well for hierarchy builder
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: Apr 20 2024 at 13:01 UTC