Lambdas in Spoofax

Today I’ve been participating in the Transformation Tool Contest 2010, which is held as part of the TOOLS 2010 conference in Malaga. The plan for my participation was the use of researchr for use in the evaluation of the results of the contest. Then it turned out that the example problem for the live part of the contest was evaluation of lambda terms. An excellent problem to tackle with Spoofax. So after doing some last improvements of researchr, I spent the afternoon creating a little lambda language environment.

The source code of the project is part of the Spoofax contributions directory.

Here is the Eclipse editor:

In the figure example.lam is the input for the transformation in concrete syntax; example.aterm is the abstract syntax for example.lam; example.nf.aterm is the result of normalizing example.aterm; finally, example.nf.lam is the result of pretty-printing the normal form. The result should be the correct addition of the lambda numeral for 2 with itself.

The syntax of the language is defined in SDF:

The Lambda.sdf module contains the definition of the concrete syntax. The Lambda.str module is automatically derived from Lambda.sdf and defines the abstract syntax (as an algebraic signature in Stratego).

The transformation is defined in Stratego. Here are the rules for pretty-printing and beta reduction:

Renaming rules are used to introduce the bindings of bound variables. The check rule verifies that no two definitions for the same name are given. The warning rule finds free variables and gives a warning in the editor.

Here’s a screencast with a little demo to give an impression of the environment: