:- module(aggregates, [
        setof/3,
        bagof/3,
        findall/3,
        findall/4,
        findnsols/4,
        findnsols/5,
 	(^)/2
        ],
	[assertions,isomodes]).

:- use_module(library(sort)).
:- use_module(library(lists),[length/2]).
:- use_module(engine(internals),['$setarg'/4]).

:- meta_predicate
        bagof(?,goal,?),
        setof(?,goal,?),
        findall(?,goal,?),
        findall(?,goal,?,?),
        findnsols(?,?,goal,?),
        findnsols(?,?,goal,?,?).

:- set_prolog_flag(multi_arity_warnings, off).

:- data solution/1.

:- on_abort(retractall_fact(solution(_))).

:- comment(title,"All solutions predicates").

:- comment(author,"First version by Richard A. O'Keefe and David
   H.D. Warren. Changes by Mats Carlsson, Daniel Cabeza, and Manuel
   Hermenegildo").

:- comment(module,"This module implements the standard solution
   aggregation predicates.

   When there are many solutions to a problem, and when all those
   solutions are required to be collected together, this can be
   achieved by repeatedly backtracking and gradually building up a
   list of the solutions.  The following built-in predicates are
   provided to automate this process.

").

/*  Original Comment: 

    This file defines two predicates which act like setof/3 and bagof/3.
    I have seen the code for these routines in Dec-10 and in C-Prolog,
    but I no longer recall it, and this code was independently derived
    in 1982 by me and me alone.

    Most of the complication comes from trying to cope with free variables
    in the Filter; these definitions actually enumerate all the solutions,
    then group together those with the same bindings for the free variables.
    There must be a better way of doing this.  I do not claim any virtue for
    this code other than the virtue of working.  In fact there is a subtle
    bug: if setof/bagof occurs as a data structure in the Generator it will
    be mistaken for a call, and free variables treated wrongly.  Given the
    current nature of Prolog, there is no way of telling a call from a data
    structure, and since nested calls are FAR more likely than use as a
    data structure, we just put up with the latter being wrong.  The same
    applies to negation.

    Would anyone incorporating this in their Prolog system please credit
    both me and David Warren;  he thought up the definitions, and my
    implementation may owe more to subconscious memory of his than I like
    to think.  At least this ought to put a stop to fraudulent claims to
    having bagof, by replacing them with genuine claims.

    Thanks to Dave Bowen for pointing out an amazingly obscure bug: if
    the Template was a variable and the Generator never bound it at all
    you got a very strange answer!  Now fixed, at a price.
*/

:- comment(setof(Template, Generator, Set), "Finds the @var{Set} of
    instances of the @var{Template} satisfying @var{Generator}.  The set
    is in ascending order (see @ref{Comparing terms} for a definition of
    this order) without duplicates, and is non-empty.  If there are no
    solutions, @tt{setof} fails.  @tt{setof} may succeed in more than
    one way, binding free variables in @var{Generator} to different
    values. This can be avoided by using existential quantifiers on the
    free variables in front of @var{Generator}, using @pred{^/2}. For
    example, given the clauses:
@begin{verbatim}
father(bill, tom).
father(bill, ann).
father(bill, john).
father(harry, july).
father(harry, daniel).
@end{verbatim}

The following query produces two  alternative solutions via backtracking:
@begin{verbatim}
?- setof(X,father(F,X),Sons).

F = bill,
Sons = [ann,john,tom] ? ;

F = harry,
Sons = [daniel,july] ? ;

no
?- 
@end{verbatim}").

:- true comp setof(X, Y, Z) + native(findall(X,Y,Z)).
:- true pred setof(@term, +callable, ?list) + iso.

%% This predicate is defined on p51 of the Dec-10 Prolog manual.

setof(Template, Filter, Set) :-
        bagof(Template, Filter, Bag),
        sort(Bag, Set).

:- comment(bagof(Template, Generator, Bag), "Finds all the instances of
   the @var{Template} produced by the @var{Generator}, and returns them
   in the @var{Bag} in the order in which they were found.  If the
   @var{Generator} contains free variables which are not bound in the
   @var{Template}, it assumes that this is like any other Prolog
   question and that you want bindings for those variables.  This can be
   avoided by using existential quantifiers on the free variables in
   front of the @var{Generator}, using @pred{^/2}.").

:- true comp bagof(X, Y, Z) + native(findall(X,Y,Z)).
:- true pred bagof(@term, +callable, ?list) + iso.

%   bagof records three things under the key '.':
%       the end-of-bag marker          -
%       terms with no free variables   -Term
%       terms with free variables   Key-Term
%   The key '.' was chosen on the grounds that most people are unlikely
%   to realise that you can use it at all, another good key might be ''.
%   The original data base is restored after this call, so that setof
%   and bagof can be nested.  If the Generator smashes the data base
%   you are asking for trouble and will probably get it.
%   The second clause is basically just findall, which of course works in
%   the common case when there are no free variables.

bagof(Template, Generator, Bag) :-
        free_variables(Generator, Template, [], Vars),
        Vars \== [], !,
        (   length(Vars, N),
            N =< 255 ->
              Key =.. [.|Vars]
        ;   Key = .(Vars)
        ),
        save_solutions(Key-Template, Generator),
        list_key_solutions(OmniumGatherum),
        keysort(OmniumGatherum, Gamut), !,
        concordant_subset(Gamut, Key, Answer),
        Bag = Answer.
bagof(Template, Generator, Bag) :-
        findall(Template, Generator, Bag),
        Bag \== [].

:- comment(findall(Template, Generator, List), "A special case of bagof,
     where all free variables in the @var{Generator} are taken to be
     existentially quantified. Faster than the other aggregation
     predicates.").

:- true pred findall(@term, +callable, ?list) + (iso, native).

%%  It is described in Clocksin & Mellish on p152.  The code they give has
%%  a bug (which the Dec-10 bagof and setof predicates share) which
%%  this has not.

findall(Template, Generator, List) :-
        save_solutions(-Template, Generator),
        list_solutions(List, []).

:- pred findall(Template, Generator, List, Tail)
   # "As @pred{findall/3}, but returning in @var{Tail} the tail of
     @var{List}.".

findall(Template, Generator, List, Tail) :-
        save_solutions(-Template, Generator),
        list_solutions(List, Tail).

:- comment(findnsols(N,Template,Generator,List),
     "As @pred{findall/3}, but generating at most @var{N} solutions of
     @var{Generator}.  Thus, the length of @var{List} will not be
     greater than @var{N}.  If @var{N}=<0, returns directly an empty
     list.  This predicate is especially useful if @var{Generator} may
     have an infinite number of solutions.").

:- true pred findnsols(+int,@term,+callable,?list).

findnsols(N,E,P,L) :-
        N > 0, !,
        NSol=n(0),
        save_n_solutions(NSol,N,-E,P),
        list_solutions(L,[]).
findnsols(_,_,_,[]).

:- comment(findnsols(N,Template,Generator,List,Tail),
     "As @pred{findnsols/4}, but returning in @var{Tail} the tail of
     @var{List}.").

:- true pred findnsols(+int,@term,+callable,?,?).

findnsols(N,E,P,L) :-
        N > 0, !,
        NSol=n(0),
        save_n_solutions(NSol,N,-E,P),
        list_solutions(L,[]).
findnsols(_,_,_,[]).

findnsols(N,E,P,L,T) :-
        N > 0, !,
        NSol=n(0),
        save_n_solutions(NSol,N,-E,P),
        list_solutions(L,T).
findnsols(_,_,_,T,T).

save_n_solutions(NSol, N, Template, Generator) :-
        asserta_fact(solution('-')),
        call(Generator),
        asserta_fact(solution(Template)),
        NSol = n(M),
        M1 is M+1,
        '$setarg'(1, NSol,M1,true),
        M1 = N -> fail.
save_n_solutions(_,_,_,_).

:- pred save_solutions(Template, Generator)

   # "Enumerates all provable instances of the @var{Generator} and
     records the associated @var{Template} instances.  Neither
     argument ends up changed.".

save_solutions(Template, Generator) :-
        asserta_fact(solution('-')),
        call(Generator),
        asserta_fact(solution(Template)),
        fail.
save_solutions(_,_).

:- pred list_solutions(List)

   # "Pulls all the @var{Template} instances out of the data base into
      @var{List}".

list_solutions(List, Tail) :-
        retract_fact(solution(Term)), !,
        list_solutions(Term,Tail,List).

list_solutions('-',L,L) :- !.
list_solutions(-Term,Sofar,List) :-
        retract_fact(solution(NewTerm)), !,
        list_solutions(NewTerm, [Term|Sofar],List).

:- pred list_key_solutions(List)

   # "Pulls all the Key-Term instances out of the data base into
     @var{List}".

%%   Note that asserting something into the data base and pulling it out
%%   again renames all the variables; to counteract this we use variables_of
%%   to enforce canonical names on all variables occurring in the Keys.
%%   This replacement must be done _before_ the keysort.
%%   The public domain version instead plugged in the original global variables
%%   whenever a solution didn't bind the corresponding variable.  My solution
%%   takes care of the case when a global variable is bound but not ground.
%%   Alternatively, canonical names could be plugged into entire Keys-Terms.
%%   I'm not sure it's a good idea, so I'm not doing it now.

list_key_solutions(List) :-
        retract_fact(solution(Term)), !,
        list_key_solutions(Term,_KeyVars,[],List).

list_key_solutions('-',_,L,L).
list_key_solutions(Term,KeyVars,SoFar,Total) :-
        Term = Key-_,
        variables_of(Key, KeyVars, KeyVars, _),
        retract_fact(solution(NewTerm)), !,
        list_key_solutions(NewTerm,KeyVars,[Term|SoFar],Total).


variables_of(T, Vars, S0, S) :-
        var(T), !, variable_in_list(T, Vars, S0, S).
variables_of(T, Vars, S0, S) :-
        functor(T, _, N),
        variables_of(N, T, Vars, S0, S).

variables_of(0, _, _, S0, S) :- !, S0=S.
variables_of(N, T, Vars, S0, S) :-
        arg(N, T, A),
        variables_of(A, Vars, S0, S1),
        M is N-1,
        variables_of(M, T, Vars, S1, S).

variable_in_list(T, Vars, S0, S) :-
        Vars==S0, !, S0=[T|S].
variable_in_list(T, [V|Vars], S0, S) :-
        (   T==V -> S0=S
        ;   variable_in_list(T, Vars, S0, S)
        ).



:- prop kvpair/1.

kvpair(_Key-_Val).

:- pred concordant_subset(list(kvpair), Key, list(Val))

   # "Takes a list of @var{Key-Val} pairs which has been keysorted to bring
     all the identical keys together, and enumerates each different
     Key and the corresponding lists of values.".

concordant_subset([Key-Val|Rest], Clavis, Answer) :-
        concordant_subset(Rest, Key, List, More),
        concordant_subset(More, Key, [Val|List], Clavis, Answer).


:-  pred concordant_subset(Rest, Key, List, More)

    # "Strips off all the Key-Val pairs from the from of Rest, putting
      the Val elements into List, and returning the left-over pairs,
      if any, as More.".

concordant_subset([Key-Val|Rest], Clavis, [Val|List], More) :-
        Key == Clavis,
        !,
        concordant_subset(Rest, Clavis, List, More).
concordant_subset(More, _, [], More).


:- pred concordant_subset/5

   # "Tries the current subset, and if that doesn't work if backs up
     and tries the next subset.  The first clause is there to save a
     choice point when this is the last possible subset.".

concordant_subset([],   Key, Subset, Key, Subset) :- !.
concordant_subset(_,    Key, Subset, Key, Subset).
concordant_subset(More, _,   _,   Clavis, Answer) :-
        concordant_subset(More, Clavis, Answer).



:- pred free_variables(Generator, Template, OldList, NewList)

   # "In order to handle variables properly, we have to find all the
      universally quantified variables in the @var{Generator}.  All
      variables as yet unbound are universally quantified, unless

       a)  they occur in the @var{Template}

       b)  they are bound by X^P, setof, or bagof

    free_variables(Generator, Template, OldList, NewList) finds this
    set, using @var{OldList} as an accumulator.".

free_variables(Term, Bound, VarList, [Term|VarList]) :-
        var(Term),
        term_is_free_of(Bound, Term),
        list_is_free_of(VarList, Term),
        !.
free_variables(Term, _, VarList, VarList) :-
        var(Term),
        !.
free_variables(Term, Bound, OldList, NewList) :-
        explicit_binding(Term, Bound, NewTerm, NewBound),
        !,
        free_variables(NewTerm, NewBound, OldList, NewList).
free_variables(Term, Bound, OldList, NewList) :-
        functor(Term, _, N),
        free_variables(N, Term, Bound, OldList, NewList).

free_variables(0, _, _, VarList, VarList) :- !.
free_variables(N, Term, Bound, OldList, NewList) :-
        arg(N, Term, Argument),
        free_variables(Argument, Bound, OldList, MidList),
        M is N-1,
        free_variables(M, Term, Bound, MidList, NewList).


:- pred explicit_binding/4

   # "Explicit_binding checks for goals known to existentially
      quantify one or more variables.  In particular \+ is quite
      common.".

explicit_binding(X, _, _, _) :- var(X), !, fail. % space saver
explicit_binding(\+ _, Bound,     fail,     Bound    ).
explicit_binding(Var^Goal, Bound, Goal,	    Bound+Var).
explicit_binding('aggregates:setof'(Var,Goal,Set), Bound,
                                  Goal-Set, Bound+Var).
explicit_binding('aggregates:bagof'(Var,Goal,Bag), Bound,
                                  Goal-Bag, Bound+Var).
explicit_binding('aggregates:findall'(_,_,Bag), Bound,
                                  Bag,      Bound    ).


term_is_free_of(Term, Var) :-
	var(Term), !,
	Term \== Var.
term_is_free_of(Term, Var) :-
	functor(Term, _, N),
	term_is_free_of(N, Term, Var).

term_is_free_of(0, _, _) :- !.
term_is_free_of(N, Term, Var) :-
	arg(N, Term, Argument),
	term_is_free_of(Argument, Var),
	M is N-1,
	term_is_free_of(M, Term, Var).


list_is_free_of([], _).
list_is_free_of([Head|Tail], Var) :-
	Head \== Var,
	list_is_free_of(Tail, Var).

:- pred '^'(X,P) # "Existential quantification: @var{X} is existentially
   quantified in @var{P}. E.g., in @tt{A^p(A,B)}, @tt{A} is
   existentially quantified.  Used only within @concept{aggregation
   predicates}. In all other contexts, simply, execute the procedure
   call @var{P}.".
:- true comp (_X^Y) + native(call(Y)).

%% %%% Was as follows when in builtin.pl:
%% (X^Y) :- undefined_goal((X^Y)).
(_X^Y) :- call(Y).

% -----------------------------------------------------------------------------

:- comment(version_maintenance,dir('../version')).

:- comment(version(1*5+115,2000/04/12,12:17*22+'CEST'), "Added
   findnsols/4 and findnsols/5 to compute a bounded number of solutions
   for a predicate. (Daniel Cabeza Gras)").

:- comment(version(0*7+9,1998/09/23,19:34*28+'MEST'), "Moved ^/2 here
   from basiccontrol.pl.  (Manuel Hermenegildo)").

:- comment(version(0*4+5,1998/2/24), "Synchronized file versions with
   global Ciao version.  (Manuel Hermenegildo)").

:- comment(version(0*2+0,1997/8/21), "Added basic
   documentation. (Manuel Hermenegildo)").

:- comment(version(0*1+0,1987/1/1), "Adapted from shared code written by
   Richard A. O'Keefe.").

:- comment(version(0*0+0,1982/1/1), "Original code written by Richard
   A. O'Keefe and David H.D. Warren.").

