/*
    monitor(Goal,Proof) :-
       Succeeds if a result of yes is returned from solving Goal at the
       solve level, in which case Proof is a proof tree representing the
       successful computation, or when the end of the computation is reached,
       in which case Proof is a list of failure branches since the last success.
*/

:-  op( 900, fy, not).
:- op(40,xfy,&).
:- op(30,xf,is_true).

    monitor(Goal,Proof) :-
       set_search_tree, solve(Goal,Result,Proof),
       filter(Result,Proof).
    monitor(Goal,Proof) :-
       collect_proof(P), reverse(P,P1),
       Proof = failed(Goal,P1).

    filter(yes,Proof) :-  reset_search_tree.
    filter(no,Proof) :-  store_proof(Proof), fail.

/*
    solve(Goal,Result,Proof)  :-
       Given a set of rules of the form rule(A,B,Name), Goal has
       Result yes if it follows from the rules and no if it does not.
       Proof  is a proof tree if the result is yes and a failure branch
       of the search tree if the result is no.
*/
    :- op(40,xfy,because).
    :- op(30,xfy,with).

    solve(A,yes,Tree) :-  fact(A), Tree = fact(A).
    solve(A,Result,Tree) :-
       rule(A,B,Name), solve_body(B,Result,Proof),
       Tree = A because B with Proof.
    solve(A,no,Tree) :-
       not fact(A), not rule(A,B,Name), Tree = no_match(A).

    solve_body(A&B,Result,Proof) :-
       solve_body(A,ResultA,ProofA),
       solve_and(ResultA,B,Result,ProofB),
       Proof = ProofA & ProofB.
    solve_body(A is_true,Result,Proof) :-  solve(A,Result,Proof).

    solve_and(no,A,no,unsearched).
    solve_and(yes,B,Result,Tree) :-  solve(B,Result,Tree).

%  The following predicates use side effects to record and remove 
%  branches of the search tree.

    collect_proof(Proof) :-  retract('search tree'(Proof)).

    store_proof(Proof) :- 
       retract('search tree'(Tree)),
       assert('search tree'([ProofjTree])).

    set_search_tree :-  assert('search tree'([ ])).

    reset_search_tree :- 
       retract('search tree'(Proof)),
       assert('search tree'([ ])).

	reverse([],[]).
	reverse([X|Xs],Zs) :- reverse(Xs,Ys), append(Ys,[X],Zs).

%    Program 17.21: A two-level rule interpreter with proof trees