From 3c32ced19571be6d40e023c74b1ed46568ab6dde Mon Sep 17 00:00:00 2001
From: Aron <arostr-5@student.ltu.se>
Date: Mon, 4 Nov 2019 15:52:51 +0100
Subject: [PATCH] added type checker

---
 HOME_EXAM.md | 229 +++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 211 insertions(+), 18 deletions(-)

diff --git a/HOME_EXAM.md b/HOME_EXAM.md
index a464103..c80fb4d 100644
--- a/HOME_EXAM.md
+++ b/HOME_EXAM.md
@@ -183,12 +183,6 @@ For furture development
 
 ## Your semantics
 
-- Give an as complete as possible Structural Operetional Semantics (SOS) for your language
-
-- Explain (in text) what an interpretation of your example should produce, do that by dry running your given example step by step. Relate back to the SOS rules. You may skip repetions to avoid cluttering.
-
-- Compare your solution to the requirements (as stated in the README.md). What are your contributions to the implementation.
-
 Structural Operational Semantics (SOS)
 
 Symbols: 
@@ -213,7 +207,7 @@ fn main() {
     test();
 }
 ```
-The function call moves the current state, $σ$ to the new derived state $σ'$ in the function, test()'s context.
+The function call moves the current state, $σ$ to the new derived state $σ'$ in the function, test()'s context. A function can evaluate void (none), i32 and bool.
 
 Command sequence
 
@@ -225,7 +219,7 @@ test();
 ```
 A sequence is a composition of commands where the first command is first executed then the second command. Otherwise the intermediate step, $σ'$ would be lost.
 
-Operands for arithmetic expressions
+Operands for lhs, rhs arithmetic expressions
 
 $\frac{<e1,σ> ⇓ n1 <e2, σ> ⇓ n2}{<e1 + e2, σ> ⇓ n1 \text{ } plus \text{ } n2}$
 
@@ -238,19 +232,25 @@ plus is addition as implemented in the computer. Other arithmetic operands imlem
 - "==", equal
 - "!=", not equal
 
-Operands for boolean expressions
+```rust
+(2 + 4) * 3;
+1 < 2; // Is valid!
+```
+
+Operands for lhs, rhs boolean expressions
 
 $\frac{<e1,σ> ⇓ b1 <e2, σ> ⇓ b2}{<e1 == e2, σ> ⇓ b1 \text{ } equal \text{ } b2}$
 
-how equals is evaluated is up to the computer. Other boolean operands implemented are
+how equal is evaluated is up to the computer. Other boolean operands implemented are
 
-- ">", greather than
--  "<", less than
 - "==", equal
 - "!=", not equal
 - "&&", and
 - "||", or
-
+```rust
+2 != 3 || true;
+1 != true; // Will panic!()
+```
 
 
 If true
@@ -271,7 +271,13 @@ $\frac{<b,σ> ⇓ false}{<while \text{ } b \text{ } do \text{ } c,σ> ⇓ σ}$
 
 While true
 
-$\frac{<b, σ> ⇓ true <c,σ> ⇓ σ' 0 <while \text{ } b \text{ } do \text{ } c, σ'> ⇓ σ''}{<while \text{ } b \text{ } do \text{ } c,σ> ⇓ σ''}$
+$\frac{<b, σ> ⇓ true <c,σ> ⇓ σ' <while \text{ } b \text{ } do \text{ } c, σ'> ⇓ σ''}{<while \text{ } b \text{ } do \text{ } c,σ> ⇓ σ''}$
+```rust
+let a : i32 = 0;
+while a < 5 {
+    a = a + 1;
+}
+```
 
 then $σ'$ is the result of the current state, $σ$ and the last state $σ''$ is the result of $σ'$.
 
@@ -281,7 +287,7 @@ $\frac{<x, σ>⇓<let \text{ } x:=e, σ>⇓σ'}{<let \text{ } x := e, σ> ⇓ σ
 ```rust
 let a : i32 = 1;
 let b : bool = true;
-let c : i32 = test(); // test() explicit return of type i32
+let c : i32 = test(); // c will be assigned whaterver test() returns
 ```
 For let commands,  if the variable is already declared the state $σ$ will be changed to the one of the second command, state $σ'$, the variable will be lost. Otherwise the variable will be assigned to the state, $σ$.
 
@@ -294,8 +300,12 @@ x = 1;
 x = true;
 x = test();
 ```
+(OBS the interpreter does not check types, above assignments are valid in the interpreter)
+
 For assignment, when the variable is assigned to a number, boolean or function the variable and corresponding rhs is moved to the same state.
 
+
+
 Return
 
 $\frac{<f, σ>⇓σ}{<return : e, σ> ⇓ σ[return : e]}$
@@ -307,18 +317,201 @@ fn main() -> i32 {
 ```
 At explicit return the expression is moved to the state of the function.
 
+Currently, the interpreter executes as above SOS describes. The interpretern does not type check e.g.
+```rust
+fn main() {
+    return 1 + 1;
+}
+```
+where an i32 is returned to a void (none) type declared funtion. It's valid in the interpreter. 
+
+Meanwhile there are cases where the interpreter will panic!() e.g. return x + true or trying to assign an undeclared variable.
 
+The interpreter has been implented with scopes and context in mind, this is described above in the SOS with state, σ. E.g. variables declared inside a if block/scope (state) are not accesible outside of that block/scope. 
+```rust
+if true {
+    let a : i32 = 0;
+}
+a = 1; // Will panic!()
+```
+```rust
+let a : i32 = 0;
+if true {
+    a = 1; // Will NOT panic!()
+}
+```
+Each function has a unique context with a collection of scopes. The way context and scope have been implemented may be a bit off to the SOS rules of rust but not off according to above described SOS rules.
 
 ## Your type checker
 
-- Give an as complete as possible set of Type Checking Rules for your language (those rules look very much like the SOS rules, but over types not values).
+Types are now defined as
+- i32
+- bool
+- none
 
-- Demonstrate each "type rule" by an example.
 
-- Compare your solution to the requirements (as stated in the README.md). What are your contributions to the implementation.
+Command sequence
+
+$\frac{<c1,σ> ⇓ σ' <c2,σ'> ⇓ σ''}{<c1;c2,σ> ⇓ σ''}$
+
+as described in the SOS rules of the interpreter.
+
+
+Operands for i32 types
+
+$\frac{<e1,σ> ⇓ i32 <e2, σ> ⇓ i32}{<e1 + e2, σ> ⇓ i32}$
+
+To operate these operands the expression need to evaluate to i32. Other arithmetic operands imlemented are
+- -, minus
+- *, multiplication
+- /, division
+- ">", greather than
+-  "<", less than
+- "==", equal
+- "!=", not equal
+
+```rust
+1 + 1;
+1 + true; //TypeError
+```
+
+Operands for boolean types
+
+$\frac{<e1,σ> ⇓ bool <e2, σ> ⇓ bool}{<e1 == e2, σ> ⇓ bool}$
+
+To operate these operands the expression need to evaluate to boolean. Other boolean operands implemented are
+
+- "==", equal
+- "!=", not equal
+- "&&", and
+- "||", or
+
+```rust
+true || false;
+1 || true; //TypeError
+```
+
+If true/false
+
+$\frac{<e, σ> ⇓ bool <c1, σ> ⇓ σ'}{<if \text{ } bool \text{ } then \text{ } c1> ⇓ σ}$
+
+```rust
+if false {
+    test(); // This will execute 
+}
+```
+
+While true/false
+
+$\frac{<e, σ> ⇓ bool <c,σ> ⇓ σ' <while \text{ } bool \text{ } do \text{ } c, σ'> ⇓ σ''}{<while \text{ } bool \text{ } do \text{ } c,σ> ⇓ σ''}$
+
+For both if and while commands their block/scope are evluated as long as their condition is evaluted to the type boolean. This differ from the interpreter which only executes the block/scope if the condition is true.
+
+
+Let assignment i32 expression
+
+$\frac{<x, σ>⇓i32<let \text{ } x:=i32, σ>⇓σ'}{<let \text{ } x := i32, σ> ⇓ σ[x := i32]}$
+```rust
+let a : i32 = 1;
+let b : i32 = test(); // test() must return type i32 otherwise Error
+```
+Let assignment bool expression
+
+$\frac{<x, σ>⇓bool<let \text{ } x:=bool, σ>⇓σ'}{<let \text{ } x := bool, σ> ⇓ σ[x := bool]}$
+```rust
+let a : bool = true;
+let b : bool = test(); // test() must return type bool otherwise Error
+```
+As previously mentioned, let assignment are unique declerations. Thus, the same variable can not be declared twice in the same scope. Here, the given return type of the variable is checked with rhs evluated type.
+
+Assignment i32 expression
+
+$\frac{<x, σ> ⇓ i32<e, σ> i32}{<x := i32, σ> ⇓ σ[x := i32]}$
+
+```rust
+x = 1;
+```
+Assignment bool expression
+
+$\frac{<x, σ> ⇓ bool<e, σ> bool}{<x := bool, σ> ⇓ σ[x := bool]}$
+
+```rust
+x = true;
+```
+For any assigment, the variable typed stored with the rhs evaluated type is checked.
+
+
+
+Return i32
+
+$\frac{<f, σ>⇓σ}{<return : i32, σ> ⇓ σ[return : i32]}$
+
+```rust
+fn main() -> i32 {
+    return 1 + 1;
+}
+```
+The function is declared to return a type i32.
+
+
+Return bool
+
+$\frac{<f, σ>⇓σ}{<return : bool, σ> ⇓ σ[return : bool]}$
+
+```rust
+fn main() -> bool {
+    return true && true;
+}
+```
+The function is declared to return a type boolean.
+
+Void (none)
+
+$\frac{<f, σ>⇓σ}{<none, σ> ⇓ σ[none]}$
+
+```rust
+fn main() {
+    let a : i32 = 1 + 1;
+    return a; //ReturnError
+}
+```
+
+If the function does not explicit return then the type none is returned.
+
+Missing in the type checker are fully checking that a function returns, see example
+```rust
+fn test() -> i32 {
+    if true {
+        return 1 - 1;
+    }
+    // Error? This block returns none, with if command, it might not return!
+}
+```
+
+SOS rules of the type checker that has not been described above are the type checking of function parameter, argument and length.
+
+TO DISCUSS:
+Alternative answer would be to defined the SOS rules for functions as
+$<f, i32>⇓i32$, $<f, bool>⇓bool$, $<f, none>⇓none$. 
+
+The type checker will return a custom error with sufficient information except location e.g.
+```rust
+enum Error {
+    TypeError(Type, Type, Expr),
+    ReturnError(Type, Type, String),
+    ...
+}
+```
+
+
+In the future the type checking can be expanded to handle mutability and memory reference. Also, to implement more sophisticated error handling as error chaining (multiple error) and location.
+
 
 ## Your borrrow checker
 
+
+
+
 - Give a specification for well versus ill formed borrows. (What are the rules the borrow checker should check).
 
 - Demonstrate the cases of ill formed borrows that your borrow checker is able to detect and reject.
-- 
GitLab