Refactor and improve CommRingSolver #1093
Conversation
felixwellen
changed the title
felixwellen
force-pushed
the
fwellen/tactical-initiative
branch
from
078c031
to
eda7ec4
Compare
There was a problem hiding this comment.
This is will hopefully make our lives much easier.
I can't claim to understand what is going on in the reflection code, so I can't comment on that part of the PR.
I still don't quite understand when using the solver in place is possible and when a where clause with an extra term is needed. Maybe some examples of things that are not expected to work could be helpful.
| -Closed I x x∈I = subst (_∈ I) (useSolver x) (·Closed (snd I) (- 1r) x∈I) | ||
| where useSolver : (x : R) → - 1r · x ≡ - x | ||
| useSolver = solve R' | ||
| -Closed I x x∈I = subst (_∈ I) useSolver (·Closed (snd I) (- 1r) x∈I) |
There was a problem hiding this comment.
I would have expected that you can just write solve! R' in place here, is there a reason why this is not possible?
There was a problem hiding this comment.
It is a bit mysterious and might be a deficiency of the reflection mechanism. I turned this into issue #1097
There was a problem hiding this comment.
This is solved now, thanks to @ncfavier :-)
|
Now it should be more easy to guess when the ring solver will work: It doesn't work well with concrete rings like the integers and sometimes you need to introduce helpers, if some meta variables cannot be solved. Otherwise it should work now in place as one might expect. |
…o fwellen/tactical-initiative
felixwellen
force-pushed
the
fwellen/tactical-initiative
branch
from
aab08fb
to
a0ca820
Compare
|
Max agreed to a merge -> merging. |
The reflection code of the CommRingSolver is pretty horrible, this PRs intends to improve the situation and make it more flexible.