Non deterministic pruning anomaly

[nguermond]

While trying to write a unifier to solve problems such as

(pi x1 x2 \
 ((unif (Y0 x1) x1),
  (unif x2 (Y1 (Y0 x1) x2))))

I get the error

Anomaly: Non deterministic pruning, delay to be implemented: t=A1 ≪.X0≫_0, delta=0

Why does this happen without even having defined unif?
The simpler example ((foo Y), (foo (X Y))) similarly gives

Called from Dune__exe__Elpi_REPL in file "elpi_REPL.ml", line 183, characters 18-42
Called from Elpi__API.Compile.query in file "src/API.ml" (inlined), line 143, characters 4-31
Called from Elpi__Compiler.query_of_ast in file "src/compiler.ml", line 2117, characters 4-94
Called from Elpi__Runtime_trace_off.HO.move in file "src/runtime.ml", line 1004, characters 3-13
Called from Elpi__Runtime_trace_off.HO.move.maux in file "src/runtime.ml", line 867, characters 16-42
Called from Elpi__Util.smart_map in file "src/util.ml", line 177, characters 15-19
Called from Elpi__Runtime_trace_off.HO.move.maux in file "src/runtime.ml", line 866, characters 16-30
Anomaly: Non deterministic pruning, delay to be implemented: t=A1 ≪.X0≫_0, delta=0

elpi version is 1.13.1

[gares]

I would need to investigate a bit more to tell you exactly why this error happens at compilation time, but the real problem is that your term contain expressions outside the pattern fragment, and Elpi does not like them. It usually tolerates them, so there is probably something buggy in your example (thanks for reporting), but you can hardly win if you play this game. May I ask what you are trying to use Elpi for?

The fatal error says that Elpi will not prune unless the result is deterministic. It will not remove an eigenvariable from the arguments of a unification variable unless there is only one way of doing it, and stuff like X (Y c) can be pruned of c in two ways at least. I don't see right now why the compiler should try to prune, I'll try to find some time tomorrow.

[nguermond]

I want to solve a set of constraints (that may fall outside the pattern fragment, but the same error occurs even with the -delay-problems-outside-pattern-fragment flag) for a type checker.

Here is a more realistic example (the previous example was a simplification of the first two constraints):

type (==) A -> A -> prop.
infix == 5.

(uvar as X) == (uvar as Y) :- !, declare_constraint (X == Y) [X, Y].
T0 == T1 :- !, T0 = T1.

test _ :-
        ((pi x1 x2 x3 x4 x5 x6 \
	  (((x3 ((((((Y22 x1) x2) x3) x4) x5) x6)) ((((((Y23 x1) x2) x3) x4) x5) x6))
	   == ((((((Y21 x1) x2) x3) x4) x5) x6))),
        % (pi x1 x2 x3 x4 x5 x6 \
 	% ((((((Y16 x1) x2) x3) x4) x5)
 	%   == (((Y2 x1) x2)
 	% 	   ((((((Y22 x1) x2) x3) x4) x5) x6)))),
	 (pi x1 x2 x3 x4 \ (((((Y15 x1) x2) x3) x4) == ((Y1 x1) x2))),
	 (pi x1 x2 x3 x4 x5 x6 \
	  x5 == ((((((Y22 x1) x2) x3) x4) x5) x6)),
	 (pi x1 x2 x3 x4 x5 \
	  ((((f0 (((((Y17 x1) x2) x3) x4) x5)) (((((Y18 x1) x2) x3) x4) x5))
		(((((Y19 x1) x2) x3) x4) x5))
          (((((Y20 x1) x2) x3) x4) x5)) == (((((Y16 x1) x2) x3) x4) x5)),
     (pi x1 x2 x3 x4 x5 \
	  ((Y0 x1) == (((((Y17 x1) x2) x3) x4) x5))),
	 (pi x1 x2 x3 x4 x5 \
	  x2 == (((((Y18 x1) x2) x3) x4) x5)),
	 (pi x1 x2 x3 x4 \ x1 == ((((Y15 x1) x2) x3) x4)),
	 (pi x1 x2 x3 \ ((x3 (((Y8 x1) x2) x3)) (((Y9 x1) x2) x3)) == (((Y7 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((((f4 (((Y10 x1) x2) x3)) (((Y11 x1) x2) x3)) (((Y12 x1) x2) x3))
	 	 (((Y14 x1) x2) x3))
      == (((Y9 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((Y0 x1) == (((Y10 x1) x2) x3))),
	 (pi x1 x2 x3 \
	  x2 == (((Y14 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  (((f1 (((Y13 x1) x2) x3)) (((Y13 x1) x2) x3)) == ((f1 (((Y10 x1) x2) x3)) (((Y11 x1) x2) x3)))),
	 (pi x1 x2 x3 \
	  (f2 (((Y13 x1) x2) x3)) == (((Y12 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((Y0 x1) == ((Y1 x1) x2))),
	 (pi x1 x2 x3 \
	  x2 == (((Y8 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((((f0 (((Y3 x1) x2) x3)) (((Y4 x1) x2) x3)) (((Y5 x1) x2) x3))
       (((Y6 x1) x2) x3))
      == (((Y2 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  (((Y1 x1) x2) == (((Y5 x1) x2) x3))),
	 (pi x1 x2 x3 \
	  x3 == (((Y6 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((Y0 x1) == (((Y3 x1) x2) x3))),
	 (pi x1 x2 x3 \
	  x2 == (((Y4 x1) x2) x3)),
	 (pi x1 x2 \ x1 == ((Y1 x1) x2)),
	 (pi x1 \ x1 == (Y0 x1))
	).

The problematic constraint is the commented one. What surprises me further (since you say this is a compilation error) is that this sometimes works depending on where in the list of constraints I place the problematic one (for example it works if placed first or last in the list).

I realize the proper way to do this is probably to use elpi's builtin constraint solver, but I haven't figured out how to use it yet :).

[gares]

I'm sorry the doc in ELPI.md is not very clear, but you can write uvar as in (uvar as X) == (uvar as Y) only when the predicate is in input mode on that argument. Also, == is already taken by same_term.

With this declaration it fails (I have no clue if the result is OK, but at least it does not abort):

infix === 5.
pred (===) i:A, i:A.
....
% the same but with == replaced by ===

[gares]

Sorry, I was not running test _ but rather main (which is what one invokes with -test) and it fails with the error I was talking about:

Anomaly: Non deterministic pruning, delay to be implemented: t=A4 c0 c1 
                                                       (≪.X0≫_0 c0 c1 c2 
                                                         c3 c4 c5), delta=0

but if I just give

infix === 5.
pred (===) i:A, i:A.

(uvar as X) === (uvar as Y) :- !, declare_constraint (X === Y) [X, Y].
T0 === T1 :- !, T0 = T1.

main :-
        (
         (pi x1 x2 x3 x4 x5 x6 \
 	 ((((((Y16 x1) x2) x3) x4) x5)
 	   === (((Y2 x1) x2)
 	 	   ((((((Y22 x1) x2) x3) x4) x5) x6))))).

then the result is the expected one, I guess:

Success:

Time: 0.000

Constraints:
 {c0 c1 c2 c3 c4 c5} : === (X0 c0 c1 c2 c3 c4) (X1 c0 c1 (X2 c0 c1 c2 c3 c4 c5))  /* suspended on X0, X1 */

[gares]

OK, this says sucess:

infix === 5.
pred (===) i:A, i:A.

(uvar as X) === (uvar as Y) :- !, declare_constraint (X === Y) [X, Y].
T0 === T1 :- !, T0 = T1.

main :-
        (
         (pi x1 x2 x3 x4 x5 x6 \
 	 ((((((Y16 x1) x2) x3) x4) x5)
 	   === (((Y2 x1) x2)
 	 	   ((((((Y22 x1) x2) x3) x4) x5) x6)))),
	 (pi x1 x2 x3 x4 \ (((((Y15 x1) x2) x3) x4) === ((Y1 x1) x2))),
	 (pi x1 x2 x3 x4 x5 x6 \
	  x5 === ((((((Y22 x1) x2) x3) x4) x5) x6)),
	 (pi x1 x2 x3 x4 x5 \
	  ((((f0 (((((Y17 x1) x2) x3) x4) x5)) (((((Y18 x1) x2) x3) x4) x5))
		(((((Y19 x1) x2) x3) x4) x5))
          (((((Y20 x1) x2) x3) x4) x5)) === (((((Y16 x1) x2) x3) x4) x5)),
     (pi x1 x2 x3 x4 x5 \
	  ((Y0 x1) === (((((Y17 x1) x2) x3) x4) x5))),
	 (pi x1 x2 x3 x4 x5 \
	  x2 === (((((Y18 x1) x2) x3) x4) x5)),
	 (pi x1 x2 x3 x4 \ x1 === ((((Y15 x1) x2) x3) x4)),
	 (pi x1 x2 x3 \ ((x3 (((Y8 x1) x2) x3)) (((Y9 x1) x2) x3)) === (((Y7 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((((f4 (((Y10 x1) x2) x3)) (((Y11 x1) x2) x3)) (((Y12 x1) x2) x3))
	 	 (((Y14 x1) x2) x3))
      === (((Y9 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((Y0 x1) === (((Y10 x1) x2) x3))),
	 (pi x1 x2 x3 \
	  x2 === (((Y14 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  (((f1 (((Y13 x1) x2) x3)) (((Y13 x1) x2) x3)) === ((f1 (((Y10 x1) x2) x3)) (((Y11 x1) x2) x3)))),
	 (pi x1 x2 x3 \
	  (f2 (((Y13 x1) x2) x3)) === (((Y12 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((Y0 x1) === ((Y1 x1) x2))),
	 (pi x1 x2 x3 \
	  x2 === (((Y8 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((((f0 (((Y3 x1) x2) x3)) (((Y4 x1) x2) x3)) (((Y5 x1) x2) x3))
       (((Y6 x1) x2) x3))
      === (((Y2 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  (((Y1 x1) x2) === (((Y5 x1) x2) x3))),
	 (pi x1 x2 x3 \
	  x3 === (((Y6 x1) x2) x3)),
	 (pi x1 x2 x3 \
	  ((Y0 x1) === (((Y3 x1) x2) x3))),
	 (pi x1 x2 x3 \
	  x2 === (((Y4 x1) x2) x3)),
	 (pi x1 x2 \ x1 === ((Y1 x1) x2)),
	 (pi x1 \ x1 === (Y0 x1))
	).

You can look at a "readable" trace by running (a.elpi is the file)

elpi -test a.elpi  -no-tc -trace-on tty stdout -trace-at run 1 100 -trace-only '\(run\|select\|user:\)'

[nguermond]

Thanks for pointing this out!
However the following still fails for me (the first constraint is missing in both of your runs, sorry if I was not clear):

infix === 5.
pred (===) i:A, i:A.


(uvar as X) === (uvar as Y) :- !, declare_constraint (X === Y) [X, Y].
T0 === T1 :- !, T0 = T1.


main :- (pi x1 x2 x3 x4 x5 x6 \
		 (((x3 ((((((Y22 x1) x2) x3) x4) x5) x6)) ((((((Y23 x1) x2) x3) x4) x5) x6))
		  === ((((((Y21 x1) x2) x3) x4) x5) x6))),
	(pi x1 x2 x3 x4 x5 x6 \
		 ((((((Y16 x1) x2) x3) x4) x5)
		  === (((Y2 x1) x2)
	 		   ((((((Y22 x1) x2) x3) x4) x5) x6)))).

with

Anomaly: Non deterministic pruning, delay to be implemented: t=A4 c0 c1 
                                                       (≪.X0≫_0 c0 c1 c2 
                                                         c3 c4 c5), delta=0

[gares]

I see. Something still escapes me, but this one

main :- (pi x1 x2 x3 x4 x5 x6 \
		 (((x3 ((((((Y22 x1) x2) x3) x4) x5) x6)) ((((((Y23 x1) x2) x3) x4) x5) x6))
		  === ((((((Y21 x1) x2) x3) x4) x5) x6))),
	(pi x1 x2 x3 x4 x5 x6 \
		 ((((((Y16 x1) x2) x3) x4) x5)
		  === (((Y2 x1) x2)
	 		   ((((((Y22b x1) x2) x3) x4) x5) x6)))),
				Y22 = Y22b.

works

[gares]

Anyway, sooner or later terms outside the pattern fragment are going to give you problems.
I'm not so sure I can point you in the right direction without a bit more context :-/

[nguermond]

I found the following trick, which works very nicely for me:

infix === 5.
pred (===) i:A, i:A.

mode (app i i).
type app (A -> B) -> (list any) -> any.

type apply (A -> B) -> (list any) -> any -> prop.
apply K [] K.
apply K [C|Args] R :- apply (K C) Args R.

pattern_args [].
pattern_args [A|Args] :- (name A), pattern_args Args.

%% rewrite (app K Args) to (K Args) if Args are of the form c0 c1 ... cn
(app (uvar as K) Args) === Y :- (pattern_args Args), print "pattern" K "@" Args, !,
			        apply K Args R, (R === Y).
X === (app (uvar as K) Args) :- (pattern_args Args), print "pattern" K "@" Args, !,
			        apply K Args R, (X === R).
%% delay (app K Args) if outside the pattern fragment
(app (uvar as K) Args) === Y :- print "delaying" K "@" Args "=" Y, !,
				(std.filter Args var FVars), print " on vars: " [K|FVars],
				declare_constraint ((app K Args) === Y) [K|FVars].
X === (app (uvar as K) Args) :- print "delaying" X "=" K "@" Args, !,
				(std.filter Args var FVars), print " on vars: " [K|FVars],
				declare_constraint (X === (app K Args)) [K|FVars].
%% otherwise unify
T0 === T1 :- print "unifying" T0 "=" T1, !, T0 = T1.

Basically, I externally inspect the terms, and replace applications of the form
(X ... (Y ...) ...) with (app X [... Y ...]), so that the resulting term lies in the pattern fragment. So taking my very first example,
(pi x1 x2 \ ((Y0 x1) === x1), (x2 === (Y1 (Y0 x1) x2)))
becomes
(pi x1 x2 \ ((Y0 x1) === x1), (x2 === (app Y1 [Y0 x1, x2])))
with output

unifying X0 c0 = c0
pattern X1 @ [c0, c1]
unifying c1 = X1 c0 c1

Success:
  Y0 = c0 \ c0
  Y1 = c0 \ c1 \ c1

It is also interesting to reverse the order of the constraints so that
(pi x1 x2 \ (x2 === (app Y1 [Y0 x1, x2])), ((Y0 x1) === x1))
produces the output

delaying c1 = X0 @ [X1 c0, c1]
 on vars:  [X0, X1 c0]
unifying X1 c0 = c0
pattern X0 @ [c0, c1]
unifying c1 = X0 c0 c1

Success:
  Y0 = c0 \ c0
  Y1 = c0 \ c1 \ c1

Thank you for your help!

[gares]

I think you found a very lightweight encoding to work around the limitations of Elpi. Bravo!

[gares]

FTR: mode (app i i). is not needed (and should raise an error). Only predicates have modes.

Your pattern_args is not 100% correct, all arguments must be names, but also distinct. I should really provide a builtin for that check. (Maybe it's not needed in your case because input terms are already validating that condition).