Stream: Elpi users & devs

Topic: Performance of wrapping `decide equality`


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 15:03 UTC