Add new file

HOME_EXAM_Type_check_part2.md

+- 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)
+
+### Expressions
+#### Arithmetic
+Addition:
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 + e2) \ : \ i32}
+```
+
+Subtraction:
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 - e2) \ : \ i32}
+```
+
+Division:
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 / e2) \ : \ i32}
+```
+
+Multiplication:
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 * e2) \ : \ i32}
+```
+
+Unary:
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32}{\Gamma \ \vdash (-e1) \ : \ i32}
+```
+
+#### Boolean
+AND:
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ bool \quad \Gamma \ \vdash \ e2 \ : \ bool}{\Gamma \ \vdash (e1 \ \&\& \ e2) \ : \ bool}
+```
+
+OR:
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ bool \quad \Gamma \ \vdash \ e2 \ : \ bool}{\Gamma \ \vdash (e1 \ || \ e2) \ : \ bool}
+```
+
+Less than (<):
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ < \ e2) \ : \ bool}
+```
+
+Greaten than (>):
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ > \ e2) \ : \ bool}
+```
+
+Less than or equals (<=):
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ <= \ e2) \ : \ bool}
+```
+
+Greater than or equals (>=):
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ >= \ e2) \ : \ bool}
+```
+
+Equals (==):
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ bool \quad \Gamma \ \vdash \ e2 \ : \ bool}{\Gamma \ \vdash (e1 \ == \ e2) \ : \ bool}
+```
+or
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ == \ e2) \ : \ bool}
+```
+
+Not equals (!=):
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ bool \quad \Gamma \ \vdash \ e2 \ : \ bool}{\Gamma \ \vdash (e1 \ != \ e2) \ : \ bool}
+```
+or
+```math
+\frac{\Gamma \ \vdash \ e1 \ : \ i32 \quad \Gamma \ \vdash \ e2 \ : \ i32}{\Gamma \ \vdash (e1 \ != \ e2) \ : \ bool}
+```
+
+### Assignment
+Given the type $`\tau`$, variable $`x`$ and value $`n`$
+
+```math
+\frac{\Gamma \ \vdash \ x \ : \ \tau \quad \Gamma \ \vdash \ n \ : \ \tau}{\lang x := n, \sigma \rang \ \Darr \ \Gamma \ \vdash x \ : \ \tau}
+```
+
+### **let** assignment
+```math
+\frac{\Gamma \ \vdash \ n \ : \ \tau}{\lang \text{let} \  x \ : \ \tau \ := \ n, \sigma \rang \ \Darr \ \Gamma \ \vdash x \ : \ \tau}
+```
+
+### **while** statement
+The condition, $`b`$, of the while statement  
+
+$`
+\frac{}{\Gamma \ \vdash b \ : \ bool}
+`$
+
+### **if/elseif** statement
+The conditions, $`b_i`$, of the if- and elseif-statements
+
+$`
+\frac{}{\Gamma \ \vdash b_i \ : \ bool}
+`$
+
+### Functions
+Given the function $`p`$ with the type of its return type
+
+$`
+\frac{\Gamma \ \vdash p \ : \ \tau \quad \lang p, \sigma \rang \ \Darr \ n}{\Gamma \ \vdash n \ : \ \tau}
+`$
+
+#### Parameters and arguments
+Given a function with parameters $`p1, \dotsb, p_i`$ and arguments $`a1, \dotsb, a_i`$ then for every parameter and argument
+
+$`
+\frac{\Gamma \ \vdash p_i \ : \ \tau}{\Gamma \ \vdash a_i \ : \ \tau}
+`$
\ No newline at end of file