Paolo Giarrusso (Oct 11 2022 at 12:09): Paolo Giarrusso (Oct 11 2022 at 12:09):On large variants (80 constructors, almost no arguments), calling decide equality from coq-elpi takes ~2x as calling it directly. As decide equality's output is quadratic, is this expected and unavoidable because of the coq-elpi <-> coq translation?
Enrico Tassi (Oct 11 2022 at 12:31):Hum, you were very unlucky. We may look into this problem, but this branch (and this paper under submission) may just be what you need:
CC @Jean-Christophe Léchenet
Enrico Tassi (Oct 11 2022 at 12:33):I don't think the 2x is justified, so there is some inefficiency somewhere. But if you need to generate a sound eq test in Elpi (for a non mutual inductive), then you have a faster option in that branch. It still needs polishing as you may notice, but we are close to merging it in.
Paolo Giarrusso (Oct 11 2022 at 19:00):okay, the paper is helpful... I need to generate stdpp EqDecision instances, but maybe I can reuse this code...
Jean-Christophe Léchenet (Oct 11 2022 at 23:26):It seems you need the sumbool version instead of the reflect one. This one is easy, either use Bool.reflect_dec from the reflect one that eqbOK generates, or build it from the correctness and completeness lemmas that eqbcorrect generates (like Scheme Equality does actually). As for the interaction with the typeclass, we started to connect derivewith the eqType from mathcomp (see https://github.com/gares/elpi-derive-mathcomp/). I don't know to what extent you can use that as a guide for your case.
Paolo Giarrusso (Oct 12 2022 at 00:43):I have the code for generating the instance, and swapping the body seems indeed easy
Last updated: Oct 13 2024 at 01:02 UTC