% Explain the proof tree in English to a certain depth bound
% with English explanation of user predicates
% e.g. family and familytalk

% Also includes primitive predicates in solve
% including negation, but not ancestor cut

% Do not show details of builtins

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

solve(true, true) :- !.

solve(A, true) :-
	builtin(A), !, A.

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

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, 
		      print, put, read, retract, see, seeing, seen,
		      setof, sort, tab, tell, telling, told,
		      true, var, write,
		      '<', '=<', '>', '>=', '=', '=..', '==', '\==',
		      '\+' ]).

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

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((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, Max),
	explain(B, Depth, Max).

% Depth = Max, don't show anything
explain(_, _, _).


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