Pattern on the LHS not equivalent to unification on the RHS? · Elpi users & devs

I thought that a clause f X <some-pat-of-X>. is equivalent to f X Y :- Y = <some-pat-of-X>. but I ran into a situation where that is not the case. Below is the relevant diff. What's the difference? (I'm hoping that this snippet is enough but I can try to make it into a complete counterexample later.)

pred f i:term i:(term -> term) o:term.

f M R {{ Some (pair lp:M (fun d => lp:(R d))) }}.
% does not behave the same as
f M R N' :- N' = {{ Some (pair lp:M (fun d => lp:(R d))) }}.

Enrico Tassi (Apr 16 2024 at 21:15):

Well, what do you observe exactly? It is hard to tell the difference in a minified example.

A difference could be that unif variables that correspond to Coq evars have a type constraint attached to them. If the goal as one of these as the third argument of f, then the former wakes up the constraint immediately after the head of the rule unifies (I imagine you have some other premises and you did put a print). In the second example the constraint is likely to be resumed a bit later, when the premise is solved.
If the typing constraint fails, then the rule will fail and backtrack. If you have a print just after :- you may see that.
If you use the vscode trace browser, than it should be clear what goes on.

Bottom line, the two rules in the example above should behave the same w.r.t. full success or failure.

Li-yao (Apr 16 2024 at 22:18):

In my larger program, the former leads to my command failing unexpectedly while the latter leads to a success. While I try to pin down the failure, here's an example where I get different results:

From elpi Require Import elpi.

Elpi Program TT lp:{{ }}.

Elpi Accumulate lp:{{
pred f o:(term -> term) o:term.
% f R N' :- N' = {{ (fun d => lp:(R d)) }}.
f R {{ (fun d => lp:(R d)) }}.

pred foo o:(term -> term) o:term.
foo R N :-
  pi d\
    f R N,
    d = (R d).
}}.
Elpi Query lp:{{
  foo R N.
}}.

With that I get N = fun `d` X0 c0 \ c1 (which seems flat out wrong, if c1 is d, then shouldn't it be out of scope?), and after swapping in the commented out definition of f, N = fun `d` X0 c0 \ c0.

Enrico Tassi (Apr 17 2024 at 12:00):

pred f o:(term -> term) o:term.
f R N :- N = (fun d\ R d).
f R (fun d\ R d).

pred foo o:(term -> term) o:term.
foo R N :-
  pi d\
    f R N,
    d = (R d).

main :-
  foo R N, print R, print N.

Stream: Elpi users & devs

Topic: Pattern on the LHS not equivalent to unification on the RHS?

Li-yao (Apr 16 2024 at 15:26):

Enrico Tassi (Apr 16 2024 at 21:15):

Li-yao (Apr 16 2024 at 22:18):

Enrico Tassi (Apr 17 2024 at 12:00):

Enrico Tassi (Apr 17 2024 at 14:51):