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.
I hate to ask, but would that API still be the right one once there's (Ltac2) support for introspecting inductives?
(I don't see an obvious problem, but it's not so obvious to me there are no problems)
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.
aside: Option.get raises Option.IsNone not Not_found
Thanks @Gaëtan Gilbert, that's now fixed! I got confused by a different anomaly triggered by Recordops.lookup_projections.
@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
It's part of the TODO list on a useful API for inductive types
note that lookup_projections is not very well specified for non-primitive records, it could be abused in weird ways
nothing prevents the user to define meaningless records
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
It works well for hierarchy builder
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 13 2024 at 01:02 UTC