1:- module(pureprimrec, []).    2:- dynamic  def/2.    3
    4% ?- eval(0,X).
    5% X = 0
    6% ?- eval(decr(s(0)),X).
    7% X = 0
    8% ?- eval(s(decr(0)),X).
    9% X = s(0)
   10% ?- eval(s(0)*s(0), X).
   11% X = s(0)
   12% ?- eval(s(0)*s(s(0)), X).
   13% X = s(s(0))
   14% ?- eval(s(s(0))*s(s(0)), X).
   15% X = s(s(s(s(0))))
   16% ?- eval(fact(s(s(0))), X).
   17% X = s(s(0))
   18% ?- eval(fact(s(s(s(0)))), X).
   19% X = s(s(s(s(s(s(0))))))
   20% ?- eval(decr(s(s(s(0)))), X).
   21% X = s(s(0))
   22% ?- eval(decr(decr(s(s(s(0))))), X).
   23% X = s(0)
   24% ?- eval(s(s(0))> s(0), X).
   25% X = s(0)
   26% ?- eval(s(s(0)) = s(0), X).
   27% X = 0
   28
   29def(
   30   fact(0)   = s(0) ; 
   31   fact(s(n)) = s(n) * fact(n) ;
   32    
   33   0 * x     =  0 ;
   34   s(n)* x   =  x + n * x ;
   35    
   36   0 + x     = x ;
   37   s(n) + x  = s(n + x) ;
   38
   39   decr(0)   = 0 ;
   40   decr(s(x)) = x ;
   41
   42  (m - 0)    = m ;
   43  (m - s(n)) = decr(m- n) ;
   44
   45   zero(0)   = s(0) ;
   46   zero(s(x))=0;
   47
   48   not(0)    = s(0) ;
   49   not(s(n)) = 0;
   50
   51   &(0, x)   = 0;
   52   &(s(n), x) = not(zero(x)) ;
   53
   54   or(x, y)  =  not(&(not(x), not(y))) ;
   55
   56   if(0, x, y) = y;
   57   if(s(n), x, y) = x;
   58
   59   positive(0) = 0;
   60   positive(s(x)) =  s(0) ;
   61    
   62   (x > y)    =  positive(x - y) ;
   63    
   64   (x = y)    =  &(zero(x-y), zero(y-x))
   65   ).
   66
   67assoc_var(X, V, A, A) :- memberchk((X,V), A), !.
   68assoc_var(X, V, A, [(X,V)|A]).
   69
   70subst_var(X, Y) :- subst_var(X, Y, [], _).
   71
   72subst_var(X, X, A, A):- integer(X), !.
   73subst_var(X, V, A, B):- atom(X), !, assoc_var(X, V, A, B).
   74subst_var(X, Y, A, B):- X=..[X0|Xs], subst_var_list(Xs, Ys, A, B),
   75         Y =..[X0|Ys].
   76
   77subst_var_list([], [], A, A).
   78subst_var_list([X|Xs], [Y|Ys], A, B):- subst_var(X, Y, A, A0),
   79	subst_var_list(Xs, Ys, A0, B).
   80
   81eval_basic(0, 0):- !.
   82eval_basic(T, V):- mapterm(eval, T, T0), apply_def(T0, V).
   83
   84apply_def(X, Y):- def(X, Body), !, eval_basic(Body, Y).
   85apply_def(X, X).
   86
   87eval(Expr, V):- def(Eqs), eval_basic(Expr, Eqs, V).
   88
   89eval_basic(Expr, Eqs, V):- abolish(def/2),
   90	assert_pr(def, Eqs),
   91	eval_basic(Expr, V).
   92
   93assert_pr(D, A; B):- !, assert_pr(D, A), assert_pr(D, B).
   94assert_pr(D, A = B):- subst_var(A=B, A0=B0),
   95	C =.. [D, A0, B0],
   96	assert(C)