$\frac{}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]}$
```math
\frac{}{\lang x := n,\sigma \rang \Downarrow \sigma[x := n]}
```
while-false:
$\frac{\lang b,\sigma \rang \Downarrow false}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma}$
```math
\frac{\lang b,\sigma \rang \Downarrow false}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma}
```
while-true:
$\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma' \lang \textit{while b do block},\sigma' \rang \Downarrow \sigma''}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma''}$
```math
\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma' \lang \textit{while b do block},\sigma' \rang \Downarrow \sigma''}{\lang \textit{while b do block},\sigma \rang \Downarrow \sigma''}
```
if:
$\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'}$
```math
\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'}
```
### Explanation
The example program starts from "main" and assigns the variable "a" to an i32 value returned from a function call to "test_one" with the argument "true".
In the "test_one" function a variable "a" is assigned to "0":
$\frac{}{\lang a := 0,\sigma \rang \Downarrow \sigma[a := 0]}$
```math
\frac{}{\lang a := 0,\sigma \rang \Downarrow \sigma[a := 0]}
```
then the if-statement is checked with the value "true":
$\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'}$
```math
\frac{\lang b,\sigma \rang \Downarrow true \lang block,\sigma \rang \Downarrow \sigma'}{\lang \textit{if b then block},\sigma \rang \Downarrow \sigma'}
```
this sets the value to "a" to be "50":
$\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]}$
```math
\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]}
In the "main" function "a" is set to the returned value:
$\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]}$
```math
\frac{}{\lang a := 50,\sigma \rang \Downarrow \sigma[a := 50]}
```
After that variable "b" is declared as an i32 value to the return value from "test_two" with the values "a", "true" and "50".
In the "test_two" function variable "variable" is declared as a boolean expression. In the boolean expression the paranthesised expressions is first evaluated:
Finally "num" is returned which has the value of "1".
Back in the "main" function "b" is set to the return value of "test_two" which was "1". And then another variable "c" is declared to "a + b". Which will be "51".
...
...
@@ -215,33 +248,47 @@ The current interpreter supports this SOS and can execute programs according to
$\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{if condition do block} \rang}$
```math
\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{if condition do block} \rang}
```
For while-statements:
```rust
...
...
@@ -281,7 +334,9 @@ while b {
and the type rule:
$\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{while condition do block} \rang}$
```math
\frac{\lang b,\sigma \rang \Downarrow bool}{\lang \textit{while condition do block} \rang}
```
The implemented type checker follows the rules above and should it find that there is a type mistmatch, errors will be returned. The current error implementation does not stack, only the first found error will be sent to the terminal. It does however send some information on where the error occured.