:- dynamic app/3.

app([],L,L).
app([E|R],L,[E|RL]) :- app(R,L,RL).


% Simple meta-interpreter for Prolog:
prove(true) :- !.
prove( (G1,G2) ) :- !, prove(G1), prove(G2).
prove(L) :- clause(L,G), prove(G).

% A meta-interpreter for Prolog which also computes the proof length:
lprove(true, 0) :- !.
lprove( (G1,G2), N) :- !, lprove(G1, N1), lprove(G2, N2), N is N1+N2.
lprove(L, N1) :- clause(L,G), lprove(G, N), N1 is N+1.

:- dynamic p/1, q/1.

% a simple example:
p(a).
p(b).
q(b).

% A meta-interpreter with tracing for Prolog:
tprove(true) :- !.
tprove( (G1,G2) ) :- !, tprove(G1), tprove(G2).
tprove(L) :- showcallfail(L), clause(L,G), tprove(G), showexitredo(L).

showcallfail(L) :- write('CALL: '), write(L), nl.
showcallfail(L) :- write('FAIL: '), write(L), nl, !, fail.

showexitredo(L) :- write('EXIT: '), write(L), nl.
showexitredo(L) :- write('REDO: '), write(L), nl, !, fail.