. TREE REWRITING
Prop's tree rewriting mechanism let us transform a tree in algebraic datatype form into another tree according to a set of rewriting rules. Unlike plain pattern matching described in section 4.3, which only apply to the root of a tree, rewriting rules are applicable to all parts of the tree. This allows the user to concentrate on developing the set of transformations; the actual traversal of the tree object is handled implicitly by Prop. When used properly, this mechanism has an advantage over plain pattern matching since rewriting rules remain valid even when a new variant to a datatype is introduced.
In Prop, a rewriting system is developed in a similar manner as a parser. The first phase requires the user to defines a rewrite class to encapsulate the rewriting rules.
Frequently, the rewriting mechanism is used to collect information about a tree structure; furthermore, more transformation rules are conditional: i.e. we want them to be applicable only if certain conditions are satisfied. We can accomplish both of these tasks by defining data members and methods in the rewriting class. These are accessible during the rewriting process. Information collected during rewriting can be stored within the data members.
In the rewriting formalism, equational
rules of the form lhs -> rhs are specified by the user.
During processing, each instance of the lhs in a complex tree is replaced
by an instance of the rhs, until no such replacement is possible.
Equational rules can often be used to specify semantics based simplification
(e.g. constant folding and simplification based on simple algebraic
identities) or transformation(e.g. code selection in a compiler
backend[AGT89]).
Unlike plain pattern matching, however, the structural traversal process in rewriting is implicitly inferred from the type structure of an algebraic datatype, as specified in its definition.
There are two main forms of rewriting modes available:
Each independent set of rewriting rules in Prop is encapsulated in its own rewrite class. A rewrite class is basically a normal C++ class with a set of rewriting rules attached. During rewriting, the data members and the member functions are visible according to the normal C++ scoping rules. This makes it is easy to encapsulate additional data computed as a side effect during the rewriting process.