I find that SWI-Prolog has a frozen/2 predicate. It allows to query freezed variables:
?- freeze(X,X=1), frozen(X,R).
R = freeze(X, user:(X=1))
Is there some analogue for when/2. frozen/2 doesn’t show anything:
?- when((nonvar(Y);nonvar(Z)), let(X, Y+Z)), frozen(X,R).
R = true
when/2 and friends use attributes, so term_attvars/2, attr_portray_hook/2, attribute_goals//1, or similar might do what you want.
Because the delays are on Y and Z, not on X …
102 ?- when((nonvar(Y);nonvar(Z)), let(X, Y+Z)), frozen(Y,R).
Correct to: "get(X,Y+Z)"? yes
R = when((nonvar(Y);nonvar(Z)), user:get(X, Y+Z)).
Got it. My bad.
Cool, so frozen/2 does indeed also show when/2.
Thats great.
But this does indeed require a recent version. Older versions (including 8.2.x) indeed only report delays from freeze/2.
I wonder whether frozen/2 works always correctly. Since
when/2 has a heuristic optimization, from the SWI-Prolog
documentation I read:
%! trigger_ground(@Term, :Goal)
%
% Trigger Goal when Term becomes ground. The current implementation
% uses nonground/2, waiting for an atribtrary variable and re-check
% Term when this variable is bound. Previous version used
% term_variables and suspended on a term constructed from these
% variables. It is clear that either approach performs better on
% certain types of terms. The term_variables/2 based approach wins on
% large terms that are almost ground. Possibly we need a nonground
% that also returns the number of tests performed and switch to the
% term_variables/2 based approach if this becomes large.
trigger_ground(X, Goal) :-
( nonground(X, V)
-> '$suspend'(V, when, trigger_ground(X, Goal))
; call(Goal)
).
So when we use when(.. ground(T) ..., G) not necessarely
all variables from T are delayed. They might be delayed later on.
Under these circumstances, is it even possible to provide a
frozen/2 predicate? An and (’,)/2 constraint in when/2 can
also apply such an optimization and only wait on one part
of the conjunction and block the rest later.
Will do some testing soon.
frozen/2 is built on top of the same hooks as copy_term/3. Thus, if it doesn’t do the right thing for when/2 or whatever constraint, the implementation of that constraint is to be blamed. This hook (Module:attribute_goals//1) is responsible for translating the attributes back to a goal that re-instantiates the attributes. This indeed isn’t always the most elegant goal. It is only buggy if the implications of the re-instantiated attributes differ from the original attributes. More elegant is better though 
See attribute_goals//1
I guess it depends on your reading. when(ground(f(X,Y), true) delays only on one of the two variables and will put a delay on the next variable of the pool if the variable on which the current delay is set is instantiated. So, frozen/2 is correct in reporting that one of the variables has no delay.
Whether this behavior is desirable is another issue. It is surely not the fault of frozen/2 though. There is simply no way it can know better. It is a design decision of when/2 not to put attributes on all involved variables. Note that you can use frozen(f(X,Y), Goal) to always get the intended result.
This is a known problem of attributed variables based constraints as the docs of
call_residue_vars/2 tell you. I’m not aware of any solutions for this. call_residue_vars/2 is merely for debugging as it avoids garbage collecting attributed variables and thus may run out of memory in otherwise perfectly fine code. It is also scales poorly in most systems, although I managed to find a fairly efficient way to handle this with the help of Bart Demoen.
Is this behaviour wanted? I get a kind of explosion, one when/2 statement becomes two when/2 statements, then three when/2 statements and so on…
Using an initial goal:
?- when((nonvar(X), nonvar(Z);nonvar(Y)), (write(f(X, Y, Z)), nl)).
when((nonvar(X), nonvar(Z)), when:check_disj(-, [(nonvar(X), nonvar(Z)), nonvar(Y)], user:(write(f(X, Y, Z)), nl))),
when((nonvar(X), nonvar(Z);nonvar(Y)), (write(f(X, Y, Z)), nl)).
And then use the displayed goal again:
?- when((nonvar(X), nonvar(Z)), when:check_disj(-, [(nonvar(X), nonvar(Z)), nonvar(Y)], user:(write(f(X, Y, Z)), nl))),
when((nonvar(X), nonvar(Z);nonvar(Y)), (write(f(X, Y, Z)), nl)).
when((nonvar(X), nonvar(Z)), when:check_disj(-, [(nonvar(X), nonvar(Z)), nonvar(Y)], user:(write(f(X, Y, Z)), nl))),
when((nonvar(X), nonvar(Z)), when:check_disj(-, [(nonvar(X), nonvar(Z)), nonvar(Y)], user:(write(f(X, Y, Z)), nl))),
when((nonvar(X), nonvar(Z);nonvar(Y)), (write(f(X, Y, Z)), nl)).
Not very good. Now there is no promise that the reported constraints are minimal or pretty. I had a brief look at the source. Seems this should be fixed by one of the hooks unifying the other variables to avoid double results. Must be a nice puzzle for anyone who considers this important enough or fancying a puzzle For those interested, the hook code is with when/2. The hooks are called from the code around copy_term/3. There you also find a brief comment on duplicate results.
Does when/2 respectively freeze/2 consume a lot of memory? Maybe
when combined with dif/2? I have a test case that runs on SICStus Prolog
and my system, but not in SWI-Prolog, even when increasing to
2GB and then 4GB, I get a crash:
/* SWI-Prolog 8.3.15 */
?- dif(Q, []), quine(Q, 6, N).
ERROR: Stack limit (1.0Gb) exceeded
/* SICStus Prolog 4.6.0 */
?- statistics(walltime, [T|_]), dif(Q,[]), quine(Q,6,N),
statistics(walltime, [S|_]), D is S-T.
D = 21262
/* Jekejeke Prolog 1.4.7 */
?- time((dif(Q, []), quine(Q, 6, N))).
Up 71,002 ms, GC 552 ms, Threads 70,438 ms (Current 12/30/20 23:37:20)
I have not yet 100% analyzed SWI-Prolog, whether there is some
intricate other artefact that makes it crash, despite memory usage.
For example an infinite recursion due to some strange semantic
of dif/2 in combination with freeze/2 resp when/2. The above timing
shows when/2. I have also benchmarked freeze/2. Results
are in the source files:
Testing freeze/2 and dif/2:
https://\gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine-pl
Testing when/2 and dif/2:
https://gist.github.com/jburse/a05e04191dcc68e542567542a7183d3b#file-quine2-pl
I simplified this to the program below, which does not terminate. If we use normal unification rather then unify_with_occurs_check/2 this also doesn’t terminate in SICStus. I guess this depends on how unify_with_occurs_check/2 is implemented. At this moment this does
Normal unification involves triggering the constraints. We could do the cycle detection before evaluating the pending constraints. This would make sense if this is a sufficient check. I’m a little in doubt. Can constraint evaluation create cycles? I think so as, in the current implementation, the above cycle detection does not go into attributed variables. Seems this is correct as also SICStus agrees this succeeds:
?- freeze(X, write(Y)), unify_with_occurs_check(X,Y).
Correct is of course a bit ambiguous as ISO says nothing about constraints.
t :-
Q=[[lambda,symbol(_3026),[cons,[quote,_3434],[quote,_3514]]],[quote,_3206]],
expr(_3434),
expr(_3514),
expr(_3206),
P=[_3434|_3514],
expr(_3434),
expr(_3514),
% Q = P,
unify_with_occurs_check(Q, P),
true.
expr(X) :- freeze(X, expr2(X)).
% expr(+Term)
expr2([X|Y]) :-
expr(X),
expr(Y).
expr2(quote).
expr2([]).
expr2(cons).
expr2(lambda).
expr2(symbol(_)).
Reported in simplified form in https://github.com/SWI-Prolog/swipl-devel/issues/758. Fixed. Thanks.
Also fixes quine:
101 ?- time((dif(Q, []), quine(Q, 6, N))).
% 209,677,737 inferences, 7.698 CPU in 7.700 seconds (100% CPU, 27236214 Lips)
Q = [[lambda, symbol(_59492), [cons, symbol(_59492), [cons, [...|...]|...]]], [quote, [lambda, symbol(_59492), [cons, symbol(...)|...]]]],
N = 5 .