% Computational Intelligence: a logical approach. 
% Prolog Code. 
% Meta-interpreter that lets you ask how a proof was found (Figure 6.9)
% Copyright (c) 1998, Poole, Mackworth, Goebel and Oxford University Press.

% This file contains simple code for creating and traversing a proof tree.
% This is useful for understanding and debugging programs that succeed.
% As an example load the file [sorting] and issue a query:
%  | ?- show(msort([4,2,8,6,1,3,4,2,9,6],S)).
% After this, give numbers that represent the branch you want to follow.
% Follow each number by a period.

% The file trace.pl is simpler and easier to understand.
% The file trace2.pl is more complex and more user friendly.
% If you want to actually use one of these, use trace2.pl.
% If you want to understand what is going on, try to understand trace.pl first.

% <- is the object-level `if' - it is an infix meta-level predicate
:- op(1150, xfx, <- ).
% `&' is the object level conjunction.
% It is an infix meta-level binary function symbol:
:- op(950,xfy, &).


% show(G) means to prove goal G and then show us a proof tree
show(G) :-
   solve(G,T),
   traverse(T).

% solve(Goal,Tree) is true if Tree is a proof tree for Goal
solve(true,true).
solve((A&B),(AT&BT)) :-
   solve(A,AT),
   solve(B,BT).
solve(H,if(H,builtin)) :-
   builtin(H),
   call(H).
solve(H,if(H,BT)) :-
%   clause(H,B),
   ( H <- B ),
   solve(B,BT).

% builtin(G) is true if goal G is defined in the system (as opposed to 
% being defined in Prolog clauses.
builtin((_ =< _)).
builtin((_ >= _)).
builtin((_ = _)).
builtin((_ < _)).
builtin((_ > _)).

% traverse(T) true if T is a tree being traversed
traverse(if(H,true)) :-
    writeln([H,' is a fact']).
traverse(if(H,builtin)) :-
    writeln([H,' is built-in.']).
traverse(if(H,B)) :-
    B \== true,
    B \== builtin,
    writeln([H,' :-']),
    printbody(B,1,_),
    read(Comm),
    interpretcommand(Comm,B).

% printbody(B,N1,N2) is true if B is a body to be printed and N1 is the 
% count of atoms before B was called and N2 is the count after
printbody(true,N,N).
printbody((A&B),N1,N3) :-
   printbody(A,N1,N2),
   printbody(B,N2,N3).
printbody(if(H,_),N,N1) :-
   writeln(['   ',N,': ',H]),
   N1 is N+1.

% interpretcommand(Comm,B) interprets the command Comm on body B
interpretcommand(N,B) :-
   integer(N),
   nth(B,N,E),
   traverse(E).

% nth(S,N,E) is true if E is the N-th element of structure S
nth(A,1,A) :-
   \+ (A = (_,_)).
nth((A&_),1,A).
nth((_&B),N,E) :-
   N>1,
   N1 is N-1,
   nth(B,N1,E).

% writeln(L) writes each element of list L
writeln([]) :- nl.
writeln([H|T]) :-
   write(H),
   writeln(T).