Stratego

Stratego is a system for specifying transformation rules (term rewriting) and strategies for the application of those rules. I am using Stratego as part of my PhD research into compiler intermediate representations.

• Official Stratego Website
• Tiger Compiler implemented in Stratego

When I first started using Stratego, I discovered that there is very little information for beginners. The best documentation I found is an introductory tutorial, but it's a little outdated. Below I outline my first Stratego program. If you are interested in learning how to use the Stratego system, then you may find it useful to work through this example below. It assumes that you have installed Stratego, and everything is set up to run properly.

Combinator reduction

The first step is to write the signature definition. This describes the term constructors (cf ML datatype constructors) in our system. We need two atomic terms S and K, together with an application operator Apply. Create the following file called comb.r

         module comb
         signature
           sorts Comb
           constructors
           K : Comb
           S : Comb
           Apply : Comb * Comb -> Comb

Now we need to specify the rewrite rules (reductions) permitted in this system. The combinator K can be reduced as follows:
(Kx) y --> x
The combinator S can be reduced as follows:
((S f) g) x --> (f x) (g x)
These are defined in a file called comb-red.r

         module comb-red
         imports comb

         rules

           T1: Apply(Apply(K, x), y) -> x
           T2: Apply(Apply(Apply(S, f), g), x) -> 
                 Apply(Apply(f, x), Apply(g, x))

Finally, we need to define strategies, to say how the reduction rules should be applied. These are defined in a file called comb-strat.r

         module comb-strat
         imports comb-red simple-traversal lib
         strategies

           T = T1 + T2

           nf = topdown(repeat(T))   (* normal form *)

           hnf = repeat(T)           (* head normal form *)

           main = stdio(nf)

We define two reduction strategies - one for normal form (terms fully reduced). And one for head normal form (only reduce from left to right, stop when left-most term cannot be reduced further,)

To compile this code, execute the following command:

            $ strc -i comb-strat.r

The Stratego compiler should process your code and output an executable file called comb-strat. You can execute comb-strat and type in a combinator term, terminated by a newline and an EOF character (ctrl-d). The system should reduce your combinator term to normal form.

Note that the main strategy is the one which is executed when the program runs. To produce head normal form instead of normal form, change the last line of comb-strat.r to be

         main = stdio(hnf)

This makes a difference. For instance, the combinator term Apply(S, Apply(Apply(K, K), K)) reduces to normal form of Apply(S, K), but it remains as Apply(S, Apply(Apply(K, K), K)) in the hnf transformation, since it is already in head normal form.