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 derive
with 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.
I have the code for generating the instance, and swapping the body seems indeed easy
Last updated: Oct 13 2024 at 01:02 UTC