% 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 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)).
% 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),
H.
solve(call(G),T) :-
solve(G,T).
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,Max),
read(Comm),
interpretcommand(Comm,B,Max,if(H,B)).
% printbody(B,N) is true if B is a body to be printed and N is the
% count of atoms before B was called (this assumes that ``&'' is
% left-associative.
printbody((A&B),N,N2) :-
printbody(A,N,N),
N1 is N+1,
printbody(B,N1,N2).
printbody(if(H,_),N,N) :-
writeln([' ',N,': ',H]).
% interpretcommand(Comm,B) interprets the command Comm on body B
interpretcommand(N,B,Max,G) :-
integer(N),
N > 0,
N =< Max,
nth(B,N,E),
traverse(E),
traverse(G).
interpretcommand(up,_,_,_).
interpretcommand(N,_,Max,G) :-
integer(N),
(N < 1 ; N > Max),
writeln(['Number out of range: ',N]),
traverse(G).
interpretcommand(help,_,_,G) :-
writeln(['Give either a number, up or retry. End command with a Period.']),
traverse(G).
interpretcommand(C,_,_,G) :-
\+ integer(C),
C \== up,
C \== help,
C \== retry,
writeln(['Illegal Command: ',C,' Type "help." for help.']),
traverse(G).
% 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).