eval.pl

% ------------------------   SYNTAX  ------------------------

m(M) :- M = true
      ; M = false
      ; M = if(M1,M2,M3)     , m(M1),m(M2),m(M3)
      ; M = zero
      ; M = succ(M1)         , m(M1)
      ; M = pred(M1)         , m(M1)
      ; M = iszero(M1)       , m(M1)
      .
n(N) :- N = zero
      ; N = succ(N1)         , n(N1)
      .
v(V) :- V = true
      ; V = false
      ; n(V)
      .

% ------------------------   EVALUATION  ------------------------

eval1(if(true,M2,_), M2,'E-IfTrue').
eval1(if(false,_,M3), M3, 'E-IfFalse').
eval1(if(M1,M2,M3), if(M1_, M2, M3), Rule) :- eval1(M1,M1_, Rule).
eval1(succ(M1),succ(M1_), Rule) :- eval1(M1,M1_, Rule).
eval1(pred(zero), zero, 'E-Pred').
eval1(pred(succ(N1)), N1, 'E-PredSucc') :- n(N1).
eval1(pred(M1), pred(M1_), Rule) :- eval1(M1,M1_, Rule).
eval1(iszero(zero), true, 'E-IsZeroZero').
eval1(iszero(succ(N1)), false, 'E-IsZeroSucc') :- n(N1).
eval1(iszero(M1), iszero(M1_), Rule) :- eval1(M1,M1_,Rule).

eval(M,_):- writeln(M),fail.
eval(M,M_) :- eval1(M,M1,Rule),write('------------------------- '),writeln(Rule), eval(M1,M_).
eval(M,M).

% ------------------------   MAIN  ------------------------

run(eval(M),Γ,Γ) :- !,m(M),!,eval(M,_),!, nl.
run(Ls) :- foldl(run,Ls,[],_).

% ------------------------   TEST  ------------------------

:- run([eval(true)]).
:- run([eval(if(false,true,false))]).

:- run([eval(zero)]).
:- run([eval(succ(pred(zero)))]).
:- run([eval(iszero(pred(succ(succ(zero)))))]).
:- run([eval(iszero(pred(pred(succ(succ(zero))))))]). 
:- run([eval(iszero(zero))]).

:- halt.