Imagine finding yourself in a situation where you have a collection of files containing source code. If this is an unreasonable prospect for you, stop reading and pick another tutorial. If you are still with us, consider these files the blueprints for your software. They are still not the award-winning, executable program you are aiming for, but by applying a compiler to them, you can generate one (with some minor provisions about syntactial and semantical correctness). If so inclined, you may also run a documentation generator like Javadoc on the source, to generate structured documentation. Or, while colleagues are not looking, you can secretly invoke tools like lint (C/C++) or FindBugs (Java) to weed out common programming errors.

The compilation, documentation generation and source-code analysis are all examples of software transformations , but they are certainly not the only ones. Software transformation has been used by the mathematically inclined for generating programs from high-level specifications, by forgetful people to recover lost design and architecture from legacy code and by reverse-engineers to obtain high-level, readable code from binary files after somebody accidentally misplaced a stack of backup tapes. Specialization of a program to known inputs in order to improve performance, optimization using domain knowledge from the application domain and improving program understanding by analysing sources are also favoured topics among software transformers.

But who uses software transformation, anyway? People with a problem resembling any in Figure 1.1 are. Compilation, the translation of a program to machine code in order to make it executable, is the standard processing technique applied to get running programs out of source code. But much more can be done. There are many other kinds of processes that can be applied to programs. For example, programs can be synthesized from high-level specifications; programs can be optimized using knowledge of the application domain; documentation for understanding a program can be automatically derived from its sources; programs can be specialized to known inputs; application programs can be generated from domain-specific languages; low-level programs can be reverse engineered into high-level programs.

All too often, Real Programmers facing such problems are of the opinion that software transformation is overly complicated dark magic, and that simple regular expression hacks solve the problem just fine. Almost equally often, their ad-hoc, text-based solutions turn out to be brittle, overly complicated and acquire a status of dark magic, with the result that no other team member dears touch the stuff. Most of the time, the problem would be easily solved in a maintainable and robust way if only the right tool could be found.

So what do should you do if you have a mountain of source code that you have to do some transformation on? Obviously, using the the right tool for the job is a good start. We don't recommend using toothpicks to move software mountains. Instead, we think using Stratego for this is a good idea. In this tutorial, we will use small, understandable and cute examples that you can try out in the leisure of your own desktop. We hope these will convince you exactly how good an idea using Stratego for software transformation really is.

Stratego/XT is a framework for implementing software transformation systems. A software transformation system is usually organized as a simple pipeline of transformation steps, see Figure 1.2. At the source of the pipeline (far left), a parser reads the text of the input program and turns it into a parse tree or abstract syntax tree. Subsequently, one or several transformations components modify the tree. At the sink of the pipeline (far right), a pretty-printer turns the output tree into program text. The output program need not be in the same language as the input program. It need not even be a programming language. This allows us to create important tools such as compilers and documentation generators using Stratego/XT.

Figure 1.2.  Pipeline of a software transformation system.

The Stratego/XT framework consists of two parts: Stratego, a language for implementing software transformations, and XT, a collection of transformation tools. The Stratego language is a powerful language for implementing the core transformations of a complete transformation system. The XT tools help with the implementation of the infrastructure required around these core transformations, such as a parser and a pretty-printer.

Stratego and XT aim at better productivity in the development of transformation systems through the use of a high-level representations of programs, domain-specific languages for the development of parts of a transformation system, and generating various aspects of a transformation system automatically.

Exactly what all this means will become clear to you as we move along in this tutorial.

This tutorial is divided into three parts. The first part introduces the XT architecture and many of the tools from the XT collection. An important point in this part that is how to construct parsers using the syntax definition formalism SDF. The parser takes source code text into structured ATerms. Another point in this part is the reverse action: going from ATerms back to source code text.

The second part of the tutorial introduces the Stratego language, starting with the concept of terms and moving on to rules and strategies. After explaining how rules and strategies may be combined to create complete transformation programs, the more advanced topics of concrete syntax and dynamic rules are covered.

The third and final part of the tutorial explains the most important strategies found in the Stratego library: basic data types such as lists, strings, hashtables and sets; basic I/O functionality; the SUnit framework for unit testing. This part also explains the technical details of how to put together complete software transformation systems from XT components using the Stratego build system, using the XTC component composition model.

The Stratego/XT project distributes several packages. So let's first make clear what you actually need to install. Stratego/XT itself is a language independent toolset for constructing program transformation systems. Language-specific extensions of Stratego/XT are distributed as separate packages, so that you only have to install what you really need for your particular application.

Stratego/XT.  All Stratego/XT users need to install the ATerm Library (aterm), the SDF2 Bundle (sdf2-bundle) and Stratego/XT (strategoxt). These packages enable you to compile Stratego programs, and provide the basic infrastructure for parsing and pretty-printing source files.

Stratego Shell.  Optionally, you can install the Stratego Shell, which provides an interpreter for Stratego and an interactive command-line for experimenting with the Stratego language. The Stratego Shell is used in the Stratego part of this tutorial to demonstrate the features of the Stratego language. The Stratego Shell is also very useful for small experiments with strategies of the Stratego Library.

Extensions.  Then there are the language-specific packages. These packages provide the basic infrastructure for parsing, pretty-printing, and in some cases also analyzing source files of a specific programming language. Reusing such a package enables you to get started immediately with the implementation of an actual transformation. Examples of such packages are Java-front, Dryad, Transformers C and C++, BibTeX Tools, Prolog Tools, AspectJ Front, and SQL Front. Also, there are some demonstration packages, for example Tiger Base, which implements a compiler for the Tiger language, and Java Borg, which demonstrates the implementation of language embeddings. All these packages can separately be installed as extensions of Stratego/XT.

Examples of the Stratego/XT Manual.  All the code examples in this manual are available for separate download, so that you can experiment based on these: examples.tar.gz

First of all, you have to decide which deployment mechanism you want to use. For users of RPM-based Linux distributions (such as Redhat, Fedora Core, and SUSE), we advise to use RPMs, which are available from the release page. For Cygwin users we provide pre-compiled binaries that can simply be unpacked. For Mac OS X users, we provide these binary packages as well, but they can also use the Nix deployment system, which will guarantee that all dependencies are installed correctly. Nix packages are also available for Linux users. Finally, it is always possible to build from source.

Next, download the required packages. Stratego/XT depends on the ATerm Library and the SDF2 Bundle, so you have to download aterm, sdf2-bundle, and strategoxt. The downloads are all available at the release page of Stratego/XT.

$ tar zxf aterm-version.tar.gz
$ cd aterm-version
$ ./configure
$ make
$ make install
$ cd ..

$ tar zxf sdf2-bundle-version.tar.gz
$ cd sdf2-bundle-version
$ ./configure
$ make
$ make install
$ cd ..

$ ./configure --prefix=/opt/aterm
$ ./configure --prefix=/opt/sdf2-bundle --with-aterm=/opt/aterm

$ ./configure --prefix=/opt/sdf2-bundle --with-aterm=/opt/aterm

$ export PKG_CONFIG_PATH=/opt/aterm/lib/pkgconfig:/opt/sdf2-bundle/lib/pkgconfig

$ tar zxf strategoxt-version.tar.gz
$ cd strategoxt-version
$ ./configure
$ make
$ make install

$ ./configure --prefix=/opt/strategoxt \
  --with-aterm=/opt/aterm --with-sdf=/opt/sdf2-bundle

$ tar zxf package-version.tar.gz
$ cd package-version
$ ./configure
$ make
$ make install

XT is a collection of components for implementing transformation systems. Some of these components generate code that can be included in a transformation system, such as a parser or pretty-printer. Other components can be used immediately, since they are generic tools. The components of XT are all executable tools: they can be used directly from the command-line.

According to the Unix philosophy, the tools that are part of XT all do just one thing (i.e. implement one aspect of a transformation system) and can be composed into a pipeline to combine them in any way you want. A sketch of a typical pipeline is shown in Figure 3.1. First, a parser is applied to a source program. This results in an abstract syntax tree, which is then transformed by a sequence of transformation tools. Finally, the tree is pretty-printed back to a source program. So, this pipeline is a source to source transformation system. The tools that are part of the pipeline exchange structured representations of a program, in the form of an abstract syntax tree. These structured representations can be read in any programming language you want, so the various components of a transformation system can be implemented in different programming languages. Usually, the real transformation components will be implemented in Stratego.

Figure 3.1.  Pipeline of a software transformation system.

Of course, some compositions are very common. For example, you definitly don't want to enter the complete pipeline of a compiler again and again. So, you want to pre-define such a composition to make it reusable as single tool. For this, you could of create a shell script, but option handling in shell scripts is quite tiresome and you cannot easily add composition specific glue code. To solve this, Stratego itself has a concise library for creating compositions of transformation tools, called XTC. We will come back to that later in Chapter 28.

The nice thing about this approach is that all the tools can be reused in different transformation systems. A parser, pretty-printer, desugarer, optimizer, simplifier, and so an is automatically available to other transformation systems that operate on the same language. Even if a tool will typically be used in a single dominant composition (e.g. a compiler), having the tool available to different transformation systems is very useful. In other words: an XT transformation system is open and its components are reusable.

Programmers write programs as texts using text editors. Some programming environments provide more graphical (visual) interfaces for programmers to specify certain domain-specific ingredients (e.g., user interface components). But ultimately, such environments have a textual interface for specifying the details. So, a program transformation system needs to deal with programs that are in text format.

However, for all but the most trivial transformations, a structured, rather than a textual, representation is needed. Working directly on the textual representation does not give the transformation enough information about what the text actually means. To bridge the gap between the textual and the structured representation, parsers and unparsers are needed. Also, we need to know how this structured representation is actually structured.

The syntactical rules of a programming language are usually expressed in a context-free grammar. This grammar (or syntax definition) of a programming language plays a central role in Stratego/XT. Most of the XT tools work on a grammar in one way or another. The grammar is a rich source of information. For example, it can be used to generate a parser, pretty-printer, disambiguator, tree grammar, format-checker, and documentation. This central role of a grammar is the most crucial aspect of XT, which is illustrated in Figure 3.2: all the components of a transformation system are directly or indirectly based on the grammar of a programming language.

What makes this all possible is the way syntax is defined in Stratego/XT. Stratego/XT uses the SDF language for syntax definition, which is a very high-level and declarative language for this purpose. SDF does not require the programmer to encode all kinds of properties of a programming language (such as associativity and priorities) in a grammar. Instead, SDF has declarative, concise, ways of defining these properties in such a way that they can actually be understood by tools that take the grammar as an input. And, of course, creating a grammar in such language is much more fun!

Figure 3.2.  Syntax definitions play a central role in a transformation system.

As mentioned before, the XT tools exchange a structured representation of a program: an abstract syntax tree. The structure of this abstract syntax tree is called the abstract syntax, as opposed to the ordinary textual syntax, which is called the concrete syntax. In XT, the abstract syntax is directly related to the syntax definition and can be generated from it. The result is a tree grammar that defines the format of the trees that are exchanged between the transformation tools. From the world of XML, you are probably already familiar with tree grammars: DTD, W3C XML Schema and RELAX NG are tree grammars in disguise.

Until now, we have been a bit vague about the format in which abstract syntax trees are actually exchanged between transformation tools. What is this structured program representation?

We can easily imagine an abstract syntax tree as a graphical structure. For example, the tree at the right is a simple abstract syntax tree for the expression (a + n) * 1. This representation corresponds closely to the representation of trees in computer memory. However, drawing pictures is not a very effective way of specifying tree transformations. We need a concise, textual, way to express an abstract syntax tree. Fortunately, there is a one-to-one correspondence between trees and so-called first-order prefix terms (terms, for short). A term is a constructor, i.e., an identifier, applied to zero or more terms. Strings and integer constants are terms as well. Thus, the following term corresponds to the abstract syntax tree that we have just drawn.

Times(Plus(Var("a"), Var("n")), Int("1"))

In Stratego/XT, programs are exchanged between transformation tools as terms. The exact format we use for terms, is the Annotated Term Format, or ATerms for short. We will discuss this format in more detail later, but some of its features are interesting to note here.

First, ATerms are not only used to exchange programs between tools. ATerms are also used in the Stratego language itself for the representation of programs. In other words, ATerms are used for the external representation as well as the internal representation of programs in Stratego/XT. This is very convenient, since we don't have to bind the ATerms to Stratego specific data-structures. Usually, if such a data-binding is necessary, then there is always a mismatch here and there.

Second, an important feature of the implementation is that terms are represented using maximal sharing. This means that any term in use in a program is represented only once. In other words, two occurrences of the same term will be represented by pointers to the same location. This greatly reduces the amount of memory needed for representing programs.

The ATerm format provides a set of constructs for representing trees, comparable to XML or abstract data types in functional programming languages. For example, the code 4 + f(5 * x) might be represented in a term as:

Plus(Int("4"), Call("f", [Mul(Int("5"), Var("x"))]))

ATerms are constructed from the following elements:

As a Stratego programmer you will be looking a lot at raw ATerms. Stratego pioneers would do this by opening an ATerm file in emacs and trying to get a sense of the structure by parenthesis highlighting and inserting newlines here and there. These days your life is much more pleasant through the tool pp-aterm, which adds layout to a term to make it readable. For example, parsing the following program

let function fact(n : int) : int =
      if n < 1 then 1 else (n * fact(n - 1))
 in printint(fact(10))
end

produces the following ATerm (say in file fac.trm):

Let([FunDecs([FunDec("fact",[FArg("n",Tp(Tid("int")))],Tp(Tid("int")),
If(Lt(Var("n"),Int("1")),Int("1"),Seq([Times(Var("n"),Call(Var("fact"),
[Minus(Var("n"),Int("1"))]))])))])],[Call(Var("printint"),[Call(Var(
"fact"),[Int("10")])])])

By pretty-printing the term using pp-aterm as

$ pp-aterm -i fac.trm

we get a much more readable term:

Let(
  [ FunDecs(
      [ FunDec(
          "fact"
        , [FArg("n", Tp(Tid("int")))]
        , Tp(Tid("int"))
        , If(
            Lt(Var("n"), Int("1"))
          , Int("1")
          , Seq(
              [ Times(
                  Var("n")
                , Call(
                    Var("fact")
                  , [Minus(Var("n"), Int("1"))]
                  )
                )
              ]
            )
          )
        )
      ]
    )
  ]
, [ Call(
      Var("printint")
    , [Call(Var("fact"), [Int("10")])]
    )
  ]
)

An important feature of the implementation is that terms are represented using maximal sharing. This means that any term in use in a program is represented only once. In other words, two occurrences of the same term will be represented by pointers to the same location. Figure 4.1 illustrates the difference between a pure tree representation and a tree, or more accurately, a directed acyclic graph, with maximal sharing. That is, any sub-term is represented exactly once in memory, with each occurrence pointing to the same memory location. This representation entails that term equality is a constant operation, since it consists of comparing pointers.

It should be noted that annotations create different terms, that is, two terms, one with and the other without annotations that are otherwise, modulo annotations, the same, are not equal.

Figure 4.1.  Tree and dag for the string (a + b) * c + (a + b)

Maximal sharing can make a big difference in the amount of bytes needed for representing programs. Therefore, we would like to preserve this maximal sharing when an ATerm is exchanged between two programs. When exporting a term using the textual exchange format, this compression is lost. Therefore, the ATerm Library also provides a binary exchange format that preserves maximal sharing.

Actually, there are three different formats:

The tool baffle can be used to convert an ATerm from one format to another. Baffle, and other tools that operate on ATerms, automatically detect the format of an input ATerm.

The ATerm Format is an external representation for terms that can be used to exchange structured data between programs. In order to use a term, a program needs to parse ATerms and transform them into some internal representation. To export a term after processing it, a program should transform the internal representation into the standard format. There are libraries supporting these operation for a number of languages, including C, Java, and Haskell.

The implementation of the Stratego transformation language is based on the C implementation of the library. The library provides term input and output, and an API for constructing and inspecting terms. Garbage collection is based on Boehms conservative garbage collection algorithm.

In this section, we review the basics of grammars, parse trees and abstract syntax trees. Although you might already be familiar with these basic concepts, the perspective from the Stratego/XT point of view might still be interesting to read.

Id          -> Var 
Var         -> Exp
IntConst    -> Exp
"-" Exp     -> Exp
Exp "*" Exp -> Exp
Exp "+" Exp -> Exp
Exp "-" Exp -> Exp
Exp "=" Exp -> Exp
Exp ">" Exp -> Exp
"(" Exp ")" -> Exp

   (a   + n  ) * 1 
-> (Id  + n  ) * 1
-> (Var + n  ) * 1
-> (Exp + n  ) * 1
-> (Exp + Id ) * 1
-> (Exp + Var) * 1
-> (Exp + Exp) * 1
-> (Exp      ) * 1
-> Exp         * 1
-> Exp         * IntConst
-> Exp         * Exp
-> Exp

5.1.2. Parse Trees

Recognition of a string only leads to its grammatical category, not to any other information. However, a context-free grammar not only describes a mapping from strings to sorts, but actually assigns structure to strings. A context-free grammar can be considered as a declaration of a set of trees of one level deep. For example, the following trees correspond to productions from the syntax definition in Figure 5.1:

Such one-level trees can be composed into larger trees by fusing trees such that the symbol at a leaf of one tree matches with the root symbol of another, as is illustrated in the fusion of the plus and times productions on the right. The fusion process can continue as long as the tree has non-terminal leaves. A tree composed in this fashion is a parse tree if all leaves are terminal symbols. Figure 5.2 shows a parse tree for the expression (a+n)*1, for which we showed a reduction sequence earlier in Figure 5.1. This illustrates the direct correspondence between a string and its grammatical structure. The string underlying a parse tree can be obtained by concatening the symbols at its leaves, also known as the yield.

Figure 5.2. Parse tree

Parse trees can be derived from the reduction sequence induced by the productions of a grammar. Each rewrite step is associated with a production, and thus with a tree fragment. Instead of replacing a symbol with the non-terminal symbol of the production, it is replaced with the tree fragment for the production fused with the trees representing the symbols being reduced. Thus, each node of a parse tree corresponds to a rewrite step in the reduction of its underlying string. This is illustrated by comparing the reduction sequence in Figure 5.1 with the tree in Figure 5.2

The recognition of strings described by a syntax definition, and the corresponding construction of parse trees can be done automatically by a parser, which can be generated from the productions of a syntax definition.

5.1.3. Abstract Syntax Trees

Parse trees contain all the details of a program including literals, whitespace, and comments. This is usually not necessary for performing transformations. A parse tree is reduced to an abstract syntax tree by eliminating irrelevant information such as literal symbols and layout. Furthermore, instead of using sort names as node labels, constructors encode the production from which a node is derived. For this purpose, the productions in a syntax definition are extended with constructor annotations. Figure 5.3 shows the extension of the syntax definition from Figure 5.1 with constructor annotations and the abstract syntax tree for the same good old string (a+n)*1. Note that some identifiers are used as sort names and and as constructors. This does not lead to a conflict since sort names and constructors are derived from separate name spaces. Some productions do not have a constructor annotation, which means that these productions do not create a node in the abstract syntax tree.

Figure 5.3.  Context-free productions with constructor annotations and an abstract syntax tree.

Id -> Var {cons("Var")} Var -> Exp IntConst -> Exp {cons("Int")} "-" Exp -> Exp {cons("Uminus")} Exp "*" Exp -> Exp {cons("Times")} Exp "+" Exp -> Exp {cons("Plus")} Exp "-" Exp -> Exp {cons("Minus")} Exp "=" Exp -> Exp {cons("Eq")} Exp ">" Exp -> Exp {cons("Gt")} "(" Exp ")" -> Exp

In the next section we will take a closer look at the various features of the SDF language, but before that it is useful to know your tools, so that you can immediately experiment with the various SDF features you will learn about. You don't need to fully understand the SDF fragments we use to explain the tools: we will come back to that later.

One of the nice things about SDF and the tools for it, is that the concepts that we have discussed directly translate to practice. For example, SDF supports all context-free grammars; the parser produces complete parse trees, which can even be yielded; parse trees can be converted to abstract syntax trees.

module Expression
imports
  Lexical Operators

exports
  context-free start-symbols Exp
  context-free syntax
    Id          -> Exp {cons("Var")}
    IntConst    -> Exp {cons("Int")}
    "(" Exp ")" -> Exp {bracket}

module Operators
exports
  sorts Exp
  context-free syntax
    Exp "*" Exp -> Exp {left, cons("Times")}
    Exp "/" Exp -> Exp {left, cons("Div")}
    Exp "%" Exp -> Exp {left, cons("Mod")}
  
    Exp "+" Exp -> Exp {left, cons("Plus")}
    Exp "-" Exp -> Exp {left, cons("Minus")}

  context-free priorities
    {left:
      Exp "*" Exp -> Exp
      Exp "/" Exp -> Exp
      Exp "%" Exp -> Exp
    } 
  > {left:
      Exp "+" Exp -> Exp
      Exp "-" Exp -> Exp
    }

module Lexical
exports
  sorts Id IntConst

  lexical syntax
    [\ \t\n]  -> LAYOUT
    [a-zA-Z]+ -> Id
    [0-9]+    -> IntConst

$ pack-sdf -i Expression.sdf -o Expression.def

$ sdf2table -i Expression.def -o Expression.tbl -m Expression

$ cat mul.exp
(a + n) * 1
$ sglri -p Expression.tbl -i mul.exp
Times(Plus(Var("a"),Var("n")),Int("1"))

$ echo "(a + n) * 1" | sglri -p Expression.tbl
Times(Plus(Var("a"),Var("n")),Int("1"))

$ echo "a" | sglri -p Expression.tbl
amb([Var("a"),"a"])

$ echo "a" | sglri -p Expression.tbl -s Exp 
Var("a")

$ echo "(a + n) * 1" | sglr -p Expression.tbl -2 -fi -fe | pp-aterm
parsetree( ... )

$ echo "(a + n) * 1" | sglr -p Expression.tbl -2 -fi -fe | implode-asfix
Times(Plus(Var("a"),Var("n")),Int("1"))

$ echo "(a + n) * 1" | sglr -p Expression.tbl -2 -fi -fe | asfix-yield
(a + n) * 1

In this section, we give an overview of the basic constructs of SDF. After this section, you will now the basic idea of SDF. The next sections will discuss these constructs more detail.

6.1.1. Modules

Before defining some actual syntax, we have to explain the basic structure of a module. For this, let's take a closer look at the language constructs that are used in the modules we showed earlier in Figure 5.4.

Example 6.1. Basic constructs of SDF

module Expression 
imports
  Lexical Operators 

exports  
  context-free start-symbol Exp 
  context-free syntax 
    Id          -> Exp {cons("Var")} 
    IntConst    -> Exp {cons("Int")} 
    "(" Exp ")" -> Exp {bracket}

module Operators
exports
  sorts Exp  
  context-free syntax
    Exp "*" Exp -> Exp {left, cons("Times")} 
    Exp "/" Exp -> Exp {left, cons("Div")}
    Exp "%" Exp -> Exp {left, cons("Mod")}
  
    Exp "+" Exp -> Exp {left, cons("Plus")} 
    Exp "-" Exp -> Exp {left, cons("Minus")}

  context-free priorities 
    {left:
      Exp "*" Exp -> Exp
      Exp "/" Exp -> Exp
      Exp "%" Exp -> Exp
    } 
  > {left:
      Exp "+" Exp -> Exp
      Exp "-" Exp -> Exp
    }

module Lexical
exports
  sorts Id IntConst 
  lexical syntax 
    [a-zA-Z]+ -> Id       
    [0-9]+    -> IntConst 
    [\ \t\n]  -> LAYOUT

  lexical restrictions 
    Id -/- [a-zA-Z]

Example 6.1 shows these modules, highlighting some of the constructs that are important to know before we dive into the details of defining syntax.

	Modules have a name, which can be a plain identifier, such as Expression in this example. The module must be in a file with same name and the .sdf extension. The module name can also be a path, for example java/expressions/Assignment. In this case, the module has to be in a file with name Assignment.sdf, which must be in a directory java/expressions.
	A module can optionally import a number of other modules. Multiple modules can be imported with a single import, as we have done in this example, or multiple imports can be used. This is not very common: usually, modules have just a single imports declaration. Modules are always imported by their full name. So, if the name of a module is a path, such as java/expressions/Assignment, then the module must be imported with that full name, even if it is in the directory java/expressions. If the name of the modules are long, which is typically the case if you use full paths to organize a large syntax definition in different directories, then the names are usually mentioned on separate lines, but still in a single import.
	Modules contain a number of sections, of which we now only consider the exports section. An exports section defines a number of syntactic aspects, called a grammar, that will be available to modules that import this module. This includes syntax, but also declarations of sorts, start symbols, priorities, restrictions, etc. A module can also just import other modules and not actually define any syntactical aspects itself. This is typically the case in main modules of large syntax definitions, which only import modules for names, expressions, statements, etc.

6.1.2. Start Symbols

Every syntax definition needs to define one or more start symbols, otherwise not a single input will accepted. Start symbols are the language constructs that are allowed at the top-level of a source file. For our simple expression language, the start symbol is Exp. For a java syntax definition, the start symbol could be CompilationUnit, which consists of a package, import, and type declarations.

6.1.3. Sorts

Every syntax definition introduces names for the syntactical sorts of a language, such as Exp and Id. These names can be declared in a sorts declaration. Declaring sorts is optional, but the SDF parser generator will give a warning if a sort that is used somewhere in the syntax definition is not declared. It is a good habit to declare all the sorts, since this makes it easier to find possible miss-spellings of these names. Note that in SDF syntax definitions we do not directly use the terminology of terminal and non-terminal, since actually only single characters are terminals in SDF, and almost everything else is a non-terminal. Lexical and context-free sorts are both declared as sorts.

6.1.4. Syntax

The actual syntax is defined in lexical and context-free syntax. The lexical syntax defines the syntax of language constructs like literals, comments, whitespace, and identifiers, or what is usally referred to as terminals. The context-free syntax defines the syntax of constructs like operators, statements, or what is usually referred to as non-terminals. In other parser generators the lexical syntax is often specified in a separate scanner specification, but in SDF these lexical aspects are integrated in the definition of the context-free syntax. We will come back to that later when we discuss the definition of lexical syntax.

Productions can have attributes can have attributes, specified between curly braces after the production. Some of these attributes, such as left have a special meaning for SDF itself. Other attributes can specify information about a production that target a different tool, such as bracket and cons, which target the tool that implodes parse trees to abstract syntax trees.

6.1.5. Disambiguation

SDF support constructs to define in a declarative way that certain kinds of derivations are not allowed, also known as disambiguation filters. In our example, there two examples of this: we define priorities of the arithmetic expressions, and there is a lexical restriction that specifies that an identifier can never be followed by a character that is allowed in an identifier. We will explain these mechanisms later.

Until now, we have mostly discussed the design of SDF. Now, it's about time to see how all these fancy ideas for syntax definition work out in practice. In this and the next section, we will present a series of examples that explain how typical language constructs are defined in SDF. This first section covers examples of lexical syntax constructs. The next section will be about context-free syntax.

lexical syntax
  [\ \t\r\n] -> LAYOUT

lexical syntax
  [A-Za-z][A-Za-z0-9]* -> Id

lexical syntax
  [A-Za-z][A-Za-z0-9]* -> Id
  "true"  -> Bool
  "false" -> Bool

context-free start-symbols Exp
context-free syntax
  Id   -> Exp {cons("Id")}
  Bool -> Exp {cons("Bool")}

$ echo "true" | sglri -p Test.tbl
amb([Bool("true"), Id("true")])

lexical syntax
  "true"  -> Id {reject}
  "false" -> Id {reject}

$ echo "true" | sglri -p Test.tbl
Bool("true")

lexical syntax
  Bool    -> Id {reject}
  Keyword -> Id {reject}

  "class" -> Keyword
  "if"    -> Keyword
  "while" -> Keyword

context-free syntax
  Id    -> Stm {cons("Goto")}
  Id Id -> Stm {cons("VarDec")}

$ echo "foo" | sglri -p Test.tbl
amb([Goto("foo"), VarDec("f","oo"), VarDec("fo","o")])

lexical restrictions
  Id -/- [A-Za-z0-9]

$ echo "foo" | sglri -p Test.tbl
Goto("foo")

context-free syntax
  "goto" Id -> Stm {cons("Goto")}

$ echo "gotox" | sglri -p Test.tbl
Goto("x")

lexical restrictions
  "goto" -/- [A-Za-z0-9]

lexical restrictions
  "goto" "if" -/- [A-Za-z0-9]

lexical syntax
  [0-9]+ -> IntConst

lexical restrictions
  IntConst -/- [0-9]

lexical syntax
  "0"         -> DecimalNumeral
  [1-9][0-9]* -> DecimalNumeral

  [0][xX] [0-9a-fA-F]+ -> HexaDecimalNumeral
  [0]     [0-7]+       -> OctalNumeral

lexical syntax
  [0-9]+ "." [0-9]* ExponentPart? [fFdD]? -> FloatLiteral
  [0-9]* "." [0-9]+ ExponentPart? [fFdD]? -> FloatLiteral
  [0-9]+            ExponentPart  [fFdD]? -> FloatLiteral
  [0-9]+            ExponentPart? [fFdD]  -> FloatLiteral

  [eE] SignedInteger -> ExponentPart
  [\+\-]? [0-9]+ -> SignedInteger

lexical syntax
  FloatDigits ExponentPart? [fFdD]? -> FloatLiteral 
  [0-9]* "." [0-9]* -> FloatDigits
  [0-9]+            -> FloatDigits

  [0-9]+ -> FloatLiteral {reject} 
  "."    -> FloatDigits  {reject} 

lexical syntax
  "//" ~[\n]* [\n] -> LAYOUT

  "/*" ~[\*]* "*/" -> LAYOUT

lexical syntax
  "/*" (~[\*] | "*")* "*/" -> LAYOUT

lexical restrictions
  "*" -/- [\/]

lexical syntax
  "/*" (~[\*] | Asterisk)* "*/" -> LAYOUT
  [\*] -> Asterisk

lexical restrictions
  Asterisk -/- [\/]

lexical syntax
  BlockComment -> LAYOUT

  "/*" CommentPart* "*/" -> BlockComment
  ~[\/\*]      -> CommentPart
  Asterisk     -> CommentPart
  Slash        -> CommentPart
  BlockComment -> CommentPart 
  [\/] -> Slash
  [\*] -> Asterisk

lexical restrictions
  Asterisk -/- [\/]
  Slash    -/- [\*]  

Context-free syntax in SDF is syntax where layout is allowed between the symbols of the productions. Context-free syntax can be defined in a natural way, thanks to the use of generalized-LR parsing, declarative disambiguation mechanism, and an extensive set of regular expression operators. To illustrate the definition of context-free syntax, we give examples of defining expressions and statements. Most of the time will be spend on explaining the disambiguation mechanisms.

module Expression
imports
  Lexical

exports
  context-free start-symbols Exp
  context-free syntax
    Id          -> Var 
    Var         -> Exp {cons("Var") }
    IntConst    -> Exp {cons("Int") }}
    "(" Exp ")" -> Exp {bracket }

    "-" Exp     -> Exp {cons("UnaryMinus")}
    Exp "*" Exp -> Exp {cons("Times"), left }
    Exp "/" Exp -> Exp {cons("Div"), left}
    Exp "%" Exp -> Exp {cons("Mod"), left}
    Exp "+" Exp -> Exp {cons("Plus") , left}
    Exp "-" Exp -> Exp {cons("Minus"), left}
    Exp "=" Exp -> Exp {cons("Eq"), non-assoc }
    Exp ">" Exp -> Exp {cons("Gt"), non-assoc}

  context-free priorities 
       "-" Exp -> Exp 
    > {left: 
        Exp "*" Exp -> Exp
        Exp "/" Exp -> Exp
        Exp "%" Exp -> Exp
      } 
    > {left: 
        Exp "+" Exp -> Exp
        Exp "-" Exp -> Exp
      }
    > {non-assoc: 
        Exp "=" Exp -> Exp
        Exp ">" Exp -> Exp
      }

$ echo "1" | sglri -p Test.tbl
Int("1")

$ echo "1+2" | sglri -p Test.tbl
Plus(Int("1"),Int("2"))

$ echo "x" | sglri -p Test.tbl
Var("x")

$ echo "(1 + 2) * 3" | sglri -p Test.tbl
Times(Plus(Int("1"),Int("2")),Int("3"))

  Exp "+" Exp -> Exp {cons("Plus")}
  Exp "-" Exp -> Exp {cons("Minus")}
  Exp "*" Exp -> Exp {cons("Mul")} 
  Exp "/" Exp -> Exp {cons("Div")}

$ echo "a + b * c" | sglri -p Test3.tbl  | pp-aterm
amb(
  [ Times(Plus(Var("a"), Var("b")), Var("c"))
  , Plus(Var("a"), Times(Var("b"), Var("c")))
  ]
)

  AddExp -> Exp

  MulExp -> AddExp
  AddExp "+" MulExp -> AddExp {cons("Plus")}
  AddExp "-" MulExp -> AddExp {cons("Minus")}

  PrimExp -> MulExp
  MulExp "*" PrimExp -> MulExp {cons("Mul")} 
  MulExp "/" PrimExp -> MulExp {cons("Div")}

  IntConst -> PrimExp {cons("Int")}
  Id       -> PrimExp {cons("Var")}

  ...
> Exp "&"  Exp -> Exp
> Exp "^"  Exp -> Exp
> Exp "|"  Exp -> Exp
> Exp "&&" Exp -> Exp
> Exp "||" Exp -> Exp
> ... 

context-free syntax
  "new" ArrayBaseType DimExp+ Dim*  -> ArrayCreationExp {cons("NewArray")}

  Exp "[" Exp "]" -> Exp {cons("ArrayAccess")}
  ArrayCreationExp "[" Exp "]" -> Exp {reject}

module Statements
imports Expressions 
exports
  sorts Dec FunDec
  context-free syntax
    Var ":=" Exp            	     -> Exp {cons("Assign")}
    "(" {Exp ";"}* ")" 		     -> Exp {cons("Seq")}
    "if" Exp "then" Exp "else" Exp   -> Exp {cons("If")}
    "while" Exp "do" Exp      	     -> Exp {cons("While")}
    "let" Dec* "in" {Exp ";"}* "end" -> Exp {cons("Let")}
    "var" Id ":=" Exp                -> Dec {cons("VarDec")}
    FunDec+ 			     -> Dec {cons("FunDecs")}
    "function" Id "(" {Id ","}* ")"  
      "=" Exp 	    	             -> FunDec {cons("FunDec")}
    Var "(" {Exp ","}* ")" 	     -> Exp {cons("Call")}
  context-free priorities
    {non-assoc:
     Exp "=" Exp 		     -> Exp
     Exp ">" Exp 		     -> Exp}
  >  Var ":=" Exp                    -> Exp
  > {right:
     "if" Exp "then" Exp "else" Exp  -> Exp
     "while" Exp "do" Exp      	     -> Exp}
  >  {Exp ";"}+ ";" {Exp ";"}+       -> {Exp ";"}+

context-free start-symbols Exp

function fact(n, x) =
  if n > 0 then fact(n - 1, n * x) else x

context-free restrictions
  LAYOUT? -/- [\ \t\12\n\r]

context-free restrictions
  LAYOUT?  -/- [\/].[\*]
  LAYOUT?  -/- [\/].[\/]

Parse-unit is a tool, part of Stratego/XT, for testing SDF syntax definitions. The spirit of unit testing is implemented in parse-unit by allowing you to check that small code fragments are parsed correctly with your syntax definition.

In a parse testsuite you can define tests with an input and an expected result. You can specify that a test should succeed (succeeds, for lazy people), fail (fails) or that the abstract syntax tree should have a specific format. The input can be an inline string or the contents of a file for larger tests.

module Exp
exports
  context-free start-symbols Exp
  sorts Id IntConst Exp
  
  lexical syntax
    [\ \t\n]  -> LAYOUT
    [a-zA-Z]+ -> Id
    [0-9]+    -> IntConst
  
  context-free syntax
    Id        -> Exp {cons("Var")}
    IntConst  -> Exp {cons("Int")}
  
    Exp "*"  Exp -> Exp  {left, cons("Mul")}
    Exp "/"  Exp -> Exp  {left, cons("Div")}
    Exp "%"  Exp -> Exp  {left, cons("Mod")}
  
    Exp "+"  Exp -> Exp  {left, cons("Plus")}
    Exp "-"  Exp -> Exp  {left, cons("Minus")}
  
  context-free priorities
    {left:
      Exp "*"  Exp -> Exp
      Exp "/"  Exp -> Exp
      Exp "%"  Exp -> Exp
    } 
  > {left:
      Exp "+"  Exp -> Exp
      Exp "-"  Exp -> Exp
    }

testsuite Expressions
topsort Exp

test simple int literal
  "5" -> Int("5")

test simple addition
  "2 + 3" -> Plus(Int("2"), Int("3"))

test addition is left associative
  "1 + 2 + 3" -> Plus(Plus(Int("1"), Int("2")), Int("3"))

test
  "1 + 2 + 3" succeeds

test multiplication has higher priority than addition
  "1 + 2 * 3" -> Plus(Int("1"), Mul(Int("2"), Int("3")))

test
  "x" -> Var("x")

test
  "x1" -> Var("x1")

test
  "x1" fails

test
  "1 * 2 * 3" -> Mul(Int("1"), Mul(Int("2"), Int("3")))

  $ parse-unit -i expression.testsuite -p Exp.tbl

-----------------------------------------------------------------------
executing testsuite Expressions with 9 tests
-----------------------------------------------------------------------
* OK   : test 1 (simple int literal)
* OK   : test 2 (simple addition)
* OK   : test 3 (addition is left associative)
* OK   : test 4 (1 + 2 + 3)
* OK   : test 5 (multiplication has higher priority than addition)
* OK   : test 6 (x)
sglr: error in g_0.tmp, line 1, col 2: character `1' (\x31) unexpected
* ERROR: test 7 (x1)
  - parsing failed
  - expected:  Var("x1")
sglr: error in h_0.tmp, line 1, col 2: character `1' (\x31) unexpected
* OK   : test 8 (x1)
* ERROR: test 9 (1 * 2 * 3)
  - succeeded: Mul(Mul(Int("1"),Int("2")),Int("3"))
  - expected:  Mul(Int("1"),Mul(Int("2"),Int("3")))
-----------------------------------------------------------------------
results testsuite Expressions
successes : 7
failures  : 2
-----------------------------------------------------------------------

%.runtestsuite : %.testsuite
      $(SDF_TOOLS)/bin/parse-unit -i $< -p $(PARSE_UNIT_PTABLE) --verbose 1 -o /dev/null
    

EXTRA_DIST = $(wildcard *.testsuite)

TESTSUITES = \
  expressions.testsuite \
  identifiers.testsuite

PARSE_UNIT_PTABLE = $(top_srcdir)/syn/Foo.tbl

installcheck-local: $(TESTSUITES:.testsuite=.runtestsuite)
    

Explains regular tree grammars and how to generate them. See thesis.

Typematch, API.

Explains rtg-script

Format-check analyzes whether the input ATerm conforms to the format that is specified in the RTG (Regular Tree Grammar).

8.4.2. Example

Consider the RTG generated in the example of sdf2rtg:

regular tree grammar
  start Exp
  productions
    Exp      -> Minus(Exp,Exp)
    Exp      -> Plus(Exp,Exp)
    Exp      -> Mod(Exp,Exp)
    Exp      -> Div(Exp,Exp)
    Exp      -> Mul(Exp,Exp)
    Exp      -> Int(IntConst)
    Exp      -> Var(Id)
    IntConst -> <string>
    Id       -> <string>

The ATerm

Plus(Var("a"), Var("b"))

is part of the language defined by this RTG. Therefore, format-check succeeds:

$ format-check --rtg Exp.rtg -i exp1.trm
Plus(Var("a"),Var("b"))
$ 

Note that format-check outputs the input term in this case. In this way format-check can be used in a pipeline of tools. On the other hand, the ATerm

Plus(Var("a"), Var(1))

is not part of the language defined by this RTG. Therefore, the invocation of format-check fails. Format-check also reports which term caused the failure:

$ format-check --rtg Exp.rtg -i exp2.trm
error: cannot type Var(1)
    inferred types of subterms:
    typed 1 as <int>
$

In large ATerms it might be difficult to find the incorrect subterm. To help with this, format-check supports the --vis argument. If this argument is used, then the result will pretty-printed (in the same way as pp-aterm) and the incorrect parts will be printed in red.

For example, consider this term:

Plus(Mul(Int(1), Var("a")), Minus(Var("b"), Div(1, Var("c"))))

format-check will visualize the errors in this ATerm:

The XHTML mode shows the errors in red as well. Moreover, if you move your moves over the terms, then you'll see the inferred types of the term.

$ format-check --rtg Exp.rtg -i exp3.trm --xhtml -o foo.html

You can now view the resulting file in your browser. You need a decent browser (Firefox or Mozilla. no IE).

The abstract syntax of a programming language or data format can be described by means of an algebraic signature. A signature declares for each constructor its arity m, the sorts of its arguments S1 * ... * Sm, and the sort of the resulting term S0 by means of a constructor declaration c:S1 * ... * Sm -> S0. A term can be validated against a signature by a format checker.

Signatures can be derived automatically from syntax definitions. For each production A1...An -> A0 {cons(c)} in a syntax definition, the corresponding constructor declaration is c:S1 * ... * Sm -> S0, where the Si are the sorts corresponding to the symbols Aj after leaving out literals and layout sorts. Figure 8.1 shows the signatures of statement and expression constructors for the example language from this chapter. The modules have been derived automatically from the syntax definitions in ??? and Figure 6.1.

module Statements
signature
  constructors
    FunDec  : Id * List(Id) * Exp -> FunDec
    FunDecs : List(FunDec) -> Dec
    VarDec  : Id * Exp -> Dec
    Call    : Var * List(Exp) -> Exp
    Let     : List(Dec) * List(Exp) -> Exp
    While   : Exp * Exp -> Exp
    If      : Exp * Exp * Exp -> Exp
    Seq     : List(Exp) -> Exp
    Assign  : Var * Exp -> Exp
    Gt      : Exp * Exp -> Exp
    Eq      : Exp * Exp -> Exp
    Minus   : Exp * Exp -> Exp
    Plus    : Exp * Exp -> Exp
    Times   : Exp * Exp -> Exp
    Uminus  : Exp -> Exp
    Int     : IntConst -> Exp
            : Var -> Exp
    Var     : Id -> Var
            : String -> IntConst
            : String -> Id
signature
  constructors
    Some : a -> Option(a)
    None : Option(a)
signature
  constructors
    Cons : a * List(a) -> List(a)
    Nil  : List(a)
    Conc : List(a) * List(a) -> List(a)

sdf2rtg -i m.def -o m.rtg -m M .  sdf2rtg derives from an SDF syntax definition m.def a regular tree grammar for the module M and all modules it imports.

rtg2sig -i m.def -o m.rtg .  rtg2sig generates from a regular tree grammar a Stratego signature.

The Box language is used in the GPP framework as a language-independent intermediate representation. The input language dependent parts and the output format dependent parts of GPP are connected through this intermediate representation.

Box is a mark-up language to describe the intended layout of text and is used in pretty print tables. A Box expression is constructed by composing sub-boxes using Box operators. These operators specify the relative ordering of boxes. Examples of Box operators are the H and V operator which format boxes horizontally and vertically, respectively.

The exact formatting of each Box operator can be customized using Box options. For example, to control the horizontal layout between boxes the H operator supports the hs space option.

For a detailed description of Box (including a description of all available Box operators) we refer to To Reuse Or To Be Reused (Chapter 4)

Pretty-print tables are used to specify how language constructs have to be pretty-printed. Pretty-print tables are used in combination with GPP front-ends, such ast2abox.

Pretty-print tables use Box as language to specify formatting of language constructs. A pretty-print table contains mappings from constructor names to Box expressions. For example, for the SDF production

Exp "+" Exp -> Exp {cons("Plus")}

A pretty-print entry looks like:

Plus -- H hs=1 [ _1 "+" _2]

Pretty-print tables are ordered such that pretty-print rules occuring first take preceedence over overlapping pretty-print rules defined later. The syntax of pretty-print tables is available in GPP.

"return" Exp? ";" -> Stm {cons("Return")}

Return       -- H [ KW["return"] _1 ";" ]
Return.1:opt -- H [ _1 ]

module Symbols
exports
context-free syntax
  A?                  -> S {cons("ex1")}
  A+                  -> S {cons("ex2")}
  A*                  -> S {cons("ex3")}
  {S1 S2}+            -> S {cons("ex4")}
  {S1 S2}*            -> S {cons("ex5")}
  "one" | "two" | S?  -> S {cons("ex6")}
  ("one"  "two" S? )  -> S {cons("ex7")}

[
  ex1                  -- _1,
  ex1.1:opt            -- _1,
  ex2                  -- _1,
  ex2.1:iter           -- _1,
  ex3                  -- _1,
  ex3.1:iter-star      -- _1,
  ex4                  -- _1,
  ex4.1:iter-sep       -- _1 _2,
  ex5                  -- _1,
  ex5.1:iter-star-sep  -- _1 _2,
  ex6                  -- _1,
  ex6.1:alt            -- KW["one"] KW["two"] _1,
  ex6.1:alt.1:opt      -- _1,
  ex7                  -- _1,
  ex7.1:seq            -- KW["one"] KW["two"] _1,
  ex7.1:seq.1:opt      -- _1
]

In this section, we explain how you can generate a tool that restores all parentheses at the places where necessary according to the priorities and associativities of a language.

In this section, we explain how you can use Box in Stratego to implement a pretty-printer by hand.

After transformation, an abstract syntax tree should be turned into text again to be useful as a program. Mapping a tree into text can be seen as the inverse as parsing, and is thus called unparsing. When an unparser makes an attempt at producing human readable, instead of just compiler parsable, program text, an unparser is called a pretty-printer. We use the pretty-printing model as provided by the Generic Pretty-Printing package GPP. In this model a tree is unparsed to a Box expression, which contains text with markup for pretty-printing. A Box expression can be interpreted by different back-ends to produce text for different displaying devices, such as plain ASCII text, HTML, and LaTeX.

9.5.1. Unparsing

Unparsing is the inverse of parsing composed with abstract syntax tree composition. That is, an unparser turns an abstract syntax tree into a string, such that if the resulting string is parsed again, it produces the same abstract syntax tree.

An unparser can be organized in two phases. In the first phase, each node in an abstract syntax tree is replaced with the concrete syntax tree of the corresponding grammar production. In the second phase, the strings at the leaves of the tree are concatenated into a string. Figure 9.1 illustrates this process. The replacement of abstract syntax tree nodes by concrete syntax patterns should be done according to the productions of the syntax definition. An unparsing table is an abstraction of a syntax definition definining the inverse mapping from constructors to concrete syntax patterns. An entry c -- s1 ... sn defines a mapping for constructor c to the sequence s1 ... sn, where each s_i is either a literal string or a parameter _i referring to the ith argument of the constructor. Figure 9.2 shows an unparsing table for some expression and statement constructors. Applying an unparsing mapping to an abstract syntax tree results in a tree structure with strings at the leafs, as illustrated in Figure 9.1.

Figure 9.1.  Unparsing an abstract syntax tree.

f(a + 10) - 3

Figure 9.2.  Unparsing table

[
   Var                  -- _1,
   Int                  -- _1,
   Plus                 -- _1 "+" _2,
   Minus                -- _1 "-" _2,
   Assign               -- _1 ":=" _2,
   Seq                  -- "(" _1 ")",
   Seq.1:iter-star-sep  -- _1 ";",
   If                   -- "if" _1 "then" _2 "else" _3,
   Call                 -- _1 "(" _2 ")",
   Call.2:iter-star-sep -- _1 ","
]

9.5.2. Pretty-Printing

Although the unparse of an abstract syntax tree is a text that can be parsed by a compiler, it is not necessarily a readable text. A pretty-printer is an unparser attempting to produce readable program text. A pretty-printer can be obtained by annotating the entries in an unparsing table with markup instructing a typesetting process. Figure 9.3 illustrates this process.

Box is a target independent formatting language, providing combinators for declaring the two-dimensional positioning of boxes of text. Typical combinators are H[b_1...b_n], which combines the b_i boxes horizontally, and V[b_1...b_n], which combines the b_i boxes vertically. Figure 9.4 shows a pretty-print table with Box markup. A more complete overview of the Box language and the GPP tools can be found in Chapter 9.

Figure 9.3.  Pretty-printing with Box markup

f(a + 10) - 3

Figure 9.4.  Pretty-print table with Box markup

[
   Var                  -- _1,
   Int                  -- _1,
   Plus                 -- H[_1 "+" _2],
   Minus                -- H[_1 "-" _2],
   Assign               -- H[_1 ":=" _2],
   Seq                  -- H hs=0["(" V[_1] ")"],
   Seq.1:iter-star-sep  -- H hs=0[_1 ";"],
   If                   -- V[V is=2[H["if" _1 "then"] _2] 
                             V is=2["else" _3]],
   Call                 -- H hs=0[_1 "(" H[_2] ")"],
   Call.2:iter-star-sep -- H hs=0[_1 ","]
]

Figure 9.5.  Pretty-printing of if-then-else statement

If(Eq(Var("n"),Int("1")),
   Int("0"),
   Times(Var("n"),
         Call(Var("fac"),[Minus(Var("n"),Int("1"))])))

if n = 1 then
  0
else
  n * fac(n - 1)

ppgen -i m.def -o m.pp .  Ppgen generates from an SDF syntax definition a pretty-print table with an entry for each context-free syntax production with a constructor annotation. Typically it is necessary to edit the pretty-print table to add appropriate Box markup to the entries. The result should be saved under a different name to avoid overwriting it.

ast2abox -p m.pp -i file.ast -o file.abox .  ast2abox maps an abstract syntax tree file.ast to an abstract syntax representation file.abox of a Box term based on a pretty-print table m.pp.

abox2text -i file.abox -o file.txt .  abox2text formats a Box term as ASCII text.

pp-aterm -i file1.trm -o file2.trm .  pp-aterm formats an ATerm as an ATerm in text format, adding newlines and indentation to make the structure of the term understandable. This is a useful tool to inspect terms while debugging transformations.

term-to-dot -i file.trm -o file.dot (--tree | --graph) .  Term-to-dot is another visualization tool for terms that creates a dot graph representation, which can be visualized using the dot tool from the graphviz graph layout package. Term-to-dot can produce an expanded tree view (--tree), or a directed acyclic graph view (--graph) preserving the maximal sharing in the term. This tool was used to produce the tree visualizations in this chapter. This tool is not part of the Stratego/XT distribution, but included in the Stratego/XT Utilities package.

Terms in Stratego are terms in the Annotated Term Format, or ATerms for short. The ATerm format provides a set of constructs for representing trees, comparable to XML or abstract data types in functional programming languages. For example, the code 4 + f(5 * x) might be represented in a term as:

Plus(Int("4"), Call("f", [Mul(Int("5"), Var("x"))]))

ATerms are constructed from the following elements:

The term format described above is used in Stratego programs to denote terms, but is also used to exchange terms between programs. Thus, the internal format and the external format exactly coincide. Of course, internally a Stratego program uses a data-structure in memory with pointers rather than manipulating a textual representation of terms. But this is completely hidden from the Stratego programmer. There are a few facts that are useful to be aware of, though.

The internal representation used in Stratego programs maintains maximal sharing of subterms. This means that all occurrences of a subterm are represented by a pointer to the same node in memory. This makes comparing terms in Stratego for syntactic equality a very cheap operation, i.e., just a pointer comparison.

TODO: picture of tree vs dag representation

When writing a term to a file in order to exchange it with another tool there are several representations to choose from. The textual format described above is the canonical `meaning' of terms, but does not preserve maximal sharing. Therefore, there is also a Binary ATerm Format (BAF) that preserves sharing in terms. The program baffle can be used to convert between the textual and binary representations.

As a Stratego programmer you will be looking a lot at raw ATerms. Stratego pioneers would do this by opening an ATerm file in emacs and trying to get a sense of the structure by parenthesis highlighting and inserting newlines here and there. These days your life is much more pleasant through the tool pp-aterm, which adds layout to a term to make it readable. For example, parsing the following program

let function fact(n : int) : int =
      if n < 1 then 1 else (n * fact(n - 1))
 in printint(fact(10))
end

produces the following ATerm (say in file fac.trm):

Let([FunDecs([FunDec("fact",[FArg("n",Tp(Tid("int")))],Tp(Tid("int")),
If(Lt(Var("n"),Int("1")),Int("1"),Seq([Times(Var("n"),Call(Var("fact"),
[Minus(Var("n"),Int("1"))]))])))])],[Call(Var("printint"),[Call(Var(
"fact"),[Int("10")])])])

By pretty-printing the term using pp-aterm as

$ pp-aterm -i fac.trm -o fac-pp.trm --max-term-size 20

we get a much more readable term:

Let(
  [ FunDecs(
      [ FunDec(
          "fact"
        , [FArg("n", Tp(Tid("int")))]
        , Tp(Tid("int"))
        , If(
            Lt(Var("n"), Int("1"))
          , Int("1")
          , Seq([ Times(Var("n"), Call(Var("fact"), [Minus(Var("n"), Int("1"))]))
                ])
          )
        )
      ]
    )
  ]
, [ Call(Var("printint"), [Call(Var("fact"), [Int("10")])])
  ]
)

To use terms in Stratego programs, their constructors should be declared in a signature. A signature declares a number of sorts and a number of constructors for these sorts. For each constructor, a signature declares the number and types of its arguments. For example, the following signature declares some typical constructors for constructing abstract syntax trees of expressions in a programming language:

signature
  sorts Id Exp
  constructors
           : String -> Id
    Var    : Id -> Exp
    Int    : Int -> Exp
    Plus   : Exp * Exp -> Exp
    Mul    : Exp * Exp -> Exp
    Call   : Id  * List(Exp) -> Exp

Currently, the Stratego compiler only checks the arity of constructor applications against the signature. Still, it is considered good style to also declare the types of constructors in a sensible manner for the purpose of documentation. Also, a later version of the language may introduce typechecking.

The simplest program you can write in Stratego is the following identity.str program:

module identity
imports list-cons
strategies
  main = id

It features the following elements: Each Stratego file is a module, which has the same name as the file it is stored in without the .str extension. A module may import other modules in order to use the definitions in those modules. A module may contain one or more strategies sections that introduce new strategy definitions. It will become clear later what strategies and strategy definitions are. Each Stratego program has one main definition, which indicates the strategy to be executed on invocation of the program. In the example, the body of this program's main definition is the identity strategy id.

Now let's see what this program means. To find that out, we first need to compile it, which we do using the Stratego compiler strc as follows:

$ strc -i identity.str
[ strc | info ] Compiling 'identity.str'
[ strc | info ] Front-end succeeded         : [user/system] = [0.59s/0.56s]
[ strc | info ] Back-end succeeded          : [user/system] = [0.46s/0.16s]
[ strc | info ] C compilation succeeded     : [user/system] = [0.28s/0.23s]
[ strc | info ] Compilation succeeded       : [user/system] = [1.35s/0.95s]

The -i option of strc indicates the module to compile. The compiler also reads all imported modules, in this case the list-cons.str module that is part of the Stratego library and that strc magically knows how to find. The compiler prints some information about what it is doing, i.e., the stages of compilation that it goes through and the times for those stages. You can turn this off using the argument --verbose 0. However, since the compiler is not very fast, it may be satisfying to see something going on.

The result of compilation is an executable named identity after the name of the main module of the program. Just to satisfy our curiosity we inspect the file system to see what the compiler has done:

$ ls -l identity*
-rwxrwxr-x  1 7182 Sep  7 14:54 identity*
-rw-------  1 1362 Sep  7 14:54 identity.c
-rw-rw-r--  1  200 Sep  7 14:54 identity.dep
-rw-rw-r--  1 2472 Sep  7 14:54 identity.o
-rw-rw-r--  1   57 Sep  7 13:03 identity.str

Here we see that in addition to the executable the compiler has produced a couple of other files. First of all the identity.c file gives away the fact that the compiler first translates a Stratego program to C and then uses the C compiler to compile to machine code. The identity.o file is the result of compiling the generated C program. Finally, the contents of the identity.dep file will look somewhat like this:

identity: \
        /usr/local/share/stratego-lib/collection/list/cons.rtree \
        /usr/local/share/stratego-lib/list-cons.rtree \
        ./identity.str

It is a rule in the Make language that declares the dependencies of the identity program. You can include this file in a Makefile to automate its compilation. For example, the following Makefile automates the compilation of the identity program:

include identity.dep

identity : identity.str
        strc -i identity.str

Just invoke make on the command-line whenever you change something in the program.

Ok, we were digressing a bit. Let's turn back to finding out what the identity program does. When we execute the program with some arbitrary arguments on the command-line, this is what happens:

$ ./identity foo bar
["./identity","foo","bar"]

The program writes to stdout the list of command-line arguments as a list of strings in the ATerm format. So what we have learned is that a Stratego program applies its main strategy to the list of command-line arguments, and writes the resulting term to stdout. Since the strategy in the identity program is the identity transformation it just writes the original command-line arguments (as a term).

That was instructive, but not very useful. We are not interested in transforming lists of strings, but rather programs represented as terms. So we want to read a term from a file, transform it, and write it to another file. Let's open the bag of tricks. The identity-io program improves the previous program:

module identity-io
imports libstrategolib
strategies
  main = io-wrap(id)

The program looks similar to the previous one, but there are a couple of differences. First, instead of importing module list-cons, this module imports libstrategolib, which is the interface to the separately compiled Stratego library. This library provides a host of useful strategies that are needed in implementing program transformations. Part IV gives an overview of the Stratego library, and we will every now and then use some useful strategies from the library before we get there.

Right now we are interested in the io-wrap strategy used above. It implements a wrapper strategy that takes care of input and output for our program. To compile the program we need to link it with the stratego-lib library using the -la option:

$ strc -i identity-io.str -la stratego-lib

What the relation is between libstrategolib and stratego-lib will become clear later; knowing that it is needed to compile programs using libstrategolib suffices for now.

If we run the compiled identity-io program with its --help option we see the standard interface supported by the io-wrap strategy:

$ ./identity-io --help
Options:
   -i f|--input f   Read input from f
   -o f|--output f  Write output to f
   -b               Write binary output
   -S|--silent      Silent execution (same as --verbose 0)
   --verbose i      Verbosity level i (default 1)
                    ( i as a number or as a verbosity descriptor:
                      emergency, alert, critical, error,
                      warning, notice, info, debug, vomit )
   -k i | --keep i  Keep intermediates (default 0)
   --statistics i  Print statistics (default 0 = none)
   -h|-?|--help     Display usage information
   --about          Display information about this program
   --version        Same as --about

The most relevant options are the -i option for the input file and the -o option for the output file. For instance, if we have some file foo-bar.trm containing an ATerm we can apply the program to it:

$ echo "Foo(Bar())" > foo-bar.trm
$ ./identity-io -i foo-bar.trm -o foo-bar2.trm
$ cat foo-bar2.trm
Foo(Bar)

If we leave out the -i and/or -o options, input is read from stdin and output is written to stdout. Thus, we can also invoke the program in a pipe:

$ echo "Foo(Bar())" | ./identity-io 
Foo(Bar)

Now it might seem that the identity-io program just copies its input file to the output file. In fact, the identity-io does not just accept any input. If we try to apply the program to a text file that is not an ATerm, it protests and fails:

$ echo "+ foo bar" | ./identity-io
readFromTextFile: parse error at line 0, col 0
not a valid term
./identity: rewriting failed

So we have written a program to check if a file represents an ATerm.

A Stratego program based on io-wrap defines a transformation from terms to terms. Such transformations can be combined into more complex transformations, by creating a chain of tool invocations. For example, if we have a Stratego program trafo-a applying some undefined transformation-a to the input term of the program

module trafo-a
imports libstrategolib
strategies
  main = io-wrap(transformation-a)
  transformation-a = ...

and we have another similar program trafo-b applying a transformation-b

module tool-b
imports libstrategolib
strategies
  main = io-wrap(transformation-b)
  transformation-b = ...

then we can combine the transformations to transform an input file to an output file using a Unix pipe, as in

$ tool-a -i input | tool-b -o output

or using an intermediate file:

$ tool-a -i input -o intermediate
$ tool-b -i intermediate -o output

We have just learned how to write, compile, and execute Stratego programs. This is the normal mode for development of transformation systems with Stratego. Indeed, we usually do not invoke the compiler from the command-line `by hand', but have an automated build system based on (auto)make to build all programs in a project at once. For learning to use the language this can be rather laborious, however. Therefore, we have also developed the Stratego Shell, an interactive interpreter for the Stratego language. The shell allows you to type in transformation strategies on the command-line and directly seeing their effect on the current term. While this does not scale to developing large programs, it can be instructive to experiment while learning the language. In the following chapters we will use the stratego-shell to illustrate various features of the language.

Here is a short session with the Stratego Shell that shows the basics of using it:

$ stratego-shell
stratego> :show
()
stratego> !Foo(Bar())
Foo(Bar)
stratego> id
Foo(Bar)
stratego> fail
command failed
stratego> :show
Foo(Bar)
stratego> :quit
Foo(Bar)
$

The shell is invoked by calling the command stratego-shell on the regular command-line. The stratego> prompt then indicates that you have entered the Stratego Shell. After the prompt you can enter strategies or special shell commands.

Strategies are the statements and functions of the Stratego language. A strategy transforms a term into a new term, or fails. The term to which a strategy is applied, is called the current term. In the Stratego Shell you can see the current term with :show. In the session above we see that the current term is the empty tuple if you have just started the Stratego Shell. At the prompt of the shell you can enter strategies. If the strategy succeeds, then the shell will show the transformed term, which is now the new current term. For example, in the session above the strategy !Foo(Bar()) replaces the current term with the term Foo(Bar()), which is echoed directly after applying the strategy. The next strategy that is applied is the identity strategy id that we saw before. Here it becomes clear that it just returns the term to which it is applied. Thus, we have the following general scheme of applying a strategy to the current term:

current term
stratego> strategy expression
transformed current
stratego>

Strategies can also fail. For example, the application of the fail strategy always fails. In the case of failure, the shell will print a message and leave the current term untouched:

current term
stratego> strategy expression
command failed
stratego> :show
current term

Finally, you can leave the shell using the :quit command.

The Stratego Shell has a number of non-strategy commands to operate the shell configuration. Theses commands are recognizable by the : prefix. The :help command tells you what commands are available in the shell:

$ stratego-shell
stratego> :help

Rewriting
  strategy          rewrite the current subject term with strategy

Defining Strategies
  id = strategy     define a strategy  (doesn't change the current subject term)
  id : rule         define a rule      (doesn't change the current subject term)
  import modname    import strategy definitions from 'modname' (file system or xtc)
  :undef id         delete defintions of all strategies 'id'/(s,t)
  :undef id(s,t)    delete defintion of strategy 'id'/(s,t)
  :reset            delete all term bindings, all strategies, reset syntax.

Debugging
  :show             show the current subject term
  :autoshow on|off  show the current subject term after each rewrite
  :binding id       show term binding of id
  :bindings         show all term bindings
  :showdef id       show defintions of all strategies 'id'/(s,t)
  :showdef id(s,t)  show defintion of strategy 'id'/(s,t)
  :showast id(s,t)  show ast of defintion of strategy 'id'/(s,t)

Concrete Syntax
  :syntax defname   set the syntax to the sdf definition in 'defname'.

XTC
  :xtc import pathname

Misc
  :include file     execute command in the script of `file`
  :verbose int      set the verbosity level (0-9)
  :clear            clear the screen
  :exit             exit the Stratego Shell
  :quit             same as :exit
  :q                same as :exit
  :about            information about the Stratego Shell
  :help             show this help information
stratego>

Let's summarize what we have learned so far about Stratego programming.

First, a Stratego program is divided into modules, which reside in files with extension .str and have the following general form:

module mod0
imports libstrategolib mod1 mod2
signature
  sorts A B C
  constructors
    Foo : A -> B
    Bar : A
strategies
  main = io-wrap(foo)
  foo = id

Modules can import other modules and can define signatures for declaring the structure of terms and can define strategies, which we not really know much about yet. However, the io-wrap strategy can be used to handle the input and output of a Stratego program. This strategy is defined in the libstrategolib module, which provides an interface to the Stratego Library. The main module of a Stratego program should have a main strategy that defines the entry point of the program.

Next, a Stratego program is compiled to an executable program using the Stratego Compiler strc.

$ strc -i mod0 -la stratego-lib

The resulting executable applies the main strategy to command-line arguments turned into a list-of-strings term. The io-wrap strategy interprets these command-line arguments to handle input and output using standard command-line options.

Finally, the Stratego Shell can be used to invoke strategies interactively.

$ stratego-shell
stratego> id
()
stratego> 

Next up: transforming terms 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 : 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.

In Chapter 12 we saw how term rewriting can be used to implement transformations on programs represented by means of terms. Term rewriting involves exhaustively applying rules to subterms until no more rules apply. This requires a strategy for selecting the order in which subterms are rewritten. The innermost strategy introduced in Chapter 12 applies rules automatically throughout a term from inner to outer terms, starting with the leaves. The nice thing about term rewriting is that there is no need to define traversals over the syntax tree; the rules express basic transformation steps and the strategy takes care of applying it everywhere. However, the complete normalization approach of rewriting turns out not to be adequate for program transformation, because rewrite systems for programming languages will often be non-terminating and/or non-confluent. In general, it is not desirable to apply all rules at the same time or to apply all rules under all circumstances.

Consider for example, the following extension of prop-dnf-rules with distribution rules to achieve conjunctive normal forms:

module prop-cnf
imports prop-dnf-rules
rules
  E : Or(And(x, y), z) -> And(Or(x, z), Or(y, z))
  E : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y))
strategies
  main = io-wrap(cnf)
  cnf  = innermost(E)

This rewrite system is non-terminating because after applying one of the and-over-or distribution rules, the or-over-and distribution rules introduced here can be applied, and vice versa.

   And(Or(Atom("p"),Atom("q")), Atom("r")) 
-> 
   Or(And(Atom("p"), Atom("r")), And(Atom("q"), Atom("r")))
->
   And(Or(Atom("p"), And(Atom("q"), Atom("r"))), 
       Or(Atom("r"), And(Atom("q"), Atom("r"))))
->
   ...

There are a number of solutions to this problem. We'll first discuss a couple of solutions within pure rewriting, and then show how programmable rewriting strategies can overcome the problems of these solutions.

The non-termination of prop-cnf is due to the fact that the and-over-or and or-over-and distribution rules interfere with each other. This can be prevented by refactoring the module structure such that the two sets of rules are not present in the same rewrite system. For example, we could split module prop-dnf-rules into prop-simplify and prop-dnf2 as follows:

module prop-simplify
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))

module prop-dnf2
imports prop-simplify
rules
  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))
strategies
  main = io-wrap(dnf)
  dnf  = innermost(E)

Now we can reuse the rules from prop-simplify without the and-over-or distribution rules to create a prop-cnf2 for normalizing to conjunctive normal form:

module prop-cnf2
imports prop-simplify
rules
  E : Or(And(x, y), z) -> And(Or(x, z), Or(y, z))
  E : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y))
strategies
  main = io-wrap(cnf)
  cnf  = innermost(E)

Although this solves the non-termination problem, it is not an ideal solution. In the first place it is not possible to apply the two transformations in the same program. In the second place, extrapolating the approach to fine-grained selection of rules might require definition of a single rule per module.

Another common solution to this kind of problem is to introduce additional constructors that achieve normalization under a restricted set of rules. That is, the original set of rules p1 -> p2 is transformed into rules of the form f(p_1) -> p_2', where f is some new constructor symbol and the right-hand side of the rule also contains such new constructors. In this style of programming, constructors such as f are called functions and are distinghuished from constructors. Normal forms over such rewrite systems are assumed to be free of these `function' symbols; otherwise the function would have an incomplete definition.

To illustrate the approach we adapt the DNF rules by introducing the function symbols Dnf and DnfR. (We ignore the evaluation rules in this example.)

module prop-dnf3
imports libstrategolib prop
signature
  constructors
    Dnf  : Prop -> Prop
    DnfR : Prop -> Prop
rules
  E : Dnf(Atom(x))    -> Atom(x)
  E : Dnf(Not(x))     -> DnfR(Not(Dnf(x)))
  E : Dnf(And(x, y))  -> DnfR(And(Dnf(x), Dnf(y)))
  E : Dnf(Or(x, y))   -> Or(Dnf(x), Dnf(y))
  E : Dnf(Impl(x, y)) -> Dnf(Or(Not(x), y))
  E : Dnf(Eq(x, y))   -> Dnf(And(Impl(x, y), Impl(y, x)))

  E : DnfR(Not(Not(x)))      -> x
  E : DnfR(Not(And(x, y)))   -> Or(Dnf(Not(x)), Dnf(Not(y)))
  E : DnfR(Not(Or(x, y)))    -> Dnf(And(Not(x), Not(y)))
  D : DnfR(Not(x))           -> Not(x)

  E : DnfR(And(Or(x, y), z)) -> Or(Dnf(And(x, z)), Dnf(And(y, z)))
  E : DnfR(And(z, Or(x, y))) -> Or(Dnf(And(z, x)), Dnf(And(z, y)))
  D : DnfR(And(x, y))        -> And(x, y)
strategies
  main = io-wrap(dnf)
  dnf  = innermost(E <+ D)

The Dnf function mimics the innermost normalization strategy by recursively traversing terms. The auxiliary transformation function DnfR is used to encode the distribution and negation rules. The D rules are default rules that are only applied if none of the E rules apply, as specified by the strategy expression E <+ D.

In order to compute the disjunctive normal form of a term, we have to `apply' the Dnf function to it, as illustrated in the following application of the prop-dnf3 program:

$ cat test1.dnf
Dnf(And(Impl(Atom("r"),And(Atom("p"),Atom("q"))),ATom("p")))

$ ./prop-dnf3 -i test1.dnf
Or(And(Not(Atom("r")),Dnf(Dnf(ATom("p")))),
   And(And(Atom("p"),Atom("q")),Dnf(Dnf(ATom("p")))))

For conjunctive normal form we can create a similar definition, which can now co-exist with the definition of DNF. Indeed, we could then simultaneously rewrite one subterm to DNF and the other to CNF.

  E : DC(x) -> (Dnf(x), Cnf(x))

In the solution above, the original rules have been completely intertwined with the Dnf transformation. The rules for negation cannot be reused in the definition of normalization to conjunctive normal form. For each new transformation a new traversal function and new transformation functions have to be defined. Many additional rules had to be added to traverse the term to find the places to apply the rules. In the modular solution we had 5 basic rules and 2 additional rules for DNF and 2 rules for CNF, 9 in total. In the functionalized version we needed 13 rules for each transformation, that is 26 rules in total.

In general, there are two problems with the functional approach to encoding the control over the application of rewrite rules, when comparing it to the original term rewriting approach: traversal overhead and loss of separation of rules and strategies.

In the first place, the functional encoding incurs a large overhead due to the explicit specification of traversal. In pure term rewriting, the strategy takes care of traversing the term in search of subterms to rewrite. In the functional approach traversal is spelled out in the definition of the function, requiring the specification of many additional rules. A traversal rule needs to be defined for each constructor in the signature and for each transformation. The overhead for transformation systems for real languages can be inferred from the number of constructors for some typical languages:

language : constructors 
Tiger    : 65 
C        : 140 
Java     : 140 
COBOL    : 300 - 1200

In the second place, rewrite rules and the strategy that defines their application are completely intertwined. Another advantage of pure term rewriting is the separation of the specification of the rules and the strategy that controls their application. Intertwining these specifications makes it more difficult to understand the specification, since rules cannot be distinghuished from the transformation they are part of. Furthermore, intertwining makes it impossible to reuse the rules in a different transformation.

Stratego introduced the paradigm of programmable rewriting strategies with generic traversals, a unifying solution in which application of rules can be carefully controlled, while incurring minimal traversal overhead and preserving separation of rules and strategies.

The following are the design criteria for strategies in Stratego:

In the next chapters we will examine the language constructs that Stratego provides for programming with strategies, starting with the low-level actions of building and matching terms. To get a feeling for the purpose of these constructs, we first look at a couple of typical idioms of strategic rewriting.

simplify = innermost(R1 <+ ... <+ Rn)

module prop-laws
imports libstrategolib prop
rules

  DefI : Impl(x, y) -> Or(Not(x), y)
  DefE : Eq(x, y)   -> And(Impl(x, y), Impl(y, x))

  DN   : Not(Not(x)) -> x

  DMA  : Not(And(x, y)) -> Or(Not(x), Not(y))
  DMO  : Not(Or(x, y))  -> And(Not(x), Not(y))

  DAOL : And(Or(x, y), z) -> Or(And(x, z), And(y, z))
  DAOR : And(z, Or(x, y)) -> Or(And(z, x), And(z, y))

  DOAL : Or(And(x, y), z) -> And(Or(x, z), Or(y, z))
  DOAR : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y))

strategies

  dnf = innermost(DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO)
  cnf = innermost(DefI <+ DefE <+ DOAL <+ DOAR <+ DN <+ DMA <+ DMO)

  main-dnf = io-wrap(dnf)
  main-cnf = io-wrap(cnf)

$ strc -i prop-laws.str -la stratego-lib --main main-dnf -o prop-dnf4

simplify = bottomup(repeat(R1 <+ ... <+ Rn))

module prop-eval2
imports libstrategolib prop
rules
  Eval : Not(True)      -> False       
  Eval : Not(False)     -> True
  Eval : And(True, x)   -> x        
  Eval : And(x, True)   -> x   
  Eval : And(False, x)  -> False     
  Eval : And(x, False)  -> False
  Eval : Or(True, x)    -> True     
  Eval : Or(x, True)    -> True  
  Eval : Or(False, x)   -> x     
  Eval : Or(x, False)   -> x
  Eval : Impl(True, x)  -> x 
  Eval : Impl(x, True)  -> True      
  Eval : Impl(False, x) -> True
  Eval : Eq(False, x)   -> Not(x)
  Eval : Eq(x, False)   -> Not(x)      
  Eval : Eq(True, x)    -> x
  Eval : Eq(x, True)    -> x
strategies
  main = io-wrap(eval)
  eval = bottomup(repeat(Eval))

simplify = topdown(try(R1 <+ ... <+ Rn))

module prop-desugar
imports prop libstrategolib

rules

  DefN  : Not(x)     -> Impl(x, False)
  DefI  : Impl(x, y) -> Or(Not(x), y)
  DefE  : Eq(x, y)   -> And(Impl(x, y), Impl(y, x))
  DefO1 : Or(x, y)   -> Impl(Not(x), y)
  DefO2 : Or(x, y)   -> Not(And(Not(x), Not(y)))
  DefA1 : And(x, y)  -> Not(Or(Not(x), Not(y)))
  DefA2 : And(x, y)  -> Not(Impl(x, Not(y)))

  IDefI : Or(Not(x), y) -> Impl(x, y)

  IDefE : And(Impl(x, y), Impl(y, x)) -> Eq(x, y)

strategies

  desugar = 
    topdown(try(DefI <+ DefE))

  impl-nf = 
    topdown(repeat(DefN <+ DefA2 <+ DefO1 <+ DefE))

  main-desugar = 
    io-wrap(desugar)
  
  main-inf =
    io-wrap(impl-nf)

simplify = downup(repeat(R1 <+ ... <+ Rn))

eval = downup(repeat(Eval))

And(... big expression ..., False)

strategies

  simplify =
    innermost(A1 <+ ... <+ Ak)
    ; innermost(B1 <+ ... <+ Bl)
    ; ...
    ; innermost(C1 <+ ... <+ Cm)

strategies

  transformation =
    alltd(
      trigger-transformation
      ; innermost(A1 <+ ... <+ An)
    )

While term rewrite rules can express individual transformation steps, the exhaustive applications of all rules to all subterms is not always desirable. The selection of rules to apply through the module system does not allow transformations to co-exist and may require very small-grained modules. The `functionalization' of rewrite rules leads to overhead in the form of traversal definitions and to the loss of separation between rules and strategy. The paradigm of rewriting with programmable strategies allows the separate definition of individual rewrite rules, which can be (re)used in different combinations with a choice of strategies to form a variety of transformations. Idioms such as cascading transformations, one-pass traversals, staged, and local transformations cater for different styles of applying strategies.

Next up: The next chapters give an in depth overview of the constructs for composing strategies.

A named rewrite rule is a declaration of the form

L : p1 -> p2

where L is the rule name, p1 the left-hand side term pattern, and p2 the right-hand side term pattern. A rule defines a transformation on terms. A rule can be applied through its name to a term. It will transform the term if it matches with p1, and will replace the term with p2 instantiated with the variables bound during the match to p1. The application fails if the term does not match p1. Thus, a transformation is a partial function from terms to terms

Let's look at an example. The SwapArgs rule swaps the subterms of the Plus constructor. Note that it is possible to introduce rules on the fly in the Stratego Shell.

stratego> SwapArgs : Plus(e1,e2) -> Plus(e2,e1)

Now we create a new term, and apply the SwapArgs rule to it by calling its name at the prompt. (The build !t of a term replaces the current term by t, as will be explained in Chapter 16.)

stratego> !Plus(Var("a"),Int("3"))
Plus(Var("a"),Int("3"))
stratego> SwapArgs 
Plus(Int("3"),Var("a"))

The application of SwapArgs fails when applied to a term to which the left-hand side does not match. For example, since the pattern Plus(e1,e2) does not match with a term constructed with Times the following application fails:

stratego> !Times(Int("4"),Var("x"))
Times(Int("4"),Var("x"))
stratego> SwapArgs 
command failed

A rule is applied at the root of a term, not at one of its subterms. Thus, the following application fails even though the term contains a Plus subterm:

stratego> !Times(Plus(Var("a"),Int("3")),Var("x"))
Times(Plus(Var("a"),Int("3")),Var("x"))
stratego> SwapArgs 
command failed

Likewise, the following application only transforms the outermost occurrence of Plus, not the inner occurrence:

stratego> !Plus(Var("a"),Plus(Var("x"),Int("42")))
Plus(Var("a"),Plus(Var("x"),Int("42")))
stratego> SwapArgs 
Plus(Plus(Var("x"),Int("42")),Var("a"))

Finally, there may be multiple rules with the same name. This has the effect that all rules with that name will be tried in turn until one succeeds, or all fail. The rules are tried in some undefined order. This means that it only makes sense to define rules with the same name if they are mutually exclusive, that is, do not have overlapping left-hand sides. For example, we can extend the definition of SwapArgs with a rule for the Times constructor, as follows:

stratego> SwapArgs : Times(e1, e2) -> Times(e2, e1)   

Now the rule can be applied to terms with a Plus and a Times constructor, as illustrated by the following applications:

stratego> !Times(Int("4"),Var("x"))
Times(Int("4"),Var("x"))
stratego> SwapArgs 
Times(Var("x"),Int("4"))

stratego> !Plus(Var("a"),Int("3"))
Plus(Var("a"),Int("3"))
stratego> SwapArgs 
Plus(Int("3"),Var("a"))

Later we will see that a rule is nothing more than a syntactical convention for a strategy definition.

A rule defines a transformation, that is, a partial function from terms to terms. A strategy expression is a combination of one or more transformations into a new transformation. So, a strategy expression also defines a transformation, i.e., a partial function from terms to terms. Strategy operators are functions from transformations to transformations.

In the previous chapter we saw some examples of strategy expressions. Lets examine these examples in the light of our new definition. First of all, rule names are basic strategy expressions. If we import module prop-laws, we have at our disposal all rules it defines as basic strategies:

stratego> import prop-laws
stratego> !Impl(True(), Atom("p"))
Impl(True, Atom("p"))
stratego> DefI
Or(Not(True),Atom("p"))

Next, given a collection of rules we can create more complex transformations by means of strategy operators. For example, the innermost strategy creates from a collection of rules a new transformation that exhaustively applies those rules.

stratego> !Eq(Atom("p"), Atom("q"))
Eq(Atom("p"),Atom("q"))

stratego> innermost(DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO)

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

(Exercise: add rules to this composition that remove tautologies or false propositions.) Here we see that the rules are first combined using the choice operator <+ into a composite transformation, which is the argument of the innermost strategy.

The innermost strategy always succeeds (but may not terminate), but this is not the case for all strategies. For example bottomup(DefI) will not succeed, since it attempts to apply rule DefI to all subterms, which is clearly not possible. Thus, strategies extend the property of rules that they are partial functions from terms to terms.

Observe that in the composition innermost(...), the term to which the transformation is applied is never mentioned. The `current term', to which a transformation is applied is often implicit in the definition of a strategy. That is, there is no variable that is bound to the current term and then passed to an argument strategy. Thus, a strategy operator such as innermost is a function from transformations to transformations.

While strategies are functions, they are not necessarily pure functions. Strategies in Stratego may have side effects such as performing input/output operations. This is of course necessary in the implementation of basic tool interaction such as provided by io-wrap, but is also useful for debugging. For example, the debug strategy prints the current term, but does not transform it. We can use it to visualize the way that innermost transforms a term.

stratego> !Not(Impl(Atom("p"), Atom("q")))
Not(Impl(Atom("p"),Atom("q")))
stratego> innermost(debug(!"in:  "); (DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO); debug(!"out: "))
in:  p
in:  Atom("p")
in:  q
in:  Atom("q")
in:  Impl(Atom("p"),Atom("q"))
out: Or(Not(Atom("p")),Atom("q"))
in:  p
in:  Atom("p")
in:  Not(Atom("p"))
in:  q
in:  Atom("q")
in:  Or(Not(Atom("p")),Atom("q"))
in:  Not(Or(Not(Atom("p")),Atom("q")))
out: And(Not(Not(Atom("p"))),Not(Atom("q")))
in:  p
in:  Atom("p")
in:  Not(Atom("p"))
in:  Not(Not(Atom("p")))
out: Atom("p")
in:  p
in:  Atom("p")
in:  q
in:  Atom("q")
in:  Not(Atom("q"))
in:  And(Atom("p"),Not(Atom("q")))
And(Atom("p"),Not(Atom("q")))

This session nicely shows how innermost traverses the term it transforms. The in: lines show terms to which it attempts to apply a rule, the out: lines indicate when this was successful and what the result of applying the rule was. Thus, innermost performs a post-order traversal applying rules after transforming the subterms of a term. (Note that when applying debug to a string constant, the quotes are not printed.)

Stratego programs are about defining transformations in the form of rules and strategy expressions that combine them. Just defining strategy expressions does not scale, however. Strategy definitions are the abstraction mechanism of Stratego and allow naming and parameterization of strategy expresssions for reuse.

module dnf-strategies
imports libstrategolib prop-dnf-rules
strategies

  dnf-rules = 
    DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO

  dnf = 
    innermost(dnf-rules)

  dnf-debug = 
    innermost(debug(!"in:  "); dnf-rules; debug(!"out: "))

  main =
    io-wrap(dnf)

f = s

f(x1,...,xn | y1,..., ym) = s

strategies
  try(s)      = s <+ id
  repeat(s)   = try(s; repeat(s))
  topdown(s)  = s; all(topdown(s))
  bottomup(s) = all(bottomup(s)); s

module prop-desugar
// ...
strategies

  desugar = 
    topdown(try(DefI <+ DefE))

  impl-nf = 
    topdown(repeat(DefN <+ DefA2 <+ DefO1 <+ DefE))

let dnf-rules = DefI <+ DefE <+ DAOL <+ DAOR <+ DN <+ DMA <+ DMO
 in innermost(dnf-rules)
end

strategies
  f = s1
  f = s2

strategies
  f = s1 <+ s2

strategies
  f = s2 <+ s1

Stratego provides combinators for composing transformations and basic operators for analyzing, creating and traversing terms. However, it does not provide built-in support for other types of computation such as input/output and process control. In order to make such functionality available to Stratego programmers, the language provides access to user-definable primitive strategies through the prim construct. For example, the following call to prim invokes the SSL_printnl function from the native code of the C library:

stratego> prim("SSL_printnl", stdout(), ["foo", "bar"])
foobar
""

In general, a call prim("f", s* | t*) represents a call to a primitive function f with strategy arguments s* and term arguments t*. Note that the `current' term is not passed automatically as argument.

This mechanism allows the incorporation of mundane tasks such as arithmetic, I/O, and other tasks not directly related to transformation, but necessary for the integration of transformations with the other parts of a transformation system.

Primitive functions should take ATerms as arguments. It is not possible to use `unboxed' values, i.e., raw native types. This requires writing a wrapper function in C. For example, the addition of two integers is defined via a call to a primitive prim("SSL_addi",x,y), where the argument should represent integer ATerms, not C integers.

Implementing Primitives.  The Stratego Library provides all the primitives for I/O, arithmetic, string processing, and process control that are usually needed in Stratego programs. However, it is possible to add new primitives to a program as well. That requires linking with the compiled program a library that implements the function. See the documentation of strc for instructions.

The Stratego Compiler is a whole program compiler. That is, the compiler includes all definitions from imported modules (transitively) into the program defined by the main module (the one being compiled). This is the reason that the compiler takes its time to compile a program. To reduce the compilation effort and the size of the resulting programs it is possible to create separately compiled libraries of Stratego definitions. The strategies that such a library provides are declared as external definitions. A declaration of the form

external f(s1 ... sn | x1 ... xm)

states that there is an externally defined strategy operator f with n strategy arguments and m term arguments. When compiling a program with external definitions a library should be provided that implements these definitions.

The Stratego Library is provided as a separately compiled library. The libstrateglib module that we have been using in the example programs contains external definitions for all strategies in the library, as illustrated by the following excerpt:

module libstrategolib
// ...
strategies
  // ...
  external io-wrap(s)
  external bottomup(s)
  external topdown(s)
  // ...

When compiling a program using the library we used the -la stratego-lib option to provide the implementation of those definitions.

External Definitions cannot be Extended.  Unlike definitions imported in the normal way, external definitions cannot be extended. If we try to compile a module extending an external definition, such as

module wrong
imports libstrategolib
strategies
  bottomup(s) = fail

compilation fails:

$ strc -i wrong.str
[ strc | info ] Compiling 'wrong.str'
error: redefining external definition: bottomup/1-0
[ strc | error ] Compilation failed (3.66 secs)

Creating Libraries.  It is possible to create your own Stratego libraries as well. Currently that exposes you to a bit of C compilation giberish; in the future this may be incorporated in the Stratego compiler. Lets create a library for the rules and strategy definitions in the prop-laws module. We do this using the --library option to indicate that a library is being built, and the -c option to indicate that we are only interested in the generated C code.

$ strc -i prop-laws.str -c -o libproplib.rtree --library
[ strc | info ] Compiling 'proplib.str'
[ strc | info ] Front-end succeeded         : [user/system] = [4.71s/0.77s]
[ strc | info ] Abstract syntax in 'libproplib.rtree'
[ strc | info ] Concrete syntax in 'libproplib.str'
[ strc | info ] Export of externals succeeded : [user/system] = [2.02s/0.11s]
[ strc | info ] Back-end succeeded          : [user/system] = [6.66s/0.19s]
[ strc | info ] Compilation succeeded       : [user/system] = [13.4s/1.08s]
$ rm libproplib.str

The result is of this compilation is a module libproplib that contains the external definitions of the module and those inherited from libstrategolib. (This module comes in to versions; one in concrete syntax libproplib.str and one in abstract syntax libproplib.rtree; for some obscure reason you should throw away the .str file.) Furthermore, the Stratego Compiler produces a C program libproplib.c with the implementation of the library. This C program should be turned into an object library using libtool, as follows:

$ libtool --mode=compile gcc -g -O -c libproplib.c -o libproplib.o -I <path/to/aterm-stratego/include>
...
$ libtool --mode=link gcc -g -O -o libproplib.la libproplib.lo
...

The result is a shared library libproplib.la that can be used in other Stratego programs. (TODO: the production of the shared library should really be incorporated into strc.)

Using Libraries.  Programmers that want to use your library can now import the module with external definitions, instead of the original module.

module dnf-tool
imports libproplib
strategies
  main = main-dnf

This program can be compiled in the usual way, adding the new library to the libraries that should be linked against:

$ strc -i dnf-tool.str -la stratego-lib -la ./libproplib.la

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

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

To correctly deploy programs based on shared libraries requires some additional effort. Chapter 29 explains how to create deployable packages for your Stratego programs.

Strategies can be called dynamically by name, i.e., where the name of the strategy is specified as a string. Such calls can be made using the call construct, which has the form:

call(f | s1, ..., sn | t1, ..., tn)

where f is a term that should evaluate to a string, which indicates the name of the strategy to be called, followed by a list of strategy arguments, and a list of term arguments.

Dynamic calls allow the name of the strategy to be computed at run-time. This is a rather recent feature of Stratego that was motivated by the need for call-backs from a separately compiled Stratego library combined with the computation of dynamic rule names. Otherwise, there is not yet much experience with the feature.

In the current version of Stratego it is necessary to 'register' a strategy to be able to call it dynamically. (In order to avoid deletion in case it is not called explicitly somewhere in the program.) Strategies are registered by means of a dummy strategy definition DYNAMIC-CALLS with calls to the strategies that should called dynamically.

DYNAMICAL-CALLS = foo(id)

We have learned that rules and strategies define transformations, that is, functions from terms to terms that can fail, i.e., partial functions. Rule and strategy definitions introduce names for transformations. Parameterized strategy definitions introduce new strategy operators, functions that construct transformations from transformations.

Primitive strategies are transformations that are implemented in some language other than Stratego (usually C), and are called through the prim construct. External definitions define an interface to a separately compiled library of Stratego definitions. Dynamic calls allow the name of the strategy to be called to be computed as a string.

The most basic operations in Stratego are id and fail. The identity strategy id always succeeds and behaves as the identity function on terms. The failure strategy fail always fails. The operations have no side effects.

stratego> !Foo(Bar())
Foo(Bar)
stratego> id
Foo(Bar)
stratego> fail
command failed

The sequential composition s1 ; s2 of the strategies s1 and s2 first applies the strategy s1 to the subject term and then s2 to the result of that first application. The strategy fails if either s1 or s2 fails.

Properties.  Sequential composition is associative. Identity is a left and right unit for sequential composition; since id always succeeds and leaves the term alone, it has no additional effect to the strategy that it is composed with. Failure is a left zero for sequential composition; since fail always fails the next strategy will never be reached.

(s1; s2) ; s3 = s1; (s2; s3)

id; s = s

s; id = s

fail; s = fail

However, not for all strategies s we have that failure is a right zero for sequential composition:

s ; fail = fail   (is not a law)

Although the composition s; fail will always fail, the execution of s may have side effects that are not performed by fail. For example, consider printing a term in s.

Examples.  As an example of the use of sequential composition consider the following rewrite rules.

stratego> A : P(Z(),x) -> x
stratego> B : P(S(x),y) -> P(x,S(y))

The following session shows the effect of first applying B and then A:

stratego> !P(S(Z()), Z())
P(S(Z),Z)
stratego> B
P(Z,S(Z))
stratego> A
S(Z)

Using the sequential composition of the two rules, this effect can be achieved `in one step':

stratego> !P(S(Z()),Z())
P(S(Z),Z)
stratego> B; A
S(Z)

The following session shows that the application of a composition fails if the second strategy in the composition fails to apply to the result of the first:

stratego> !P(S(Z()),Z())
P(S(Z),Z)
stratego> B; B
command failed

Choosing between rules to apply is achieved using one of several choice combinators, all of which are based on the guarded choice combinator. The common approach is that failure to apply one strategy leads to backtracking to an alternative strategy.

(s1 <+ s2) <+ s3 = s1 <+ (s2 <+ s3)

id <+ s  = id

fail <+ s = s

s <+ fail = s

s <+ id =  s    (is not a law)

(s1 <+ s2); s3 = (s1; s3) <+ (s2; s3)    (is not a law)

stratego> !P(S(Z()),Z())
P(S(Z),Z)
stratego> (B <+ id); B
command failed

stratego> !P(S(Z()),Z())
P(S(Z),Z)
stratego> (B <+ id)
P(Z,S(Z))
stratego> B
command failed

stratego> (B; B) <+ (id; B)
P(Z,S(Z))

stratego> PlusAssoc : Plus(Plus(e1, e2), e3) -> Plus(e1, Plus(e2, e3))
stratego> PlusZero  : Plus(Int("0"),e) -> e

stratego> !Plus(Int("0"),Int("3"))
Plus(Int("0"),Int("3"))

stratego> PlusAssoc
command failed
stratego> PlusAssoc <+ PlusZero
Int("3")

stratego> !Plus(Plus(Var("x"),Int("42")),Int("3"))
Plus(Plus(Var("x"),Int("42")),Int("3"))

stratego> PlusZero
command failed
stratego> PlusAssoc <+ PlusZero
Plus(Var("x"),Plus(Int("42"),Int("3")))

stratego> Mem1 : Mem(x,[]) -> False()
stratego> Mem2 : Mem(x,[x|xs]) -> True()
stratego> Mem3 : Mem(x,[y|ys]) -> Mem(x,ys)

stratego> !Mem(1, [1,2,3])
Mem(1, [1,2,3])
stratego> Mem2
True
stratego> !Mem(1, [1,2,3])
Mem(1,[1,2,3])
stratego> Mem3
Mem(1,[2,3])

try(s) = s <+ id

s1 <+ s2 = s1 < id + s2

id < s2 + s3  = s2

fail < s2 + s3 = s3

s1 < s2 + fail = s1; s2

(s1 < s2 + s3) < s4 + s5 = s1 < s2 + (s3 < s4 + s5)    (not a law)

(s1 < s2 + s3); s4 = s1 < (s2; s4) + (s3; s4)

s0; (s1 < s2 + s3) = (s0; s1) < s2 + s3

not(s) = s < fail + id

not(id) = fail
not(fail) = id

not(not(s)) = s   (not a law)

restore-always(s, r) = s < r + (r; fail)

if s1 then s2 else s3 end  =  where(s1) < s2 + s3

if id   then s2 else s3 end  =  s2

if fail then s2 else s3 end  =  s3

if s1 then s2 end  =  where(s1) < s2 + id

or(s1, s2) = 
  if s1 then try(where(s2)) else where(s2) end

and(s1, s2) = 
  if s1 then where(s2) else where(s2); fail end

  switch s0
    case s1 : s1'
    case s2 : s2'
    ...
    otherwise : sdef
  end

  {x : where(s0 => x);
       if <s1> x 
       then s1' 
       else if <s2> x 
            then s2' 
            else if ...
                 then ...
                 else sdef
                 end
            end 
       end}

  f = s1  f = s2      ==>    f = s1 + s2

Repeated application of a strategy can be achieved with recursion. There are two styles for doing this; with a recursive definition or using the fixpoint operator rec. A recursive definition is a normal strategy definition with a recursive call in its body.

f(s) = ... f(s) ...

Another way to define recursion is using the fixpoint operator rec x(s), which recurses on applications of x within s. For example, the definition

f(s) = rec x(... x ...)

is equivalent to the one above. The advantage of the rec operator is that it allows the definition of an unnamed strategy expression to be recursive. For example, in the definition

g(s) = foo; rec x(... x ...); bar

the strategy between foo and bar is a recursive strategy that does not recurse to g(s).

Originally, the rec operator was the only way to define recursive strategies. It is still in the language in the first place because it is widely used in many existing programs, and in the second place because it can be a concise expression of a recursive strategy, since call parameters are not included in the call. Furthermore, all free variables remain in scope.

Examples.  The repeat strategy applies a transformation s until it fails. It is defined as a recursive definition using try as follows:

try(s)    = s <+ id
repeat(s) = try(s; repeat(s))

An equivalent definition using rec is:

repeat(s) = rec x(try(s; x))

The following Stratego Shell session illustrates how it works. We first define the strategies:

stratego> try(s) = s <+ id
stratego> repeat(s) = try(s; repeat(s))
stratego> A : P(Z(),x) -> x
stratego> B : P(S(x),y) -> P(x,S(y))

Then we observe that the repeated application of the individual rules A and B reduces terms:

stratego> !P(S(Z()),Z())
P(S(Z),Z)
stratego> B
P(Z,S(Z))
stratego> A
S(Z)

We can automate this using the repeat strategy, which will repeat the rules as often as possible:

stratego> !P(S(Z()),Z())
P(S(Z),Z)
stratego> repeat(A <+ B)
S(Z)

stratego> !P(S(S(S(Z()))),Z())
P(S(S(S(Z))),Z)
stratego> repeat(A <+ B)
S(S(S(Z)))

To illustrate the intermediate steps of the transformation we can use debug from the Stratego Library.

stratego> import liblib
stratego> !P(S(S(S(Z()))),Z())
P(S(S(S(Z))),Z)
stratego> repeat(debug; (A <+ B))
P(S(S(S(Z))),Z)
P(S(S(Z)),S(Z))
P(S(Z),S(S(Z)))
P(Z,S(S(S(Z))))
S(S(S(Z)))
S(S(S(Z)))

A Library of Iteration Strategies.  Using sequential composition, choice, and recursion a large variety of iteration strategies can be defined. The following definitions are part of the Stratego Library (in module strategy/iteration).

repeat(s) = 
  rec x(try(s; x))

repeat(s, c) =
  (s; repeat(s, c)) <+ c

repeat1(s, c) = 
  s; (repeat1(s, c) <+ c)

repeat1(s) = 
  repeat1(s, id)

repeat-until(s, c) = 
  s; if c then id else repeat-until(s, c) end

while(c, s) = 
  if c then s; while(c, s) end

do-while(s, c) =
  s; if c then do-while(s, c) end

The following equations describe some relations between these strategies:

  do-while(s, c) = repeat-until(s, not(c))

  do-while(s, c) = s; while(c, s)

We have seen that rules and strategies can be combined into more complex strategies by means of strategy combinators. Cumulative effects are obtained by sequential composition of strategies using the s1 ; s2 combinator. Choice combinators allow a strategy to decide between alternative transformations. While Stratego provides a variety of choice combinators, they are all based on the guarded choice combinator s1 < s2 + s3. Repetition of transformations is achieved using recursion, which can be achieved through recursive definitions or the rec combinator.

Next up: Chapter 16 shows the stuff that rewrite rules are made of.

The build operation !p replaces the subject term with the instantiation of the pattern p using the bindings from the environment to the variables occurring in p. For example, the strategy !Or(And(x, z), And(y, z)) replaces the subject term with the instantiation of Or(And(x, z), And(y, z)) using bindings to variables x, y and z.

stratego> !Int("10")
Int("10")
stratego> !Plus(Var("a"), Int("10"))
Plus(Var("a"), Int("10"))

It is possible to build terms with variables. We call this building a term pattern. A pattern is a term with meta-variables. The current term is replaced by an instantiation of pattern p.

stratego> :binding e
e is bound to Var("b")
stratego> !Plus(Var("a"),e)
Plus(Var("a"),Var("b"))
stratego> !e
Var("b")

Pattern matching allows the analysis of terms. The simplest case is matching against a literal term. The match operation ?t matches the subject term against the term t.

Plus(Var("a"),Int("3"))
stratego> ?Plus(Var("a"),Int("3"))
stratego> ?Plus(Int("3"),Var("b"))
command failed

Matching against a term pattern with variables binds those variables to (parts of) the current term. The match strategy ?x compares the current term (t) to variable x. It binds variable x to term t in the environment. A variable can only be bound once, or to the same term.

Plus(Var("a"),Int("3"))
stratego> ?e
stratego> :binding e
e is bound to Plus(Var("a"),Int("3")) 
stratego> !Int("17")
stratego> ?e
command failed

The general case is matching against an arbitrary term pattern. The match strategy ?p compares the current term to a pattern p. It will add bindings for the variables in pattern p to the environment. The wildcard _ in a match will match any term.

Plus(Var("a"),Int("3"))
stratego> ?Plus(e,_)
stratego> :binding e
e is bound to Var("a")
Plus(Var("a"),Int("3"))

Patterns may be non-linear. Multiple occurences of the same variable can occur and each occurence matches the same term.

Plus(Var("a"),Int("3"))
stratego> ?Plus(e,e)
command failed
stratego> !Plus(Var("a"),Var("a"))
stratego> ?Plus(e,e)
stratego> :binding e
e is bound to Var("a")

Non-linear pattern matching is a way to test equality of terms. Indeed the equality predicates from the Stratego Library are defined using non-linear pattern matching:

equal = ?(x, x)
equal(|x) = ?x

The equal strategy tests whether the current term is a a pair of the same terms. The equal(|x) strategy tests whether the current term is equal to the argument term.

stratego> equal = ?(x, x)
stratego> !("a", "a")
("a", "a")
stratego> equal
("a", "a")
stratego> !("a", "b")
("a", "b")
stratego> equal
command failed

stratego> equal(|x) = ?x
stratego> !Foo(Bar())
Foo(Bar)
stratego> equal(|Foo(Baz()))
command failed
stratego> equal(|Foo(Bar()))
Foo(Bar)

Match and build are first-class citizens in Stratego, which means that they can be used and combined just like any other strategy expressions. In particular, we can implement rewrite rules using these operations, since a rewrite rule is basically a match followed by a build. For example, consider the following combination of match and build:

Plus(Var("a"),Int("3"))
stratego> ?Plus(e1, e2); !Plus(e2, e1)
Plus(Int("3"),Var("a"))

This combination first recognizes a term, binds variables to the pattern in the match, and then replaces the current term with the instantiation of the build pattern. Note that the variable bindings are propagated from the match to the build.

Stratego provides syntactic sugar for various combinations of match and build. We'll explore these in the rest of this chapter.

Plus(Var("a"),Int("3")) 
stratego> (Plus(e1, e2) -> Plus(e2, e1)) 
Plus(Int("3"),Var("a"))

stratego> !Plus(Var("a"),Int("3"))
Plus(Var("a"),Int("3"))
stratego> (Plus(e1,e2) -> Plus(e2,e1))
Plus(Int("3"),Var("a"))

stratego> :binding e1
e1 is bound to Var("a")
stratego> :binding e2
e2 is bound to Int("3")

stratego> !Plus(Var("a"),Var("b"))
Plus(Var("a"),Var("b"))
stratego> (Plus(e1,e2) -> Plus(e2,e1))
command failed

stratego> !Plus(Var("a"),Int("3"))
Plus(Var("a"),Int("3"))
stratego> {e3,e4 : (Plus(e3,e4) -> Plus(e4,e3))}
Plus(Var("a"),Int("3"))
stratego> :binding e3 
e3 is not bound to a term

stratego> !Plus(Var("a"),Var("b"))
Plus(Var("a"),Var("b"))
stratego> {e3,e4 : (Plus(e3,e4) -> Plus(e4,e3))}
Plus(Var("b"),Var("a"))

stratego> SwapArgs = {e1,e2 : (Plus(e1,e2) -> Plus(e2,e1))}
stratego> !Plus(Var("a"),Int("3"))
Plus(Var("a"),Int("3"))
stratego> SwapArgs 
Plus(Int("3"),Var("a"))

SwapArgs = {e1,e2 : (Plus(e1,e2) -> Plus(e2,e1))}

SwapArgs = (Plus(e1,e2) -> Plus(e2,e1))

let  SwapArgs = (Plus(e1,e2) -> Plus(e2,e1))  in ... end

Plus(Int("14"),Int("3"))
stratego> where(?Plus(Int(i),Int(j)); <addS>(i,j) => k)
Plus(Int("14"),Int("3"))
stratego> :binding i 
i is bound to "14"
stratego> :binding k 
k is bound to "17"

stratego> EvalPlus: Plus(Int(i),Int(j)) -> Int(k) where !(i,j); addS; ?k
stratego> !Plus(Int("14"),Int("3"))
Plus(Int("14"),Int("3"))
stratego> EvalPlus
Int("17")

L : p1 -> p2 where s

L = ?p1; where(s); !p2

EvalPlus : Add(Int(i),Int(j)) -> Int(k) where !(i,j); addS; ?k

EvalPlus = ?Add(Int(i),Int(j)); where(!(i,j); addS; ?k); !Int(k)

\ p1 -> p2 where s \

{x1,...,xn : (p1 -> p2 where s)}

stratego> ![(1,2),(3,4),(5,6)]
[(1,2),(3,4),(5,6)]
stratego> map(\ (x, y) -> x \ )
[1,3,5]

One frequently occuring scenario is that of applying a strategy to a term and then matching the result against a pattern. This typically occurs in the condition of a rule. In the constant folding example above we saw this scenario:

EvalPlus : Add(Int(i),Int(j)) -> Int(k) where !(i,j); addS; ?k

In the condition, first the term (i,j) is built, then the strategy addS is applied to it, and finally the result is matched against the pattern k.

To improve the readability of such expressions, the following two constructs are provided. The operation <s> p captures the notion of applying a strategy to a term, i.e., the scenario !p; s. The operation s => p capture the notion of applying a strategy to the current subject term and then matching the result against the pattern p, i.e., s; ?p. The combined operation <s> p1 => p2 thus captures the notion of applying a strategy to a term p1 and matching the result against p2, i.e, !t1; s; ?t2. Using this notation we can improve the constant folding rule above as

EvalPlus : Add(Int(i),Int(j)) -> Int(k) where <add>(i,j) => k

Applying Strategies in Build.  Sometimes it useful to apply a strategy directly to a subterm of a pattern, for example in the right-hand side of a rule, instead of computing a value in a condition, binding the result to a variable, and then using the variable in the build pattern. The constant folding rule above, for example, could be further simplified by directly applying the addition in the right-hand side:

EvalPlus : Add(Int(i),Int(j)) -> Int(<add>(i,j))

This abbreviates the conditional rule above. In general, a strategy application in a build pattern can always be expressed by computing the application before the build and binding the result to a new variable, which then replaces the application in the build pattern.

Another example is the following definition of the map(s) strategy, which applies a strategy to each term in a list:

map(s) : [] -> []
map(s) : [x | xs] -> [<s> x | <map(s)> xs]

Term wrapping and projection are concise idioms for constructing terms that wrap the current term and for extracting subterms from the current term.

3
stratego> !(<id>,<id>)
(3,3)
stratego> !(<Fst; inc>,<Snd>)
(4,3)
stratego> !"foobar"
"foobar"
stratego> !Call(<id>, [])
Call("foobar", [])
stratego> mod2 = <mod>(<id>,2)
stratego> !6
6
stratego> mod2
0

{x: where(s => x); !p[x]}  

\{x: where(id => x); !Foo(Bar(x))}

map(?FunDec(<id>,_,_))

[1,2,3]
stratego> ?[_|<id>]
[2,3]
stratego> !Call("foobar", [])
Call("foobar", [])
stratego> ?Call(<id>, [])
"foobar"

{x: ?p[x]; <s> x}

We have seen that Stratego makes the atomic actions of transformations, matching and building terms, available to Stratego programmers. A number of higher-level concepts, including rewrite rules, are implemented by translation to these basic actions.

In Chapter 16 we saw the following definition of the map strategy, which applies a strategy to each element of a list:

map(s) : [] -> []
map(s) : [x | xs] -> [<s> x | <map(s)> xs]

The definition uses explicit recursive calls to the strategy in the right-hand side of the second rule. What map does is to traverse the list in order to apply the argument strategy to all elements. We can use the same technique to other term structures as well.

We will explore the definition of traversals using the propositional formulae from Chapter 13, where we introduced the following rewrite rules:

module prop-rules
imports libstrategolib prop
rules
  DefI : Impl(x, y)       -> Or(Not(x), y)
  DefE : Eq(x, y)         -> And(Impl(x, y), Impl(y, x))
  DN   : Not(Not(x))      -> x
  DMA  : Not(And(x, y))   -> Or(Not(x), Not(y))
  DMO  : Not(Or(x, y))    -> And(Not(x), Not(y))
  DAOL : And(Or(x, y), z) -> Or(And(x, z), And(y, z))
  DAOR : And(z, Or(x, y)) -> Or(And(z, x), And(z, y))
  DOAL : Or(And(x, y), z) -> And(Or(x, z), Or(y, z))
  DOAR : Or(z, And(x, y)) -> And(Or(z, x), Or(z, y))

In Chapter 13 we saw how a functional style of rewriting could be encoded using extra constructors. In Stratego we can achieve a similar approach by using rule names, instead of extra constructors. Thus, one way to achieve normalization to disjunctive normal form, is the use of an explicitly programmed traversal, implemented using recursive rules, similarly to the map example above:

module prop-dnf4
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
rules
  dnf : True       ->          True
  dnf : False      ->          False
  dnf : Atom(x)    ->          Atom(x)
  dnf : Not(x)     -> <dnfred> Not (<dnf>x)
  dnf : And(x, y)  -> <dnfred> And (<dnf>x, <dnf>y)
  dnf : Or(x, y)   ->          Or  (<dnf>x, <dnf>y)  
  dnf : Impl(x, y) -> <dnfred> Impl(<dnf>x, <dnf>y)
  dnf : Eq(x, y)   -> <dnfred> Eq  (<dnf>x, <dnf>y)
strategies
  dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)

The dnf rules recursively apply themselves to the direct subterms and then apply dnfred to actually apply the rewrite rules.

We can reduce this program by abstracting over the base cases. Since there is no traversal into True, False, and Atoms, these rules can be be left out.

module prop-dnf5
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
rules
  dnft : Not(x)     -> <dnfred> Not (<dnf>x)
  dnft : And(x, y)  -> <dnfred> And (<dnf>x, <dnf>y)
  dnft : Or(x, y)   ->          Or  (<dnf>x, <dnf>y)  
  dnft : Impl(x, y) -> <dnfred> Impl(<dnf>x, <dnf>y)
  dnft : Eq(x, y)   -> <dnfred> Eq  (<dnf>x, <dnf>y)
strategies
  dnf    = try(dnft)
  dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)

The dnf strategy is now defined in terms of the dnft rules, which implement traversal over the constructors. By using try(dnft), terms for which no traversal rule has been specified are not transformed.

We can further simplify the definition by observing that the application of dnfred does not necessarily have to take place in the right-hand side of the traversal rules.

module prop-dnf6
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
rules
  dnft : Not(x)     -> Not (<dnf>x)
  dnft : And(x, y)  -> And (<dnf>x, <dnf>y)
  dnft : Or(x, y)   -> Or  (<dnf>x, <dnf>y)
  dnft : Impl(x, y) -> Impl(<dnf>x, <dnf>y)
  dnft : Eq(x, y)   -> Eq  (<dnf>x, <dnf>y)
strategies
  dnf    = try(dnft); dnfred
  dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)

In this program dnf first calls dnft to transform the subterms of the subject term, and then calls dnfred to apply the transformation rules (and possibly a recursive invocation of dnf).

The program above has two problems. First, the traversal behaviour is mostly uniform, so we would like to specify that more concisely. We will address that concern below. Second, the traversal is not reusable, for example, to define a conjunctive normal form transformation. This last concern can be addressed by factoring out the recursive call to dnf and making it a parameter of the traversal rules.

module prop-dnf7
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
rules
  proptr(s) : Not(x)     -> Not (<s>x)
  proptr(s) : And(x, y)  -> And (<s>x, <s>y)
  proptr(s) : Or(x, y)   -> Or  (<s>x, <s>y)  
  proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y)
  proptr(s) : Eq(x, y)   -> Eq  (<s>x, <s>y)
strategies
  dnf    = try(proptr(dnf)); dnfred
  dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)
  cnf    = try(proptr(cnf)); cnfred
  cnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf)

Now the traversal rules are reusable and used in two different transformations, by instantiation with a call to the particular strategy in which they are used (dnf or cnf).

But we can do better, and also make the composition of this strategy reusable.

module prop-dnf8
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
rules
  proptr(s) : Not(x)     -> Not (<s>x)
  proptr(s) : And(x, y)  -> And (<s>x, <s>y)
  proptr(s) : Or(x, y)   -> Or  (<s>x, <s>y)
  proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y)
  proptr(s) : Eq(x, y)   -> Eq  (<s>x, <s>y)
strategies
  propbu(s) = proptr(propbu(s)); s
strategies
  dnf    = propbu(dnfred)
  dnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf)
  cnf    = propbu(cnfred)
  cnfred = try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf)

That is, the propbu(s) strategy defines a complete bottom-up traversal over propostion terms, applying the strategy s to a term after transforming its subterms. The strategy is completely independent of the dnf and cnf transformations, which instantiate the strategy using the dnfred and cnfred strategies.

Come to think of it, dnfred and cnfred are somewhat useless now and can be inlined directly in the instantiation of the propbu(s) strategy:

module prop-dnf9
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
rules
  proptr(s) : Not(x)     -> Not (<s>x)
  proptr(s) : And(x, y)  -> And (<s>x, <s>y)
  proptr(s) : Or(x, y)   -> Or  (<s>x, <s>y)
  proptr(s) : Impl(x, y) -> Impl(<s>x, <s>y)
  proptr(s) : Eq(x, y)   -> Eq  (<s>x, <s>y)
strategies
  propbu(s) = proptr(propbu(s)); s
strategies
  dnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf))
  cnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))

Now we have defined a transformation independent traversal strategy that is specific for proposition terms.

Next we consider cheaper ways for defining the traversal rules, and then ways to get completely rid of them.

The definition of the traversal rules above frequently occurs in the definition of transformation strategies. Congruence operators provide a convenient abbreviation of precisely this operation. A congruence operator applies a strategy to each direct subterm of a specific constructor. For each n-ary constructor c declared in a signature, there is a corresponding congruence operator c(s1 , ..., sn), which applies to terms of the form c(t1 , ..., tn) by applying the argument strategies to the corresponding argument terms. A congruence fails if the application of one the argument strategies fails or if constructor of the operator and that of the term do not match.

Example.  For example, consider the following signature of expressions:

module expressions
signature
  sorts Exp
  constructors
    Int   : String -> Exp
    Var   : String -> Exp
    Plus  : Exp * Exp -> Exp
    Times : Exp * Exp -> Exp

The following Stratego Shell session applies the congruence operators Plus and Times to a term:

stratego> import expressions
stratego> !Plus(Int("14"),Int("3"))
Plus(Int("14"),Int("3"))
stratego> Plus(!Var("a"), id)
Plus(Var("a"),Int("3"))
stratego> Times(id, !Int("42"))
command failed

The first application shows how a congruence transforms a specific subterm, that is the strategy applied can be different for each subterm. The second application shows that a congruence only succeeds for terms constructed with the same constructor.

The import at the start of the session is necessary to declare the constructors used; the definitions of congruences are derived from constructor declarations. Forgetting this import would lead to a complaint about an undeclared operator:

stratego> !Plus(Int("14"),Int("3"))
Plus(Int("14"),Int("3"))
stratego> Plus(!Var("a"), id)
operator Plus/(2,0) not defined
command failed

Defining Traversals with Congruences.  Now we return to our dnf/cnf example, to see how congruence operators can help in their implementation. Since congruence operators basically define a one-step traversal for a specific constructor, they capture the traversal rules defined above. That is, a traversal rule such as

proptr(s) : And(x, y) -> And(<s>x, <s>y)

can be written by the congruence And(s,s). Applying this to the prop-dnf program we can replace the traversal rules by congruences as follows:

module prop-dnf10
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
strategies
  proptr(s) = Not(s) <+ And(s, s) <+ Or(s, s) <+ Impl(s, s) <+ Eq(s, s)
  propbu(s) = proptr(propbu(s)); s
strategies
  dnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf))
  cnf = propbu(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))

Observe how the five traversal rules have been reduced to five congruences which fit on a single line.

Traversing Tuples and Lists.  Congruences can also be applied to tuples, (s1,s2,...,sn), and lists, [s1,s2,...,sn]. A special list congruence is [] which 'visits' the empty list. As an example, consider again the definition of map(s) using recursive traversal rules:

map(s) : [] -> []
map(s) : [x | xs] -> [<s> x | <map(s)> xs]

Using list congruences we can define this strategy as:

map(s) = [] <+ [s | map(s)]

The [] congruence matches an empty list. The [s | map(s)] congruence matches a non-empty list, and applies s to the head of the list and map(s) to the tail. Thus, map(s) applies s to each element of a list:

stratego> import liblib
stratego> ![1,2,3]
[1,2,3]
stratego> map(inc)
[2,3,4]

Note that map(s) only succeeds if s succeeds for each element of the list. The fetch and filter strategies are variations on map that use the failure of s to list elements.

fetch(s) = [s | id] <+ [id | fetch(s)]

The fetch strategy traverses a list until it finds a element for which s succeeds and then stops. That element is the only one that is transformed.

filter(s) = [] + ([s | filter(s)] <+ ?[ |<id>]; filter(s))

The filter strategy applies s to each element of a list, but only keeps the elements for which it succeeds.

stratego> import liblib
stratego> even = where(<eq>(<mod>(<id>,2),0))
stratego> ![1,2,3,4,5,6,7,8]
[1,2,3,4,5,6,7,8]
stratego> filter(even)
[2,4,6,8]

Format Checking.  Another application of congruences is in the definition of format checkers. A format checker describes a subset of a term language using a recursive pattern. This can be used to verify input or output of a transformation, and for documentation purposes. Format checkers defined with congruences can check subsets of signatures or regular tree grammars. For example, the subset of terms of a signature in a some normal form.

As an example, consider checking the output of the dnf and cnf transformations.

conj(s) = And(conj(s), conj(s)) <+ s
disj(s) = Or (disj(s), disj(s)) <+ s

// Conjunctive normal form
conj-nf = conj(disj(Not(Atom(x)) <+ Atom(x)))

// Disjunctive normal form
disj-nf = disj(conj(Not(Atom(x)) <+ Atom(x)))

The strategies conj(s) and disj(s) check that the subject term is a conjunct or a disjunct, respectively, with terms satisfying s at the leaves. The strategies conj-nf and disj-nf check that the subject term is in conjunctive or disjunctive normal form, respectively.

Using congruence operators we constructed a generic, i.e. transformation independent, bottom-up traversal for proposition terms. The same can be done for other data types. However, since the sets of constructors of abstract syntax trees of typical programming languages can be quite large, this may still amount to quite a bit of work that is not reusable across data types; even though a strategy such as `bottom-up traversal', is basically data-type independent. Thus, Stratego provides generic traversal by means of several generic one-step descent operators. The operator all, applies a strategy to all direct subterms. The operator one, applies a strategy to one direct subterm, and the operator some, applies a strategy to as many direct subterms as possible, and at least one.

stratego> !Plus(Int("14"),Int("3"))
Plus(Int("14"),Int("3"))
stratego> all(!Var("a"))
Plus(Var("a"),Var("a"))
stratego> !Times(Var("b"),Int("3"))
Times(Var("b"),Int("3"))
stratego> all(!Var("z"))
Times(Var("z"),Var("z"))

proptr(s) = Not(s) <+ And(s, s) <+ Or(s, s) <+ Impl(s, s) <+ Eq(s, s)
propbu(s) = proptr(propbu(s)); s

propbu(s) = all(propbu(s)); s

bottomup(s) = all(bottomup(s)); s

module prop-dnf11
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
strategies
  dnf = bottomup(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR); dnf))
  cnf = bottomup(try(DN <+ (DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR); cnf))

dnf = bottomup(try(dnf-rules; dnf))
cnf = bottomup(try(cnf-rules; cnf))

innermost(s) = bottomup(try(s; innermost(s)))

module prop-dnf12
imports libstrategolib prop-rules
strategies
  main = io-wrap(dnf)
strategies
  dnf = innermost(DN <+ DefI <+ DefE <+ DMA <+ DMO <+ DAOL <+ DAOR)
  cnf = innermost(DN <+ DefI <+ DefE <+ DMA <+ DMO <+ DOAL <+ DOAR)

stratego> !Plus(Int("14"),Int("3"))
Plus(Int("14"),Int("3"))
stratego> one(!Var("a"))
Plus(Var("a"),Int("3"))
stratego> one(\ Int(x) -> Int(<addS>(x,"1")) \ )
Plus(Var("a"),Int("4"))
stratego> one(?Plus(_,_))
command failed

oncetd(s) = s <+ one(oncetd(s))

contains(|t) = oncetd(?t)

oncebu(s)  = one(oncebu(s)) <+ s
spinetd(s) = s; try(one(spinetd(s)))
spinebu(s) = try(one(spinebu(s))); s

reduce(s)     = repeat(rec x(one(x) + s)) 
outermost(s)  = repeat(oncetd(s)) 
innermostI(s) = repeat(oncebu(s))

sometd(s) = s <+ some(sometd(s)) 
somebu(s) = some(somebu(s)) <+ s

reduce-par(s) = repeat(rec x(some(x) + s))

Above we have seen the basic mechanisms for defining traversals in Stratego: custom traversal rules, data-type specific congruence operators, and generic traversal operators. Term traversals can be categorized into classes according to how much of the term they traverse and to which parts of the term they modify. We will consider a number of idioms and standard strategies from the Stratego Library that are useful in the definition of traversals.

bottomup(s) = all(bottomup(s)); s

topdown(s) = s; all(topdown(s))

downup(s) = s; all(downup(s)); s

downup(s1, s2) = s1; all(downup(s1, s2)); s2

topdown(try(R1 <+ R2 <+ ...))

T : And(True(), x) -> x
T : And(x, True()) -> x
T : And(False(), x) -> False()
T : And(x, False()) -> False()
T : Or(True(), x) -> True()
T : Or(x, True()) -> True()
T : Or(False(), x) -> x
T : Or(x, False()) -> x
T : Not(False()) -> True()
T : Not(True()) -> False()

eval = bottomup(try(T))

eval2 = topdown(try(T)) // bad strategy

stratego> !And(True(), Not(Or(False(), True())))
And(True,Not(Or(False,True)))
stratego> eval
False
stratego> !And(True(), Not(Or(False(), True())))
And(True,Not(Or(False,True)))
stratego> eval2
Not(True)

DefI : Impl(x, y) -> Or(Not(x), y)
DefE : Eq(x, y) -> And(Impl(x, y), Impl(y, x))

desugar = topdown(try(DefI <+ DefE))

desugar2 = bottomup(try(DefI <+ DefE))   // bad strategy

stratego> !Eq(Atom("p"), Atom("q"))
Eq(Atom("p"),Atom("q"))
stratego> desugar
And(Or(Not(Atom("p")),Atom("q")),Or(Not(Atom("q")),Atom("p")))
stratego> !Eq(Atom("p"), Atom("q"))
Eq(Atom("p"),Atom("q"))
stratego> desugar2
And(Impl(Atom("p"),Atom("q")),Impl(Atom("q"),Atom("p")))

DefT  : True() -> Impl(False(), False())
DefN  : Not(x) -> Impl(x, False())
DefA2 : And(x, y) -> Not(Impl(x, Not(y)))
DefO1 : Or(x, y) -> Impl(Not(x), y)
DefE  : Eq(x, y) -> And(Impl(x, y), Impl(y, x))

impl-nf = topdown(repeat(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))

impl-nf2 = topdown(try(DefT <+ DefN <+ DefA2 <+ DefO1 <+ DefE))  // bad strategy

stratego> !And(Atom("p"),Atom("q"))
And(Atom("p"),Atom("q"))
stratego> impl-nf
Impl(Impl(Atom("p"),Impl(Atom("q"),False)),False)
stratego> !And(Atom("p"),Atom("q"))
And(Atom("p"),Atom("q"))
stratego> impl-nf2
Not(Impl(Atom("p"),Impl(Atom("q"),False)))

bottomup-para(s) = <s>(<id>, <all(bottomup-para(s))>)

simplify =
  innermost(R1 <+ ... <+ Rn)

innermost(s) = bottomup(try(s; innermost(s)))

simplify =
  innermost(A1 <+ ... <+ Ak)
  ; innermost(B1 <+ ... <+ Bl)
  ; ...
  ; innermost(C1 <+ ... <+ Cm)

simplify =
  topdown(try(A1 <+ ... <+ Ak))
  ; innermost(B1 <+ ... <+ Bl)
  ; ...
  ; bottomup(repeat(C1 <+ ... <+ Cm))

transformation =
  special-case1
  <+ special-case2
  <+ special-case3
  <+ all(transformation); reduce

reduce = ...

module propconst
imports 
  liblib

signature
  constructors
    Var    : String -> Exp
    Plus   : Exp * Exp -> Exp
    Assign : String * Exp -> Stat
    If     : Exp * Stat * Stat -> Stat
    While  : Exp * Stat -> Stat
    
strategies

  propconst = 
    PropConst 
    <+ propconst-assign
    <+ propconst-if
    <+ propconst-while
    <+ all(propconst); try(EvalBinOp) 

  EvalBinOp : 
    Plus(Int(i), Int(j)) -> Int(k) where <addS>(i,j) => k

  EvalIf :
    If(Int("0"), s1, s2) -> s2

  EvalIf :
    If(Int(i), s1, s2) -> s1 where <not(eq)>(i, "0")

  propconst-assign = 
    Assign(?x, propconst => e)
    ; if <is-value> e then
        rules( PropConst : Var(x) -> e )
      else
        rules( PropConst :- Var(x) )
      end

  propconst-if = 
    If(propconst, id, id)
    ; (EvalIf; propconst
       <+ (If(id, propconst, id) /PropConst\ If(id,id,propconst)))

  propconst-while = 
    While(id,id)
    ; (/PropConst\* While(propconst, propconst))

  is-value = Int(id)

Block([
  Assign("x", Int("1")),
  Assign("y", Int("42")),
  Assign("z", Plus(Var("x"), Var("y"))),
  If(Plux(Var("a"), Var("z")),
     Assign("b", Plus(Var("x"), Int("1"))),
     Block([
       Assign("z", Int("17")),
       Assign("b", Int("2"))
     ])),
  Assign("c", Plus(Var("b"), Plus(Var("z"), Var("y"))))
])

stratego> import libstrategolib
stratego> import propconst
stratego> <ReadFromFile> "foo.prg"
...
stratego> propconst
Block([Assign("x",Int("1")),Assign("y",Int("42")),Assign("z",Int("43")),
If(Plux(Var("a"),Int("43")),Assign("b",Int("2")),Block([Assign("z",
Int("17")),Assign("b",Int("2"))])),Assign("c",Plus(Int("2"),Plus(
Var("z"),Int("42"))))])

stratego> <ReadFromFile> "foo.prg"
...
stratego> propconst; <WriteToTextFile> ("foo-pc.prg", <id>)
...
stratego> :quit
...
$ pp-aterm -i foo-pc.prg
Block(
  [ Assign("x", Int("1"))
  , Assign("y", Int("42"))
  , Assign("z", Int("43"))
  , If(
      Plux(Var("a"), Int("43"))
    , Assign("b", Int("2"))
    , Block(
        [Assign("z", Int("17")), Assign("b", Int("2"))]
      )
    )
  , Assign(
      "c"
    , Plus(Int("2"), Plus(Var("z"), Int("42")))
    )
  ]
)

topdownS(s, stop: (a -> a) * b -> b) =
  rec x(s; (stop(x) <+ all(x)))

bottomupS(s, stop: (a -> a) * b -> b) =
  rec x((stop(x) <+ all(x)); s)

downupS(s, stop: (a -> a) * b -> b) =
  rec x(s; (stop(x) <+ all(x)); s)

downupS(s1, s2, stop: (a -> a) * b -> b) =
  rec x(s1; (stop(x) <+ all(x)); s2)

oncetd(s) = s <+ one(oncetd(s))
oncebu(s) = one(oncebu(s)) <+ s

sometd(s) = s <+ some(sometd(s))
somebu(s) = some(somebu(s)) <+ s

manybu(s) = rec x(some(x); try(s) <+ s)
manytd(s) = rec x(s; all(try(x)) <+ some(x))

somedownup(s) = rec x(s; all(x); try(s) <+ some(x); try(s))

  alltd(s) = s <+ all(alltd(s))

transformation =
  alltd(
    trigger-transformation
    ; innermost(A1 <+ ... <+ An) 
  )

alldownup2(s1, s2) = rec x((s1 <+ all(x)); s2)
alltd-fold(s1, s2) = rec x(s1 <+ all(x); s2)

leaves(s, is-leaf, skip: a * (a -> a) -> a) =
  rec x((is-leaf; s) <+ skip(x) <+ all(x))

leaves(s, is-leaf) =
  rec x((is-leaf; s) <+ all(x))

spinetd(s)  = s; try(one(spinetd(s)))
spinebu(s)  = try(one(spinebu(s))); s
spinetd'(s) = s; (one(spinetd'(s)) + all(fail))
spinebu'(s) = (one(spinebu'(s)) + all(fail)); s

somespinetd(s) = rec x(s; try(some(x)))
somespinebu(s) = rec x(try(some(x)); s)
spinetd'(s)    = rec x(s; (one(x) + all(fail)))
spinebu'(s)    = rec x((one(x) + all(fail)); s)

We have seen that tree traversals can be defined in several ways. Recursive traversal rules allow finegrained specification of a traversal, but usually require too much boilerplate code. Congruence operators provide syntactic sugar for traversal rules that apply a strategy to each direct subterm of a term. The generic traversal operators all, one, and some allow consise, data-type independent implementation of traversals. A host of traversal strategies can be obtained by a combination of the strategy combinators from the previous chapters with these traversal operators.

We start with considering type-unifying operations on lists.

Sum.  Reducing a list to a value can be conveniently expressed by means of a fold, which has as parameters operations for reducing the list constructors. The foldr/2 strategy reduces a list by replacing each Cons by an application of s2, and the empty list by s1.

foldr(s1, s2) = 
  []; s1 <+ \ [y|ys] -> <s2>(y, <foldr(s1, s2)> ys) \ 

Thus, when applied to a list with three terms the result is

<foldr(s1,s2)> [t1,t2,t3] => <s2>(t1, <s2>(t2, <s2>(t3, <s1> [])))

A typical application of foldr/2 is sum, which reduces a list to the sum of its elements. It sums the elements of a list of integers, using 0 for the empty list and add to combine the head of a list and the result of folding the tail.

sum = foldr(!0, add)

The effect of sum is illustrated by the following application:

<foldr(!0,add)> [1,2,3] => <add>(1, <add>(2, <add>(3, <!0> []))) => 6

Note the build operator for replacing the empty list with 0; writing foldr(0, add) would be wrong, since 0 by itself is a congruence operator, which basically matches the subject term with the term 0 (rather than replacing it).

Size.  The foldr/2 strategy does not touch the elements of a list. The foldr/3 strategy is a combination of fold and map that extends foldr/2 with a parameter that is applied to the elements of the list.

foldr(s1, s2, f) = 
  []; s1 <+ \ [y|ys] -> <s2>(<f>y, <foldr(s1,s2,f)>ys) \ 

Thus, when applying it to a list with three elements, we get:

<foldr(s1,s2)> [t1,t2,t3] => <s2>(<f>t1, <s2>(<f>t2, <s2>(<f>t3, <s1> [])))

Now we can solve our first example problem term-size. The size of a list is its length, which corresponds to the sum of the list with the elements replaced by 1.

length = foldr(!0, add, !1)

Number of occurrences.  The number of occurrences in a list of terms that satisfy some predicate, entails only counting those elements in the list for which the predicate succeeds. (Where a predicate is implemented with a strategy that succeeds only for the elements in the domain of the predicate.) This follows the same pattern as counting the length of a list, but now only counting the elements for which s succeeds.

list-occurrences(s) = foldr(!0, add, s < !1 + !0)

Using list-occurrences and a match strategy we can count the number of variables in a list:

list-occurrences(?Var(_))

Collect.  The next problem is to collect all terms for which a strategy succeeds. We have already seen how to do this for lists. The filter strategy reduces a list to the elements for which its argument strategy succeeds.

filter(s) = [] <+ [s | filter(s)] <+ ?[ |<filter(s)>]

Collecting the variables in a list is a matter of filtering with the ?Var(_) match.

filter(?Var(_)) 

The final problem, collecting the free variables in a term, does not really have a counter part in lists, but we can mimick this if we consider having two lists; where the second list is the one with the bound variables that should be excluded.

(filter(?Var(_)),id); diff

This collects the variables in the first list and subtracts the variables in the second list.

We have seen how to do typical analysis transformations on lists. How can we generalize this to arbitrary terms? The general idea of a folding operator is that it replaces the constructors of a data-type by applying a function to combine the reduced arguments of constructor applications. For example, the following definition is a sketch for a fold over abstract syntax trees:

fold-exp(binop, assign, if, ...) = rec f( 
  fold-binop(f, binop)
  <+ fold-assign(f, assign)
  <+ fold-if(f, if)
  <+ ... )

fold-binop(f, s)  : BinOp(op, e1, e2) -> <s>(op, <f>e1, <f>e2)
fold-assign(f, s) : Assign(e1, e2)    -> <s>(<f>e1, <f>e2)
fold-if(f, s)     : If(e1, e2, e3)    -> <s>(<f>e1, <f>e2, <f>e3)

For each constructor of the data-type the fold has an argument strategy and a rule that matches applications of the constructor, which it replaces with an application of the strategy to the tuple of subterms reduced by a recursive invocation of the fold.

Instantation of this strategy requires a rule for each constructor of the data-type. For instance, the following instantiation defines term-size using fold-exp by providing rules that sum up the sizes of the subterms and add one (inc) to account for the node itself.

term-size  = fold-exp(BinOpSize, AssignSize, IfSize, ...)

BinOpSize  : (Plus(), e1, e2) -> <add; inc>(e1, e2)
AssignSize : (e1, e2)         -> <add; inc>(e1, e2)
IfSize     : (e1, e2, e3)     -> <add; inc>(e1, <add>(e2, e3))

This looks suspiciously like the traversal rules in Chapter 17. Defining folds in this manner has several limitations. In the definition of fold, one parameter for each constructor is provided and traversal is defined explicitly for each constructor. Furthermore, in the instantiation of fold, one rule for each constructor is needed, and the default behaviour is not generically specified.

One solution would be to use the generic traversal strategy bottomup to deal with fold:

fold-exp(s) = bottomup(s) 

term-size   = fold-exp(BinOpSize <+ AssignSize <+ IfSize <+ ...) 

BinOpSize   : BinOp(Plus(), e1, e2) -> <add>(1, <add>(e1, e2))
AssignSize  : Assign(e1, e2)        -> <add>(e1, e2)
IfSize      : If(e1, e2, e3)        -> <add>(e1, <add>(e2, e3))

Although the recursive application to subterms is now defined generically , one still has to specify rules for the default behaviour.

Instead of having folding rules that are specific to a data type, such as

BinOpSize  : BinOp(op, e1, e2) -> <add>(1, <add>(e1, e2)) 
AssignSize : Assign(e1, e2)    -> <add>(1, <add>(e1, e2)) 

we would like to have a generic definition of the form

CSize : c(e1, e2, ...) -> <add>(e1, <add>(e2, ...)) 

This requires generic decomposition of a constructor application into its constructor and the list with children. This can be done using the # operator. The match strategy ?p1#(p2) decomposes a constructor application into its constructor name and the list of direct subterms. Matching such a pattern against a term of the form C(t1,...,tn) results in a match of "C" against p1 and a match of [t1,...,tn] against p2.

Plus(Int("1"), Var("2")) 
stratego> ?c#(xs)
stratego> :binding c
variable c bound to "Plus" 
stratego> :binding xs 
variable xs bound to [Int("1"), Var("2")]

Crush.  Using generic term deconstruction we can now generalize the type unifying operations on lists to arbitrary terms. In analogy with the generic traversal operators we need a generic one-level reduction operator. The crush/3 strategy reduces a constructor application by folding the list of its subterms using foldr/3.

crush(nul, sum, s) : c#(xs) -> <foldr(nul, sum, s)> xs

Thus, crush performs a fold-map over the direct subterms of a term. The following application illustrates what

<crush(s1, s2, f)> C(t1, t2) => <s2>(<f>t1, <s2>(<f>t2, <s1>[]))

The following Shell session instantiates this application in two ways:

stratego> import libstrategolib
stratego> !Plus(Int("1"), Var("2"))
Plus(Int("1"),Var("2"))

stratego> crush(id, id, id)
(Int("1"),(Var("2"),[]))

stratego> !Plus(Int("1"), Var("2"))
Plus(Int("1"),Var("2"))

stratego> crush(!Tail(<id>), !Sum(<Fst>,<Snd>), !Arg(<id>))
Sum(Arg(Int("1")),Sum(Arg(Var("2")),Tail([])))

The crush strategy is the tool we need to implement solutions for the example problems above.

Size.  Counting the number of direct subterms of a term is similar to counting the number of elements of a list. The definition of node-size is the same as the definition of length, except that it uses crush instead of foldr:

node-size = crush(!0, add, !1)

Counting the number of subterms (nodes) in a term is a similar problem. But, instead of counting each direct subterm as 1, we need to count its subterms.

term-size = crush(!1, add, term-size) 

The term-size strategy achieves this simply with a recursive call to itself.

stratego> <node-size> Plus(Int("1"), Var("2"))
2
stratego> <term-size> Plus(Int("1"), Var("2"))
5

Occurrences.  Counting the number of occurrences of a certain term in another term, or more generally, counting the number of subterms that satisfy some predicate is similar to counting the term size. However, only those terms satisfying the predicate should be counted. The solution is again similar to the solution for lists, but now using crush.

om-occurrences(s) = s < !1 + crush(!0, add, om-occurrences(s))

The om-occurrences strategy counts the outermost subterms satisfying s. That is, the strategy stops counting as soon as it finds a subterm for which s succeeds.

The following strategy counts all occurrences:

occurrences(s) = <add>(<s < !1 + !0>, <crush(!0, add, occurrences(s))>)

It counts the current term if it satisfies s and adds that to the occurrences in the subterms.

stratego> <om-occurrences(?Int(_))> Plus(Int("1"), Plus(Int("34"), Var("2")))
2
stratego> <om-occurrences(?Plus(_,_))> Plus(Int("1"), Plus(Int("34"), Var("2")))
1
stratego> <occurrences(?Plus(_,_))> Plus(Int("1"), Plus(Int("34"), Var("2")))
2

Collect.  Collecting the subterms that satisfy a predicate is similar to counting, but now a list of subterms is produced. The collect(s) strategy collects all outermost occurrences satisfying s.

collect(s) = ![<s>] <+ crush(![], union, collect(s)) 

When encountering a subterm for which s succeeds, a singleton list is produced. For other terms, the matching subterms are collected for each direct subterm, and the resulting lists are combined with union to remove duplicates.

A typical application of collect is the collection of all variables in an expression, which can be defined as follows:

get-vars = collect(?Var(_))

Applying get-vars to an expression AST produces the list of all subterms matching Var(_).

The collect-all(s) strategy collects all occurrences satisfying s.

collect-all(s) = 
  ![<s> | <crush(![], union, collect(s))>] <+ crush(![], union, collect(s))

If s succeeds for the subject term combines the subject term with the collected terms from the subterms.

Free Variables.  Collecting the variables in an expression is easy, as we saw above. However, when dealing with languages with variable bindings, a common operation is to extract only the free variables in an expression or block of statements. That is, the occurrences of variables that are not bound by a variable declaration. For example, in the expression

x + let var y := x + 1 in f(y, a + x + b) end 

the free variables are {x, a, b}, but not y, since it is bound by the declaration in the let. Similarly, in the function definition

function f(x : int) = let var y := h(x) in x + g(z) * y end 

the only free variable is z since x and y are declared.

Here is a free variable extraction strategy for Tiger expressions. It follows a similar pattern of mixing generic and data-type specific operations as we saw in Chapter 17. The crush alternative takes care of the non-special constructors, while ExpVars and FreeVars deal with the special cases, i.e. variables and variable binding constructs:

free-vars = 
  ExpVars 
  <+ FreeVars(free-vars) 
  <+ crush(![], union, free-vars) 

ExpVars : 
  Var(x) -> [x]

FreeVars(fv) : 
  Let([VarDec(x, t, e1)], e2) -> <union>(<fv> e1, <diff>(<fv> e2, [x])) 

FreeVars(fv) : 
  Let([FunctionDec(fdecs)], e2) -> <diff>(<union>(<fv> fdecs, <fv>e2), fs) 
  where <map(?FunDec(<id>,_,_,_))> fdecs => fs 

FreeVars(fv) : 
  FunDec(f, xs, t, e) -> <diff>(<fv>e, xs) 
  where <map(Fst)> xs => xs

The FreeVars rules for binding constructs use their fv parameter to recursively get the free variables from subterms, and they subtract the bound variables from any free variables found using diff.

We can even capture the pattern exhibited here in a generic collection algorithm with support for special cases:

collect-exc(base, special : (a -> b) * a -> b) = 
  base 
  <+ special(collect-exc(base, special)) 
  <+ crush(![], union, collect-exc(base, special)) 

The special parameter is a strategy parameterized with a recursive call to the collection strategy. The original definition of free-vars above, can now be replaced with

free-vars = collect-exc(ExpVars, FreeVars)

It can also be useful to construct terms generically. For example, in parse tree implosion, application nodes should be reduced to constructor applications. Hence build operators can also use the # operator. In a strategy !p1#(p2), the current subject term is replaced by a constructor application, where the constructor name is provided by p1 and the list of subterms by p2. So, if p1 evaluates to "C" and p2 evaluates to [t1,...,tn], the expression !p1#(p2) build the term C(t1,...,tn).

Imploding Parse Trees.  A typical application of generic term construction is the implosion of parse trees to abstract syntax trees performed by implode-asfix. Parse trees produced by sglr have the form:

appl(prod(sorts, sort, attrs([cons("C")])),[t1,...,tn]) 

That is, a node in a parse tree consists of an encoding of the original production from the syntax definition, and a list with subtrees. The production includes a constructor annotation cons("C") with the name of the abstract syntax tree constructor. Such a tree node should be imploded to an abstract syntax tree node of the form C(t1,...,tn). Thus, this requires the construction of a term with constructor C given the string with its name. The following implosion strategy achieves this using generic term construction:

implode = appl(id, map(implode)); Implode 
Implode : appl(prod(sorts, sort, attrs([cons(c)])), ts) -> c#(ts) 

The Implode rule rewrites an appl term to a constructor application, by extracing the constructor name from the production and then using generic term construction to apply the constructor.

Note that this is a gross over simplification of the actual implementation of implode-asfix. See the source code for the full strategy.

Generic term construction and deconstruction support the definition of generic analysis and generic translation problems. The generic solutions for the example problems term size, number of occurrences, and subterm collection demonstrate the general approach to solving these types of problems.

To appreciate the need for concrete syntax in program transformation, it is illuminating to constrast the use of concrete syntax with the traditional use of abstract syntax in a larger example. Program instrumentation is the extension of a program in a systematic way in order to obtain measurements during run-time. Instrumentation is used, for example, in debugging to get information about the run-time behaviour of a program, and in profiling to collect statistics about about run-time and call frequency of program elements. Here we consider a simple instrumentation scheme that instruments Tiger functions with calls to trace functions.

The following Stratego fragment shows rewrite rules that instrument a function f such that it prints f entry on entry of the function and f exit at the exit. The actual printing is delegated to the functions enterfun and exitfun. Functions are instrumented differently than procedures, since the body of a function is an expression statement and the return value is the value of the expression. It is not possible to just glue a print statement or function call at the end of the body. Therefore, a let expression is introduced, which introduces a temporary variable to which the body expression of the function is assigned. The code for the functions enterfun and exitfun is generated by rule IntroducePrinters. Note that the declarations of the Let generated by that rule have been omitted.

instrument = 
  topdown(try(TraceProcedure + TraceFunction))
  ; IntroducePrinters
  ; simplify

TraceProcedure :
  FunDec(f, x*, NoTp, e) ->
  FunDec(f, x*, NoTp,
         Seq([Call(Var("enterfun"),[String(f)]), e,
              Call(Var("exitfun"),[String(f)])]))

TraceFunction :
  FunDec(f, x*, Tp(tid), e) ->
  FunDec(f, x*, Tp(tid),
         Seq([Call(Var("enterfun"),[String(f)]),
              Let([VarDec(x,Tp(tid),NilExp)],
                  [Assign(Var(x), e),
                   Call(Var("exitfun"),[String(f)]),
                   Var(x)])]))

IntroducePrinters : 
  e -> Let(..., e)

The next program program fragment implements the same instrumentation transformation, but now it uses concrete syntax.

TraceProcedure :
  |[ function f(x*) = e ]| ->
  |[ function f(x*) = (enterfun(s); e; exitfun(s)) ]|
  where !f => s

TraceFunction :
  |[ function f(x*) : tid = e ]| ->
  |[ function f(x*) : tid =
       (enterfun(s);
        let var x : tid
         in x := e; exitfun(s); x
        end) ]|
  where new => x ; !f => s

IntroducePrinters :
  e -> |[ let var ind := 0
              function enterfun(name : string) = (
                ind := +(ind, 1);
                for i := 2 to ind do print(" ");
                print(name); print(" entry\\n"))
              function exitfun(name : string) = (
                for i := 2 to ind do print(" ");
                ind := -(ind, 1);
                print(name); print(" exit\\n"))
           in e end ]|

It is clear that the concrete syntax version is much more concise and easier to read. This is partly due to the fact that the concrete version is shorter than the abstract version: 225 bytes vs 320 bytes after eliminating all non-significant whitespace. However, the concrete version does not use much fewer lines. A more important reason for the increased understandability is that in order to read the concrete version it is not necessary to mentally translate the abstract syntax constructors into concrete ones. The implementation of IntroducePrinters is only shown in concrete syntax since its encoding in abstract syntax leads to unreadable code for code fragments of this size.

Note that these rewrite rules cannot be applied as such using simple innermost rewriting. After instrumenting a function declaration, it is still a function declaration and can thus be instrumented again. Therefore, we use a single pass topdown strategy for applying the rules.

The example gives rise to several observations. The concrete syntax version can be read without knowledge of the abstract syntax. On the other hand, the abstract syntax version makes the tree structure of the expressions explicit. The abstract syntax version is much more verbose and is harder to read and write. Especially the definition of large code fragments such as in rule IntroducePrinters is unattractive in abstract syntax.

The abstract syntax version implements the concrete syntax version. The concrete syntax version has all properties of the abstract syntax version: pattern matching, term structure, can be traversed, etc.. In short, the concrete syntax is just syntactic sugar for the abstract syntax.

Extension of the Meta Language.  The instrumentation rules make use of the concrete syntax of Tiger. However, program transformation should not be restricted to transformation of Tiger programs. Rather we would like to be able to handle arbitrary object languages. Thus, the object language or object languages that are used in a module should be a parameter to the compiler. The specification of instrumentation is based on the real syntax of Tiger, not on some combinators or infix expressions. This entails that the syntax of Stratego should be extended with the syntax of Tiger.

Meta-Variables.  The patterns in the transformation rules are not just fragments of Tiger programs. Rather some elements of these fragments are considered as meta-variables. For example in the term

|[ function f(x*) = e ]|

the identifiers f, x*, and e are not intended to be Tiger variables, but rather meta-variables, i.e., variables at the level of the Stratego specification, ranging over identifiers, lists of function arguments, and expresssions, respectively.

Antiquotation.  Instead of indicating meta-variables implicitly we could opt for an antiquotation mechanism that lets us splice in meta-level expressions into a concrete syntax fragment. For example, using ~ and ~* as antiquotation operators, a variant of rule TraceProcedure becomes:

TraceProcedure :
  |[ function ~f(~* x*) = ~e ]| -> 
  |[ function ~f(~* x*) = 
       (enterfun(~String(f)); ~e; exitfun(~String(f))) ]|

With such antiquotation operators it becomes possible to directly embed meta-level computations that produce a piece of code within a syntax fragment.

In the previous section we have seen how the extension of Stratego with concrete syntax for terms improves the readability of meta-programs. In this section we describe the techniques used to achieve this extension.

Meta([Syntax("StrategoTiger")])

module Stratego-Terms
exports
  context-free syntax
    Int                             -> Term {cons("Int")}
    String                          -> Term {cons("Str")}
    Var                             -> Term {cons("Var")}
    Id "(" {Term ","}* ")"          -> Term {cons("Op")}
    Term "->" Term                  -> Rule {cons("RuleNoCond")}
    Term "->" Term "where" Strategy -> Rule {cons("Rule")}

module StrategoTiger
imports Stratego [ Term => StrategoTerm
                   Var => StrategoVar
                   Id => StrategoId
                   StrChar => StrategoStrChar ]
imports Tiger Tiger-Variables
exports
  context-free syntax
    "|[" Dec     "]|"    -> StrategoTerm {cons("ToTerm"),prefer}
    "|[" TypeDec "]|"    -> StrategoTerm {cons("ToTerm"),prefer}
    "|[" FunDec  "]|"    -> StrategoTerm {cons("ToTerm"),prefer}
    "|[" Exp     "]|"    -> StrategoTerm {cons("ToTerm"),prefer}
    "~"  StrategoTerm    -> Exp          {cons("FromTerm"),prefer}
    "~*" StrategoTerm    -> {Exp ","}+   {cons("FromTerm")}
    "~*" StrategoTerm    -> {Exp ";"}+   {cons("FromTerm")}
    "~int:" StrategoTerm -> IntConst     {cons("FromTerm")}

"|[" Exp "]|" -> StrategoTerm {cons("ToTerm"),prefer}

module Tiger-Variables
exports
  variables
    [s][0-9]*      -> StrConst    {prefer}
    [xyzfgh][0-9]* -> Id          {prefer}
    [e][0-9]*      -> Exp         {prefer}
    "ta"[0-9]*     -> TypeAn      {prefer}
    "x"[0-9]* "*"  -> {FArg ","}+ {prefer}
    "d"[0-9]* "*"  -> Dec+        {prefer}
    "e"[0-9]* "*"  -> {Exp ";"}+  {prefer}

 |[ x := let d* in ~* e* end ]| -> |[ let d* in x := (~* e*) end ]|

Rule(ToTerm(Assign(Var(meta-var("x")),
                   Let(meta-var("d*"),FromTerm(Var("e*"))))),
     ToTerm(Let(meta-var("d*"),
                [Assign(Var(meta-var("x")),
                        Seq(FromTerm(Var("e*"))))])))

Rule(Op("Assign",[Op("Var",[Var("x")]),
                  Op("Let",[Var("d*"),Var("e*")])]),
     Op("Let",[Var("d*"),
               Op("Cons",[Op("Assign",[Op("Var",[Var("x")]),
                                       Op("Seq",[Var("e*")])]),
                          Op("Nil",[])])]))

Assign(Var(x),Let(d*,e*)) -> Let(d*,[Assign(Var(x),Seq(e*))])

Disambiguating Quotations.  Sometimes the fragments used within quotations are too small for the parser to be able to disambiguate them. In those cases it is useful to have alternative versions of the quotation operators that make the sort of the fragment explicit. A useful, although somewhat verbose, convention is to use the sort of the fragment as operator:

   "exp" "|[" Exp "]|" -> StrategoTerm {cons("ToTerm")}

Other Quotation Conventions.  The convention of using |[...]| and ~ as quotation and anti-quotation delimiters is inspired by the notation used in texts about semantics. It really depends on the application, the languages involved, and the `audience' what kind of delimiters are most appropriate.

The following notation was inspired by active web pages is developed. For instance, the following quotation %>...<% and antiquotation <%...%> delimiters are defined for use of XML in Stratego programs:

  context-free syntax
    "%>" Content "<%" -> StrategoTerm {cons("ToTerm"),prefer}
    "<%=" StrategoTerm     "%>" -> Content {cons("FromTerm")}
    "<%"  StrategoStrategy "%>" -> Content {cons("FromApp")}

Desugaring Patterns.  Some meta-programs first desugar a program before transforming it further. This reduces the number of constructs and shapes a program can have. For example, the Tiger binary operators are desugared to prefix form:

  DefTimes : |[ e1 * e2 ]|  -> |[ *(e1, e2) ]|
  DefPlus  : |[ e1 + e2 ]|  -> |[ +(e1, e2) ]|

or in abstract syntax

  DefPlus : Plus(e1, e2) -> BinOp(PLUS, e1, e2)

This makes it easy to write generic transformations for binary operators. However, all subsequent transformations on binary operators should then be done on these prefix forms, instead of on the usual infix form. However, users/meta-programmers think in terms of the infix operators and would like to write rules such as

  Simplify : |[ e + 0 ]| -> |[ e ]|

However, this rule will not match since the term to which it is applied has been desugared. Thus, it might be desirable to desugar embedded abstract syntax with the same rules with which programs are desugared. This phenomenon occurs in many forms ranging from removing parentheses and generalizing binary operators as above, to decorating abstract syntax trees with information resulting from static analysis such as type checking.

We have seen how the use of concrete object syntax can make the definition of transformation rules more readable.