% Explain the proof tree in English to a certain depth bound
% (with English explanation of user predicates). Recognize built-in
% predicates, including negation, but not ancestor cut. No details of 
% input-output and other builtins, but setof details are shown.

why(G) :-
	solve(G, P),
	explain(P).

solve(true, true) :- !.

solve(A, true) :-
	builtin(A), !, A.  % no proof tree for built-in's

solve((A, B), (ProofA, ProofB)) :- !,
	solve(A, ProofA), 
	solve(B, ProofB).

solve(setof(T,G,L), (setof(T,G,TGPL) :- true)) :- !,
	setof([T, G-Proof], solve(G, Proof), TGPL),
	extract_set(TGPL, L).

solve(not(A), (not(A) :- true)) :- !,
	not(solve(A, _)).

solve(A, (A :- Proof)) :-
	clause(A, B),
	solve(B, Proof).

builtin(A) :- 
	A =.. [Pred | _],
	member(Pred, [arg, assert, asserta, assertz, atom, atomic,
		      bagof, call, clause, close, consult,
		      display, fail, functor, get, get0,
		      integer, is, nonvar, number, nl, 
%		      not,
		      print, put, read, retract, see, seeing, seen,
%		      setof, 
		      sort, tab, tell, telling, told,
		      true, var, write,
		      '<', '=<', '>', '>=', '=', '=..', '==', '\==',
		      '\+' ]).

not(G) :- G, !, fail.
not(G).

extract_set([], []).
extract_set([[T|_]|L], [T|S]) :- 
	extract_set(L,S).


explain((A :- Proof)) :-
	nl, write('To what depth? '), read(DMax),
	talk(A),
	explain(Proof, 1, DMax).

explain(true, Depth, DMax) :- !.

explain((not(A) :- true), Depth, DMax) :-
	Depth < DMax, !,
	nl, tab(Depth*3), write('because it is not true that '), talk(A).

explain((setof(T,G,TGPL) :- true), Depth, DMax) :-
	Depth < DMax, !,
	nl, tab(Depth*3), write('because the solution set for '), 
	write(G), write(' is '), 
	nl, tab(3*Depth+9), write('{ '), write_setof(TGPL, Depth), write('}'),
	D is Depth + 1,
	explain_setof(TGPL, D, DMax).

explain((A :- true), Depth, DMax) :-
	Depth < DMax, !,
	(builtin(A) -> 
		true;
		nl, tab(Depth*3), write('because '), talk(A)).

explain((A :- Proof), Depth, DMax) :-
	Depth < DMax, !,
	nl, tab(Depth*3), write('because '), talk(A),
	D is Depth + 1,
	explain(Proof, D, DMax).

explain((A, B), Depth, DMax) :-
	Depth < DMax, !,
	explain(A, Depth, DMax),
	explain(B, Depth, DMax).

explain(_, _, _).

explain_setof([], Depth, DMax).
explain_setof([[_, G-Proof] | L], Depth, DMax) :-
	explain(Proof, Depth, DMax),
	explain_setof(L, Depth, DMax).

talk(A) :- ptalk(A), !.
talk(A) :- write(A).

write_setof([], Depth).
write_setof([[T|_]|L], Depth) :- 
	nl, tab(3*Depth+11), write(T), write(' '), write_setof(L, Depth).

member(X, [X|_]).
member(X, [_|T]) :- member(X, T).