diff --git a/info/labs/amy-specification/AmySpec.md b/info/labs/amy-specification/AmySpec.md
new file mode 100644
index 0000000000000000000000000000000000000000..f5d27cf7dc3b27267c45ade9c6580e3ebde93106
--- /dev/null
+++ b/info/labs/amy-specification/AmySpec.md
@@ -0,0 +1,556 @@
+# Specification of the Amy Language
+
+**Computer Language Processing**
+**LARA**
+**Spring 2025**
+
+## 1. Introduction
+
+Welcome to the Amy project! This semester you will learn how to compile a simple functional Scala-like language from source files down to executable code. When your compiler is complete, it will be able to take Amy source (text) files as input and produce WebAssembly bytecode files. WebAssembly is a new format for portable bytecode which is meant to be run in browsers.
+
+This document is the specification of Amy. Its purpose is to help you clearly and unambiguously understand what an Amy program means, and to be the Amy language reference, along with the reference compiler. It does not deal with how you will actually implement the compiler; this will be described to you as assignments are released.
+
+### 1.1 Features of Amy
+
+Let us demonstrate the basic features of Amy through some examples:
+
+#### 1.1.1 The factorial function
+
+```scala
+object Factorial
+
+fn fact(i: Int(32)): Int(32) = {
+ if (i < 2) { 1 }
+ else { i * fact(i-1) }
+}
+
+end Factorial
+```
+
+Every program in Amy is contained in a module, also called `object`. A function is introduced with the keyword `fn`, and all its parameters and result type must be explicitly typed. Amy supports conditional (or if-) expressions with obligatory brackets. Notice that conditionals are not statements, but return a value, in this case an `Int(32)`.
+
+In fact, there is no distinction between expressions and statements in Amy. Even expressions that are called only for their side-effects return a value of type `Unit`.
+
+The condition of an if-expression must be of type `Boolean` and its branches must have the same type, which is also the type of the whole expression.
+
+#### 1.1.2 Saying hello
+
+```scala
+object Hello
+ Std.printString("Hello " ++ "world!")
+end Hello
+```
+
+Amy supports compiling multiple modules together. To refer to functions (or other definitions) in another module, one must explicitly use a qualified name. There is no import statement like in Scala.
+
+In this example, we refer to the `printString` function in the `Std` module, which contains some builtin functions to interact with the user. The string we print is constructed by concatenating two smaller strings with the `++` operator.
+
+#### 1.1.3 Input, local variables and sequencing expressions
+
+```scala
+object ReadName
+ Std.printString("What is your name?");
+ val name: String = Std.readString();
+ Std.printString("Hello " ++ name)
+end ReadName
+```
+
+We can read input from the console with the `readX` functions provided in `Std`.
+
+We can define local variables with `val`, which must always be typed explicitly. The value of the variable is given after `=`, followed by a semicolon.
+
+We can sequence expressions with `;`. The value of the first expression is discarded, and the value of the second one is returned. Note that `;` is an operator and not a terminator: you are not allowed to put it at the end of a sequence of expressions.
+
+#### 1.1.4 Type definitions
+
+Except for the basic types, a user can define their own types in Amy. The user-definable types in Amy come from functional programming and are called algebraic data types. In this case, we define a type, `List`, and two constructors `Nil` and `Cons`, which we can call to construct values of type `List`.
+
+```scala
+object L
+ abstract class List
+ case class Nil() extends List
+ case class Cons(h: Int(32), t: List) extends List
+end L
+```
+
+#### 1.1.5 Constructing ADT values
+
+```scala
+fn range(from: Int(32), to: Int(32)): List = {
+ if (to < from) { Nil() }
+ else {
+ Cons(from, range(from + 1, to))
+ }
+}
+```
+
+We can create a `List` by calling one of its two constructors like a function, as demonstrated in the `range` function.
+
+#### 1.1.6 Pattern matching
+
+```scala
+fn length(l: List): Int(32) = {
+ l match {
+ case Nil() => 0
+ case Cons(h, t) => 1 + length(t)
+ }
+}
+```
+
+To use a list value in any meaningful way, we have to break it down, according to the constructor used to construct it. This is called pattern matching and is a powerful feature of functional programming.
+
+In `length` we pattern match against the input value `l`. Pattern matching will check if its argument matches the pattern of the first case, and if so will evaluate the corresponding expression. Otherwise it will continue with the second case etc. If no pattern matches, the program will exit with an error. If the constructor has arguments, as does `Cons` in this case, we can bind their values to fresh variables in the pattern, so we can use them in the case expression.
+
+#### 1.1.7 Wildcard patterns and errors
+
+The `error` keyword takes a string as argument, prints `Error:` and its argument on the screen, then exits the program immediately with an error code. In this function, we are trying to compute the head of a list, which should fail if the list is empty.
+
+Notice that in the second case, we don’t really care what the tail of the list is. Therefore, we use a wildcard pattern (`_`), which matches any value without binding it to a name.
+
+```scala
+fn head(l: List): Int(32) = {
+ l match {
+ case Cons(h, _) => h
+ case Nil() => error("head(Nil)")
+ }
+}
+```
+
+### 1.2 Relation to Scala
+
+Amy, with mild syntactic variations, is designed to be as close to a simple subset of Scala as possible. However, it is not a perfect subset. You can easily come up with Amy programs that are not legal in Scala. However, many “reasonable†programs will be compilable with `scalac`, provided you provide an implementation of the Amy standard library along with your code. This should not be required however, as we are providing a reference implementation of Amy.
+
+---
+
+## 2. Syntax
+
+The syntax of Amy is given formally by the context-free grammar of Figure 1. Everything spelled in *italic* is a nonterminal symbol of the grammar, whereas the terminal symbols are spelled in monospace font. `*` is the Kleene star, `s+` stands for one or more repetitions of `s`, and `?` stands for optional presence of a symbol (zero or one repetitions). The square brackets `[]` are not symbols of the grammar; they merely group symbols together.
+
+Before parsing an Amy program, the Amy lexer generates a sequence of terminal symbols (tokens) from the source files. Some non-terminal symbols mentioned, but not specified, in Figure 1 are also represented as a single token by the lexer. They are lexed according to the rules in Figure 2. In Figure 2, we denote the range between characters α and β (included) with `[α-β]`.
+
+The syntax in Figure 1 is an *overapproximation* of the real syntax of Amy. This means that it allows some programs that should not be allowed in Amy. To get the real syntax of Amy, there are some additional restrictions presented (among other things) in the following notes:
+
+- The reserved words of Amy are the following:
+ `abstract`, `Boolean`, `case`, `class`, `fn`, `else`, `error`, `extends`, `false`, `if`, `Int`, `match`, `object`, `end`, `String`, `true`, `Unit`, `val`, `_` (the wildcard pattern).
+
+ Identifiers are not allowed to coincide with a reserved word.
+
+- The operators and language constructs of Amy have the following precedence, starting from the lowest:
+
+ 1) `val`, `;`
+ 2) `if`, `match`
+ 3) `||`
+ 4) `&&`
+ 5) `==`
+ 6) `<`, `<=`
+ 7) `+`, `-`, `++`
+ 8) `*`, `/`, `%`
+ 9) Unary `-`, `!`
+ 10) `error`, calls, variables, literals, parenthesized expressions.
+
+ For example,
+ `1 + 2 * 3` means `1 + (2 * 3)` and
+ `1 + 2 match {...}` means `(1 + 2) match {...}`.
+
+ A little more complicated is the interaction between `;` and `val`:
+ the definition part of the `val` extends only as little as the first semicolon, but then the variable defined is visible through any number of semicolons. Thus `(val x: Int(32) = y; z; x)` means `(val x: Int(32) = y; (z; x))` and not `(val x: Int(32) = (y; z); x)` or `((val x: Int(32) = y; z); x)` (i.e. `x` takes the value of `y` and is visible until the end of the expression).
+
+ All operators are left-associative. That means that within the same precedence category, the leftmost application of an operator takes precedence. An exception is the sequence operator, which for ease of the implementation (you will understand during parsing) can be considered right-associative (it is an associative operator so it does not really matter).
+
+- A `val` definition is not allowed directly in the value assigned by an enclosing `val` definition. E.g.
+ `(val x: Int(32) = val y: Int(32) = 0; 1; 2)` is **not** allowed.
+ On the other hand,
+ `(val x: Int(32) = 0; val y: Int(32) = 1; 2)` is allowed.
+
+- It is not allowed to use a `val` as a (second) operand to an operator. E.g.
+ `(1 + val x: Int(32) = 2; x)` is **not** allowed.
+
+- A unary operator is not allowed as a direct argument of another unary operator. E.g. `--x` is **not** allowed.
+
+- It is not allowed to use `match` as a first operand of any binary operator, except `;`. E.g. `(x match { ... } + 1)` is **not** allowed. On the other hand `(x match { ... }; x)` is allowed.
+
+- The syntax `[ Id . ]? Id` refers to an optionally qualified name, for example either `MyModule.foo` or `foo`. If the qualifier is included, the qualified name refers to a definition `foo` in another module `MyModule`; otherwise, `foo` should be defined in the current module. Since Amy does not have the import statement of Scala or Java, this is the only way to refer to definitions in other modules.
+
+- One line comments are introduced with `//`: `//This is a comment.` Everything until the end of the line is a comment and should be ignored by the lexer.
+
+- Multiline comments can be used as follows: `/*This is a comment */`. Everything between the delimiters is a comment, notably including newline characters and `/*`. **Nested comments are not allowed**.
+
+- Escaped characters are not recognised inside string literals. I.e. `"\n"` stands for a string literal which contains a *backslash* and an `n`.
+
+---
+
+```text
+Figure 1: Syntax of Amy
+
+Program ::= Module∗
+
+Module ::= object Id Definition∗ Expr? end Id
+Definition ::= AbstractClassDef | CaseClassDef | FunDef
+
+AbstractClassDef ::= abstract class Id
+CaseClassDef ::= case class Id ( Params ) extends Id
+
+FunDef ::= fn Id ( Params ) : Type = { Expr }
+Params ::= ϵ | ParamDef [ , ParamDef ]∗
+
+ParamDef ::= Id : Type
+Type ::= Int ( 32 ) | String | Boolean | Unit | [ Id . ]? Id
+Expr ::= Id
+ | Literal
+ | Expr BinOp Expr
+ | UnaryOp Expr
+ | [ Id . ]? Id ( Args )
+ | Expr ; Expr
+ | val ParamDef = Expr ; Expr
+ | if ( Expr ) { Expr } else { Expr }
+ | Expr match { MatchCase+ }
+ | error ( Expr )
+ | ( Expr )
+
+Literal ::= true | false | ( )
+ | IntLiteral | StringLiteral
+
+BinOp ::= + | - | * | / | % | < | <=
+ | && | || | == | ++
+
+UnaryOp ::= - | !
+
+MatchCase ::= case Pattern => Expr
+Pattern ::= [ Id . ]? Id ( Patterns ) | Id | Literal |
+Patterns ::= ϵ | Pattern [ , Pattern ]∗
+
+Args ::= ϵ | Expr [ , Expr ]∗
+```
+
+```text
+Figure 2: Lexical rules for Amy
+
+IntLiteral ::= Digit+
+
+Id ::= Alpha AlphaNum∗ (and not a reserved word)
+AlphaNum ::= Alpha | Digit |
+Alpha ::= [a-z] | [A-Z]
+Digit ::= [0-9]
+
+StringLiteral ::= " StringChar∗ "
+StringChar ::= Any character except newline and "
+```
+
+---
+
+## 3. Semantics
+
+In this section we will give the semantics of Amy, i.e. we will systematically explain what an Amy program represents, as well as give the restrictions that a legal Amy program must obey. The discussion will be informal, except for the typing rules of Amy.
+
+### 3.1 Program Structure
+
+An Amy program consists of one or more source files. Each file contains a single module (object), which in turn consists of a series of type and function definitions, optionally followed by an expression. We will use the terms *object* and *module* interchangeably.
+
+### 3.2 Execution
+
+When an Amy program is executed, the expression at the end of each module, if present, is evaluated. The order of execution among modules is the same that the user gave when compiling or interpreting the program. Each module’s definitions are visible within the module automatically, and in all other modules provided a qualified name is used.
+
+### 3.3 Naming rules
+
+In this section, we will give the restrictions that a legal Amy program must obey with regard to naming or referring to entities defined in the program. Any program not following these restrictions should be rejected by the Amy name analyzer.
+
+- Amy is case-sensitive.
+- No two modules in the program can have the same name.
+- No two classes, constructors, and/or functions in the same module can have the same name.
+- No two parameters of the same function can have the same name.
+- No two local variables of the same function can have the same name if they are visible from one another. This includes binders in patterns of match-expressions. Variables that are not mutually visible can have the same name. E.g. the program
+ `val x : Int(32) = 0; val x : Int(32) = 1; 2` is not legal, whereas
+ `(val x : Int(32) = 0; 1); (val x : Int(32) = 1; 2)` is.
+- A local variable can have the same name as a parameter. In this case, the local variable definition shadows the parameter definition.
+- Every variable encountered in an expression has to refer to a function parameter or a local variable definition.
+- All case classes have to extend a class in the same module.
+- All function or constructor calls or type references have to refer to a function/constructor/type defined in the same module, or another module provided a qualified name is given. It is allowed to refer to a constructor/type/function before declaring it.
+- All calls to constructors and functions have to have the same number of arguments as the respective constructor/function definition.
+Below is the **Types and Classes** section (Section 3.4) reproduced more faithfully, in Markdown format:
+
+### 3.4 Types and Classes
+
+Every expression, function parameter, and class parameter in Amy has a type. Types catch some common programming errors by introducing typing restrictions. Programs that do not obey these restrictions are illegal and will be rejected by the Amy type checker.
+
+The built-in types of Amy are `Int(32)`, `String`, `Boolean` and `Unit`. `Int(32)` represents 32-bit signed integers. `String` is a sequence of characters. Strings have poor support in Amy: the only operations defined on them are concatenation and conversion to integer. In fact, not even equality is “properly†supported (see Section 3.5). `Boolean` values can take the values `true` and `false`. `Unit` represents a type with a single value, `()`. It is usually used as the result of a computation which is invoked for its side-effects only, for example, printing some output to the user. It corresponds to Java’s `void`.
+
+In addition to the built-in types, the programmer can define their own types. The sort of types that are definable in Amy are called **Algebraic Data Types (ADTs)** and come from the functional programming world, but they have also been successfully adopted in Scala.
+
+An ADT is a type along with several constructors that can create values of that type. For example, an ADT defining a list of integers in pseudo syntax may look like this:
+
+```scala
+type List = Nil() | Cons(Int(32), List)
+```
+
+which states that a `List` is either `Nil` (the empty list), or a `Cons` of an integer and another list. We will say that `Cons` has two fields of types `Int(32)` and `List`, whereas `Nil` has no fields. Inside the program, the only way to construct values of the `List` type is to call one of these constructors, e.g. `Nil()` or `Cons(1, Cons(2, Nil()))`. You can think of them as functions from their field types to the `List` type.
+
+Notice that in the above syntax, `Nil` and `Cons` are not types. More specifically, they are not *subtypes* of `List`: in fact, there is no subtyping in Amy. Only `List` is a type, and values such as `Nil()` or `Cons(1, Cons(2, Nil()))` have the type `List`.
+
+In Amy, we use Scala syntax to define ADTs. A type is defined with an abstract class and the constructors with case classes. The above definition in Amy would be:
+
+```scala
+abstract class List
+case class Nil() extends List
+case class Cons(h: Int(32), t: List) extends List
+```
+
+Notice that the names of the fields have no practical meaning, and we only use them to stay close to Scala.
+
+We will sometimes use the term **abstract class** for a type and **case class** for a type constructor.
+
+The main programming structure to manipulate class types is pattern matching. In Section 3.5 we define how pattern matching works.
+
+### 3.5 Typing Rules and Semantics of Expressions
+
+Each expression in Amy is associated with a typing rule, which constrains and connects its type and the types of its subexpressions. An Amy program is said to *typecheck* if:
+1) All its expressions obey their respective typing rules,
+2) The body of each function corresponds to its declared return type.
+
+A program that does not typecheck will be rejected by the compiler.
+
+In the following, we will informally give the typing rules and explain the semantics (meaning) of each type of expression in Amy. We will use function type notation for typing of the various operators. For example, `(A,B) => C` denotes that an operator takes arguments of types `A` and `B` and returns a value of type `C`.
+
+When talking about the semantics of an expression we will refer to a *context*. A context is a mapping from variables to the values that have been assigned to them.
+
+- **Literals** of Amy are expressions of the base types that are values, i.e. they cannot be evaluated further. The literals `true` and `false` have type `Boolean`. `()` (the unit literal) has type `Unit`. String literals have type `String` and integer literals have type `Int(32)`.
+
+- A **variable** has the type of the corresponding definition (function parameter or local variable definition). Its value is the value assigned to it in the current context.
+
+- `+`, `-`, `*`, `/` and `%` have type `(Int(32), Int(32)) => Int(32)`, and are the usual integer operators.
+
+- Unary `-` has type `(Int(32)) => Int(32)` and is the integer negation.
+
+- `<` and `<=` have type `(Int(32), Int(32)) => Boolean` and are the usual arithmetic comparison operators.
+
+- `&&` and `||` have type `(Boolean, Boolean) => Boolean` and are the boolean conjunction and disjunction. Notice that these operators are short-circuiting. This means that the second argument does not get evaluated if the result is known after computing the first one. For example, `true || error("")` will yield `true` and not result in an error, whereas `false || error("")` will result in an error in the program.
+
+- `!` has type `(Boolean) => Boolean` and is the boolean negation.
+
+- `++` has type `(String, String) => String` and is the string concatenation operator.
+
+- `==` is the equality operator. It has type `(A,A) => Boolean` for every type `A`.
+ - Equality for values of the `Int(32)`, `Boolean` and `Unit` types is defined as value equality, i.e. two values are equal if they have the same representation. E.g. `0 == 0`, `() == ()` and `(1 + 2) == 3`.
+ - Equality for the reference types `String` and all user-defined types is defined as reference equality, i.e. two values are equal only if they refer to the same object. I.e. `"" == ""`, `"a" ++ "b" == "ab"` and `Nil() == Nil()` all evaluate to `false`, whereas
+ `(val s = "Hello"; s == s)` evaluates to `true`.
+
+- `error()` has type `(String) => A` for any type `A`, i.e. `error` is always acceptable, regardless of the expected type. When a program encounters `error`, it needs to print something like `Error: <msg>`, where `<msg>` is its evaluated argument, and then exit immediately.
+
+- `if(..) {..} else {..}` has type `(Boolean, A, A) => A` for any type `A`, and has the following meaning: First, evaluate the condition of `if`. If it evaluates to `true`, evaluate and return the then-branch; otherwise, evaluate and return the else-branch. Notice that the value that is not taken is not evaluated.
+
+- `;` is the sequence operator. It has type `(A, B) => B` for any types `A` and `B`. Notice that the first expression has to be well typed, although its precise type does not matter. `;` evaluates and discards its first argument (which we will usually invoke just for its side-effects) and then evaluates and returns its second argument.
+
+- `val n = e; b` defines a local variable with name `n` and adds it to the context, mapped to the value of `e`. It is visible in `b` but not in `e`. `n` has to obey the name restrictions described in Section 3.3.
+
+- An expression `f(..)` or `m.f(..)` denotes either a function call or an invocation of a type constructor. `f` has to be the name of a function/constructor defined in the program. The types of the real arguments of the function/constructor invocation have to match the corresponding types of the formal arguments in the definition of the function/constructor. The type of a function/constructor call is the return type of the function, or the parent type of the constructor respectively.
+
+ Evaluating a function call means evaluating its body in a new context, containing the function’s formal arguments mapped to the values of the real arguments provided at the function call. Evaluating a call to a constructor means generating and returning a fresh object containing (a reference to) the constructor and the arguments passed to it. Notice that an invocation of a type constructor on values is itself a value, i.e. cannot be evaluated further. It corresponds to literals of the other types.
+
+- `match` is the pattern-matching construct of Amy. It corresponds to Scala’s pattern matching. Java programmers can think of it as a generalized `switch`-statement. `match` is the only way to access the structure of a value of a class type. It also happens to be the most complicated structure of Amy.
+
+ **Terminology:** To explain how the match-expression works, let us first establish some terminology. A match expression has a *scrutinee* (the first operand, which gets pattern matched on), and a number of *match cases* (or simply cases). A case is introduced with the keyword `case`, followed by the (case) pattern, then the symbol `=>` and finally an expression, which we will call the *case expression*.
+
+ As seen in Section 2, a pattern comes in four different forms, which in the grammar are denoted as:
+ 1) `Id(Patterns)` — **case class pattern**
+ 2) `Id` — **identifier pattern**
+ 3) `Literal` — **literal pattern**
+ 4) `_` — **wildcard pattern**
+
+ The identifier at the beginning of **case class pattern** is called the constructor of the pattern, and its arguments are called its *subpatterns*.
+
+ **Typing rules:** For the match-expression to typecheck, two conditions have to hold:
+ 1) All its case expressions have the same type, which is also the type of the whole match expression.
+ 2) All case patterns have to follow the type of the scrutinee. For a pattern to follow a type means the following, according to its form:
+ - Each literal pattern follows exactly the type of its literal.
+ - Wildcard and identifier patterns follow any type.
+ - A case class pattern follows only the resulting type of its constructor, if and only if all its subpatterns follow the types of the respective fields of the constructor.
+
+ For example, `Nil() match { case Cons(_, t) => () }` typechecks, whereas `Nil() match { case 0 => () }` does not.
+
+ **Semantics:** The semantics of pattern matching are as follows: First, the scrutinee is evaluated, then cases are scanned one by one until one is found whose pattern matches the scrutinee value. If such case is found, its case expression is evaluated, after adding to the environment the variables bound in the case pattern (see below). The value produced in this way is returned as the value of the match-expression. If none is found, the program terminates with an error.
+
+ We say that a pattern *matches* a value when the following holds:
+ - A wildcard pattern (`_`) or an identifier pattern (e.g. `x`) match any value. In the second case, `x` is bound to that value when evaluating the case expression.
+ - A literal pattern matches exactly the value of its literal. Notice that string literals are compared by reference, so they can never match.
+ - A case class pattern `case C(..)` matches a value `v`, if and only if `v` has been constructed with the same constructor `C` and every subpattern of the pattern matches the corresponding field of `v`. Notice that we have to recursively bind identifiers in subpatterns.
+
+- **Parentheses** `(e)` can be used freely around an expression `e`, mainly to override operator precedence or to make the program more readable. `(e)` is equivalent to `e`.
+
+- When evaluating an expression composed of sub-expressions (e.g. `f(a,b)`), the different sub-expressions are evaluated in left-to-right order (i.e. in the previous example, the sub-expressions would be evaluated in the following order: `f` then `a` then `b`). Function calls are done using the *call by value* strategy.
+
+### 3.6 Formal discussion of types
+
+In this section, we give a formal (i.e. mathematically robust) description of the Amy typing rules. A typing rule will be given as:
+
+```text
+ Rule Name
+ P1 ... Pn
+ -----------
+ C
+```
+
+where `Pi` are the rule premises and `C` is the rule conclusion. A typing rule means that the conclusion is true under the premises.
+
+Conclusions and most premises will be type judgements in an environment. A type judgement `Γ ⊢ e : T` means that an expression (or pattern) `e` has type `T` in environment `Γ`. Environments `Γ` are mappings from variables to types and will be written as `Γ = v1 : T1, . . . , vn : Tn`. We can add a new pair to an environment `Γ` by writing `Γ, vn+1 : Tn+1`. We will also sometimes write a type judgement of the form `Γ ⊢ p`. This means that `p` typechecks, but we don’t assign a type to it. Type checking will try to typecheck a program under the initial environment, and reject the program if it fails to do so.
+
+The initial environment `Γ0(p)` of a program `p` is one that contains the types of all functions and constructors in `p`, where a constructor is treated as a function from its fields to its parent type (see Section 3.4). The initial environment is used to kickstart typechecking at the function definition level.
+
+Below are the typing rules for expressions, patterns, functions, and programs:
+
+```text
+Figure 3: Typing rules for expressions
+
+Variable
+v : T ∈ Γ
+-----------
+Γ ⊢ v : T
+
+Int Literal
+i is an integer literal
+------------------------
+Γ ⊢ i : Int(32)
+
+String Literal
+s is a string literal
+----------------------
+Γ ⊢ s : String
+
+Unit
+--------------
+Γ ⊢ () : Unit
+
+Boolean Literal
+b ∈ {true, false}
+------------------
+Γ ⊢ b : Boolean
+
+Arith. Bin. Operators
+Γ ⊢ e1 : Int(32) Γ ⊢ e2 : Int(32)
+op ∈ {+, -, *, /, %}
+--------------------------------------
+Γ ⊢ e1 op e2 : Int(32)
+
+Arith. Comp. Operators
+Γ ⊢ e1 : Int(32) Γ ⊢ e2 : Int(32)
+op ∈ {<, <=}
+-------------------------------------
+Γ ⊢ e1 op e2 : Boolean
+
+Arith. Negation
+Γ ⊢ e : Int(32)
+-----------------
+Γ ⊢ -e : Int(32)
+
+Boolean Bin. Operators
+Γ ⊢ e1 : Boolean Γ ⊢ e2 : Boolean
+op ∈ {&&, ||}
+-------------------------------------
+Γ ⊢ e1 op e2 : Boolean
+
+Boolean Negation
+Γ ⊢ e : Boolean
+------------------
+Γ ⊢ !e : Boolean
+
+String Concatenation
+Γ ⊢ e1 : String Γ ⊢ e2 : String
+-----------------------------------
+Γ ⊢ e1 ++ e2 : String
+
+Equality
+Γ ⊢ e1 : T Γ ⊢ e2 : T
+-------------------------
+Γ ⊢ e1 == e2 : Boolean
+
+Sequence
+Γ ⊢ e1 : T1 Γ ⊢ e2 : T2
+---------------------------
+Γ ⊢ e1 ; e2 : T2
+
+Local Variable Definition
+Γ ⊢ e1 : T1 Γ, n : T1 ⊢ e2 : T2
+-----------------------------------
+Γ ⊢ val n : T1 = e1 ; e2 : T2
+
+Function/Class Constructor Invocation
+Γ ⊢ e1 : T1 ... Γ ⊢ en : Tn
+Γ ⊢ f : (T1, ... , Tn) ⇒ T
+--------------------------------
+Γ ⊢ f(e1, ... , en) : T
+
+If-Then-Else
+Γ ⊢ e1 : Boolean Γ ⊢ e2 : T Γ ⊢ e3 : T
+--------------------------------------------
+Γ ⊢ if (e1) {e2} else {e3} : T
+
+Error
+Γ ⊢ e : String
+---------------
+Γ ⊢ error(e) : T
+
+Pattern Matching
+Γ ⊢ e : Ts
+∀i ∈ [1, n]. Γ ⊢ pi : Ts
+∀i ∈ [1, n]. Γ, bindings(pi) ⊢ ei : Tc
+-------------------------------------------------------------
+Γ ⊢ e match { case p1 => e1 ... case pn => en } : Tc
+```
+
+```text
+Figure 4: Typing rules for patterns, functions and programs
+
+Wildcard Pattern
+-------------
+Γ ⊢ _ : T
+
+Identifier Pattern
+--------------
+Γ ⊢ v : T
+
+Case Class Pattern
+Γ ⊢ p1 : T1 ... Γ ⊢ pn : Tn
+Γ ⊢ C : (T1, ... , Tn) ⇒ T
+----------------------------------
+Γ ⊢ C(p1, ... , pn) : T
+
+Function Definition
+Γ, v1 : T1, ... , vn : Tn ⊢ e : T
+---------------------------------------------
+Γ ⊢ fn f(v1 : T1, ... , vn : Tn): T = { e }
+
+Program
+∀f ∈ p. Γ0(p) ⊢ f
+--------------------
+⊢ p
+```
+
+---
+
+## 4. The standard library of Amy
+
+Amy comes with a library of predefined functions, which are accessible in the `Std` object. Some of these functions implement functionalities that are not expressible in Amy, e.g. printing to the standard output. These built-in functions are implemented in JavaScript and WebAssembly in case of compilation, and in Scala in the interpreter. Built-in functions have stub implementations in the Amy `Std` module for purposes of name analysis and type checking.
+
+The Amy compiler will not automatically include `Std` to the input files. If you want them included, you have to provide them manually.
+
+The signature of the `Std` module is the following:
+
+```scala
+object Std
+
+// Output
+fn printString(s: String): Unit = ...
+fn printInt(i: Int(32)): Unit = ...
+fn printBoolean(b: Boolean): Unit = ...
+
+// Input
+fn readString(): String = ...
+fn readInt(): Int(32) = ...
+
+// Conversions
+fn intToString(i: Int(32)): String = ...
+fn digitToString(i: Int(32)): String = ...
+fn booleanToString(b: Boolean): String = ...
+
+end Std
+```
+
+---
\ No newline at end of file
diff --git a/info/labs/amy-specification/Factorial.scala b/info/labs/amy-specification/Factorial.scala
deleted file mode 100644
index 5520a8f85ee6b9b47235b4ed4d21e97d8c64b644..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/Factorial.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-object Factorial
- fn fact(i: Int(32)): Int(32) = {
- if (i < 2) { 1 }
- else { i * fact(i-1) }
- }
-end Factorial
diff --git a/info/labs/amy-specification/Hello1.scala b/info/labs/amy-specification/Hello1.scala
deleted file mode 100644
index a6dd117a53cd092d8c420a825edb81fbf037d278..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/Hello1.scala
+++ /dev/null
@@ -1,3 +0,0 @@
-object Hello
- Std.printString("Hello " ++ "world!")
-end Hello
diff --git a/info/labs/amy-specification/Hello2.scala b/info/labs/amy-specification/Hello2.scala
deleted file mode 100644
index 2340a6a164857303af066ebba2be1caf898f7975..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/Hello2.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-object ReadName
- Std.printString("What is your name?");
- val name: String = Std.readString();
- Std.printString("Hello " ++ name)
-end ReadName
diff --git a/info/labs/amy-specification/List1.scala b/info/labs/amy-specification/List1.scala
deleted file mode 100644
index cf2dd66c7d179c3573543aa94dc027eb683934f5..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/List1.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-object L
- abstract class List
- case class Nil() extends List
- case class Cons(h: Int(32), t: List) extends List
-end L
diff --git a/info/labs/amy-specification/List2.scala b/info/labs/amy-specification/List2.scala
deleted file mode 100644
index 2b3d6c55debcbddc8e496f8c9d9d24ea3d42a65c..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/List2.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-fn range(from: Int(32), to: Int(32)): List = {
- if (to < from) { Nil() }
- else {
- Cons(from, range(from + 1, to))
- }
-}
diff --git a/info/labs/amy-specification/List3.scala b/info/labs/amy-specification/List3.scala
deleted file mode 100644
index c061c4cb158e6c2e4b438f4a76e2b8e3b953e920..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/List3.scala
+++ /dev/null
@@ -1,4 +0,0 @@
-fn length(l: List): Int(32) = { l match {
- case Nil() => 0
- case Cons(h, t) => 1 + length(t)
-}}
diff --git a/info/labs/amy-specification/List4.scala b/info/labs/amy-specification/List4.scala
deleted file mode 100644
index e6d6ac3b1b35e32dd9379e0810ee0cb71b73b392..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/List4.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-fn head(l: List): Int(32) = {
- l match {
- case Cons(h, _) => h
- case Nil() => error("head(Nil)")
- }
-}
diff --git a/info/labs/amy-specification/amy-specification.pdf b/info/labs/amy-specification/amy-specification.pdf
deleted file mode 100644
index a5f884d1bfd3f7418d04d748655d7f8140c81698..0000000000000000000000000000000000000000
Binary files a/info/labs/amy-specification/amy-specification.pdf and /dev/null differ
diff --git a/info/labs/amy-specification/amy-specification.tex b/info/labs/amy-specification/amy-specification.tex
deleted file mode 100644
index 0c068fe9dc899c87c4a6dc446cbc72f931cc7d2f..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/amy-specification.tex
+++ /dev/null
@@ -1,37 +0,0 @@
-\documentclass[]{article}
-%\settopmatter{printfolios=true}
-
-% For final camera-ready submission
-% \documentclass[acmlarge]{acmart}
-% \settopmatter{}
-
-\usepackage{amssymb}
-\usepackage{amsmath}
-\usepackage{defs}
-\usepackage{listings}
-\usepackage{stmaryrd}
-\usepackage{xcolor}
-\usepackage{xspace}
-\usepackage[colorlinks]{hyperref}
-\hypersetup{urlcolor=cyan}
-\usepackage{caption} % Link to beginning of figures
-\usepackage{mathpartir}
-%\usepackage{subcaption}
-
-\input{scalalistings}
-
-\title{Specification of the \langname language}
-\date{Computer Language Processing\\~\\LARA\\~\\Autumn 2021}
-
-\begin{document}
-\maketitle
-
-\input{introduction}
-\input{syntax}
-\input{semantics}
- \input{informal}
- \input{formal}
- \input{types}
- \input{moretypes}
-\input{library}
-\end{document}
diff --git a/info/labs/amy-specification/compile.sh b/info/labs/amy-specification/compile.sh
deleted file mode 100644
index e1caad85ca2f1422820411200867e0fce1f0cf64..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/compile.sh
+++ /dev/null
@@ -1,2 +0,0 @@
-pdflatex amy-specification
-pdflatex amy-specification
diff --git a/info/labs/amy-specification/defs.sty b/info/labs/amy-specification/defs.sty
deleted file mode 100644
index 1f50b83793f75095e22c97690a12763ea188379c..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/defs.sty
+++ /dev/null
@@ -1,89 +0,0 @@
-\newcommand{\CEGIS}{\textsf{CEGIS}}
-\newcommand{\TerminalRule}{\textsf{Terminal}}
-\newcommand{\Search}{\textsf{Search}}
-\newcommand{\Verify}{\textsf{Verify}}
-\newcommand{\Enumerate}{\textsf{Enumerate}}
-
-\newcommand{\from}{\mathbin{\leftarrow}}
-\newcommand{\union}{\mathbin{\cup}}
-
-\newcommand{\expt}{\mathcal{E}}
-\newcommand{\Expansions}{\mathcal{E}}
-\newcommand{\prob}[1]{\operatorname{Pr}[#1]}
-\newcommand{\R}{\mathbb{R}}
-\newcommand{\Land}{\bigwedge}
-\newcommand{\cost}{\operatorname{cost}}
-\newcommand{\horizon}{h}
-\newcommand{\score}{score}
-
-\newtheorem{thm}{Theorem}[section]
-
-\newcommand{\smartparagraph}[1]{\noindent\textbf{#1}}
-\newcommand{\sparagraph}[1]{\noindent\textbf{#1}}
-
-\newcommand{\TODO}[1]{\marginpar{\color{red}TODO}{\color{red}#1}\xspace}
-
-% Name calling
-\newcommand{\leon}{Leon\xspace}
-\newcommand{\leonsyn}{LeonSyn\xspace}
-\newcommand{\ourcegis}{STE\xspace} % DONE : find a non-ridiculous name
-\newcommand{\ourca}{CA\xspace}
-\newcommand{\andor}{\textsc{and/or}\xspace}
-\newcommand{\insynth}{InSynth\xspace}
-
-% General math
-\newcommand{\ALL}[2]{\ensuremath{\forall #1 :~ #2}}
-\newcommand{\EX}[2]{\ensuremath{\exists #1 :~ #2}}
-\newcommand{\seq}[1]{\ensuremath{\bar{#1}}}
-\newcommand{\seqa}{\seq{a}\xspace}
-\newcommand{\seqx}{\seq{x}\xspace}
-\newcommand{\seqt}{\seq{T}}
-\newcommand{\seqg}{\seq{G}}
-\newcommand{\seqr}{\seq{r}}
-\newcommand{\varsof}[1]{\ensuremath{\text{vars}(#1)}}
-\newcommand{\splus}{\ensuremath{\mathop{,}}} % separator in sequences
-
-% Synthesis framework
-\newcommand{\br}[4]{\ensuremath{\left\llbracket #1 \ \left\langle #2 \rhd #3 \right\rangle \ #4\right\rrbracket}}
-\newcommand{\pg}[2]{\langle {#1} \mid {#2} \rangle}
-\newcommand{\similar}[1]{\ensuremath{G(\textsf{#1})}}
-\newcommand{\similarr}[2]{\ensuremath{G_{#2}(\textsf{#1})}}
-\newcommand{\prename}{\ensuremath{P}\xspace}
-\newcommand{\pcname}{\ensuremath{\Pi}\xspace}
-\newcommand{\pgname}{\seqt}
-\newcommand{\inputs}{\mathcal{I}}
-\newcommand{\pgite}[3]{\ensuremath{\text{\textsf{if(}}#1\text{\textsf{) \{}}#2\text{\textsf{\} else \{}}#3\text{\textsf{\}}}}}
-\newcommand{\pglet}[3]{\ensuremath{\text{\textsf{val}} \ #1 \colonequals #2 \text{\textsf{;}} \ #3}}
-\newcommand{\match}[2]{\ensuremath{\text{#1\textsf{ match \{ }}#2\text{\textsf{\}}}}}
-\newcommand{\mcase}[2]{\ensuremath{\text{\textsf{ case }}#1 \Rightarrow #2}}
-\newcommand{\code}[1]{\text{\textsf{#1}}}
-
-\newcommand{\guide}[1]{\ensuremath{\odot\mkern-4mu\left[#1\right]}}
-\newcommand{\terminates}[1]{\ensuremath{\Downarrow\mkern-4mu\left[#1\right]}}
-
-% Listing-like things.
-\newcommand{\cl}[1]{\lstinline[mathescape]@#1@}
-\newcommand{\clnoat}[1]{\lstinline[mathescape]!#1!}
-\newcommand{\mcl}[1]{\ensuremath{\mathsf{#1}}}
-% \newcommand{\mcl}[1]{\ensuremath{\text{\lstinline{#1}}}}
-\newcommand{\choosesym}{\cl{choose}}
-
-% Hoare triples
-\newcommand{\HoareTriple}[3]{
- \begin{displaymath}
- \left\{\begin{array}{l}#1\end{array}\right\}
- \begin{array}{l}#2\end{array}
- \left\{\begin{array}{l}#3\end{array}\right\}
- \end{displaymath}
-}
-\newcommand{\hoareTriple}[3]{\{$#1$\} $#2$ \{$#3$\}}
-
-\newcommand{\btrue}{\mcl{true}}
-
-\newcommand{\gpo}{::=}
-\newcommand{\gnt}[1]{~#1~}
-\newcommand{\gt}[1]{\text{\tt \textbf{~#1~}}}
-\newcommand{\gtns}[1]{\text{\tt \textbf{#1}}}
-
-\newcommand{\FIXME}[1]{ {\color{red} FIXME: #1}}
-\newcommand\langname{Amy\xspace}
diff --git a/info/labs/amy-specification/formal.tex b/info/labs/amy-specification/formal.tex
deleted file mode 100644
index 20a3c142a1080cb14effd08ea550d465162a4064..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/formal.tex
+++ /dev/null
@@ -1,36 +0,0 @@
-\subsection{Formal discussion of types}
-
-\newcommand{\hastype}[2]{\Gamma \vdash #1: #2}
-
-In this section, we give a formal (i.e. mathematically robust) description of the Amy typing rules.
-A typing rule will be given as
-\begin{mathpar}
- \inferrule[Rule Name]{P_1 \and \ldots \and P_n}{C}
-\end{mathpar}
-
-\noindent where $P_i$ are the rule \emph{premises} and $C$ is the rule \emph{conclusion}.
-A typing rule means that the conclusion is true under the premises.
-
-Conclusions and most premises will be \emph{type judgements} in an \emph{environment}.
-A type judgement $\hastype{e}{T}$ means that an expression (or pattern) $e$ has type $T$
-in environment $\Gamma$.
-Environments $\Gamma$ are mappings from variables to types and will be written as
-\hbox{$\Gamma = v_1: T_1, \ldots, v_n: T_n$}. We can add a new pair to an environment $\Gamma$
-by writing $\Gamma, v_{n+1}: T_{n+1}$.
-We will also sometimes write a type judgement of the form $\Gamma \vdash p$.
-This means that $p$ typechecks, but we don't assign a type to it.
-Type checking will try to typecheck a program under the \emph{initial environment},
-and reject the program if it fails to do so.
-
-The \emph{initial environment} $\Gamma_0(p)$ of a program $p$ is one
-that contains the types of all functions and constructors in $p$,
-where a constructor is treated as a function from its fields to its parent type
-(see Section~\ref{sec:classes}).
-The initial environment is used to kickstart typechecking at the function definition level.
-
-Figure~\ref{figure:types} lists typing rules for expressions.
-Figure~\ref{figure:moretypes} lists typing rules for patterns, functions and programs.
-In the typing rule for pattern matching,
-$bindings(p)$ refers to the variable bindings implied by a pattern as explained in Section~\ref{sec:expr}.
-Rules for literal patterns are omitted because they are the same as literal expressions.
-
diff --git a/info/labs/amy-specification/informal.tex b/info/labs/amy-specification/informal.tex
deleted file mode 100644
index e1beea72994f08df3ae9d5c840fc6369d466f289..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/informal.tex
+++ /dev/null
@@ -1,168 +0,0 @@
-\subsection{Typing Rules and Semantics of Expressions}
-\label{sec:expr}
-
-Each expression in \langname is associated with a \emph{typing rule},
-which constrains and connects its type and the types of its subexpressions.
-An \langname program is said to \emph{typecheck} if
-(1) all its expressions obey their respective typing rules, and
-(2) the body of each function corresponds to its declared return type.
-A program that does not typecheck will be rejected by the compiler.
-
-\newcommand\Int{\gtns{Int(32)}\xspace}
-\newcommand\Boolean{\gtns{Boolean}\xspace}
-\newcommand\String{\gtns{String}\xspace}
-\newcommand\Unit{\gtns{Unit}\xspace}
-\newcommand{\typeI}[2]{\ensuremath{( #1 ) \RA #2 }}
-\newcommand{\typeII}[3]{\ensuremath{( #1 , #2 ) \RA #3 }}
-\newcommand{\typeIII}[4]{\ensuremath{( #1 , #2 , #3 ) \RA #4 }}
-
-In the following, we will informally give the typing rules
-and explain the semantics (meaning) of each type of expression in \langname.
-We will use function type notation for typing of the various operators.
-For example, $(A, B) \Rightarrow C$ denotes that an operator takes arguments of types $A$ and $B$
-and returns a value of type $C$.
-
-When talking about the semantics of an expression we will refer to a \emph{context}.
-A context is a mapping from variables to the values that have been assigned to them.
-
-\begin{itemize}
- \item Literals of \langname are expressions of the base types that are \emph{values},
- i.e. they cannot be evaluated further.
- The literals \lstinline{true} and \lstinline{false} have type \Boolean.
- \lstinline{()}, the unit literal, has type \Unit.
- String literals have type \String and integer literals have type \Int.
- \item A variable has the type of the corresponding definition
- (function parameter or local variable definition).
- Its value is the value assigned to it in the current context.
- \item \gtns{+}, \gtns{-}, \gtns{*}, \gtns{/} and \gtns{\%} have type \typeII{\Int}{\Int}{\Int},
- and are the usual integer operators.
- \item Unary \gtns{-} has type \typeI{\Int}{\Int} and is the integer negation.
- \item \gtns{<} and \gtns{<=} have type \typeII{\Int}{\Int}{\Boolean} and are the usual arithmetic
- comparison operators.
- \item \gtns{\&\&} and \gtns{||} have type \typeII{\Boolean}{\Boolean}{\Boolean}
- and are the boolean conjunction and disjunction. \emph{Notice that these operators
- are short-circuiting}. This means that the second argument does not get evaluated
- if the result is known after computing the first one.
- For example, \lstinline{true || error("")} will yield \lstinline{true} and not result in an error,
- whereas \lstinline{false || error("")} will result in an error in the program.
- \item \gtns{!} has type \typeI{\Boolean}{\Boolean} and is the boolean negation.
- \item \gtns{++} has type \typeII{\String}{\String}{\String} and is the string concatenation.
- \item \gtns{==} is the equality operator. It has type \typeII{A}{A}{\Boolean} for every type A.
- Equality for values of the \lstinline{Int(32)}, \lstinline{Boolean} and \lstinline{Unit} types
- is defined as \emph{value equality}, i.e. two values are equal if they have the
- same representation. E.g. \lstinline{0 == 0}, \lstinline{() == ()} and \lstinline{(1 + 2) == 3}.
- Equality for the \emph{reference types} \lstinline{String} and all user-defined types
- is defined as \emph{reference equality}, i.e. two values are equal only if they refer to the
- same object.
- I.e. \hbox{\lstinline{""}\ \lstinline{ == ""}},
- \hbox{\lstinline{"a"}\ \lstinline{++ "b"}\ \lstinline{ == "ab"}} and
- \hbox{\lstinline{Nil() == Nil()}} all evaluate to \lstinline{false},
- whereas \hbox{\lstinline{(val s = "Hello"; s == s)}} evaluates to \lstinline{true}.
- \item \gtns{error()} has type \typeI{\String}{A} for any type $A$, i.e. \gtns{error} is always acceptable,
- regardless of the expected type. When a program encounters \gtns{error}, it needs to print
- something like \lstinline{Error: <msg>}, where \lstinline{<msg>} is its evaluated argument,
- and then exit immediately.
- \item \lstinline|if(..) {..} else {..}| has type \typeIII{\Boolean}{A}{A}{A} for any type $A$,
- and has the following meaning:
- First, evaluate the condition of \lstinline{if}. If it evaluates to \lstinline{true},
- evaluate and return the then-branch; otherwise, evaluate and return the else-branch.
- Notice that the value that is not taken is not evaluated.
- \item \lstinline{;} is the \emph{sequence} operator. It has type
- \typeII{A}{B}{B} for any types $A$ and $B$.
- Notice that the first expression has to be well typed, although its precise type does not matter.
- \lstinline{;} evaluates and discards its first argument
- (which we will usually invoke just for its side-effects)
- and then evaluates and returns its second argument.
- \item \lstinline{val n = e; b} defines a local variable with name \lstinline{n} and
- adds it to the context, mapped to the value of \lstinline{e}.
- It is visible in \lstinline{b} but not in \lstinline{e}.
- \lstinline{n} has to obey the name restrictions described in Section~\ref{sec:names}.
- \item An expression \lstinline{f(..)} or \lstinline{m.f(..)} denotes either a function call,
- or an invocation of a type constructor.
- \lstinline{f} has to be the name of a function/constructor defined in the program.
- The types of the real arguments of the function/constructor invocation have to match
- the corresponding types of the formal arguments in the definition of the function/constructor.
- The type of a function/constructor call is the return type of the function,
- or the parent type of the constructor respectively.
-
- Evaluating a function call means evaluating its body in a new context,
- containing the function's formal arguments mapped to the values of the real
- arguments provided at the function call.
- Evaluating a call to a constructor means generating and returning a fresh object
- containing (a reference to) the constructor and the arguments passed to it.
-
- Notice that an invocation of a type constructor \emph{on values} is itself a value,
- i.e. cannot be evaluated further. It corresponds to literals of the other types.
-
- \item \lstinline{match} is the pattern-matching construct of \langname.
- It corresponds to Scala's pattern matching. Java programmers can think of
- it as a generalized switch-statement.
- \lstinline{match} is the only way to access the structure of a value
- of a class type. It also happens to be the most complicated structure
- of \langname.
-
- \paragraph{Terminology:} To explain how the match-expression works, let us first establish some
- terminology. A match case has a \emph{scrutinee} (the first operand,
- which gets pattern matched on), and a number of \emph{match cases}
- (or simply cases). A case is introduced with the keyword \gt{case},
- followed by the \emph{(case) pattern}, then the symbol \gt{=>} and finally
- an expression, which we will call the \emph{case expression}.
-
- As seen in Section~\ref{sec:syntax}, a pattern comes in four different forms,
- which in the grammar are denoted as
- (1) $Id\gtns{(}Patterns\gtns{)}$, (2) $Id$, (3) $Literal$ and \hbox{(4) $\gnt{\_}$}.
- We will call those forms \emph{case class pattern}, \emph{identifier pattern},
- \emph{literal pattern} and \emph{wildcard pattern} respectively.
- The identifier at the beginning of case class pattern is called the \emph{constructor} of the pattern,
- and its arguments are called its \emph{subpatterns}.
-
- \paragraph{Typing rules:} For the match-expression to typecheck, two conditions have to hold:
- \begin{itemize}
- \item All its case expressions have the same type,
- which is also the type of the whole match expression.
- \item All case patterns have to \emph{follow} the type of the scrutinee.
- For a pattern to follow a type means the following, according to its form:
- \begin{itemize}
- \item Each literal pattern follows exactly the type of its literal.
- \item Wildcard and identifier patterns follow any type.
- \item A case class pattern follows only the resulting type of its constructor,
- if and only if all its subpatterns follow the types of the respective
- fields of the constructor.
-
- For example, \lstinline|Nil() match { case Cons(_, t) => () }| typechecks,
- whereas \lstinline|Nil() match { case 0 => () }| does not.
- \end{itemize}
- \end{itemize}
-
- \paragraph{Semantics:} The semantics of pattern matching are as follows:
- First, the scrutinee is evaluated, then cases are scanned one by one
- until one is found whose pattern \emph{matches} the scrutinee value.
- If such case is found, its case expression is evaluated,
- after adding to the environment the variables bound in the case pattern (see below).
- The value produced in this way is returned as the value of the match-expression.
- If none is found, the program terminates with an error.
-
- We say that a pattern \emph{matches} a value when the following holds:
- \begin{itemize}
- \item A wildcard pattern $\gtns{\_}$ or an identifier pattern
- \lstinline{x} match any value. In the second case,
- \lstinline{x} is bound to that value when evaluating
- the case expression.
- \item A literal pattern matches exactly the value of its literal.
- Notice that string literals are compared by reference,
- so they can never match.
- \item A case class pattern \lstinline{case C(..)} matches a value $v$,
- if and only if $v$ has been constructed with the same constructor \lstinline{C}
- and every subpattern of the pattern matches the corresponding field of $v$.
- Notice that we have to recursively bind identifiers in subpatterns.
- \end{itemize}
-
- \item Parentheses \lstinline{(e)} can be used freely around an expression \lstinline{e},
- mainly to override operator precedence or to make the program more readable.
- \lstinline{(e)} is equivalent to \lstinline{e}.
-
- \item When evaluating an expression composed of sub-expressions (e.g. \lstinline{f(a,b)}),
- the different sub-expressions are evaluated in left-to-right order (i.e. in the previous example, the sub-expressions would be valuated in the following order: \lstinline{f} then \lstinline{a} then \lstinline{b}).
- Function calls are done using the call by value strategy.
-\end{itemize}
-
diff --git a/info/labs/amy-specification/introduction.tex b/info/labs/amy-specification/introduction.tex
deleted file mode 100644
index bd4717c680489da26025561812724ef25510bc8e..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/introduction.tex
+++ /dev/null
@@ -1,142 +0,0 @@
-\section{Introduction}
-
-Welcome to the \langname project! This semester you will learn how to compile a simple functional
-Scala-like language
-from source files down to executable code. When your compiler is complete,
-it will be able to take \langname source (text) files as input and produce
-\href{http://webassembly.org}{WebAssembly} bytecode files.
-WebAssembly is a new format for portable bytecode which is meant to be run in browsers.
-
-This document is the specification of \langname. Its purpose is to help you clearly
-and unambiguously understand what an \langname program means,
-and to be the \langname language reference,
-along with the reference compiler.
-It does not deal with how you will actually implement the compiler;
-this will be described to you as assignments are released.
-
-\subsection{Features of \langname}
-Let us demonstrate the basic features of \langname through some examples:
-
-\subsubsection{The factorial function}
-
-\begin{figure}[h]
- \lstinputlisting{Factorial.scala}
-\end{figure}
-
-Every program in \langname is contained in a module, also called \lstinline{object}.
-A function is introduced with the keyword \lstinline{fn}, and all its parameters
-and result type must be explicitly typed.
-\langname supports conditional (or \lstinline{if}-) expressions with obligatory brackets.
-Notice that conditionals are not statements, but return a value,
-in this case an \lstinline{Int}(32).
-
-In fact, there is no distinction between expressions
-and statements in \langname. Even expressions that are called only for their
-side-effects return a value of type \lstinline{Unit}.
-
-The condition of an \lstinline{if}-expression must be of type \lstinline{Boolean}
-and its branches must have the same type, which is also the type of the whole expression.
-
-\subsubsection{Saying hello}
-
-\begin{figure}[h]
- \lstinputlisting{Hello1.scala}
-\end{figure}
-
-\langname supports compiling multiple modules together.
-To refer to functions (or other definitions) in another module,
-one must explicitly use a qualified name.
-There is no import statement like in Scala.
-
-In this example, we refer to the \lstinline{printString} function in the
-\lstinline{Std} module, which contains some builtin functions to interact with the user.
-The string we print is constructed by concatenating two smaller strings
-with the \lstinline{++} operator.
-
-\subsubsection{Input, local variables and sequencing expressions}
-
-\begin{figure}[h]
- \lstinputlisting{Hello2.scala}
-\end{figure}
-
-We can read input from the console with the \lstinline{readX} functions
-provided in \lstinline{Std}.
-
-We can define local variables with \lstinline{val},
-which must always be typed explicitly.
-The value of the variable is given after ``\lstinline{=}'',
-followed by a semicolon.
-
-We can sequence expressions with ``\lstinline{;}''.
-The value of the first expression is discarded,
-and the value of the second one is returned.
-Note that ``\lstinline{;}'' is an \emph{operator}
-and not a terminator: you are not allowed to put it
-at the end of a sequence of expressions.
-
-\subsubsection{Type definitions}
-
-\begin{figure}[h]
- \lstinputlisting{List1.scala}
-\end{figure}
-
-Except for the basic types, a user can define their own types in \langname.
-The user-definable types in \langname come from functional programming and
-are called \emph{algebraic data types}.
-In this case, we define a type, \lstinline{List},
-and two constructors \lstinline{Nil} and \lstinline{Cons},
-which we can call to construct values of type \lstinline{List}.
-
-\subsubsection{Constructing ADT values}
-
-\begin{figure}[h!]
- \lstinputlisting{List2.scala}
-\end{figure}
-
-We can create a \lstinline{List} by calling one of its two constructors like a function,
-as demonstrated in the \lstinline{range} function.
-
-\subsubsection{Pattern matching}
-
-\begin{figure}[h!]
- \lstinputlisting{List3.scala}
-\end{figure}
-
-To use a list value in any meaningful way,
-we have to break it down, according to the constructor used to construct it.
-This is called \emph{pattern matching} and is a powerful feature of functional programming.
-
-In \lstinline{length} we pattern match against the input value \lstinline{l}.
-Pattern matching will check if its argument matches the pattern of the first case,
-and if so will evaluate the corresponding expression.
-Otherwise it will continue with the second case etc.
-If no pattern matches, the program will exit with an error.
-If the constructor has arguments, as does \lstinline{Cons} in this case,
-we can bind their values to fresh variables in the pattern,
-so we can use them in the case expression.
-
-\subsubsection{Wildcard patterns and errors}
-
-\begin{figure}[h]
- \lstinputlisting{List4.scala}
-\end{figure}
-
-The \lstinline{error} keyword takes a string as argument,
-prints \lstinline{Error: } and its argument on the screen,
-then exits the program immediately with an error code.
-In this function, we are trying to compute the head of a list,
-which should fail if the list is empty.
-
-Notice that in the second case,
-we don't really care what the tail of the list is.
-Therefore, we use a \emph{wildcard pattern} (\lstinline{_}),
-which matches any value without binding it to a name.
-
-\subsection{Relation to Scala}
-\langname, with mild syntactic variations, is designed to be as close to a simple subset of Scala as possible.
-However, it is not a perfect subset. You can easily come up with \langname programs
-that are not legal in Scala.
-However, many ``reasonable'' programs will be compilable with \lstinline{scalac},
-provided you provide an implementation of the \langname standard library along with your code.
-This should not be required however, as we are providing a reference implementation of \langname.
-
diff --git a/info/labs/amy-specification/library.tex b/info/labs/amy-specification/library.tex
deleted file mode 100644
index bc231e2b52cd20f488baf1ad37c6251c63e7f829..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/library.tex
+++ /dev/null
@@ -1,38 +0,0 @@
-\section{The standard library of \langname}
-
-\langname comes with a library of predefined functions,
-which are accessible in the \lstinline{Std} object.
-Some of these function implement functionalities
-that are not expressible in \langname,
-e.g. printing to the standard output.
-These \emph{built-in functions} are implemented in JavaScript and \hbox{WebAssembly} in case of compilation,
-and in Scala in the interpreter.
-Built-in functions have stub implementations in the \langname \lstinline{Std} module
-for purposes of name analysis and type checking.
-
-The \langname compiler will not automatically include \lstinline{Std} to the input files.
-If you want them included, you have to provide them manually.
-
-The signature of the \lstinline{Std} module is shown in Figure~\ref{fig:std}.
-
-\begin{figure}
-\begin{lstlisting}
-object Std
- // Output
- fn printString(s: String): Unit = ...
- fn printInt(i: Int(32)): Unit = ...
- fn printBoolean(b: Boolean): Unit = ...
-
- // Input
- fn readString(): String = ...
- fn readInt(): Int(32) = ...
-
- // Conversions
- fn intToString(i: Int(32)): String = ...
- fn digitToString(i: Int(32)): String = ...
- fn booleanToString(b: Boolean): String = ...
-end Std
-\end{lstlisting}
-\caption{The \lstinline{Std} module}
- \label{fig:std}
-\end{figure}
diff --git a/info/labs/amy-specification/moretypes.tex b/info/labs/amy-specification/moretypes.tex
deleted file mode 100644
index 479cffbc1ab4c3307e7defe2536cb63e7f2b742a..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/moretypes.tex
+++ /dev/null
@@ -1,27 +0,0 @@
-\begin{figure}
-\begin{mathpar}
- \inferrule[Wildcard Pattern]
- {~}
- {\hastype{\gtns{\_}}{T}}
-
- \inferrule[Identifier Pattern]
- {~}
- {\hastype{v}{T}}
-
- \inferrule[Case Class Pattern]
- {\hastype{p_1}{T_1} \and \ldots \and \hastype{p_n}{T_n} \and \hastype{C}{(T_1,\ \ldots, T_n) \RA T}}
- {\hastype{C\gtns{(}p_1,\ \ldots, p_n \gtns{)}}{T}}
-
- \inferrule[Function Definition]
- {\Gamma, v_1: T_1,\ \ldots, v_n: T_n \vdash e: T}
- {\Gamma \vdash \gt{fn} f\gtns{(}v_1: T_1,\ \ldots, v_n: T_n\gtns{):}\ T \gt{= \{} e \gt{\}}}
-
- \inferrule[Program]
- {\forall f \in p.\ \Gamma_0(p) \vdash f}
- {\vdash p}
-\end{mathpar}
-\caption{Typing rules for patterns, functions and programs}
-\label{figure:moretypes}
-\end{figure}
-
-
diff --git a/info/labs/amy-specification/scalalistings.tex b/info/labs/amy-specification/scalalistings.tex
deleted file mode 100644
index 8482aca5358577beadef83c7ec4e0b5982ea98a2..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/scalalistings.tex
+++ /dev/null
@@ -1,87 +0,0 @@
-%% To import in the preambule
-%\usepackage{listings}
-
-\usepackage{letltxmacro}
-\newcommand*{\SavedLstInline}{}
-\LetLtxMacro\SavedLstInline\lstinline
-\DeclareRobustCommand*{\lstinline}{%
- \ifmmode
- \let\SavedBGroup\bgroup
- \def\bgroup{%
- \let\bgroup\SavedBGroup
- \hbox\bgroup
- }%
- \fi
- \SavedLstInline
-}
-
-\lstdefinelanguage{ML}{
- alsoletter={*},
- morekeywords={datatype, of, if, *},
- sensitive=true,
- morecomment=[s]{/*}{*/},
- morestring=[b]"
-}
-
-% "define" Scala
-\lstdefinelanguage{scala}{
- alsoletter={@,=,>},
- morekeywords={abstract, Boolean, case, class, fn,
- else, error, extends, false, if, Int, match,
- object, String, true, Unit, val, end},
- sensitive=true,
- morecomment=[l]{//},
- morecomment=[s]{/*}{*/},
- morestring=[b]"
-}
-
-% \newcommand{\codestyle}{\tiny\sffamily}
-\newcommand{\codestyle}{\ttfamily}
-
-\newcommand{\SAND}{\mbox{\tt \&\&}\xspace}
-\newcommand{\SOR}{\mbox{\tt ||}\xspace}
-\newcommand{\MOD}{\mbox{\tt \%}\xspace}
-\newcommand{\DIV}{\mbox{\tt /}\xspace}
-\newcommand{\PP}{\mbox{\tt ++}\xspace}
-\newcommand{\MM}{\mbox{\tt {-}{-}}\xspace}
-\newcommand{\RA}{\Rightarrow}
-\newcommand{\EQ}{\mbox{\tt ==}}
-\newcommand{\NEQ}{\mbox{\tt !=}}
-\newcommand{\SLE}{\ensuremath{\leq}}
-\newcommand{\SGE}{\ensuremath{\geq}}
-\newcommand{\SGT}{\mbox{\tt >}}
-\newcommand{\SLT}{\mbox{\tt <}}
-\newcommand{\rA}{\rightarrow}
-\newcommand{\lA}{\leftarrow}
-
-%============================
-% To make it colorful uncomment \color in next 30 lines
-%\makeatletter
-%\newcommand*\idstyle{%
-% \expandafter\id@style\the\lst@token\relax
-%}
-%\def\id@style#1#2\relax{%
-% \ifcat#1\relax\else
-% \ifnum`#1=\uccode`#1\color{blue!60!black}
-% \fi
-% \fi
- %}
-\makeatother
-% Default settings for code listings
-\lstset{
- language=scala,
- showstringspaces=false,
- columns=fullflexible,
- mathescape=true,
- numbers=none,
- % numberstyle=\tiny,
- basicstyle=\codestyle,
- keywordstyle=\bfseries\color{blue!60!black}
- ,
- commentstyle=\itshape\color{red!60!black}
- ,
- %identifierstyle=\idstyle,
- tabsize=2,
- aboveskip=0pt,
- belowskip=0pt
-}
diff --git a/info/labs/amy-specification/semantics.tex b/info/labs/amy-specification/semantics.tex
deleted file mode 100644
index 052b317bcff30f44d2bd2bbf2d5250e564df372d..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/semantics.tex
+++ /dev/null
@@ -1,120 +0,0 @@
-\section{Semantics}
-In this section we will give the semantics of \langname, i.e. we
-will systematically explain what an \langname program represents,
-as well as give the restrictions that a legal \langname program must obey.
-The discussion will be informal, except for the typing rules
-of \langname.
-
-
-\subsection{Program Structure}
-An \langname program consists of one or more source files.
-Each file contains a single module (\gtns{object}),
-which in turn consists of a series of type and function definitions,
-optionally followed by an expression.
-We will use the terms object and module interchangeably.
-
-\subsection{Execution}
-When an \langname program is executed,
-the expression at the end of each module, if present, is evaluated.
-The order of execution among modules is the same that the user gave
-when compiling or interpreting the program.
-Each module's definitions are visible within the module automatically,
-and in all other modules provided a qualified name is used.
-
-\subsection{Naming rules}
-In this section, we will give the restrictions that a legal \langname program
-must obey with regard to naming or referring to entities defined in the program.
-Any program not following these restrictions should be rejected by the \langname
-name analyzer.
-
-\label{sec:names}
-\begin{itemize}
- \item \langname is case-sensitive.
- \item No two modules in the program can have the same name.
- \item No two classes, constructors, and/or functions in the same module can have the same name.
- \item No two parameters of the same function can have the same name.
- \item No two local variables of the same function can have the same name if they are visible from
- one another.
- This includes binders in patterns of match-expressions.
- Variables that are not mutually visible can have the same name.
- E.g. the program \\
- \lstinline{val x : Int(32) = 0; val x : Int(32) = 1; 2} is not legal, whereas \\
- \lstinline{(val x : Int(32) = 0; 1); (val x : Int(32) = 1; 2)} is.
- \item A local variable can have the same name as a parameter. In this case, the local
- variable definition shadows the parameter definition.
- \item Every variable encountered in an expression
- has to refer to a function parameter or a local variable definition.
- \item All case classes have to extend a class in the same module.
- \item All function or constructor calls or type references have to refer to a function/constructor/type
- defined in the same module, or another module provided a qualified name is given.
- It is allowed to refer to a constructor/type/function before declaring it.
- \item All calls to constructors and functions have to have the same number of arguments
- as the respective constructor/function definition.
-\end{itemize}
-
-\subsection{Types and Classes}
-\label{sec:classes}
-Every expression, function parameter, and class parameter in \langname has a \emph{type}.
-Types catch some common programming errors by introducing \emph{typing restrictions}.
-Programs that do not obey these restrictions are illegal and will be rejected by
-the \langname type checker.
-
-The built-in types of \langname are \gtns{Int(32)}, \gtns{String}, \gtns{Boolean} and \gtns{Unit}.
-
-\gtns{Int(32)} represents 32-bit signed integers.
-\gtns{String} is a sequence of characters. Strings have poor support in \langname:
-the only operations defined on them are are concatenation and conversion to integer.
-In fact, not even equality is ``properly'' supported (see Section~\ref{sec:expr}).
-\gtns{Boolean} values can take the values \gtns{true} and \gtns{false}.
-\gtns{Unit} represents a type with a single value, \gtns{()}.
-It is usually used as the result of a computation which is invoked for its side-effects only,
-for example, printing some output to the user.
-It corresponds to Java's \gtns{void}.
-
-In addition to the built-in types, the programmer can define their own types.
-The sort of types that are definable in \langname are called
-\href{https://en.wikipedia.org/wiki/Algebraic_data_type}{Algebraic Data Types} (ADTs)
-and come from the functional programming world,
-but they have also been successfully adopted in Scala.
-
-An ADT is a \emph{type} along with several \emph{constructors} that can create
-values of that type. For example, an ADT defining a list of integers
-in pseudo syntax may look like this:
-\lstinline{type List = Nil() | Cons(Int(32), List)},
-which states that a \lstinline{List} is either \lstinline{Nil} (the empty list),
-or a \lstinline{Cons} of an integer and another list.
-We will say that \lstinline{Cons} has two \emph{fields} of types \lstinline{Int(32)} and \lstinline{List},
-whereas \lstinline{Nil} has no fields.
-Inside the program, the only way to construct values of the \lstinline{List} type
-is to call one of these constructors, e.g. \lstinline{Nil()} or \lstinline{Cons(1, Cons(2, Nil()))}.
-You can think of them as functions from their field types to the \lstinline{List} type.
-
-Notice that in the above syntax, \lstinline{Nil} and \lstinline{Cons}
-are \textbf{not} types. More specifically, they are not subtypes of \lstinline{List}:
-in fact, there is no subtyping in \langname.
-Only \lstinline{List} is a type, and values such as \lstinline{Nil()} or \lstinline{Cons(1, Cons(2, Nil()))}
-have the type \lstinline{List}.
-
-In \langname, we use Scala syntax to define ADTs.
-A type is defined with an abstract class and the constructors with case classes.
-The above definition in \langname would be:
-\begin{figure}[h]
-\begin{lstlisting}
-abstract class List
-case class Nil() extends List
-case class Cons(h: Int(32), t: List) extends List
-\end{lstlisting}
-\end{figure}
-
-Notice that the names of the fields have no practical meaning,
-and we only use then to stay close to Scala.
-
-We will sometimes use the term abstract class for a type
-and case class for a type constructor.
-
-The main programming structure to manipulate class types
-is \emph{pattern matching}. In Section~\ref{sec:expr} we define how pattern matching works.
-
-
-% Cont. in informal.tex
-
diff --git a/info/labs/amy-specification/syntax.tex b/info/labs/amy-specification/syntax.tex
deleted file mode 100644
index 8b33059e9728caef28e7ab7c39bc243a69a34f84..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/syntax.tex
+++ /dev/null
@@ -1,152 +0,0 @@
-\section{Syntax}
-\label{sec:syntax}
-\def\alt{~~|~~}
-
-\def\Expr{\gnt{Expr}}
-\def\Id{\gnt{Id}}
-\def\ID{\gnt{ID}}
-\def\({\gt{(}}
-\def\){\gt{)}}
-
-\begin{figure}
-\begin{equation*}
-\begin{array}{rl}
-\gnt{Program} \gpo & \gnt{Module^*} \\
-\gnt{Module} \gpo & \gt{object} \Id \gnt{Definition^*} \gnt{Expr?} \gt{end} \Id \\
-\gnt{Definition} \gpo & \gnt{AbstractClassDef} \alt \gnt{CaseClassDef} \alt \gnt{FunDef} \\
-\gnt{AbstractClassDef} \gpo & \gt{abstract} \gt{class} \Id \\
-\gnt{CaseClassDef} \gpo & \gt{case} \gt{class} \Id \( \gnt{Params} \) \gt{extends} \Id \\
-\gnt{FunDef} \gpo & \gt{fn} \gnt{Id} \( \gnt{Params} \) \gt{:} \gnt{Type} \gt{=} \gt{\{} \Expr \gt{\}} \\
- \gnt{Params} \gpo & \ \, \epsilon \alt \gnt{ParamDef} [\gt{,} \gnt{ParamDef}]^* \\
-\gnt{ParamDef} \gpo & \gnt{Id} \gt{:} \gnt{Type} \\
-\gnt{Type} \gpo & \gt{Int} \( \gnt{32} \) \alt \gt{String} \alt \gt{Boolean} \alt \gt{Unit} \alt [\Id \gnt{.}]? \Id \\
-\gnt{Expr} \gpo & \Id \\
- \alt & \gnt{Literal} \\
- \alt & \Expr\ \ \gnt{BinOp}\ \ \Expr \\
- \alt & \gnt{UnaryOp} \Expr \\
- \alt & \; [\Id \gnt{.}]? \Id \( \gnt{Args} \) \\
- \alt & \Expr \gt{;} \Expr \\
- \alt & \gt{val} \gnt{ParamDef} \gt{=} \gnt{Expr} \gt{;} \gnt{Expr} \\
- \alt & \gt{if} \( \Expr \) \gt{\{} \gnt{Expr} \gt{\}} \gt{else} \gt{\{} \gnt{Expr} \gt{\}} \\
- \alt & \Expr \gt{match} \gt{\{} \gnt{MatchCase^+} \gt{\}} \\
- \alt & \gt{error} \gt{(} \Expr \gt{)} \\
- \alt & \( \Expr \) \\
-\gnt{Literal} \gpo & \gt{true} \alt \gt{false} \alt \( \) \\
- \alt & \gnt{IntLiteral} \alt \gnt{StringLiteral} \\
-\gnt{BinOp} \gpo & \gt{+}\alt \gt{-} \alt \gt{*} \alt \gt{/} \alt \gt{\%} \alt \gt{<} \alt \gt{<=} \\
- \alt & \gt{\&\&} \alt \gt{||} \alt \gt{==} \alt \gt{++} \\
-\gnt{UnaryOp} \gpo & \gt{-} \alt \gt{!} \\
-\gnt{MatchCase} \gpo & \gt{case} \gnt{Pattern} \gt{=>} \Expr \\
-\gnt{Pattern} \gpo & \; [\Id \gnt{.}]? \Id \( \gnt{Patterns} \) \alt \Id \alt \gnt{Literal} \alt \gt{\_} \\
- \gnt{Patterns} \gpo & \ \; \epsilon \alt \gnt{Pattern} [\gt{,} \gnt{Pattern}]^* \\
- \gnt{Args} \gpo & \ \, \epsilon \alt \Expr [\gt{,} \Expr]^* \\
-\end{array}
-\end{equation*}
-\caption{Syntax of \langname}
-\label{figure:syntax}
-\end{figure}
-
-\begin{figure}
-\begin{equation*}
-\begin{array}{rl}
-\gnt{IntLiteral} \gpo & \gnt{Digit^+}\\
-\gnt{Id} \gpo & \gnt{Alpha} \gnt{AlphaNum^*} \text{(and not a reserved word)}\\
-\gnt{AlphaNum} \gpo & \gnt{Alpha} \alt \gnt{Digit}\ \alt \gtns{\_} \\
-\gnt{Alpha} \gpo & ~[\gtns{a}-\gtns{z}]\ \alt [\gtns{A}-\gtns{Z}] \\
-\gnt{Digit} \gpo & ~[\gtns{0}-\gtns{9}] \\
-\gnt{StringLiteral} \gpo & ~\gtns{"} \gnt{StringChar^*} \gtns{"}\\
-\gnt{StringChar} \gpo & ~\text{Any character except newline and $\gtns{"}$}
-\end{array}
-\end{equation*}
-\caption{Lexical rules for \langname}
-\label{figure:lexing}
-\end{figure}
-
-
-The syntax of \langname is given formally by the context-free grammar of Figure~\ref{figure:syntax}.
-Everything spelled in $italic$ is a nonterminal symbol of the grammar,
-whereas the terminal symbols are spelled in \gtns{monospace} font.
-$^*$ is the Kleene star, $s^+$ stands for one or more repetitions of $s$,
-and $?$ stands for optional presence of a symbol (zero or one repetitions).
-The square brackets $[]$ are not symbols of the grammar,
-they merely group symbols together.
-
-Before parsing an \langname program, the Amy \emph{lexer} generates a sequence of terminal symbols
-(\emph{tokens}) from the source files.
-Some non-terminal symbols mentioned, but not specified, in Figure~\ref{figure:syntax}
-are also represented as a single token by the lexer.
-They are lexed according to the rules in Figure~\ref{figure:lexing}.
-In Figure~\ref{figure:lexing}, we denote the range between characters $\alpha$ and $\beta$ (included)
-with $[\alpha - \beta]$.
-
-The syntax in Figure~\ref{figure:syntax} is an \emph{overapproximation} of the real syntax of \langname.
-This means that it allows some programs that should not be allowed in Amy.
-To get the real syntax of Amy, there are some additional restrictions presented (among other things)
-in the following notes:
-
-\begin{itemize}
- \item The reserved words of \langname are the following:
- \gtns{abstract}, \gtns{Boolean}, \gtns{case}, \gtns{class}, \gtns{fn},
- \gtns{else}, \gtns{error}, \gtns{extends}, \gtns{false}, \gtns{if}, \gtns{Int}, \gtns{match},
- \gtns{object},
- \gtns{end},
- \gtns{String}, \gtns{true}, \gtns{Unit}, \gtns{val}, \gtns{\_} (the wildcard pattern).
-
- Identifiers are not allowed to coincide with a reserved word.
- \item The operators and language constructs of \langname
- have the following precedence, starting from the \emph{lowest}:
-
- (1) \lstinline{val}, \lstinline{;}
- (2) \lstinline{if}, \lstinline{match} (3) \lstinline{||}
- (4) \lstinline{&&} (5) \lstinline{==}
- (6) \lstinline{<}, \lstinline{<=} (7) \lstinline{+}, \lstinline{-}, \lstinline{++}
- (8) \lstinline{*}, \lstinline{/}, \lstinline{%}
- (9) Unary \lstinline{-}, \lstinline{!}
- (10) \lstinline{error}, calls, variables, literals, parenthesized expressions.
-
- For example,\\
- \lstinline{1 + 2 * 3} means \lstinline{1 + (2 * 3)} and \\
- \lstinline|1 + 2 match {...}| means \lstinline|(1 + 2) match {...}|.
-
- A little more complicated is the interaction between \lstinline{;} and \lstinline{val}:
- the definition part of the \lstinline{val} extends only as little as the first semicolon,
- but then the variable defined is visible through any number of semicolons.
- Thus
- \lstinline{(val x: Int(32) = y; z; x)} means \lstinline{(val x: Int(32) = y; (z; x)) }
- \sloppy{and not \lstinline{(val x: Int(32) = (y; z); x)} or \lstinline{((val x: Int(32) = y; z); x)}}
- (i.e. \lstinline{x} takes the value of y and is visible until the end of the expression).
-
- All operators are left-associative. That means that within
- the same precedence category, the leftmost application of an operator takes precedence.
- An exception is the sequence operator, which for ease of the implementation
- (you will understand during parsing)
- can be considered right-associative (it is an associative operator so it does not really
- matter).
- \item A \lstinline{val} definition is not allowed directly in the value assigned
- by an enclosing \lstinline{val} definition.
- E.g. \lstinline{(val x: Int(32) = val y: Int(32) = 0; 1; 2)} is not allowed.
- On the other hand, \lstinline{(val x: Int(32) = 0; val y: Int(32) = 1; 2)} is allowed.
- \item It is not allowed to use a \lstinline{val} as a (second) operand to an operator.
- E.g. \lstinline{(1 + val x: Int(32) = 2; x)} is not allowed.
- \item A unary operator is not allowed as a direct argument of another unary operator.
- E.g. \lstinline{--x} is not allowed.
- \item It is not allowed to use \lstinline{match} as a first operand of any binary operator,
- except \lstinline{;}. E.g. \lstinline|(x match { ... } + 1)| is not allowed.
- On the other hand \lstinline|(x match { ... }; x)| is allowed.
- \item The syntax $[\Id \gnt{.}]? \Id$ refers to an optionally qualified name,
- for example either \lstinline{MyModule.foo} or \lstinline{foo}.
- If the qualifier is included, the qualified name refers to a definition
- \lstinline{foo} in another module \lstinline{MyModule};
- otherwise, \lstinline{foo} should be defined in the current module.
- Since \langname does not have the import statement of Scala or Java,
- this is the only way to refer to definitions in other modules.
- \item One line comments are introduced with ``\lstinline{//}'': \lstinline{// This is a comment}.
- Everything until the end of the line is a comment and should be ignored by the lexer.
- \item Multiline comments can be used as follows: \lstinline{/* This is a comment */}.
- Everything between the delimiters is a comment, notably including newline characters
- and \lstinline{/*}. Nested comments are not allowed.
- \item Escaped characters are not recognised inside string literals.
- I.e. \lstinline{"\n"} stands for a string literal which contains
- a backspace and an ``n''.
-\end{itemize}
-
diff --git a/info/labs/amy-specification/types.tex b/info/labs/amy-specification/types.tex
deleted file mode 100644
index 86af857a4ab74a26b0ed67ac139edebba2fd4f80..0000000000000000000000000000000000000000
--- a/info/labs/amy-specification/types.tex
+++ /dev/null
@@ -1,66 +0,0 @@
-\newcommand{\typingI}[5]{\inferrule[#1]{\Gamma \vdash #2: #3}{\Gamma \vdash #4: #5}}
-\newcommand{\typingII}[7]{\inferrule[#1]{\Gamma \vdash #2: #3 \and \Gamma \vdash #4: #5}{\Gamma \vdash #6: #7}}
-
-\begin{figure}
-\begin{mathpar}
- \inferrule[Variable]{v: T \in \Gamma}{\hastype{v}{T}}
-
- \inferrule[Int Literal]{i \text{ is an integer literal}}{\hastype{i}{\Int}}
-
- \inferrule[String Literal]{s \text { is a string literal}}{\hastype{s}{\String}}
-
- \inferrule[Unit]{~}{\hastype{\gtns{()}}{\Unit}}
-
- \inferrule[Boolean Literal]{b \in \{\gtns{true}, \gtns{false}\}}{\hastype{b}{\Boolean}}
-
- \inferrule[Arith. Bin. Operators]
- {\hastype{e_1}{\Int} \and \hastype{e_2}{\Int} \and op \in \{\gtns{+}, \gtns{-}, \gtns{*}, \gtns{/}, \gtns{\%} \} }
- {\hastype{e_1\ op\ e_2}{\Int}}
-
- \inferrule[Arith. Comp. Operators]
- {\hastype{e_1}{\Int} \and \hastype{e_2}{\Int} \and op \in \{\gtns{<}, \gtns{<=} \} }
- {\hastype{e_1\ op\ e_2}{\Boolean}}
-
- \inferrule[Arith. Negation]{\hastype{e}{\Int}}{\hastype{\gtns{-}e}{\Int}}
-
- \inferrule[Boolean Bin. Operators]
- {\hastype{e_1}{\Boolean} \hskip -5pt \and \hastype{e_2}{\Boolean} \hskip -5pt \and op \in \{\gtns{\&\&}, \gtns{||}\} }
- {\hastype{e_1\ op\ e_2}{\Boolean}}
-
- \inferrule[Boolean Negation]{\hastype{e}{\Boolean}}{\hastype{\gtns{!}e}{\Boolean}}
-
- \inferrule[String Concatenation]
- {\hastype{e_1}{\String} \and \hastype{e_2}{\String} }
- {\hastype{e_1 \gt{++} e_2}{\String}}
-
- \inferrule[Equality]
- {\hastype{e_1}{T} \and \hastype{e_2}{T}}
- {\hastype{e_1 \gt{==} e_2}{\Boolean}}
-
- \inferrule[Sequence]
- {\hastype{e_1}{T_1} \and \hastype{e_2}{T_2}}
- {\hastype{e_1 \gt{;} e_2}{T_2}}
-
- \inferrule[Local Variable Definition]
- {\hastype{e_1}{T_1} \and \Gamma, n: T_1 \vdash e_2: T_2}
- {\hastype{\gtns{val}~ n \gt{:} T_1 \gt{=} e_1\gt{;} e_2}{T_2}}
-
- \inferrule[Function/Class Constructor Invocation]
- {\hastype{e_1}{T_1} \and \ldots \and \hastype{e_n}{T_n} \and \hastype{f}{(T_1, \ldots, T_n) \RA T}}
- {\hastype{f(e_1, \ldots, e_n)}{T}}
-
- \inferrule[If-Then-Else]
- {\hastype{e_1}{\Boolean} \and \hastype{e_2}{T} \and \hastype{e_3}{T}}
- {\hastype{\gtns{if (}e_1 \gtns{) \{} e_2 \gtns{\} else \{}e_3\gtns{\}}}{T}}
-
- \inferrule[Error]{\hastype{e}{\String}}{\hastype{\gtns{error(}e\gtns{)}}{T}}
-
- \inferrule[Pattern Matching]
- {\hastype{e}{T_s} \and \forall i \in [1,n].\ \hastype{p_i}{T_s} \and \forall i \in [1,n].\ \Gamma, bindings(p_i) \vdash e_i : T_c}
- {\hastype{e \gt{match \{ case} p_1 \gt{=>} e_1\ \ldots \gt{case} p_n \gt{=>} e_n\ \gtns{\}}}{T_c}}
-\end{mathpar}
-\caption{Typing rules for expressions}
-\label{figure:types}
-\end{figure}
-
-