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
menus
  menu: "Manual" (openeditor) (source)
    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.