A rewriting example

Consider an abbreviated simplifier for the well-formed formula datatype Wff defined in the section 4.1.2. The rewrite class for this can be defined as follows. Since there is no encapsulated data in this example, only the default constructor for the class needs to be defined. A rewrite class definition requires the traversal list to be specified. This is simply a list of datatypes involved in the rewriting traversal process. In this instance only Wff is needed.

   rewrite class Simplify (Wff)
   {
   public:
      Simplify() {}
   };

The rewrite rules for the simplifier can then be specified succinctly as follows. Like the match statement, in general the rhs of a rewrite rule can be any statement. A special statement rewrite(e) can be used to rewrite the current redex into another form. If the rhs is of the form rewrite(e), then it can be abbreviated to e, as in below:

   rewrite Simplify
   {  And(F,  _):      F
   |  And(_,  F):      F
   |  And(T,  ?X):     ?X
   |  And(?X, T):      ?X
   |  Or (T,  _):      T
   |  Or (_,  T):      T
   |  Or (F,  ?X):     ?X
   |  Or (?X, F):      ?X
   |  Not(Not(?X)):    ?X
   |  Not(And(?X,?Y)): Or(Not(?X), Not(?Y))
   |  Not(Or(?X,?Y)):  And(Not(?X), Not(?Y))
   |  Implies(?X,?Y):  Or(Not(?X), ?Y)
   |  And (?X, ?X):     ?X
   |  Or (?X, ?X):      ?X
   // etc ...
   };

The rewrite class definition creates a new class of the same name. This new class defines an implicit operator () with the protocol below. This member function can be invoked to perform the rewriting in a functional syntax.

   class Simplify : ... {
   {  ...
   public:
      void operator () (Wff);
      // Wff operator () (Wff); // if rewrite class is applicative
   };

   Wff wff = ...;
   Simplify simplify; // create a new instance of the rewrite class
   simplify(wff);    // rewrite the term wff

 
• Conditional rewriting and actions