Assignment Term Rewriting

Pt

Tiger

Tiger is the example language we will be using in the rest of this course.

Tiger Abstract Syntax

The full abstract syntax is presented at

Tiger Tools

In directory /projects/stratego/tiger the components of the Tiger compiler have been installed. The following components are relevant for this assignment:

  • tiger-xmpl -x name : returns the contents of the example program name
  • parse-tiger : parses a Tiger program, returning its abstract syntax tree
  • Tiger-Desugar : eliminates syntactic sugar, in particular it splits let bindings
  • Tiger-Rename : renames bound variables
  • pp-tiger : pretty-prints a Tiger abstract syntax tree

The example programs can also be found in

The components can be combined in a pipe-line as follows:

 tiger-xmpl -x fac-tail | parse-tiger 
 | Tiger-Desugar | Tiger-Rename | Tiger-Ensugar | pp-tiger

To work smoothly with these components add /projects/stratego/tiger/bin to your PATH.

The Assignment

The goal of this assignment is to write two components transforming Tiger programs:

  • simplify : eliminates nested expression operators
  • let-flat : undoes let splitting

You should submit the following files (in a .tgz file):

  • simplify.str
  • let-flat.str
  • run.sh
  • any example Tiger programs you wrote to test the transformation

The run.sh should be a shell script that compiles the two programs and applies it to a number of files from the example directory (using tiger-xmpl) in a pipeline as follows:

tiger-xmpl -x fac-tail | parse-tiger 
   | Tiger-Desugar | Tiger-Rename 
   | ./simplify | ./let-flat 
   | Tiger-Ensugar | pp-tiger > fac-tail.smp

In your program import the signature of Tiger

  imports Tiger lib
and compile with argument -I /projects/stratego/tiger/share/tiger-front to make the module available to the compiler.

Simplification

This component should achieve two things. In the first place it should make sure that expressions used as arguments of operators, function calls, if conditions, while conditions, are either constants or variables. New variables should be introduced to hold the intermediate values of expressions.

For example, in the statement

  x := a + 34 - b
the expression (a + 34) is an argument of the - operator and should be transformed to
  let var a_0 
   in a_0 := a + 34;
      x := a_0 - b
  end

Similarly,

  if x < 34 then e1 else e2
should be transformed to
  let var a_0
   in a_0 := x < 34;
      if a_0 then e1 else e2
  end

Secondly it should simplify the result of this first transformation as much as possible by lifting the generated let bindings to top-level.

For example, the sequence

  (x := a + 34 - b * c ;
   y := c * x + 2)
should be transformed to
  let var a_0 
   in let var b_0 
       in let var c_0
           in a_0 := a + 34;
              b_0 := b * c;
              x   := a_0 - b_0 ;
              c_0 := c * x;
              y   := c_0 + 2
          end
      end
  end

Let-Flattening

The second component should undo the splitting of let bindings, and combine nested let bindings into a single list of let bindings. Thus, the last expression above should be transformed to:

  let var a_0 
      var b_0 
      var c_0 
   in a_0 := a + 34;
      b_0 := b * c;
      x   := a_0 - b_0 ;
      c_0 := c * x;
      y   := c_0 + 2
  end

Approach

The simplification should be done in small steps. It is not necessary to complete the transformation for all kinds of operators in order to get sufficient grade. The assignment will be judged based on far you get and on correctness. It is better to have a transformation that does fewer things, than a transformation that is incorrect. Approach the transformation in the following steps

  1. Lift non-atomic arguments of arguments of binary operators and relational operators
  2. Lift let bindings as far up as possible
  3. Flatten let bindings (let-flat.str)
  4. Lift non-atomic if condition
  5. Lift non-atomic while condition
  6. Lift non-atomic arguments of function calls (difficult)

Tips

Make small example programs to test the transformation.

Make a script for applying the pipeline of transformations.

Lifting Operands

The basic transformation should be a rewrite rule that performs the following transformation:

  x + (y + 3)
should be transformed to
  let var a_0
   in a_0 := y + 3;
      x + a_0
  end

In the pipeline described above the transformation component Tiger-Desugar is applied. It rewrites binary infix operators such as (e1 + e2) to a generic prefix operator +(e1, e2). The abstract syntax representation of this operator is BinOp(PLUS, e1, e2). Using this representation it is possible to define the transformation above as a single rewrite rule for all possible binary operators.

Conditional Rewrite Rules

To define the rewrite rules, you will need more than plain, unconditional rewrite rules. A conditional rewrite rule has the form

  L : p1 -> p2 where s
where s is a strategy. A condition often has the following form
  <s1> t1 => t1'; <s2> t2 => t2' 
That is, a sequence of applications of strategies to terms. The expression
  <s1> t1 => t1'
is an application of strategy s1 to term t1 matching the result against term t1'. The general structure of strategies will be discussed later. For now it is useful to know a few standard operations that you could use.

Useful Operations

Generate a unique string and bind it to (meta-)variable x:

  new => x

Concatenate the lists xs and ys:

  <conc>(xs, ys) => zs

The initial part of list xs, i.e., without its last argument:

  <init> xs => ys

The last element of list xs

  <last> xs => x : 

Law

  <conc>(<init>xs, [<last> xs]) => xs

Atomic

A special operation that is useful in this transformation is the following definition (which you should add to module simplify.str):

  atomic = Var(id) + Int(id) + Real(id) + String(id)
Then you can use
  <atomic>e
to test whether an expression is a variable or constant, and
  not(<atomic>e)
to test whether it is something else than a variable or constant.

Lift Call Arguments

If you get as far as lifting the arguments from function calls you may want to use the following operations.

Test if (at least) one of the expressions in a list is not atomic:

  <fetch(not(atomic))> es

Lift expressions in a list of arguments es:

  <map(LiftArg); unzip; (id, unzip)> es => (xs, (ds, stas))
where LiftArg is a rewrite rule that rewrites a single expression to (a variable, (a declaration, a statement)). The result is (a list of variables, (a list of declarations, a list of statements)).

Example

Here is a complete example of the effect of the transformation on the program fac-tail.tig:

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

------------------------------------------------------
let function fact_a_0(b_0 : int) : int =
      let function f_c_0(d_0: int, e_0 : int) : int =
            let var f_0
                var a_0
                var c_0
            in f_0 := d_0 < 1;
               if f_0
               then e_0
               else (a_0 := d_0 - 1;
                     c_0 := d_0 * e_0;
                     f_c_0(a_0, c_0))
            end
      in f_c_0(b_0, 1)
      end
in fact_a_0(10)
end
------------------------------------------------------