Spoofax is a language workbench that provides meta-languages for the specification of (domain specific) programming languages. A language implementation, including an interactive editor environment, is derived from the specifications. In this workshop, we discover interactive language development and several of the meta-languages in Spoofax by extending an existing language definition for STLC-with-Records with new syntactic constructs and typing rules.

Prerequisites

Install Spoofax. Download a premade Eclipse containing Spoofax for your platform here. Using a version with embedded JRE is recommended, as it will most likely work regardless of your local Java setup. Unzip the archive somewhere convenient.

Download prepared workspace. Download the archive with the prepared workspace here. Unzipping it creates a directory workspace containing the projects we will use for the workshop.

Start Spoofax. Start the Spoofax Eclipse instance you downloaded. When asked for a workspace, select the workspace directory downloaded before. Spoofax should now start with two open projects, lang.stlcrec and lang.stlcrec.test.

You are now good to go!

Documentation

You can download the slides of the talk here.

Spoofax documentation, including for most of the meta-langauges, is found here. There is no online documentation for Statix yet, but the specification from the project and the text here should give you enough to work with.

Practice: Building the Language

Spoofax supports interactive language development. This means that the language you are developing can be used immediately in the same IDE. The project lang.stlcrec contains the language definition: IDE related configuration in editor/, syntax in syntax/, and transformation and static semantics in trans/. Build the language by selecting the lang.stlcrec project in the left sidebar, and select Project > Build Project from the menu (Ctrl+Alt+B should also work).

If the build succeeded, the console at the bottom ends with something like:

18:19 | INFO  | o.m.s.e.m.b.PackageBuilder     - Reloading language project eclipse:///lang.stlcrec

If the build fails, the console usually contains useful error messages.

Open the file example/simple.stlcrec. It should show an editor with a small program, which is syntax highlighted. Try editor reference resolution by Ctrl+LeftClick on the x reference.

Practice: Testing the Language

Language tests can be defined in the SPT meta-language. Tests for our language can be found in the project lang.stlcrec.test. Open the file stlc.spt to see an example. Tests consist of programs and test expectations. For example:

test function literal [[
  (fun([[x]]: num) { [[x]] + 1 }) : (num -> num)  
]] analysis succeeds
   resolve #2 to #1

Tests specify the test expectation. Examples of test expectations are parse fails, parse succeeds, analysis fails and analysis succeeds to test parsing and type checking. We can also test whether references resolve to the correct declarations using expectations like resolve #2 to #1; the numbers refer to the identifiers between double square brackets in the test program.

To run the tests from the open test file, select Spoofax (meta) > Run selected test. This opens a test runner at the bottom, which shows the result of running the tests. It is also possible to run all test files from a project: select the project in the left sidebar and select Spoofax (meta) > Run all selected tests.

Exercise: Add a let construct

We are going to add syntax and typing rules for a multi-armed let construct. They should look like:

let x = 1; y = 2 in x + 1

  1. The file stlc.spt contains some commented out tests for let constructs. Start by uncommenting those tests, and setting their test expectation to parse succeeds. Running the tests should result in three failing tests in the test runner.

  2. Add syntax for the let construct in the file syntax/STLCrec.sdf3. There is a comment placeholder in the file for the production Exp.Let that you should use.

    Syntax in the SDF3 meta-language is written using templates. Templates are fragments of concrete syntax, delimited by < and >, or [ and ]. Inside the fragment, it is possible to refer to non-terminals by escaping their names in the same delimiters. For example, the production for plus:

    Exp.Plus = <<Exp> + <Exp>>

    defines a production for the sort (non-terminal) Exp with constructor Plus, using the concrete + and expressions on the left and right. Lists are supported by built-in syntax with syntax like {N ","}+ or {N " "}*.

    Write the rule for let, and uncomment the line for Exp.Let in the context-free priorities section as well. Build the project, and run your tests again to see if it works.

  3. Write the typing rule for let in trans/statics.stx. Start by filling in the signature for the let constructor (unfortunately these are not yet generated from the syntax).

    Now you have a choice for the semantics of the let. It can be

    • Parallel. Bound expressions can only refer to variables from the lexical context.
    • Recursive. Bound expressions can refer to the binders in the let as well.
    • Sequential. Bound expressions can refer to preceding binders in the same let, but not subsequent binders.

    Choose which option you want to implement. Adjust the tests, so that the test for your chosen variant expects analysis succeeds, and the other two analysis fails.

    Use the following constraints to assert and query the scope graph:

    • s1 -l-> s2 asserts an l labeled edge from scope s1 to scope s2.
    • s -> Var{x@x} with typeOfDecl T asserts a variable declaration with name x in scope s with type T.
    • typeOfDecl of Var{x@x} in s |-> [(p, (d, T))] resolves the type of a variable of name x in scope s, resulting in a singleton list with a pair of a path p, the declaration d, and the type T. The result doesn’t have to be a singleton, any list is possible.

    Use example programs and the tests to assist you in writing the rule.

Exercise: Add a with construct

Our language also supports records. A with construct brings the fields of a record in scope as if it were lexical variables. For example:

let x = 2 in
let y = 3 in
let r = { x = 1 } in
with r do x + y

In this example, the x from the record should shadow the x from the surrounding let.

The syntax and Statix files already contain placeholders for the with construct. Tests can be found in records.spt. Follow the same procedure as for the previous exercise.