final changes in SOS

HOME_EXAM.md

@@ -24,7 +24,7 @@ Func
 Params
 ```ebnf
     : "()"
-    | "(" [ "," ], Param ")"
+    | "(" (Param ",") + ")"
     ;
 ```
 Param
@@ -110,7 +110,7 @@ Lit
 Exprs
 ```ebnf
     : "()"
-    | "(" [ "," ], Expr1 ")"
+    | "(" (Expr1 ",") + ")"
 ```
 LoCode
 ```ebnf
@@ -266,6 +266,18 @@ Expression can be either a
 - n, number 
 - f, function 
 
+### Function sequence
+```math
+\langle f, σ \rangle → σ'
+```
+
+```rust
+fn main() {
+    test();
+}
+```
+
+
 ### Command sequence
 
 ```math
@@ -345,7 +357,7 @@ true || false;
 
 ### Function call
 ```math
-\frac{ \langle f(e_1,...,e_n)σ \rangle → \langle v,σ' \rangle ; \langle e_1,σ \rangle → v ; \langle e_n,σ \rangle → v}{ \langle f,σ \rangle → v}
+\frac{ \langle f(v_1,...,v_n),σ \rangle → \langle v,σ' \rangle ; \langle e_1,σ \rangle → v_1 ; \text{...} \langle e_n,σ \rangle → v_n}{ \langle f(e_1,...,e_n),σ \rangle → v}
 ```
 
 
@@ -361,7 +373,7 @@ fn main(){
 
 ### Let
 ```math
-\frac{ \langle  e, σ \rangle   →  v ,σ'}{ \langle  \text{let id } \text{ = } e,σ \rangle  → σ'[\text{id = }e]}
+\frac{ \langle  e, σ \rangle   →  v}{ \langle  \text{let id } \text{ = } e,σ \rangle  → σ'[\text{id = }v]}
 ```
 
 ```rust
@@ -456,6 +468,17 @@ Types are now defined as
 - ()
 - Unknown
 
+### Function sequence
+```math
+\langle f, σ \rangle → t
+```
+
+### Command sequence
+
+```math
+\frac{\langle c_1,σ \rangle → t \text{;} \langle c_2,σ\rangle → t}{ \langle c_1;c_2,σ \rangle → t}
+```
+
 ### Operands for i32
 ```math
 \frac{ \langle  e_1,σ \rangle  → \text{i32} \text{;} \langle  e_2,σ \rangle   → \text{i32}}{ \langle  e_1 \text{ + } e_2,σ \rangle  → \text{i32}}
@@ -474,7 +497,7 @@ Same thing for the following operands but results in bool instead of i32:
 - "!=", Not equal
 
 ```math
-\frac{ \langle  e_1,σ \rangle  → \text{i32} \text{;} \langle  e_2,σ \rangle   → \text{i32}}{ \langle  e_1 \text{ + } e_2,σ \rangle  → \text{bool}}
+\frac{ \langle  e_1,σ \rangle  → \text{i32} \text{;} \langle  e_2,σ \rangle   → \text{i32}}{ \langle  e_1 \text{ == } e_2,σ \rangle  → \text{bool}}
 ```
 
 ```rust
@@ -484,7 +507,7 @@ Same thing for the following operands but results in bool instead of i32:
 
 ### Operands for boolean
 ```math
-\frac{ \langle  e_1,σ \rangle  → \text{bool} \text{;} \langle  e_2,σ \rangle   → \text{bool}}{ \langle  e_1 \text{ + } e_2,σ \rangle  → \text{bool}}
+\frac{ \langle  e_1,σ \rangle  → \text{bool} \text{;} \langle  e_2,σ \rangle   → \text{bool}}{ \langle  e_1 \text{ == } e_2,σ \rangle  → \text{bool}}
 ```
 Expression need to evaluate to bool. Similar SOS for all the following operands:
 - "!=", Not equal
@@ -500,7 +523,7 @@ true || false;
 ```math
 \frac{ \langle  e,σ \rangle   → \&t}{ \langle  *e,σ \rangle  →t}
 ```
-### References with mutex
+### References with mutable
 ```math
 \frac{ \langle  e,σ \rangle   → \&\text{mut }t}{ \langle  *e,σ \rangle  → \text{mut }t}
 ```
@@ -519,7 +542,7 @@ let d: bool = *b; // <-- Type missmatch
 
 ### Function call
 ```math
-\frac{ \langle f(e_1,...,e_n)σ \rangle → \langle t,σ' \rangle ; \langle e_1,σ \rangle → t ; \langle e_n,σ \rangle → t}{ \langle f,σ \rangle → t}
+\frac{ \langle f(v_1,...,v_n),σ \rangle → t ; \langle e_1,σ \rangle → v_1 ; \text{...} \langle e_n,σ \rangle → v_n}{ \langle f(e_1,...,e_n),σ \rangle → t}
 ```
 ```rust
 fn a() -> i32 {
@@ -534,7 +557,7 @@ fn main(){
 
 ### Let
 ```math
-\frac{ \langle  e, σ \rangle   →  t ,σ'}{ \langle  \text{let id } \text{ = } e,σ \rangle  → σ'[\text{id = }e]}
+\frac{ \langle  e, σ \rangle   →  t}{ \langle  \text{let id } \text{ = } e,σ \rangle  → σ'[\text{id = }t]}
 ```
 
 ```rust
@@ -571,7 +594,7 @@ if 4 + 5 { // <-- Type missmatch
 
 ### While
 ```math
-\frac{ \langle e,σ \rangle → \text{bool} ; \langle c,σ \rangle → σ'}{ \langle \text{while } e \text{ do } c,σ \rangle → ()}
+\frac{ \langle e,σ \rangle → \text{bool} ; \langle c,σ \rangle → t}{ \langle \text{while } e \text{ do } c,σ \rangle → ()}
 ```
 
 ```rust