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?
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
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.
okay, the paper is helpful... I need to generate stdpp
EqDecision instances, but maybe I can reuse this code...
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
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.
I have the code for generating the instance, and swapping the body seems indeed easy
Last updated: Jun 06 2023 at 22:01 UTC