Stratego Transformations in the Spoofax Eclipse IDE

The Stratego Tutorial/Reference manual in the official Spoofax documentation presents a comprehensive overview of the Stratego approach to abstract syntax tree (AST) transformations. It employs a running example of an abstract syntax intended to represent classical Propositional Logic, which we will dub here the “Spoofax Propositional Language.” The manual introduces the concepts of rules and strategies for applying them, and then shows how both of those facilities can be created from more primitive operations of term matching and replacement. Every step of the way is illustrated with actual, working Stratego programs.

This Gitea repository provides a working implementation of most of the examples in the manual. It can be cloned as an Eclipse project (note the git root is at the project level rather than in the directory above the project, as may be more common; in other words, this repository should be cloned within an existing Eclipse workspace, rather than as the workspace itself). Within that project, all of the examples from the Stratego Tutorial manual that employ the propositional language (see below), starting from Section 4 on, can be executed directly. This repository does not attempt to implement the portion of examples dealing with an arithmetical/imperative language (except in a couple of isolated instances in which the relevant phenomenon is recast in the propositional language).

Preliminaries

I recommend working with a complete pre-built Eclipse installation of Spoofax as provided by the Spoofax project, for example one that you can download from their development release page. Sometimes I have had difficulty getting the examples in this repository working starting from plain Eclipse and installing Spoofax in it using the Spoofax update site.

If at any point in using the examples things appear to stop working, and especially if the Spoofax menu item disappears or the Spoofax menu turns into a thin white rectangle with no items to select, try the following:

Build the project and try again.
Clean the workspace, and when it is done, build the project again and try again.
Right click on the project, select Maven > Update Project, make sure everything is checked except “Offline” and “Force update of Snapshots/Releases”, and then click “OK”. When it is done, clean the workspace, then build the project and try again.
If that still hasn’t done it, restart (the Spoofax version of!) Eclipse and clean the workspace, then build the project and try again.

Running with a version of Spoofax later than 2.5.13 (I was using a 2.6.0 development snapshot), the Spoofax menu would always come back into proper operation at some point in the above process.

Abstract syntax

With the preliminaries out of the way, note that the examples in the Stratego manual deal exclusively with Abstract Syntax Trees (ASTs). The trees used are primarily for a language concerning propositional logic, which we dub the Spoofax Propositional Language (SPL). It is defined at the top of Section 4.1 of the manual. It consists of the following signature of constructors:

signature
  sorts
    Prop String

  constructors
    True         : Prop
    False        : Prop
    Atom         : String -> Prop
    Not          : Prop -> Prop
    And          : Prop * Prop -> Prop
    Or           : Prop * Prop -> Prop
    Impl         : Prop * Prop -> Prop
    Eq           : Prop * Prop -> Prop