<commit_before># Day 8: Type Analysis

In this lab, you define typing rules and constraints for MiniJava. 
From this definition, you generate an Eclipse editor, that provides type information in hover help and type constraint checking.

## Overview

### Objectives

Specify type analysis for MiniJava in NaBL, TS, and Stratego, and generate an Eclipse editor from it. 
The specification should include:

1. Name binding rules for
  * `this` expressions,
  * method declarations and
  * method calls.
2. Typing rules for
  * integer and boolean literals,
  * unary and binary expressions,
  * variable and field references,
  * object creation,
  * `this` expressions,
  * and method calls.
4. Custom constraint rules for type errors in 
  * expressions,
  * statements and
  * method declarations.
  
### Submission

You need to submit your MiniJava project with a pull request against branch `assignment8` on GitHub. 
Your GitHub repository contains a step-by-step procedure how to file such a request. 
This project should contain a `README.md` with a short paragraph explaining the organisation of your NaBL, TS, and Stratego files.

The deadline for submissions is November 26th, 17:59.

### Grading

You can earn up to 75 points for the correctness of your type analysis.
Therefore, we run several test cases against your implementation. 
You earn points, when your implementation passes test cases.
The total number of points depends on how many test cases you pass in each of the following groups:

* name binding (15 points)
  * this expressions (5 points)
  * method declarations (4 points)
  * method calls (6 points)
* typing rules (25 points)
  * unary expressions (5 points)
  * binary expressions (10 points)
  * object creation (1 point)
  * `this` expression (2 points)
  * variable and field references (2 points)
  * method call (5 points)
* constraints (30 points)
  * expressions (10 points)
  * statements and method declarations (20 points)
* challenge (5 points)

You can earn up to 10 points for your messages in errors and warnings.
We particular focus on 
 readability, 
 precision, 
 and the level of detail in your messages.

Finally, you can earn up to 5 points for the organisation of your NaBL, TS and Stratego files and 
up to 10 points for the quality of your code.
We focus on
  readability in general,
  meaningful variable names and
  the consistent use of NaBL Stratego paradigms.
We will consider the fact that both languages are new to you.

## Detailed Instructions

### TS

In this lab you specify typing rules and constraints in TS, a brand new metalanguage for specifying type systems of programming languages.
TS has a number of rough edges:

1. Imports of Stratego files (such as desugared signatures) will show errors, you can ignore these.
2. Generated Stratego files can contain errors, but compile fine.
3. Generated variable names change in each compilation.
4. The language lacks syntactic sugar for typical typing rule patterns.

Despite these issues, the language allows you to specify typing rules and constraints in a declarative and concise way.
TS files end in `.ts` and generate corresponding `.generated.str` files, __be sure to import these modules in your minijava.str file__.
The overall structure looks like this:

```
module types

imports
  
  common/src-gen/signatures/MiniJava-sig
  common/desugar
     
type rules
  
  ...
```

### Tasks

To support incremental name and type analysis, we use tasks to specify name and type analysis.
You have seen tasks already in the assignment on name analysis.

#### Idea

A task is a unit of computation, which might depend on index entries (such as definitions or properties) or on the results of other tasks.
Tasks are collected in a traversal, before they are evaluated.
Results of evaluated tasks are cached.
When a file is changed, tasks are only re-collected for this file.
A task is only re-evaluated, if it is new or if one of its dependencies changed.
This might include tasks which originated from a different file than the file that changed.

#### Building

Name and type tasks are executed incrementally based on changes made in MiniJava programs. 
However, tasks do not take changes of your language specification into account.
If you encounter an unexpected result after changing your naming or typing rules, right click the project containing your example files, and choose `Spoofax -> Reload analysis data`.

#### Debugging

Hovers offer a quick way to check if type analysis works as expected. When you move your mouse over an expression or definition in a MiniJava editor, you should see its type in a hover text.

Your test cases from the previous lab should enable a more principled way of testing type analysis. 
Tests that expect a class type as a result have to be modified to accept annotations on the name of the class. For example, an expectation `ClassType("A")` needs to be changed to `ClassType("A"{_})`.

When you get unexpected results, you can inspect index entries and 
  collected tasks with the *Show analysis*, *Show tasks* and *Show index* builders.
Probably the most useful builders for you are those which show them only for the current file (also called a partition) or for a selection.

Consider the following task entry:

```
task 1 [2, 3] =
  produce &2
  ->
  [Int()]
```
      
This entry consists of

* an identifier `1`,
* a list `[2, 3]` of dependencies on other tasks,
* an instruction `produce &2` which refers the result of task `2`,
* and a list of results `[Int()]`.

You can navigate the dependencies of tasks to find the reasons for failing tasks.
The following instructions exist:

* `resolve ns n in s* wrt props []` resolves a name `n` of namespace `ns` in scopes `s*`.
* `choose x <+ y` chooses from alternatives `x` and `y` deterministically. 
  If `x` is a term or a task with a result, `x` is chosen.
  Otherwise, `y` is chosen.
* `concat t1 + t2` combines the results of tasks `t1` and `t2`.
* `Message(tsk, [], result, trm, msg)` shows an error message `msg` on term `trm` based on the `result` (either succeeding, failing, or producing multiple results) of task `tsk`.
  There are similar variants for warnings and other conditions such as the success of a task.
* `produce x` produces result `x`.
* `CollectDefs(x)` retrieves the definition of a reference `x`.
* `lookup Type() props on d` looks up the type of a definition `d`.
* `check Type() prop t1 against t2 wrt Eq()` checks if types `t1` and `t2` are equal.
* `rewrite t wrt s` rewrites term `t` using strategy `s`.

### Typing Rules

Typing rules specify the types of expressions.

#### Literals

In the simplest case, the type of an expression is directly known.
An typical example for such expressions are literals.
For example, integer literals are of type `int`:

    IntValue(v): Int()

Note that you cannot use wildcards in TS patterns.

#### Unary and Binary Expressions

In more complicated cases, you need to check the types of subexpressions.
The general idea is that only well-typed expressions have a type.
For example, `1 + true` should have no type, since the right subexpression is of type `boolean` instead of type `int`.
In TS, the general pattern for checking subexpressions is this:

    e: ty
    where e1: ety1
      and ety1 == ty1
      and e2: ety2
      and ety2 == ty2

In TS, you need to specify the types of operators in axioms:

    Length(): (IntArray(), Int())

Here, `e` should match an expression with subexpressions `e1` and `e2` and
`ty` should be the type of `e`, while `ty1` and `ty2` should be the expected types of `e1` and `e2`, respectively.

You can follow this pattern for the rules for unary and binary expressions.
You should define the following rules:

1. One rule for `UnExp`.
2. One rule for `BinExp`.
3. A rule for each unary and binary operator, which rewrites the operator to a tuple.
   This tuple should consist of the expected types of subexpressions and the type of the operator itself.
   For example, the following rule states that the operator for `Length` requires a subexpression of type `int[]` and yields an expression of type `int`:   
``` 
LengthOp(): (IntArray(), Int())
```

The array subscript expression also requires a type, similar to a binary expression.

The signatures for desugared expressions are missing from the intial project, so here they are for reference:

```
signature
  constructors
   	
    BinExp      : BinOp * Exp * Exp -> Exp
    UnExp       : UnOp * Exp -> Exp
    Plus        : BinOp<commit_msg>Update day8.md<commit_after># Day 8: Type Analysis

In this lab, you define typing rules and constraints for MiniJava. 
From this definition, you generate an Eclipse editor, that provides type information in hover help and type constraint checking.

## Overview

### Objectives

Specify type analysis for MiniJava in NaBL, TS, and Stratego, and generate an Eclipse editor from it. 
The specification should include:

1. Name binding rules for
  * `this` expressions,
  * method declarations and
  * method calls.
2. Typing rules for
  * integer and boolean literals,
  * unary and binary expressions,
  * variable and field references,
  * object creation,
  * `this` expressions,
  * and method calls.
4. Custom constraint rules for type errors in 
  * expressions,
  * statements and
  * method declarations.
  
### Submission

You need to submit your MiniJava project with a pull request against branch `assignment8` on GitHub. 
Your GitHub repository contains a step-by-step procedure how to file such a request. 
This project should contain a `README.md` with a short paragraph explaining the organisation of your NaBL, TS, and Stratego files.

The deadline for submissions is November 26th, 17:59.

### Grading

You can earn up to 75 points for the correctness of your type analysis.
Therefore, we run several test cases against your implementation. 
You earn points, when your implementation passes test cases.
The total number of points depends on how many test cases you pass in each of the following groups:

* name binding (15 points)
  * this expressions (5 points)
  * method declarations (4 points)
  * method calls (6 points)
* typing rules (25 points)
  * unary expressions (5 points)
  * binary expressions (10 points)
  * object creation (1 point)
  * `this` expression (2 points)
  * variable and field references (2 points)
  * method call (5 points)
* constraints (30 points)
  * expressions (10 points)
  * statements and method declarations (20 points)
* challenge (5 points)

You can earn up to 10 points for your messages in errors and warnings.
We particular focus on 
 readability, 
 precision, 
 and the level of detail in your messages.

Finally, you can earn up to 5 points for the organisation of your NaBL, TS and Stratego files and 
up to 10 points for the quality of your code.
We focus on
  readability in general,
  meaningful variable names and
  the consistent use of NaBL Stratego paradigms.
We will consider the fact that both languages are new to you.

## Detailed Instructions

### TS

In this lab you specify typing rules and constraints in TS, a brand new metalanguage for specifying type systems of programming languages.
TS has a number of rough edges:

1. Imports of Stratego files (such as desugared signatures) will show errors, you can ignore these.
2. Generated Stratego files can contain errors, but compile fine.
3. Generated variable names change in each compilation.
4. The language lacks syntactic sugar for typical typing rule patterns.

Despite these issues, the language allows you to specify typing rules and constraints in a declarative and concise way.
TS files end in `.ts` and generate corresponding `.generated.str` files, __be sure to import these modules in your minijava.str file__.
The overall structure looks like this:

```
module types

imports
  
  common/src-gen/signatures/MiniJava-sig
  common/desugar
     
type rules
  
  ...
```

### Tasks

To support incremental name and type analysis, we use tasks to specify name and type analysis.
You have seen tasks already in the assignment on name analysis.

#### Idea

A task is a unit of computation, which might depend on index entries (such as definitions or properties) or on the results of other tasks.
Tasks are collected in a traversal, before they are evaluated.
Results of evaluated tasks are cached.
When a file is changed, tasks are only re-collected for this file.
A task is only re-evaluated, if it is new or if one of its dependencies changed.
This might include tasks which originated from a different file than the file that changed.

#### Building

Name and type tasks are executed incrementally based on changes made in MiniJava programs. 
However, tasks do not take changes of your language specification into account.
If you encounter an unexpected result after changing your naming or typing rules, right click the project containing your example files, and choose `Spoofax -> Reload analysis data`.

#### Debugging

Hovers offer a quick way to check if type analysis works as expected. When you move your mouse over an expression or definition in a MiniJava editor, you should see its type in a hover text.

Your test cases from the previous lab should enable a more principled way of testing type analysis. 
Tests that expect a class type as a result have to be modified to accept annotations on the name of the class. For example, an expectation `ClassType("A")` needs to be changed to `ClassType("A"{_})`.

When you get unexpected results, you can inspect index entries and 
  collected tasks with the *Show analysis*, *Show tasks* and *Show index* builders.
Probably the most useful builders for you are those which show them only for the current file (also called a partition) or for a selection.

Consider the following task entry:

```
task 1 [2, 3] =
  produce &2
  ->
  [Int()]
```
      
This entry consists of

* an identifier `1`,
* a list `[2, 3]` of dependencies on other tasks,
* an instruction `produce &2` which refers the result of task `2`,
* and a list of results `[Int()]`.

You can navigate the dependencies of tasks to find the reasons for failing tasks.
The following instructions exist:

* `resolve ns n in s* wrt props []` resolves a name `n` of namespace `ns` in scopes `s*`.
* `choose x <+ y` chooses from alternatives `x` and `y` deterministically. 
  If `x` is a term or a task with a result, `x` is chosen.
  Otherwise, `y` is chosen.
* `concat t1 + t2` combines the results of tasks `t1` and `t2`.
* `Message(tsk, [], result, trm, msg)` shows an error message `msg` on term `trm` based on the `result` (either succeeding, failing, or producing multiple results) of task `tsk`.
  There are similar variants for warnings and other conditions such as the success of a task.
* `produce x` produces result `x`.
* `CollectDefs(x)` retrieves the definition of a reference `x`.
* `lookup Type() props on d` looks up the type of a definition `d`.
* `check Type() prop t1 against t2 wrt Eq()` checks if types `t1` and `t2` are equal.
* `rewrite t wrt s` rewrites term `t` using strategy `s`.

### Typing Rules

Typing rules specify the types of expressions.

#### Literals

In the simplest case, the type of an expression is directly known.
An typical example for such expressions are literals.
For example, integer literals are of type `int`:

    IntValue(v): Int()

Note that you cannot use wildcards in TS patterns.

#### Unary and Binary Expressions

In more complicated cases, you need to check the types of subexpressions.
The general idea is that only well-typed expressions have a type.
For example, `1 + true` should have no type, since the right subexpression is of type `boolean` instead of type `int`.
In TS, the general pattern for checking subexpressions is this:

    e: ty
    where e1: ety1
      and ety1 == ty1
      and e2: ety2
      and ety2 == ty2

In TS, you need to specify the types of operators in axioms:

    LengthOp(): (IntArray(), Int())

Here, `e` should match an expression with subexpressions `e1` and `e2` and
`ty` should be the type of `e`, while `ty1` and `ty2` should be the expected types of `e1` and `e2`, respectively.

You can follow this pattern for the rules for unary and binary expressions.
You should define the following rules:

1. One rule for `UnExp`.
2. One rule for `BinExp`.
3. A rule for each unary and binary operator, which rewrites the operator to a tuple.
   This tuple should consist of the expected types of subexpressions and the type of the operator itself.
   For example, the following rule states that the operator for `Length` requires a subexpression of type `int[]` and yields an expression of type `int`:   
``` 
LengthOp(): (IntArray(), Int())
```

The array subscript expression also requires a type, similar to a binary expression.

The signatures for desugared expressions are missing from the intial project, so here they are for reference:

```
signature
  constructors
   	
    BinExp      : BinOp * Exp * Exp -> Exp
    UnExp       : UnOp * Exp -> Exp
    Plus        : BinOp
{'fraction_non_alphanumeric': 0.06474144509009802, 'fraction_numerical': 0.009215237424429184, 'mean_word_length': 3.9143351600807614, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5295559', 'n_tokens_mistral': 4628, 'n_tokens_neox': 4439, 'n_words': 2616}