diff --git a/HOME_EXAM.md b/HOME_EXAM.md index 9194812a33db47267aba2ecf7df8364b3892b516..aad26f7b546aab407862663e5723378a11a8532e 100644 --- a/HOME_EXAM.md +++ b/HOME_EXAM.md @@ -435,9 +435,125 @@ For the interpreter to accept a program is a main() method needed. Currently the interpreter does not handle the right scopes compleatly but this is not a problem due to the type checker taking care of it. ## Type checker +Supported types: +- i32 +- bool +- unit +- unknown + +##### Arithmetic, boolean & comparison operations +```math +\frac{<e0,σ> → i32 <e1,σ> → i32}{<e0 + e1,σ> → i32} +``` +SOS for addition between two types, if an expression does not follow this rule the expression will be rejected. + +Similar SOS goes for the following operands: +- "-", subtraction +- "*", multiplication +- "/", division + +```math +\frac{<e0,σ> → i32 <e1,σ> → i32}{<e0 > e1,σ> → bool} +``` +SOS for comparison between two i32 types returning a boolean. + +Simliar SOS goes for the following operands: +- "<", less +- ">=", greater of equal +- "<=", less or equal +- "==", equals +- "!=", not equals + +For the two last operands can the types for e0 and e1 be both i32 and boolean, concluding in a boolean. + +```math +\frac{<e0,σ> → bool <e1,σ> → bool}{<e0 || e1,σ> → bool} +``` +SOS for the or operand between two boolean types returning a boolean. + +Similar SOS goes for the following operand: +- "&&", and + +```rust + 5 * 3; + 3 > 2; + (true || false) == true; + 1 + false; //Invalid type bool for operand + + true && 5; //Invalid type i32 for operand && +``` + +##### Assignment +```math +\frac{<x,σ> → bool <e,σ> → bool}{<x:=e,σ>} +``` +Let statements works in a similiar way. For an assignment to be valid needs the variable to be initialized as mutable together with a type. An assignment will only be accepted by the type checker if the new type matches the current. + +The initialization of a function does also follow a similiar SOS rule. + +```rust +fn a() -> () { + let mut x: bool = true; + x = false; + x = 5; // Invalid, x has type bool +} +fn b() -> bool { + 1 + 2 +} // Invalid, block returns i32 but return type is bool +``` + +##### Conditional command +```math +\frac{<e,σ> → \text{ bool } <c0,σ> → σ'}{<\text{ if bool then } c0 \text{ else } c1,σ> → σ'}; +``` + +For the if statement to go through the type checker need the expression, e, be a boolean. + +```rust + if 5 > 3 { + x = x + 1; + } // Valid + if 5 + 3 { + x = x - 1; + } // Invalid, expression 5 + 3 does not return a boolean +``` + +##### While command +```math +\frac{<e,σ> → \text{ bool } <c,σ> → σ'' <\text{ while bool do } c,σ''> → σ'}{<\text{ while bool do } c,σ> → σ'} +``` + +```rust + while 3 > 5 { + x = x - 1; + } // Valid for type checker + while 3 * 5 { + x = x + 1; + } // Invalid, expression is not a boolean +``` +The example above is valid for the type checker due to it only checking that the expression is a boolean. The interpreter will not execute the block statement due to the expression being false. + +#### Coverage +The type checker rejects programs where: + +- Expressions contains mismatching types +- Assignment are done with conflicting types (both for expression and functioncalls) +- Assignment are trying to be done to non mutable variables +- If and while statements does not have a boolean as an expression +- Function does not return the specified type +- Variables not found in scope + +Information is being spawn about the error when occuring. + +#### Future improvements +It would be nice do add the following in the future: + +- Multiple error reporting +- Type inference ## Borrow checker + + ## Conclusion