% Meta interpreter for Prolog

prove(true) :- !. % body of facts
prove( (A,B) ) :- !,
        prove(A), % prove first conjunct
        prove(B). % prove second conjunct
prove(L) :-
        clause(L,B), % find appropriate clause for L
        prove(B).

%:- dynamic app/3.
app([],Ys,Ys).
app([X|Xs],Ys,[X|Zs]) :- app(Xs,Ys,Zs).


% Meta interpreter for Prolog with computation of number of resolution steps.
lprove(true,0) :- !. % body of facts
lprove( (A,B), N) :- !,
        lprove(A,NA), % prove first conjunct
        lprove(B,NB), % prove second conjunct
        N is NA + NB.
lprove(L, N) :-
        clause(L,B), % find appropriate clause for L
        lprove(B,NB),
        N is NB + 1.


p(a).
p(b).
q(b).

% Meta interpreter for Prolog with tracing output:
tprove(true) :- !. % body of facts
tprove( (A,B) ) :- !,
        tprove(A), % prove first conjunct
        tprove(B). % prove second conjunct
tprove(L) :-
        callfail(L),
        clause(L,B), % find appropriate clause for L
        tprove(B),
        exitredo(L).

callfail(L) :- write('Call: '), write(L), nl.
callfail(L) :- write('Fail: '), write(L), nl, fail.

exitredo(L) :- write('Exit: '), write(L), nl.
exitredo(L) :- write('Redo: '), write(L), nl, fail.

