diff --git a/HOME_EXAM_Type_check_part2.md b/HOME_EXAM_Type_check_part2.md new file mode 100644 index 0000000000000000000000000000000000000000..bd6c199af1d477c853e2512d690f09c668e3290d --- /dev/null +++ b/HOME_EXAM_Type_check_part2.md @@ -0,0 +1,117 @@ +- 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