Gordon Stewart (Dec 19 2022 at 21:04): Gordon Stewart (Dec 19 2022 at 21:04):We have an internal library at BedRock called deriving.v that we use to generate instances of stdpp classes like Inhabited, Finite, Decision, Countable, etc. Right now, it's not very extensible and supports a very limited set of types.
We're considering making it more re-usable and are wondering whether there are others who've implemented similar things who might be interested in coordinating efforts. (@Enrico Tassi: I know you have coq-elpi/apps/derive for deriving equality tests and wondered whether that's a potential upstreaming target?)
Here's a small example of how the library currently works:
Module DerivingTest.
Variant t := A | B | C.
#[instance(eq_dec,countable)] Deriving t.
Goal forall x y : t, if bool_decide (x = y) then True else True.
Proof. by move => x y; case (bool_decide_reflect (x = y)). Qed.
Goal forall x y : t, encode x = encode y -> x = y.
Proof. by move => x y X; apply encode_inj in X. Qed.
Goal match Pos.compare (encode A) (encode B) with
| Eq => True
| Lt => True
| Gt => True
end.
Proof.
Succeed by vm_compute.
(* Even [simpl] normalizes this goal - that's nice! *)
by simpl; assert_True.
Qed.
End DerivingTest.
hmm, isn't the current closest thing in the MathComp world deriving? Very different approach, though.
Karl Palmskog (Dec 19 2022 at 21:30):if there is some technical reason for not upstreaming this into coq-elpi (I guess it depends on stdpp?), then we would welcome a library like this into Coq-community (as long as it's under a license approved by OSI or considered a free software license by FSF). We collaboratively maintain a bunch of projects that are in Coq's CI, MathComp's CI, and in the Coq Platform.
Paolo Giarrusso (Dec 19 2022 at 21:42):Math-comp-wise, what Gordon mentioned and/or Enrico's https://drops.dagstuhl.de/opus/volltexte/2019/11084/pdf/LIPIcs-ITP-2019-29.pdf seem closer, but our generator is more limited
Enrico Tassi (Dec 19 2022 at 21:56):I've reworked derive very recently (for the CPP 2023 work) so that one can hook into it and break the dependencies. E.g. https://github.com/gares/elpi-derive-mathcomp (not released by lack of time) contains math-comp specific glue, so that coq-elpi (apps/derive actually) does not depend on MC. So the same would apply to stdpp, hopefully.
About upstreaming, I'm wondering if it is not the time for elpi/apps/derive to quit the nest and become a separate project. And that project would be welcoming all contributions. About style, one thing I found very handy is to define an AST which almost captures the inductives you can derive. The resulting code is much cleaner.
In any case I'm happy to help making "just one derive" (written in Elpi) a reality.
Gordon Stewart (Dec 20 2022 at 14:14):Thanks, Karl and Enrico, for the pointers and the support.
... coq-elpi (apps/derive actually) does not depend on MC. So the same would apply to stdpp, hopefully.
I took a closer look at apps/derive. It seems like it's already pretty extensible? (In which case, the best strategy is probably for us to build derive-compatible extensions, one for stdpp instances, one for our C++ logic, etc.)
I'm wondering if it is not the time for elpi/apps/derive to quit the nest...
That would be ideal! We're planning on revisiting our deriving.v in the first few months of '23. We can start the porting even before apps/derive becomes its own package. But targeting a standalone library would probably facilitate things.
Notification Bot (Dec 20 2022 at 14:14):Gordon Stewart has marked this topic as resolved.
Enrico Tassi (Dec 20 2022 at 20:42):The hope is that most of the code can be in derive (be it part of coq-elpi or not) and only the final "instance declaration" can live outside, and depend on the library it targets.
Yes, look at the derivations in derive.std for example, they all hook into derive. I think I wrote some doc in the README, suggestions appreciated
Enrico Tassi (Dec 21 2022 at 16:19):@Gordon Stewart here the doc: https://github.com/LPCIC/coq-elpi/tree/master/apps/derive#writing-a-new-derivation
Gordon Stewart (Dec 21 2022 at 16:37):I did see those docs; thanks! @David Swasey and I started looking a bit more closely at apps/derive this morning. I'm pretty confident we could adapt our existing derivations into your framework. At some point soon, we may have some additional questions and/or small change suggestions that would facilitate the ports. Though given the upcoming Christmas holiday, we probably won't make a huge amount of progress until January or so.
Enrico Tassi (Dec 21 2022 at 20:03):Great!
Gordon Stewart (Jan 17 2023 at 14:46):Following up, here's an initial version of our derive plugins: https://github.com/bedrocksystems/BRiCk/blob/master/theories/prelude/elpi/derive.v.
We currently support stdpp EqDecision, Inhabited, Finite, Countable, and some custom extensions related to bitsets.
Current known deficiencies:
Countable instances so that the encoding to positives computes properly; but the decoding function (positives to T) is currently inefficient. Gordon Stewart (Jan 17 2023 at 14:53):We noticed an issue in a test case at line https://github.com/bedrocksystems/BRiCk/blob/master/theories/prelude/elpi/derive.v#L44 (derive gives error Anomaly: Uncaught exception Failure("split dirpath")). I suspected this may be a derive bug but haven't yet had time to investigate.
This is only when doing
#[only(finite)] derive
Variant T2 := A2 | B2 | C2.
The following works fine:
Variant T2 := A2 | B2 | C2.
#[only(finite)] derive T2.
This is all in:
coq-elpi 1.16.0 Elpi extension language for Coq
Gordon Stewart has marked this topic as unresolved.
Enrico Tassi (Jan 17 2023 at 17:18):great, I'll look at that ASAP!
Last updated: Oct 13 2024 at 01:02 UTC