% Meta interpreter for Prolog

prove(true) :- !.
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).

% Extend the interpreter: return the length of a proof
lprove(true,0) :- !.
lprove( (A,B), L) :- !,
        lprove(A,LA), % prove first conjunct
        lprove(B,LB), % prove second conjunct
        L is LA+LB.
lprove(H,L) :-
        clause(H,B), % find appropriate clause for L
        lprove(B,LB),
        L is LB+1.

:- dynamic p/1, q/1.
p(a).
p(b).
q(b).

% ?- trace, p(X), q(X).

% Meta interpreter with tracing
tprove(true) :- !.
tprove( (A,B) ) :- !,
        tprove(A), % tprove first conjunct
        tprove(B). % tprove second conjunct
tprove(L) :-
        callfail(L), % show call/fail port for L
        clause(L,B), % find appropriate clause for L
        tprove(B),
        exitredo(L). % show exit/redo port for 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.

