Exercise 3 Simply typed Lambda-Calculus
English only

If you have not finished the Evaluator last week, you are kindly asked to do so, because you need it for today's exercise.

### Exercise 3 Simply typed Lambda Calculus

Source Language Internal Language Values
 ```E ::= x T ::= Num E E Bool \x: T.E T->T true false zero succ E pred E iszero E if E then E else E let x = E in E let rec x: T = E in E```
 ```E ::= x T ::= Num E E Bool \x: T.E T->T true false zero succ E pred E iszero E if E then E else E fix E let x = E in E```
 ```V ::= BV NV \x: T.E BV ::= true false NV ::= zero succ NV```

In this exercise, we are using an internal language. The transformation that the parser applies to a source program is described here:

 ``` let rec f:T = E1 in E2 ----> let f = fix \f:T.E1 in E2 ```

As you can see, all `fix` nodes will always have a lambda as argument.

The new or changed tree nodes are (from `Expr.scala`)

```case class Lam(inf: Int, n: String, tpe: Type, e: Expr) extends Expr; // \x:T.E
case class Let(inf: Int, n: String, e1: Expr, e2: Expr) extends Expr; // let x = e1 in e2
case class Fix(inf: Int, e: Expr) extends Expr;                       // fix E

class Type { ... }
case object TyBool extends Type;                                      // Bool
case object TyNum extends Type;                                       // Num
case class  TyFun(domain: Type, range:Type) extends Type;             // T -> T
```

Again, the first parameter is the sourcefile position to report useful error messages.

Type System
Γ |- true: Bool

Γ |- false: Bool

Γ |- zero: Num

 x: T ∈ Γ Γ |- x: T
 Γ |- E: Num Γ |- pred E: Num
 Γ |- E: Num Γ |- succ E: Num
 Γ |- E: Num Γ |- iszero E: Bool
 Γ |- E1: Bool  E2: T   E3: T Γ |- if E1 then E2 else E3: T
 Γ, x: T1 |- E: T2 Γ |- \x: T1. E: T1->T2
 Γ |- E1: T1 ->T2   Γ |- E2: T1 Γ |- E1 E2: T2
 Γ |- E1: T1   Γ, f: T1 |- E2:T2 Γ |- let f = E1 in E2: T2
 Γ |- E: T -> T Γ |- fix E : T

The new computation rules for the nodes `Let` and `Fix` are as follows:

 let x = E1 in E2 → [x/E1] E2
 fix \f.E → [f / fix \f.E] E

Implement the missing method `analyze` in class `TypeChecking.scala` according to the specification given above.

Modify the evaluator so it can deal with the nodes `Lam,Let` and `Fix`.

You can copy the code from last weeks task and add some cases.

You can run the interpreter with `scala slambda.Main <sourcefile>`

 source - `Parser`-> Expr (with `RawVar` nodes) - `DeBruijnPhase`-> Expr - `TypeChecking`-> Expr - `Evaluator`-> Expr(value)

### Tips

The context Γ has to be updated with a type binding in the `Lam` case.

There is a new class `case class VarBind(ty: Type) extends Binding;` that you can use to make contexts Γ of the form `x:T1,...,z:T3`.

The class `Context` has now a method `getTypeFromContext`. You can call it with a name (must be a string) and a source file position `i` like this:

```case Var(i:Int,j:Int) => ... // i = debugging info, j = de Bruijn index
ctx.getTypeFromContext(i, ctx(vName), vName);
```
The first and third parameter are just to make useful error messages. Remember that you have to get the variable name from the context.

A context is updated just like before.

For error reporting, use the method `Main.reportError`, for instance

`case App(inf, x1, x2) => ...Main.reportError(inf, " error in application ...");`