/* REWRIT.

Simple depth first search rewrite rule system
see Artificial Mathematicians p 104.
Use with UTIL

Alan Bundy  10.7.81 */


/* Find Normal Form of Expression */

normalize(Expression, NormalForm) :-    % To put an expression in normal form:
        rewrite(Expression, Rewriting),         % Rewrite it once
        normalize(Rewriting, NormalForm).       % and recurse

normalize(Expression, Expression) :-    % The expression is in normal form
        not rewrite(Expression, _).     % if it cannot be rewritten


/* Rewrite Rule of Inference */

rewrite(Expression, Rewriting) :-       % To rewrite Expression
        rule(Name,LHS, RHS),            % get a rule LHS => RHS
        replace(LHS, RHS, Expression, Rewriting),       % replace LHS by RHS
        writef('%t rewritten to %t by rule %t\n', [Expression,Rewriting,Name]).


/* Replace single occurrence of T by S in Old to get New */

replace(T,S,T,S).               % replace this occurence

replace(T,S,Old,New) :-         % replace one of the arguments
        Old =.. [Sym | OldArgs],        % get the arguments
        some(replace(T,S),OldArgs,NewArgs),     % replace one
        New =.. [Sym | NewArgs].        % put it all together again

/* Apply Pred to just one element of list */

some(Pred, [Hd1 | Tl], [Hd2 | Tl]) :-
        apply(Pred, [Hd1,Hd2]).         % apply it to this one

some(Pred, [Hd | Tl1], [Hd | Tl2]) :-
        some( Pred, Tl1, Tl2).          % or one of the others


/* Some rules */

rule(1,X*0, 0).         % Algebraic Simplification rules
rule(2,1*X, X).
rule(3,X^0, 1).
rule(4,X+0, X).


/* A Typical Problem */

go :- normalize( (a^(2*0))*5 + b*0, NormalForm),
        writef('Normal Form is %t\n\n', [NormalForm]),
        fail.


/* MINI-PROJECTS

1. Try out the system with the arithmetic rules given above.

2.  Experiment with some rules of your own devising (Suggestions can be
found in chapter 9 and section 5.2 of 'Artificial Mathematicians').

3.  Modify the system so that it works by:  (a) call by value, (b) call
by name (See p107 of 'Artificial Mathematicians').

*/