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?

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.

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).

`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.

see https://hal.inria.fr/hal-01410567v3/document page 13 and next

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.

no, the variable must occur, IIRC

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)

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.

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.

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).

Logically speaking $\forall x y, p~x \to q~y \to F~x~y$ and $\forall x y, p~y \to q~x \to F~y~x$ are the same (semantically) but not syntactically, and this is what you inspect with CHR rules

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.

Hope it helps

Last updated: May 24 2024 at 22:02 UTC