# 4. Term Rewriting¶

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.

## 4.1. Transformation with 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 : Impl(x, False()) -> Not(x)
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. The `innermost` strategy from the library exhaustively applies its argument transformation to the term it is applied to, starting with inner subterms.

As an aside, we have now seen Stratego modules with `rules` and `strategies` sections. It’s worth noting that a module can have any number of sections of either type, and that there is no actual semantic difference between the two section headings. In fact, either rewrite rules and/or strategy definitions can occur in either kind of section. Nevertheless, it often helps with making your transformations clearer to generally segregate rules and strategy definitions, and so both headings are allowed so you can punctuate your Stratego modules with them to improve readability.

In any case, we can now compile the above program:

```\$ 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 8.)

The next commands apply the `eval` strategy to various terms.

## 4.2. Running `prop-eval` in Spoofax/Eclipse¶

If you’d like to try out some of these Stratego examples in Spoofax/Eclipse, the first step is to define a concrete syntax for Boolean expressions that will parse to the sorts of ATerms that we have been working with. The SDF3 Manual provides the best introduction to how one might go about doing that, but here is the bulk of an SDF3 syntax definition that will allow us to represent any of the ATerms above:

```context-free syntax

Prop.True  = <1>
Prop.False = <0>
Prop.Atom  = String
Prop.Not   = <!<Prop>>
Prop.And   = <<Prop> & <Prop>>  {left}
Prop.Or    = <<Prop> | <Prop>>  {left}
Prop.Impl  = [[Prop] -> [Prop]] {right}
Prop.Eq    = <<Prop> = <Prop>>  {non-assoc}
Prop       = <(<Prop>)> {bracket}

String = ID

context-free priorities

Prop.Not
> Prop.And
> Prop.Or
> Prop.Impl
> Prop.Eq
```

With this grammar in place, the first two examples at the beginning of this chapter (just below the `prop` signature) can be expressed by `(1 -> 0) & 0` and `p & 0`, respectively. So you can see that the concrete syntax will actually make it much easier to construct the example expressions used throughout this manual.

If you’d like to see this in action in Spoofax/Eclipse, you can set up a language with the above grammar. Or you can clone the publicly-available repository containing most of the `prop` language examples from this manual.

Either way, you can place either of the above expressions in a file (`syntax/examples/sec4.1_A.spl` or …`_B.spl` in the repository) and visit it in Eclipse. Then if you select “Syntax > Show parsed AST” from the Spoofax menu, the parsed AST matching our first expressions above will pop up in the editor.

### 4.2.1 Using Editor Services to run a Stratego transformation¶

Naturally, we’d now like to run `prop-eval` in Spoofax/Eclipse. So we can take the `prop-eval-rules` module above and save it as `trans/prop-eval-rules.str`, with just one small change. Instead of `import prop` in the second line, we can say `import signatures/-`, since Spoofax has written out the signature implied by the grammar for us.

We’re also going to have a small module `trans/prop-eval.str` to call the `prop-eval-rules`. It starts out rather similarly to the `prop-eval` for Stratego/XT; here’s the first four lines:

```module prop-eval
imports libstrategolib prop-eval-rules
strategies
eval = innermost(E)
```

Note that we don’t have the `main = io-wrap(eval)` line. For Stratego/XT, that was the sort of “glue” we needed to connect the execution environment with the basic `eval` strategy we’ve defined in Stratego. Similarly, a “glue” expression is needed in Spoofax/Eclipse as well. Because the Eclipse environment is more flexible, the necessary glue is rather more complicated; for now we needn’t worry much about its details:

```// Interface eval strategy with editor services and file system
do-eval: (selected, _, _, path, project-path) -> (filename, result)
with filename := <guarantee-extension(|"eval.aterm")> path
; result   := <eval> selected
```

How do we now invoke this interface? That’s where the Spoofax Editor Services (ESV) comes in. ESV is responsible, among other things, for the “Spoofax” menu item on the top bar of Eclipse. And you can add a new submenu, which we’ll call “Manual”, to that menu with a little module `editor/Manual.esv` like this:

```module Manual
action: "prop-eval" = do-eval
```

Finally, we have to get Spoofax to see our new Stratego and ESV modules. We do this by importing them in the main Stratego and ESV files of the project. In the repository these are in `trans/spoofax_propositional_language.str` and `editor/Main.esv`, respectively. Their beginnings end up looking like:

```module spoofax_propositional_language

imports

completion/completion
pp
outline
analysis
prop-eval
rules // Debugging
```

and

```module Main
imports
Syntax
Analysis
Manual
language
```

Now at last we’re ready to invoke the `eval` transformation. Make sure you have your project rebuilt cleanly. Visit a `.spl` file that has the expression you’d like to evaluate, such as `syntax/examples/sec4.1_test1.spl` containing `(1 -> 0 & 1) & 1`. Then select “Spoofax > Manual > prop-eval” from the menu bar to see the value (in this case `False()`. (There’s also a …`_test2.spl` with `(1 -> p & q) & p` for the other example, and you can create your own files for some of the expressions in the Stratego Shell session shown above, if you like.)

## 4.3. Adding Rules to a Rewrite System¶

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")))
```

## 4.4. Using Spoofax Testing Language to run a Stratego Transformation¶

We can of course run `prop-dnf` in Spoofax/Eclipse in the same way as before. The `prop-dnf-rules` module is saved verbatim in `trans/prop-dnf-rules.str`, and the `prop-dnf` module becomes the following `trans/prop-dnf.str`:

```module prop-dnf
imports libstrategolib prop-dnf-rules
strategies
dnf = innermost(E)

// Interface dnf strategy with editor services and file system
do-dnf: (selected, _, _, path, project-path) -> (filename, result)
with filename := <guarantee-extension(|"dnf.aterm")> path
; result   := <dnf> selected
```

If you add a “prop-dnf” action to `editor/Manual.esv` calling `do-dnf` and rebuild the project, then you can visit, say, `syntax/examples.sec4.2_test3.spl` containing `(r -> p & q) & p` to produce exactly the DNF shown above.

However, we also want use this example to show another method of running Stratego strategies from the Eclipse IDE.

The Spoofax Testing Language (SPT) is a declarative language that provides for a full range of tests for a Spoofax language project. As such, it includes the ability to run an arbitrary Stratego strategy on the results of parsing an arbitrary piece of the language you’re working with.

So, we can just take our test3 expression above and make it a part of an SPT test suite, which we will call `test/manual-suite.spt`:

```module manual-suite
language Spoofax-Propositional-Language

test sec4_2_test3 [[
(r -> p & q) & p
]] run dnf
```

Once we have saved this file, the tests run automatically. What does this mean? The file seems to be just “sitting there;” there’s no indication that anything is happening. That’s because this test we’ve just written succeeds. All we asked is that Spoofax run the dnf transformation on the results of parsing the test expression. It did that, and the transformation succeeded. So all is well, and no output is generated.

But of course, we want to check the result of the transformation as well. Fortunately, we know what we expect it to be. So we can change the test like so:

```test sec4_2_test3_ex [[
(r -> p & q) & p
]] run dnf to Or(And(Not(Atom("r")),Atom("p")),
And(And(Atom("p"),Atom("q")),Atom("p")))
```

Now if there is no error or warning on this test then you know the `dnf` strategy produced the result shown in the `to` clause, and otherwise, the actual result will be shown in the error popup.

What if you don’t know what the expression is going to produce? Then you can just put a dummy expression like `Atom("x")` in the `to` clause, and you will be sure to get an error. The error popup will show the actual transformation results. But beware! The results will be hard to read because of the annotations that Spoofax adds to track where in the source code each part of the AST originates. (For example, in the example above we get

```Got: Or(And(Not(Atom("r"{TermIndex("test/manual-suite.spt",1)}){TermIndex
("test/manual-suite.spt",2)}),Atom("p"{TermIndex("test/manual-suite.spt",9)})
{TermIndex("test/manual-suite.spt",10)}),And(And(Atom("p"{TermIndex("test/manual-
suite.spt",3)}){TermIndex("test/manual-suite.spt",4)},Atom("q"{TermIndex
("test/manual-suite.spt",5)}){TermIndex("test/manual-suite.spt",6)}){TermIndex
("test/manual-suite.spt",7)},Atom("p"{TermIndex("test/manual-suite.spt",9)})
{TermIndex("test/manual-suite.spt",10)}))
```

Nevertheless, with the editor outliner you can puzzle out what your transformation has done. The fact remains that it is most practical to put the actual expected result of the transformation in the `to` clause.