**Table of Contents**

In Part II we saw how terms provide a
structured representation for programs derived from a formal
definition of the syntax of a programming language.
Transforming programs then requires tranformation of terms.
In this chapter we show how to implement term transformations using
*term rewriting* in Stratego. In term rewriting
a term is transformed by repeated application of *rewrite
rules*.

To see how this works we take as example the language of propositional formulae, also known as Boolean expressions:

module prop signature sorts Prop constructors False : Prop True : Prop Atom : String -> Prop Not : Prop -> Prop And : Prop * Prop -> Prop Or : Prop * Prop -> Prop Impl : Prop * Prop -> Prop Eq : Prop * Prop -> Prop

Given this signature we can write terms such as
`And(Impl(True,False),False)`

, and
`And(Atom("p"),False))`

. Atoms are also known as
proposition letters; they are the variables in propositional
formulae. That is, the truth value of an atom should be provided in
order to fully evaluate an expression. Here we will evaluate
expressions as far as possible, a transformation also known as
*constant folding*. We will do this using
*rewrite rules* that define how to simplify a
single operator application.

A *term pattern* is a term with *meta
variables*, which are identifiers that are not declared
as (nullary) constructors. For example, `And(x, True)`

is a term pattern with variable `x`

. Variables in term
patterns are sometimes called *meta* variables,
to distinguish them from variables in the source language being
processed. For example, while atoms in the proposition expressions
are variables from the point of view of the language, they are not
variables from the perspective of a Stratego program.

A term pattern `p`

*matches* with a
term `t`

, if there is a
*substitution* that replaces the variables in
`p`

such that it becomes equal to `t`

. For
example, the pattern `And(x, True)`

matches the term
`And(Impl(True,Atom("p")),True)`

because replacing the
variable `x`

in the pattern by
`Impl(True,Atom("p"))`

makes the pattern equal to the
term. Note that `And(Atom("x"),True)`

does
*not* match the term
`And(Impl(True,Atom("p")),True)`

, since the subterms
`Atom("x")`

and `Impl(True,Atom("p"))`

do not
match.

An *unconditional rewrite rule* has the form
`L : p1 -> p2`

, where `L`

is the name of the
rule, `p1`

is the left-hand side and `p2`

the
right-hand side term pattern.
A rewrite rule `L : p1 -> p2`

applies to a term
`t`

when the pattern `p1`

matches
`t`

. The result is the instantiation of `p2`

with the variable bindings found during matching.
For example, the rewrite rule

E : Eq(x, False) -> Not(x)

rewrites the term `Eq(Atom("q"),False)`

to
`Not(Atom("q"))`

, since the variable `x`

is
bound to the subterm `Atom("q")`

.

Now we can create similar evaluation rules for all constructors of
sort `Prop`

:

module prop-eval-rules imports prop rules E : Not(True) -> False E : Not(False) -> True E : And(True, x) -> x E : And(x, True) -> x E : And(False, x) -> False E : And(x, False) -> False E : Or(True, x) -> True E : Or(x, True) -> True E : Or(False, x) -> x E : Or(x, False) -> x E : Impl(True, x) -> x E : Impl(x, True) -> True E : Impl(False, x) -> True E : Eq(False, x) -> Not(x) E : Eq(x, False) -> Not(x) E : Eq(True, x) -> x E : Eq(x, True) -> x

Note that all rules have the same name, which is allowed in Stratego.

Next we want to *normalize* terms with respect to
a collection of rewrite rules. This entails applying all rules to
all subterms until no more rules can be applied.
The following module defines a rewrite system based on the rules for
propositions above:

module prop-eval imports libstrategolib prop-eval-rules strategies main = io-wrap(eval) eval = innermost(E)

The module imports the Stratego Library
(`libstrategolib`

) and the module with the evaluation
rules, and then defines the `main`

strategy to apply
`innermost(E)`

to the input term. (See the discussion of
`io-wrap`

in Section 11.2.)
The `innermost`

strategy from the library exhaustively
applies its argument transformation to the term it is applied to,
starting with `inner' subterms.

We can now compile the program as discussed in Chapter 11:

`$`

strc -i prop-eval.str -la stratego-lib

This results in an executable `prop-eval`

that can be
used to evaluate Boolean expressions. For example, here are some
applications of the program:

`$`

cat test1.prop And(Impl(True,And(False,True)),True)`$`

./prop-eval -i test1.prop False`$`

cat test2.prop And(Impl(True,And(Atom("p"),Atom("q"))),ATom("p"))`$`

./prop-eval -i test2.prop And(And(Atom("p"),Atom("q")),ATom("p"))

We can also import these definitions in the Stratego Shell, as illustrated by the following session:

`$`

stratego-shell`stratego>`

import prop-eval`stratego>`

!And(Impl(True(),And(False(),True())),True()) And(Impl(True,And(False,True)),True)`stratego>`

eval False`stratego>`

!And(Impl(True(),And(Atom("p"),Atom("q"))),ATom("p")) And(Impl(True,And(Atom("p"),Atom("q"))),ATom("p"))`stratego>`

eval And(And(Atom("p"),Atom("q")),ATom("p"))`stratego>`

:quit And(And(Atom("p"),Atom("q")),ATom("p"))`$`

The first command imports the `prop-eval`

module, which
recursively loads the evaluation rules and the library, thus making
its definitions available in the shell. The `!`

commands
replace the current term with a new term. (This
*build* strategy will be properly introduced in
Chapter 16.)

The next commands apply the `eval`

strategy to various
terms.

Next we extend the rewrite rules above to rewrite a Boolean expression to disjunctive normal form. A Boolean expression is in disjunctive normal form if it conforms to the following signature:

signature sorts Or And NAtom Atom constructors Or : Or * Or -> Or : And -> Or And : And * And -> And : NAtom -> And Not : Atom -> NAtom : Atom -> NAtom Atom : String -> Atom

We use this signature only to describe what a disjunctive normal
form is, not in an the actual Stratego program. This is not
necessary, since terms conforming to the DNF signature are also
`Prop`

terms as defined before.
For example, the disjunctive normal form of

And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),ATom("p"))

is

Or(And(Not(Atom("r")),ATom("p")), And(And(Atom("p"),Atom("q")),ATom("p")))

Module `prop-dnf-rules`

extends the rules defined in
`prop-eval-rules`

with rules to achieve disjunctive
normal forms:

module prop-dnf-rules imports prop-eval-rules rules E : Impl(x, y) -> Or(Not(x), y) E : Eq(x, y) -> And(Impl(x, y), Impl(y, x)) E : Not(Not(x)) -> x E : Not(And(x, y)) -> Or(Not(x), Not(y)) E : Not(Or(x, y)) -> And(Not(x), Not(y)) E : And(Or(x, y), z) -> Or(And(x, z), And(y, z)) E : And(z, Or(x, y)) -> Or(And(z, x), And(z, y))

The first two rules rewrite implication (`Impl`

) and
equivalence (`Eq`

) to combinations of `And`

,
`Or`

, and `Not`

.
The third rule removes double negation.
The fifth and sixth rules implement the well known DeMorgan laws.
The last two rules define distribution of conjunction over
disjunction.

We turn this set of rewrite rules into a compilable Stratego program in the same way as before:

module prop-dnf imports libstrategolib prop-dnf-rules strategies main = io-wrap(dnf) dnf = innermost(E)

compile it in the usual way

`$`

strc -i prop-dnf.str -la stratego-lib

so that we can use it to transform terms:

`$`

cat test3.prop And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),ATom("p"))`$`

./prop-dnf -i test3.prop Or(And(Not(Atom("r")),ATom("p")),And(And(Atom("p"),Atom("q")),ATom("p")))

We have seen how to define simple transformations on terms using
unconditional term rewrite rules. Using the `innermost`

strategy, rules are applied exhaustively to all subterms of the
subject term.
The implementation of a rewrite system in Stratego has the following
form:

module mod imports libstrategolib signature sorts A B C constructors Foo : A * B -> C rules R : p1 -> p2 R : p3 -> p4 strategies main = io-wrap(rewr) rewr = innermost(R)

The ingredients of such a program can be divided over several modules. Thus, a set of rules can be used in multiple rewrite systems.

Compiling the module by means of the command

`$`

strc -i mod.str -la stratego-lib

produces an executable `mod`

that can be used to
transform terms.