1:- module(arith_partial_eval,[]).    2
    3% ?- arith_partial_eval(0, X).
    4%@ X = 0.
    5% ?- arith_partial_eval(0+A+0, X).%@ A = X.
    6%@ A = X.
    7% ?- arith_partial_eval(1+(A+B)*0, X).
    8%@ X = 1.
    9% ?- arith_partial_eval(0+ (X<<((2*A*1 + 4*B*1)*0))*(1+2), R).
   10%@ R = X+X*2.
   11%@ R = X+X*2.
   12% ?- arith_partial_eval(0+ X<<(((((2*A*1 + 4*B*1)*0)))*(1+2)), R).
   13%@ X = R.
   14% ?- arith_partial_eval(X+Y+Z -(Y + Z), R).
   15%@ X = R.
   16% ?- arith_partial_eval(X - Y + Z -(Y + Z), R).
   17%@ R = X+ -Y+ -Y.
   18% ?- arith_partial_eval(X << (Y - Y + Z - Z), R).
   19%@ X = R.
   20% ?- arith_partial_eval(X ^ (1-1), R).
   21
   22% ?- arith_partial_eval(0 ^ (1-1), R).
   23% ?- arith_partial_eval(X + X + X, R).
   24%@ R = X+X+X.
   25% ?- arith_partial_eval(X + X + Y + X , R).
   26
   27
   28% ?- listing(arith_rule).
   29
   30elim_term(A, B, 0)	:- A==B.
   31elim_term(A, B, X)	:- nonvar(B, X+Y), A==Y.
   32elim_term(A, B, Z+Y):- nonvar(B, X+Y), elim_term(A, X, Z).
   33%
   34nonvar(X, Y):- nonvar(X), Y=X.
   35%
   36ground_compound_basic_exp(E):- compound(E),
   37	arg(1, E, A),
   38	integer(A),
   39	(	arg(2, E, B) -> integer(B)
   40	;	true
   41	).
   42%
   43arith_partial_eval(X, Y):- arith_rule(X, X0), !,
   44	arith_partial_eval(X0, Y).
   45arith_partial_eval(X, X).
   46%
   47arith_rule(A, _)			:- var(A), !, fail.
   48arith_rule(A - B, A + -(B)).
   49arith_rule(E*C, A*C+B*C)	:- nonvar(E, A+B).
   50arith_rule(C*E, C*A+C*B)	:- nonvar(E, A+B).
   51arith_rule(A+E, (A+B)+C)	:- nonvar(E, B+C).
   52arith_rule(A*E, (A*B)*C)	:- nonvar(E, B*C).
   53arith_rule(A+B, A0+B)		:- arith_rule(A, A0).
   54arith_rule(A+B, A+B0)		:- arith_rule(B, B0).
   55arith_rule(+(A), +(A0))		:- arith_rule(A, A0).
   56arith_rule(-E, -A + -B)		:- nonvar(E, A+B).
   57arith_rule(-E, A)			:- nonvar(E, -A).
   58arith_rule(-(A), -(A0))		:- arith_rule(A, A0).
   59arith_rule(E, V)			:- ground_compound_basic_exp(E), V is E.
   60arith_rule(A*B, A0*B)		:- arith_rule(A, A0).
   61arith_rule(A*B, A*B0)		:- arith_rule(B, B0).
   62arith_rule(A//B, A0//B)		:- arith_rule(A, A0).
   63arith_rule(A//B, A//B0)		:- arith_rule(B, B0).
   64arith_rule(A<<B, A0<<B)		:- arith_rule(A, A0).
   65arith_rule(A<<B, A<<B0)		:- arith_rule(B, B0).
   66arith_rule(A>>B, A0>>B)		:- arith_rule(A, A0).
   67arith_rule(A>>B, A>>B0)		:- arith_rule(B, B0).
   68arith_rule(A^B, A0^B)		:- arith_rule(A, A0).
   69arith_rule(A^B, A^B0)		:- arith_rule(B, B0).
   70arith_rule(A mod B, A0 mod B)	 :- arith_rule(A, A0).
   71arith_rule(A mod B, A mod B0)	 :- arith_rule(B, B0).
   72arith_rule(E*_, 0)		:- E == 0.
   73arith_rule(_*E, 0)		:- E == 0.
   74arith_rule(E+X, X)		:- E == 0.
   75arith_rule(X+E, X)		:- E == 0.
   76arith_rule(X>>E, X)		:- E == 0.
   77arith_rule(X<<E, X)		:- E == 0.
   78arith_rule(E//_, 0)		:- E == 0.
   79arith_rule(E*X, X)		:- E == 1.
   80arith_rule(X*E, X)		:- E == 1.
   81arith_rule(_^E, 1)		:- E == 0.
   82arith_rule(A^E, A)		:- E == 1.
   83arith_rule(E^_, 1)		:- E == 1.
   84arith_rule(A+B, B+A)	:- integer(A).
   85arith_rule(A*B, B*A)	:- integer(A).
   86arith_rule(A+B, B+A)	:- nonvar(A, A0*H), nonvar(B, B0*K),
   87	integer(H), integer(K),
   88	A0 @< B0.
   89arith_rule(A+B, A0*D)	:- nonvar(A, A0*H), nonvar(B, B0*K),
   90					A0 == B0,
   91					D is H+K.
   92arith_rule(A+B, B+A)	:- arith_mono_compare(<, A, B).
   93arith_rule(A+B, (U+B)+V)	:- nonvar(A, U+V),
   94	arith_mono_compare(<, V, B).
   95
   96%
   97arith_mono_compare(=, A, B):-integer(A), integer(B).
   98arith_mono_compare(<, A, _):-integer(A).
   99arith_mono_compare(>, _, B):-integer(B).
  100arith_mono_compare(C, A, B):- nonvar(A, A0*I), nonvar(B, B0*K),
  101	integer(I),
  102	integer(K),
  103	compare(C, B0, A0).
  104arith_mono_compare(C, A, B):- nonvar(A, A0*I),
  105	integer(I),
  106	B0 = B,
  107	compare(C, B0, A0).
  108arith_mono_compare(C, A, B):- nonvar(B, B0*I),
  109	integer(I),
  110	A0 = A,
  111	compare(C, B0, A0).
  112arith_mono_compare(C, A, B):- compare(C, A, B)