Enzo Crance (Feb 21 2023 at 12:24): Enzo Crance (Feb 21 2023 at 12:24):Hello.
I want to link Elpi variables to integers so that I can reason on my constraints more easily, without having to handle variables everywhere (e.g. I can have more robust lookup and update operations with a map than using an association list and calls to same_var).
For this, I am using a link X I constraint linking variable X to the Elpi integer I. To look for the integer linked to a variable in the constraint store, I introduced another "query" constraint get-link X I along with a rule that removes it upon finding the right link entry in the constraint store.
rule (link C I) \ (get-link C' I')
| (coq.say "check same" C C', same_var C C', coq.say "TRUE")
<=> (I' = I).
However, I feel like same_var does not work in the way I expected. Indeed, sometimes the first call to coq.say prints twice the same thing
check same uvar frozen--1047 [] uvar frozen--1047 []
yet same_var never succeeds so I never see TRUE on my screen.
I tried to reduce the amount of checks by suspending all constraints on the X that is being added / looked for. Now the first coq.say call always prints twice the same variable, yet same_var fails. Why?
Enrico Tassi (Feb 21 2023 at 12:48):Sorry, this is not very well documented.
The CHR part of the language works at the "meta level", so it sees unification variables and manipulates them as constants.
They are replaced by these 'frozen--XX' constants. They are defrost if they occur in the new goal.
This makes it possible to write rules like
rule (link C I1) (link C I2) <=> (I1 = I2)
with the meaning you were trying to obtain, which is you don't want the potentially different uvars to be unified, but fire the rule only if the they are the same variable.
Enrico Tassi (Feb 21 2023 at 12:49):Note that inside rules you can write uvar to match any unification variable, and uvar X L to match it and get its "name" and its arguments (names in scope). (also uvar as X should work).
Enrico Tassi (Feb 21 2023 at 12:50):rule (link (uvar as C) I1) (link (uvar as C) I2) <=> (I1 = I2) is more precise, but you don't need that I guess, since your constraints are likely suspended on C.
Enrico Tassi (Feb 21 2023 at 12:52):see https://hal.inria.fr/hal-01410567v3/document page 13 and next
Enzo Crance (Feb 21 2023 at 12:53):Thanks. With your answer I will try to fix it!
Another related question: would it be possible to have a constraint link I with only one argument, the variable being the one the constraint is blocked on?
I mean, knowing by design that a link I and a get-link I' together in the same rule come from a constraint blocked on the same variable, thus not mentioning it at all.
Enrico Tassi (Feb 21 2023 at 13:01):no, the variable must occur, IIRC
Enzo Crance (Feb 22 2023 at 10:55):Hello. I'm coming back to this point about frozen variables. It seems like this syntactic matching does no longer work under binders.
Context: I still have this link C I rule linking an Elpi variable C to an integer, but now I also have another one link2 M C linking the variable to a Coq term M.
Before starting to reduce the constraints, a call to print_constraints gives a lot of constraints, some of them being under binders:
link2 X7 X9 /* suspended on X3 */
link X9 2 /* suspended on X3 */
link X12 1 /* suspended on X3 */
...
{c0 c1 c2} : link2 (X0 c0 c1 c2) (X2 c0 c1 c2) /* suspended on X3 */
{c0 c1 c2} : link (X2 c0 c1 c2) 4 /* suspended on X3 */
My reduction rules do something for each link in the constraint store, with a special case if a link2 is present for the same variable:
rule \ % ...
(link C I) (link2 M C) <=> (
coq.say "RULE 1" C,
% [...]
).
rule \ % ...
(link C I) <=> (
coq.say "RULE 2" C,
% [...]
).
Running the reduction prints this to the screen:
RULE 1 X12
RULE 1 X9
RULE 1 X6
RULE 2 X2 c3 c4 c5
and I am left with the link2 constraint, except the variable C was filled (but nothing was done on the M because the second rule was executed):
{c0 c1 c2} : link2 (X0 c0 c1 c2) x /* suspended on X3 */
It looks like link X9 2 and link2 X7 X9 matched, so something was done on X7, but link (X2 c0 c1 c2) 4 and link2 (X0 c0 c1 c2) (X2 c0 c1 c2) did not match together, even though these are the same variables. The context is even identical in this case, I don't really know why different variables were printed in the RULE 2 X2 c3 c4 c5 output.
How can I make a variable match with itself under binders? (I don't mind pruning and ignoring the context, these variables get assigned constant values in the end and don't depend on their context)
Enzo Crance (Feb 22 2023 at 12:44):NB: using prune C [] on each created variable C in the constraint store seems to work. Maybe it is sufficient for my needs but I'm not sure it's robust.
Enrico Tassi (Feb 22 2023 at 13:44):This is a bit unfortunate but is expected.
It is briefly mentioned in the paper: the constaints are injected in the disjoint union of the names, so you have (X9 c0 c1c c2) and (X9 c3 c4 c5) (likely). This is because the two contexts may be unrelated, and if would be up to you to discover a mapping between these names.
If you are first order, you can prune but also use in the rules uvar C _L to say you don't care about _L which would be [c0,c1,c2] in one case and [c3,c4,c5] in the other.
Enrico Tassi (Feb 22 2023 at 13:45):I'd recommend using the (not yet documented) browser for the trace, but there is a little bug in CHR traces, so I'm not sure it would help in practice. :-/ If you have a file I can test it and see if the bug shows up, otherwise it should help you see which rules apply and which don't (and why).
Enrico Tassi (Feb 22 2023 at 13:49):Logically speaking and are the same (semantically) but not syntactically, and this is what you inspect with CHR rules
Enrico Tassi (Feb 22 2023 at 13:52):So elpi gives you [p c0, q c1] ?- F c0 c1 and [q c2, p c3] ?- F c3 c2, which are different w.r.t. = but can be "aligned", eg by realizing that copy c0 c3 and copy c1 c2 can map the former to the latter. This is what we do in the paper, roughly.
Enrico Tassi (Feb 22 2023 at 13:52):Hope it helps
Last updated: Oct 13 2024 at 01:02 UTC