Non-destructive universal quantification in Prolog

A good language for logic programming should allow the programmer to use a language close to the language used by the mathematicians. Therefore, I have always considered the lack of proper universal quantifier in Prolog an important shortcoming.

Today an idea came to me how to define something much better than forall and foreach.

forany(Var, {Context}, Condition, Body)

This predicate tries to prove Body for all instantiations Var gets successively on backtracking over Condition. All variables in Condition and Body are considered local unless listed in Var or Context. Condition is not permitted to modify in any way the variables listed in Context, otherwise forany won't work correctly.

Here is the implementation (based on yall):

forany(V, {Vars}, Goal1, Goal2) :-
    (   bagof(V, {V,Vars}/Goal1, Solutions)
    ->  maplist({Vars}/[V]>>Goal2, Solutions)
    ;   true ).

My first question is about the second argument of forany. I'd like to eliminate it.

Now some examples

Construct a list of the first 8 squares:

?- length(X,8), forany(N, {X}, between(1,8,N), 
                      (Q is N*N, nth1(N, X, Q))).
X = [1, 4, 9, 16, 25, 36, 49, 64].

Reverse a list:

?- X=[1,2,3,4,5], length(X,N), length(Y,N),
     forany(I, {X,Y,N}, between(1,N,I),
           (J is N-I+1, nth1(I,X,A), nth1(J,Y,A))).
X = [1, 2, 3, 4, 5],
N = 5,
Y = [5, 4, 3, 2, 1].

Subset:

subset(X, Y) :- forany(A, {X,Y}, member(A,X), member(A, Y)).

A funny way to generate all permutations of a list without duplicates:

permutation(X, Y) :-
     length(X, N), length(Y, N), subset(X, Y).

?- permutation([1,2,3],X).
X = [1, 2, 3] ;
X = [1, 3, 2] ;
X = [2, 1, 3] ;
X = [2, 3, 1] ;
X = [3, 1, 2] ;
X = [3, 2, 1] ;
false.

A funny way to sort a list of different integers. Notice that constraints are used to make the list sorted so most permutations won't be generated:

sorted(X) :- forany(A-B, {X}, append(_, [A,B|_], X),
                    A#<B).

?- X=[7,3,8,2,6,4,9,5,1], length(X, N), length(Y, N),
                          sorted(Y), subset(X,Y).

X = [7, 3, 8, 2, 6, 4, 9, 5, 1],
N = 9,
Y = [1, 2, 3, 4, 5, 6, 7, 8, 9] .

The problem

It seems that this forany works brilliantly when constraints are not used. Also, it can be used to generate constraints, but at least on SWI-Prolog there are problems when constraints already have been generated. The reason for this is that forany uses bagof and according to the manual of SWI-Prolog:

Term-copying operations (assertz/1, retract/1, findall/3, copy_term/2, etc.) generally also copy constraints. The effect varies from ok, silent copying of huge constraint networks to violations of the internal consistency of constraint networks. As a rule of thumb, copying terms holding attributes must be deprecated. If you need to reason about a term that is involved in constraints, use copy_term/3 to obtain the constraints as Prolog goals, and use these goals for further processing.

Here is a demonstration of the problem bagof creates with constraints:

?- X=[A,B,C], dif(C,D), bagof(_, K^member(K,X), _).
X = [A, B, C],
dif(C, _5306),
dif(C, _5318),
dif(C, _5330),
dif(C, D).

As you can see, three unnecessary constraints are created.

My second question is if this is a problem only of SWI-Prolog.

And the third question: is there a way to fix this in SWI-Prolog. The above quote from the manual suggests that copy_term/3 should be used. Unfortunately, I don't understand this suggestion and I don't know if it is useful for forany.

Great news! I was surprised that bagof is written in Prolog. By looking at its code I learned that some things I thought are impossible are in fact possible. And just as the manual of SWI-Prolog suggested, copy_term/3 or rather the similar predicate copy_term_nat/2 helped.

So with great joy I am able to present a fully working (as far as I can tell) universal quantifier for SWI-Prolog:

forany(V, {Vars}, Condition, Body) :-
    findall(V-Vars, Condition, Solutions),
    % For SWI-Prolog.  Can be replaced by Solutions=Clean_solutions in other systems
    copy_term_nat(Solutions, Clean_solutions),
    forany_execute_goals(Clean_solutions, Vars, V, Body).

forany_execute_goals([], _, _, _).
forany_execute_goals([Sol-NewVars|Solutions], Vars, V, Body) :-
    % The following test can be removed
    assertion(subsumes_term(NewVars, Vars)),
    % or replaced by the following more standard use of throw/1:
%   (  subsumes_term(NewVars, Vars)
%   -> true
%   ;  throw('Forbidden instantiation of context variables by the antecedent of forany')  ),
    NewVars = Vars,
    call({Vars}/[V]>>Body, Sol),
    forany_execute_goals(Solutions, Vars, V, Body).