:-module(prove_examples, [prove_examples/6
                         ,debug_clauses/3
                         ,print_clauses/2
                         ,print_clauses/1
                         ]).

/** <module> Collect refutation sequences of a set of examples of a learning target.

Predicate prove_examples/7 collects all refutation paths of an example
atom by first invoking indexed_program/2 to transform each clause in the
input program by adding a new body literal at the end of the clause. The
new literal asserts to the dynamic database a term '$called_clause'/1
that has as a single argument an integer indexing the clause in the
input program. Clauses of '$called_clause'/1 are collected from the
dynamic database on exit and the corresponding clauses are returned.

Example query:

==
?- _Ts = [(nat(X1) :- even(X1)), (nat(X2) :- odd(X2))],
_BK = [(odd(A):-s(A,B),even(B)), s(s(X3),X3), even(0), (even(s(X4)):-odd(X4))],
_Pos = [nat(s(s(0))), nat(s(s(s(0))))],
_Neg = [], _Ss = [nat/1],
prove_examples(_Ts, _Pos, _Neg, _BK, _Ss, _Ts_), print_clauses(_Ts_).

nat(A):-even(A).
nat(A):-odd(A).
nat(s(s(0))).
nat(s(s(s(0)))).
true.
==

Note that the input program is tabled before processing. This makes the
program incomplete because tabling means that only one refutation
sequence for each example is found. So this is not a perfect solution.

*/

% Not the best possbile name.
:-dynamic '$remove_null':'$called_clause'/1.


%!	prove_examples(+Program,+Pos,+Neg,+BK,+Symbols,-Paths) is det.
%
%	Collect clauses in refutation sequences of a set of examples.
%
%	Program is a list of clauses of a definition of a set of target
%	predicates.
%
%	Pos is a list of examples of the target predicates from which
%	Program was learned.
%
%	Neg is a list of negative examples of 0 or more of the target
%	predicates in Pos. Negative examples are negative atoms of the
%	form ":-A".
%
%	BK is a list of clauses of BK predicate	definitions.
%
%	Symbols is the list of predicate indicators of the target
%	predicates in Pos.
%
%	Paths is a subset of the clauses in Top that were found in a
%	refutation sequence of an example in Pos given Top and BK and
%	_not_ in the refutation sequence of an example in Neg.
%
%	@tbd This predicate starts by adding the positive examples to
%	the learned Program, which is necessary because some clauses in
%	the learned Program may have recursive goals that can only
%	resolve with an example. This is likely when an example is the
%	atomic base-case of a recursive predicate, for instance. The
%	trick is that the clauses of the examples cannot go above the
%	clauses of the Program, otherwise the first refutation
%	sequence found by Prolog's search will be the one that refutes
%	(the negation of) an example as a goal by itself.
%
prove_examples(Ts,Pos,Neg,BK,Ss,Ts_):-
	append(Ts,Pos,Ps)
	,S = (indexed_program(Ps,Ps_i)
	     ,assert_program('$remove_null',Ps_i,Rs_1)
	     ,debug_clauses(remove_null,'Indexed program',Ps_i)
	     ,assert_program('$remove_null',BK,Rs_2)
	     ,table_targets(Ss)
	     )
	,G = (prove_examples(Pos,[],Is_plus)
	     ,debug(remove_null,'Is_plus: ~w',[Is_plus])
	     ,prove_examples(Neg,[],Is_minus)
	     ,debug(remove_null,'Is_minus: ~w',[Is_minus])
	     ,ord_intersection(Is_plus,Is_minus,Ints)
	     ,debug(remove_null,'Intersection: ~w',[Ints])
	     ,(	  Ints = []
	      ->  Inds = Is_plus
	      ;	  Inds = Ints
	      )
	     ,debug(remove_null,'Kept indices: ~w',[Inds])
	     ,collect_indexed(Ps,Inds,Ts_)
	     ,debug_clauses(remove_null,'Top Program:',Ts_)
	     )
	,C = (eraseall_program_clauses(Rs_1)
	     ,eraseall_program_clauses(Rs_2)
	     ,untable_targets(Ss)
	     ,cleanup_indexed_clauses
	     )
	,setup_call_cleanup(S,G,C).


%!	prove_examples(+Examples,+Acc,-Indices) is det.
%
%	Prove Examples and collect indices of called clauses.
%
%	Business end of prove_examples/5. Calls each example and
%	collects from the dynamic database the indices of clauses in
%	the example's successful refutation sequences. Clause indices
%	are recorded to the dynamic database as dynamic
%	'$called_clause'/1 Prolog terms.
%
%	While attempting to prove an example, Prolog may call any number
%	of clauses that do not entail the example. We don't want those
%	to be registered as members of a _successful_ refutation
%	sequence. This is ensured, hopefully, by the fact that
%	'$called_clause'1 terms are only recorded when all the body
%	goals of a clause are refuted successfully. Additionally, if a
%	refutation of an example fails, we return no clause indices and
%	we remove the '$called_clause'/1 terms asserted to the database
%	in the process.
%
%	In the following, the first clause is the base-case, the second
%	clause proves negative examples (negated atoms ":-A"), the
%	second clause proves positive examples, the fourth clause cleans
%	up the dynamic database after the proof of a negative example
%	fails and the last clause does the same for positive examples.
%
prove_examples([],Acc,Is):-
	!
       ,flatten(Acc,Is_)
       ,sort(Is_,Is).
prove_examples([:-E|Pos],Acc,Bind):-
	debug_clauses(remove_null,'Proving negative example',[E])
	%,call('$remove_null':E) % Stop at one successful refutation.
        ,findall(_,call('$remove_null':E),_)
	,!
	,debug_clauses(remove_null,'Proved negative example',[E])
	,collect_indices(Is)
	,debug_clauses(remove_null,'Collected clause indices',[Is])
	,cleanup_indexed_clauses
	,debug(remove_null,'Cleaned up indexed clauses',[])
	,prove_examples(Pos,[Is|Acc],Bind).
prove_examples([E|Pos],Acc,Bind):-
	\+ functor(E,:-,_)
	,debug_clauses(remove_null,'Proving positive example',[E])
	%,call('$remove_null':E)
        ,findall(_,call('$remove_null':E),_)
	,!
	,debug_clauses(remove_null,'Proved positive example',[E])
	,collect_indices(Is)
	,debug_clauses(remove_null,'Collected clause indices',[Is])
	,cleanup_indexed_clauses
	,debug(remove_null,'Cleaned up indexed clauses',[])
	,prove_examples(Pos,[Is|Acc],Bind).
prove_examples([:-E|Pos],Acc,Bind):-
	!
	,debug_clauses(remove_null,'Failed to prove negative example',[E])
	,cleanup_indexed_clauses
	,prove_examples(Pos,Acc,Bind).
prove_examples([E|Pos],Acc,Bind):-
	\+ functor(E,:-,_)
	,debug_clauses(remove_null,'Failed to prove positive example',[E])
	,cleanup_indexed_clauses
	,prove_examples(Pos,Acc,Bind).


%!	collect_indices(-Indices) is det.
%
%	Collect indices of clauses in a refutation sequence.
%
%	Clause indices are recorded in the database as terms of
%	'$called_clause'/1.
%
%	@tbd '$called_clause'/1 needs a better name.
%
collect_indices(Is):-
	findall(I
	       ,('$remove_null':'$called_clause'(I)
		)
	       ,Is).


%!	indexed(+Program,+Indices,-Clauses) is det.
%
%	Collect clauses found in a refutation sequence.
%
%	Program is a hypothesis learned from a set of examples.
%
%	Indices is a list of numbers, the indices of clauses in Program
%	that were found in the refutation sequences of one or more
%	examples, with respect to BK.
%
%	Clauses is the set of clauses of the Program with the given
%	Indices.
%
collect_indexed(Ts,Is,Cs):-
% TODO: optimise this quadratic s$%tz.
	findall(C
	       ,(member(I,Is)
		,nth1(I,Ts,C)
		)
	       ,Cs).


%!	indexed_program(+Program,-Indexed) is det.
%
%	Add indexing literals to the clauses of a Program.
%
indexed_program(Ps,Ps_):-
	findall(C_
	       ,(nth1(I,Ps,C)
		,indexed_clause(I,C,C_)
		)
	       ,Ps_).


%!	indexed_clause(+Index,+Clause,-Indexed) is det.
%
%	Add an indexing literal to the body of a clause.
%
%	Index is a number, the index over a learned program program of
%	the input Clause that we want to index.
%
%	Clause is a clause in a learned program that is to be indexed.
%
%	Indexed is Clause with an indexing literal appended to its
%	body (i.e. the indexing literal is the last body literal of the
%	indexed Clause).
%
%	Note that Clause may not have a body. In that case, the indexing
%	literal becomes its only body literal.
%
%	An indexing literal asserts a term '$called_clauase'(Index) to
%	the dynamic database from where it can later be retrieved to
%	reconstruct a refutation sequence of an example, particularly
%	in order to collect the clauses in the sequence.
%
%	@tbd Note that since the indexing literal is the last body
%	literal in a clause, tail-call optimisation is not possible,
%	with the obvious implications for efficiency.
%
%	@tbd Actually, this predicate also adds a pair of debugging
%	literals to the end of a clause, and that's the very last
%	literal in the body of a clause.
%
%	@tbd And why stop there? We could add _any_ number of new
%	literals to the end of the clause. An entire implementation of
%	Prolog in Lisp in Prolog, say. :shakes head:
%
indexed_clause(I,H:-B,H:-B_):-
	once(list_tree(Bs,B))
	,T = prove_examples:assert_program('$remove_null',['$called_clause'(I)], _Ref)
	,T1 = debug(remove_null,'Called clause ~w',[I])
	,T2 = prove_examples:debug_clauses(remove_null,[H:-B])
	%,append(Bs, [T,T1], Bs_)
	,append(Bs, [T,T1,T2], Bs_)
	,once(list_tree(Bs_, B_)).
indexed_clause(I,C,H:-B):-
	C \= (_:-_)
	,T = prove_examples:assert_program('$remove_null',['$called_clause'(I)], _Ref)
	,T1 = debug(remove_null,'Called clause ~w',[I])
	,T2 = prove_examples:debug_clauses(remove_null,[C])
	%,append([C], [T,T1], Bs_)
	,append([C], [T,T1,T2], Bs_)
	,once(list_tree(Bs_, (H,B))).


%!	cleanup_indexed_clauses is det.
%
%	Remove indexed clauses from the database.
%
cleanup_indexed_clauses:-
	 retractall('$remove_null':'$called_clause'(_)).


%!	table_targets(+Targets) is det.
%
%	Table each target predicate defined in a learned program.
%
%	Targets is the set of predicate symbols and arities of the
%	learning targets defined in a program learned from a set of
%	examples.
%
table_targets(Ts):-
	forall(member(F/A,Ts)
	      ,(table('$remove_null':F/A)
	       ,debug_clauses(remove_null,'Tabled predicate',[F/A])
	       )
	      ).


%!	untable_targets(+Targets) is det.
%
%	Untable tabled predicates of a learned program.
%
%	Counterpart of table_targets/1 to cleanup tabling declarations.
%
untable_targets(Ts):-
	forall(member(F/A,Ts)
	      ,(untable('$remove_null':F/A)
	       ,debug_clauses(remove_null,'Untabled predicate',[F/A])
	       )
	      ).



% ================================================================================
% Auxiliary predicates
% ================================================================================


%!	list_tree(?List, ?Tree) is det.
%
%	Convert between a list and a Prolog binary tree.
%
%	Tree is a Prolog term (L1,...,Ln). A binary tree, yes?
%
list_tree(Ls, Ts):-
	phrase(list_tree(Ts), Ls).


%!	list_tree(?Tree) is nondet.
%
%	Business end of clause_literals/2.
%
list_tree((T,Ts)) --> [T], list_tree(Ts).
list_tree((T:-Ts)) --> [T], list_tree(Ts).
list_tree(T) --> [T].




% ================================================================================
% Logging and printing predicats
% ================================================================================

%!	debug_clauses(+Topic,+Message,-Clauses) is det.
%
%	Log a Message followed by a set of Clauses.
%
debug_clauses(T,M,Cs):-
	debug(T,'~w',[M])
	,debug_clauses(T,Cs).


%!	debug_clauses(+Topic,+Clauses) is det.
%
%	Debug a list of Clauses if Topic is being debugged.
%
debug_clauses(T,[]):-
	!
	,debug(T,'[]',[]).
debug_clauses(T,L):-
	\+ is_list(L)
	,!
	,debug_clauses(T,[L]).
debug_clauses(T,Cs):-
	forall(member(C,Cs)
	      ,(copy_term(C,C_)
	       ,numbervars(C_)
	       ,format(atom(A),'~W',[C_, [fullstop(true)
					 ,numbervars(true)
					 ,quoted(true)]
				    ])
	       ,debug(T,'~w',A)
	       )
	      ).



%!	print_clauses(+Message,-Clauses) is det.
%
%	Print a Message followed by a set of Clauses.
%
print_clauses(M,Cs):-
	format('~w~n',[M])
	,print_clauses(Cs).


%!	print_clauses(+Clauses) is det.
%
%	Print a list of Clauses to standard output.
%
print_clauses([]):-
	!
	,writeln([]).
print_clauses(L):-
	\+ is_list(L)
	,!
	,print_clauses([L]).
print_clauses(Cs):-
	forall(member(C,Cs)
	      ,(copy_term(C,C_)
	       ,numbervars(C_)
	       ,write_term(C_, [fullstop(true)
			       ,nl(true)
			       ,numbervars(true)
			       ,quoted(true)
			       ])
	       )
	      ).




%!	assert_program(+Module,+Program,-Clause_References) is det.
%
%	As assert_program/2 but also binds a list of Clause_References.
%
assert_program(M,Ps,Rs):-
	assert_program(M,Ps,[],Rs).

assert_program(_,[],Rs,Rs):-
	!.
assert_program(M,[A|P],Acc,Bind):-
	copy_term(A,A_)
	,numbervars(A_)
	,clause(M:A_,true)
	,!
	,assert_program(M,P,Acc,Bind).
assert_program(M,[C|P],Acc,Bind):-
	copy_term(C,H:-B)
	,numbervars(H:-B)
	,clause(M:H,B)
	,!
	,assert_program(M,P,Acc,Bind).
assert_program(M,[C|P],Acc,Bind):-
	assert(M:C,Ref)
	,assert_program(M,P,[Ref|Acc],Bind).



%!	eraseall_program_clauses(+Refs) is det.
%
%	retractall-like clause erasure.
%
%	"Retractall-like" in the sense that if a reference in Refs is
%	now found, this doesn't fail and simply continues with the next
%	reference.
%
eraseall_program_clauses([]):-
	!.
eraseall_program_clauses([Ref|Rs]):-
	erase(Ref)
	,!
	,eraseall_program_clauses(Rs).
eraseall_program_clauses([_Ref|Rs]):-
	eraseall_program_clauses(Rs).
