I wanted to test whether a dif/2 constraint stays live even if the involved terms involved go out of scope.
It correctly does:
% Call p/2, building a term involving X and Y.
% Then make X and Y identical, dis-equal
% or keep them "optimistically different"
q :-
p( X, Y),
X=x, writeln("X is now x"),
Y=y, writeln("Y is now y, which should have failed").
r :-
p( X,_Y),
X=y, writeln("X is now y, so the constraint is resolved affirmatively").
s :-
p(_X,_Y),
writeln("the constraint remains unresolved").
% Construct superterms A and B of which X and Y are
% subterms, and set up a dif/2 constraint
% between A and B. A and B then go out of scope and
% the terms denoted by them become unreachable.
% The dif/2 constraint, however, correctly persists:
p(X,Y) :- A = f(X,y), B = f(x,Y), dif(A,B), writeln("dif/2 passed").
Then we run the above:
?- q.
dif/2 passed
X is now x
false.
?- r.
dif/2 passed
X is now y, so the constraint is resolved affirmatively
true.
?- s.
dif/2 passed
the constraint remains unresolved
true.
In the call to s, I expected the toplevel to print the still open dif/2 constraint, but it’s quiet.
Is this related to this discussion, whereby anonymous variables in the term passed to dif/2 will lead to non-printing at the toplevel?
% dif succeeds optimistically
?- dif((p(1) :- q),(_B:-_C)),format("Hey\n").
Hey
dif(f(_B, _C), f(p(1), q)).
% dif succeeds optimistically but doesn't print the dif/2 expression
?- dif((p(1) :- q),(_:-_)),format("Hey\n").
Hey
true.