Homework Assignments Week 1.7: Specifications with NaBL2

Writing NaBL2 Rules

A sequential let is a let with multiple binds, where each bound identifier is visible in the definition of the next identifier. For example, all references in the following program resolve:

let x = 2;
    y = 10 * x;
    z = x * y
in z + 2

Write the constraint rules that implement this let behavior. Use the following skeleton rules:

[[ LetSeq(binds, e) ^ (s) : ty ]] := ...

BindSeq[[ [] ^ (s, s') ]] := ...
BindSeq[[ [Bind(x, e)|binds] ^ (s, s') ]] := ...

[[ VarRef(x) ^ (s) : ty ]] :=
  Var{x} -> s, Var{x} |-> d, d : ty.

Applying NaBL2 Rules

 1. Given the following constraint rules:

[[ LetRec(binds, e) ^ (s) : ty ]] :=
  new s_let, s_let ---> s,
  Map1[[ binds ^ (s_let) ]],
  [[ e ^ (s_let) : ty ]].

[[ Bind(x, e) ^ (s) ]] :=
  Var{x} <- s, Var{x} : ty,
  [[ e ^ (s) : ty ]].

[[ IntLit(_) ^ (s) : INT() ]].

[[ VarRef(x) ^ (s) : ty ]] :=
  Var{x} -> s, Var{x} |-> d, d : ty. 

and the program represented by the following abstract syntax tree:

LetRec([
  Bind("x"{1},IntLit(42)), 
  Bind("y"{2},VarRef("x"{3})),
], VarRef("y"{4}))

The positions of the names in the AST are given by the annotations. For example "x"{1} is the occurrence of x at positions 1.

Show the constraints that would be generated by applying these rules to the program. Feel free to rename variables if necessary to avoid capture. Make positions in occurrences explicit, by writing Var{"x"@1}, for example.

 2. The rules from (1) model a recursive let. An alternative semantics for let is called parallel let, where the bodies of the bindings cannot refer to any of the variables that are bound in the let, but only to variables defined outside the let. Give a set of modified rules that implement these let semantics.

Answers

Verify your answers with the model answers.