Module 5: Mutability and Loops#

In this module we extend the Hygge0 programming language with two new features: we add support for Mutable Variables, and then we add a “While” Loop. In principle, the two features are independent — but in practice, most programs using a while loop need to update the value of some variable that is checked in the loop condition.

These extensions are the starting point for the Project Ideas of this module.

Overall Objective#

Our goal is to interpret, compile and run Hygge programs like the one shown in Example 27 below, which computes and displays the first $n$ terms of the Fibonacci sequence.

Example 27 (A Hygge Program with Mutable Variables and a Loop)

// Number of terms of the Fibonacci sequence to print (minimum 2).
let n = 16;

let mutable t0 = 0;   // First term in the Fibonacci sequence
let mutable t1 = 1;   // Second term in the Fibonacci sequence

println(t0);
println(t1);

let mutable i = 2;    // Counter: how many terms we printed
let mutable next = 0; // Next term in the Fibonacci sequence

while (i < n) do {
    next <- t0 + t1;
    println(next);
    t0 <- t1;
    t1 <- next;
    i <- i + 1
}

Important

The extensions described in this Module (Mutable Variables and “While” Loop) are already implemented in the upstream Git repositories of hyggec, respectively at the tags mutable-vars and while: you should pull and merge the relevant changes into your project compiler. The Project Ideas of this Module further extend Hygge with more assignment operators and more loop constructs.

Mutable Variables#

We extend Hygge0 with an assignment expression “$\hygAssign{x}{e}$” that, intuitively, works as follows:

the expression $e$ on the right-hand-side of the assignment is reduced into a value $v$;
then, in the expression “$\hygAssign{x}{v}$”, the value $v$ is assigned to the variable $x$, and the whole expression “$\hygAssign{x}{v}$” reduces to $v$ itself. This way, it is possible to chain assignments — e.g. the expression “$\hygAssign{x}{\hygAssign{y}{\hygAssign{z}{2+3}}}$” assigns the value $5$ to variables the $z$, $y$, and $x$ (in this order).

Design Considerations#

Typical imperative programming languages (like C, C++, Java, Python…) have mutable variables, whose value can be freely changed while a program runs. Instead, Hygge0 is inspired by programming languages with functional elements (like F#, Scala, Haskell, Erlang, Elixir, Kotlin…) where variables are (by default) immutable: their value is determined once and for all, when they are initialised.

Extending the Hygge0 syntax in Definition 1 with a new assignment operation is quite straightforward. However, mutable variables introduce side effects that cannot be easily captured by the Hygge0 semantics. In fact, introducing mutable variables adds significant complexity to the specification of Hygge — because in general, specifying the behaviour of programs with mutable variables (and reasoning about such a behaviour) is significantly harder.

To see the issue, consider what would happen if we simply tried to use assignments within the existing Hygge0 semantics from Definition 4: we would not be able to write any meaningful programs with mutable variables! This is because in Hygge0, each (immutable) variable $x$ is introduced by a “$\hygLetUNoInit{x}\ldots$” binder — and according to the semantics in Definition 4 (rule $\ruleFmt{R-Let-Subst}$), whenever we start reducing the scope where $x$ is defined, then $x$ “diappears” because it is substituted with its initialisation value (see Example 28 below).

Example 28 (Assignment to a Variable Bound By “let”)

Consider the following Hygge program with an assignment:

\[\begin{split} \begin{array}{l} \hygLetUInit{x}{1} \\ \hygAssign{x}{2}; \\ \hygPrint{x} \end{array} \end{split}\]

If we naively extended the Hygge0 semantics in Definition 4 with an assignment expression, program would reduce as follows (in any runtime environment $R$):

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{} \UnaryInfCLab{R-Let-Subst}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetUInit{x}{1} \\ \hygAssign{x}{2}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{1}{2}; \\ \hygPrint{1} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

Therefore, the program would get stuck. We could try to tweak the substitution rules to avoid substituting $x$ on the left-hand-side of the assignment, as follows:

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{} \UnaryInfCLab{R-Let-Subst}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetUInit{x}{1} \\ \hygAssign{x}{2}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{2}; \\ \hygPrint{1} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

Still, this is not what we want, because we would expect to have $\hygPrint{2}$ after the assignment — but instead, we have $\hygPrint{1}$.

Therefore, there is an overall language design decision to make:

Do we want to change the semantics in Definition 4 to make all Hygge variables potentially mutable?
Or rather, do we want Hygge to keep its immutable variables, and let programmers specify when they want a mutable variable instead?

Here we follow the second approach, inspired by the F# programming language design:

we introduce a new binder expression “$\hygLetMut{x}{e}{e'}$”, which introduces $x$ as a mutable variable that is initialised with the result of $e$, and is only defined in the scope $e'$;
to give a semantics to mutable variables, we extend the runtime environment $R$ (used by the semantic rules in Definition 4) to keep track of mutable variables and their current values in the current scope; and
we define the semantics of “$\hygLetMut{x}{e_1}{e_2}$” and “$\hygAssign{x}{e_3}$” to make use of the extended runtime environment $R$:
- we limit the visibility of the mutable variable $x$ to the expression $e_2$, and
- we define the semantics of assignment to cause the desired side effect: besides producing a value, the reduction of the assignment “$\hygAssign{x}{v}$” also updates the runtime environment $R$ in its scope, causing the mutable variable $x$ to be re-assigned the new value $v$.

Example 29 below outlines how the resulting extension of Hygge0 will behave, while Example 30 shows some tricky cases that our specification must get right.

Example 29 (An Intuition of Mutable Variable Binding)

Consider again the program in Example 28. By introducing a new “$\hygLetMutNoInit{x}\ldots$” expression, we want it to reduce as follows.

Observe that the “$\hygLetMutInit{x}{1}\ldots$” binder does not substitute the variable $x$ in its scope — and when the assignment changes the value of $x$ from $1$ to $2$, then the new value is reflected in the updated binder “$\hygLetMutInit{x}{2}\ldots$”.

\[\begin{split} \begin{array}{rcl} \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{1} \\ \hygAssign{x}{2}; \\ \hygPrint{x} \end{array} }} &\to& \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygPrint{x} \end{array} }} \\ &\to& \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygPrint{2} \end{array} }} \\[2mm] &\to& \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ () \end{array} }} \;\to\; \hygEvalConf{R}{()} \end{array} \end{split}\]

Example 30 (Some Tricky Cases of Mutable Variable Binding)

Here are some tricky cases that we want to get right, when specifying how mutable variable binding and assignment should work.

In the program below, an immutable variable is shadowed by a mutable variable. We don’t want the inner assignment to influence the outer variable.

let x = 0;
{
    let mutable x = 3;
    x <- x + 1;
    assert(x = 4)
}
assert(x = 0)

The following program is similar, but now a mutable variable is shadowed by another mutable variable.

let mutable x = 0;
x <- x + 1;
{
    let mutable x = 3;
    x <- x + 1;
    assert(x = 4)
}
assert(x = 1)

The program below updates two mutable variables with different scopes: we want the the assignments to be correctly propagated.

let mutable x = 0;
{
    let mutable y = 3;
    x <- x + 1;
    y <- y + 2;
    assert(x + y = 6)
}
assert(x = 1)

We also want to chain assignments, and make sure that when a variable is read and reassigned, the result is correct.

let mutable x = 1.0f;
let mutable y = 2.0f;
let mutable z = 3.0f;

x <- y <- z <- x + y + z;

assert(x = y);
assert(y = z);
assert(z = 1.0f + 2.0f + 3.0f)

Syntax#

We now extend the syntax of Hygge0 according to the Design Considerations above.

Definition 13 (Mutable Variable Binding and Assignment)

We define the syntax of Hygge0 with mutable variable binding and assignment by extending Definition 1 with two new expressions:

\[\begin{split} \begin{array}{rrcll} \text{Expression} & e & ::= & \ldots \\ & & \mid & \hygLetMut{x}{e}{e'} & \text{(Declare $x$ as a mutable variable)} \\ & & \mid & \hygAssign{e}{e'} & \text{(Assignment)} \end{array} \end{split}\]

Note

In Definition 13, the use of a generic expression $e$ for the target of the assignment “$\hygAssign{e}{e'}$” is not strictly necessary at this stage: we will see that the semantics of assignment in Definition 15 gets stuck if the assignment target is not a variable, and the typing rules in Definition 16 only support assignments that have a variable on their left-hand-side. Consequently, since we only really support assignments to a variable $x$, it would be sufficient to define the syntax of assignments as just “$\hygAssign{x}{e'}$”.

However, later in the course we will extend assignments to support targets that are not just variables — hence, it is useful to define a more generic syntactic rule now.

Operational Semantics#

We now extend the semantics of Hygge0 according to Definition 13 and the Design Considerations above. This involves two steps:

extending the definition of substitution to cover the new expressions (Definition 14), and
extending the semantic rules (Definition 15). This is the trickiest part, because the Design Considerations above make the behaviour of mutable variables non-trivial.

Definition 14 (Substitution for Mutable Variable Binding and Assignment)

We extend Definition 2 (substitution) with the following new cases:

\[\begin{split} \begin{array}{rcl} \subst{(\hygLetMut{x}{e_1}{e_2})}{x}{e'} & = & \hygLetMut{x}{\subst{e_1}{x}{e'}}{e_2} \\ \subst{(\hygLetMut{y}{e_1}{e_2})}{x}{e'} & = & \hygLetMut{y}{\subst{e_1}{x}{e'}}{\subst{e_2}{x}{e'}} \quad \text{(when $y \neq x$)} \\ \subst{(\hygAssign{e_1}{e_2})}{x}{e'} & = & \hygAssign{(\subst{e_1}{x}{e'})}{(\subst{e_2}{x}{e'})} \end{array} \end{split}\]

The substitution a variable $x$ defined in Definition 14 works as follows:

the substitution on “$\hygLetMutNoInit{x}\ldots$” works like the substitution on “$\hygLetUNoInit{x}\ldots$” in Definition 2;
the substitution on the assignment “$\hygAssign{e_1}{e_2}$” propagates the substitution on both sub-expressions $e_1$ and $e_2$.

Definition 15 (Semantics of Mutable Variable Binding and Assignment)

We extend the definition of the runtime environment $R$ in the Structural Operational Semantics of Hygge0 by adding the following field to the record $R$:

$\envField{R}{Mutables}$ is a mapping from variables $x$ to values $v$, specifying which mutable variables are known in the current scope, and what is their current value.

Then, we define the semantics of Hygge0 with mutable variable binding and assignment by extending Definition 4 to use the extended runtime environment $R$ above, and by adding the following rules:

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$\hygEvalConf{R}{e} \to \hygEvalConf{R'}{e'}$} \UnaryInfCLab{R-LetM-Eval-Init}{$\hygEvalConf{R}{\hygLetMut{x}{e}{e_2}} \;\to\; \hygEvalConf{R'}{\hygLetMut{x}{e'}{e_2}}$} \end{prooftree} \\\\ \begin{prooftree} \AxiomC{$R' = \left\{R \text{ with } \text{Mutables} + (x \mapsto v)\right\}$} \AxiomC{$\hygEvalConf{R'}{e} \to \hygEvalConf{R''}{e'}$} \AxiomC{$ \begin{array}{@{}l@{}} \envField{R''}{Mutables}(x) = v' \\ \envField{R}{Mutables}(x) = v_? \\ R''' = \{R'' \text{ with } \text{Mutables}(x) = v_?\} \end{array} $} \TrinaryInfCLab{R-LetM-Eval-Scope}{$\hygEvalConf{R}{\hygLetMut{x}{v}{e}} \;\to\; \hygEvalConf{ R''' }{\hygLetMut{x}{v'}{e'}}$} \end{prooftree} \\\\ \begin{prooftree} \AxiomC{} \UnaryInfCLab{R-LetM-Res}{$\hygEvalConf{R}{\hygLetMut{x}{v}{v'}} \;\to\; \hygEvalConf{R}{v'}$} \end{prooftree} \\\\ \begin{prooftree} \AxiomC{$\envField{R}{Mutables}(x) = v$} \UnaryInfCLab{R-Var-Res}{$\hygEvalConf{R}{x} \;\to\; \hygEvalConf{R}{v}$} \end{prooftree} \\\\ \begin{prooftree} \AxiomC{$\hygEvalConf{R}{e} \to \hygEvalConf{R'}{e'}$} \UnaryInfCLab{R-Assign-Eval-Arg}{$\hygEvalConf{R}{\hygAssign{x}{e}} \;\to\; \hygEvalConf{R'}{\hygAssign{x}{e'}}$} \end{prooftree} \\\\ \begin{prooftree} \AxiomC{$\envField{R}{Mutables}(x) = v'$} \AxiomC{$R' = \left\{R \text{ with } \text{Mutables} + (x \mapsto v)\right\}$} \BinaryInfCLab{R-Assign-Res}{$\hygEvalConf{R}{\hygAssign{x}{v}} \;\to\; \hygEvalConf{R'}{v}$} \end{prooftree} \end{array} \end{split}\]

The rules in Definition 15 work as follows (see also Example 31 below to see them in action).

Rule $\ruleFmt{R-LetM-Eval-Init}$ is very similar to rule $\ruleFmt{R-Let-Eval-Init}$ in Definition 4: it reduces the expression $e$ that initialises a mutable variable $x$;
Rule $\ruleFmt{R-LetM-Eval-Scope}$ can be applied to reduce “$\hygLetMut{x}{v}{e}$” where $x$ is initialised with a value $v$ (that cannot be reduced further): in this case, the rule reduces the scope $e$ of the mutable variable. Observe the crucial difference with $\ruleFmt{R-Let-Subst}$ in Definition 4: the new rule $\ruleFmt{R-LetM-Eval-Scope}$ does not substitute $x$ with $v$ in the scope $e$. Instead, the new rule proceeds as follows:
1. in its first premise, the rule computes a runtime environment $R'$ that is equal to $R$, except that $\envField{R'}{Mutables}$ maps $x$ to the initialisation value $v$;
2. in its second premise, the rule recursively attempts to reduce the scope $e$ in the runtime environment $R'$, obtaining $\hygEvalConf{R''}{e'}$;
3. in its third premise, the rule does the following:
  - takes the value $v'$ assigned to $x$ in $\envField{R''}{Mutables}$;
  - takes the value $v_?$ assigned to $x$ in $\envField{R}{Mutables}$ (this value may be undefined); and
  - computes a runtime environment $R'''$ that is equal to $R''$, except that $\envField{R'''}{Mutables}(x)$ has the value $v_?$ that was given to $x$ by $\envField{R}{Mutables}(x)$ (if the latter was defined; if not, then $\envField{R'''}{Mutables}(x)$ is also undefined);
4. in its conclusion, the rule produces the reduction result “$\hygEvalConf{R}{\hygLetMut{x}{v'}{e'}}$” (with $v'$ taken from the third premise above).
With this rule, the mutable variable $x$ is only known in the scope expression $e$, and the reduction of $e$ into $e'$ might change the value assigned to $x$: in fact, the values $v$ and $v'$ may differ, if $x$ is reassigned in the reduction from $e$ to $e'$ (using rule $\ruleFmt{R-Assign-Res}$ below).Moreover, the original runtime environment $R$ reduces to $R'''$, where:
- if there was already a mutable variable also called $x$ in $R$, then the value of $x$ in $R'''$ is unchanged (because the $x$ defined in $R$ is outside the scope of the “let mutable” binder, so it is not the same $x$ defined in $R'$ and $R''$);
- instead, other mutable variables defined in $R$ might be changed when $e$ reduces to $e'$, and such changes are reflected in $R'''$.
Rule $\ruleFmt{R-LetM-Res}$ reduces the whole expression “$\hygLetMut{x}{v}{v'}$” into the value $v'$ (i.e. this rule can only be applied when the scope of the “$\hygLetMutNoInit{x}\ldots$” is a value, hence the variable $x$ is unused).
Rule $\ruleFmt{R-Var-Res}$ allows a variable $x$ to reduce into a value $v$ in a runtime environment $R$ — but the rule premise requires that $x$ is assigned value $v$ in the mapping $\envField{R}{Mutables}$. This rule may be applied e.g. when the expression $e$ in the scope of “$\hygLetMut{x}{v}{e}$” reduces in the premise of rule $\ruleFmt{R-LetM-Eval-Scope}$ above, because $e$ might contain a sub-expression that uses $x$, like “$42 + x$”.
Rule $\ruleFmt{R-Assign-Eval-Arg}$ reduces an expression $e$ being assigned to a variable $x$.
Rule $\ruleFmt{R-Assign-Res}$ performs the assignment of value $v$ to variable $x$ in the runtime environment $R$, as follows:
1. the first premise of the rule requires that $x$ has some value $v'$ already assigned in the mapping $\envField{R}{Mutables}$ (therefore, $x$ must be a known mutable variable in the current scope);
2. the second premise of the rule computes an updated runtime environment $R'$ that is equal to $R$, except that $\envField{R'}{Mutables}$ maps $x$ to the new assigned value $v$;
3. in the conclusion, the rule reduces “$\hygAssign{x}{v}$” into $v$, in the updated runtime environment $R'$.

Example 31 (A Program with a Mutable Variable)

Let us examine the reductions of the following Hygge expression, according to the semantic rules in Definition 15 and Definition 4:

\[\begin{split} \begin{array}{l} \hygLetMutInit{x}{1 + 1} \\ \hygAssign{x}{x + 40}; \\ \hygPrint{x} \end{array} \end{split}\]

Let us use a runtime environment $R$ where:

$\envField{R}{Printer}$ is defined (i.e. we can produce console output), and
$\envField{R}{Mutables} = \emptyset$ (i.e. there are no known mutable variables in the current scope).

For the first reduction, the only rule we can apply is $\ruleFmt{R-LetM-Eval-Init}$, which produces:

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{1 + 1 = 2} \UnaryInfCLab{R-Add-Res}{$\hygEvalConf{R}{1 + 1} \to \hygEvalConf{R}{2}$} \UnaryInfCLab{R-LetM-Eval-Init}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{1 + 1} \\ \hygAssign{x}{x + 40}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygAssign{x}{x + 40}; \\ \hygPrint{x} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the second reduction, the only rule we can apply is $\ruleFmt{R-LetM-Eval-Scope}$, which reduces the expression in the scope of “$\hygLetMutNoInit{x}\ldots$”. To this purpose, let us now define $R'$ as a runtime environment equal to $R$, except that $\envField{R}{Mutables}$ maps $x$ to the initialisation value $2$ (this is omitted with “$\cdots$” below). Notice that:

in the scope of “$\hygLetMutNoInit{x}\ldots$”, we use rule $\ruleFmt{R-Assign-Eval-Arg}$ to reduce the expression “$x + 40$” being assigned to $x$;
moreover, in order to reduce the sub-expression “$x + 40$” into “$2 + 40$”, we use rule $\ruleFmt{R-Var-Res}$ to retrieve the current value of $x$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$\envField{R'}{Mutables}(x) = 2$} \UnaryInfCLab{R-Var-Res}{$\hygEvalConf{R'}{x} \;\to\; \hygEvalConf{R'}{2}$} \UnaryInfCLab{R-Add-L}{$\hygEvalConf{R'}{x + 40} \;\to\; \hygEvalConf{R'}{2 + 40}$} \UnaryInfCLab{R-Assign-Eval-Arg}{$\hygEvalConf{R'}{\hygAssign{x}{x + 40}} \;\to\; \hygEvalConf{R'}{\hygAssign{x}{2 + 40}}$} \UnaryInfCLab{R-Seq-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{x + 40}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{2 + 40}; \\ \hygPrint{x} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 2$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygAssign{x}{x + 40}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygAssign{x}{2 + 40}; \\ \hygPrint{x} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the third reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$; in the scope of “$\hygLetMutNoInit{x}\ldots$”, we use (again) rule $\ruleFmt{R-Assign-Eval-Arg}$ to reduce the expression being assigned to $x$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$2 + 40 = 42$} \UnaryInfCLab{R-Add-Res}{$\hygEvalConf{R'}{2 + 40} \;\to\; \hygEvalConf{R'}{42}$} \UnaryInfCLab{R-Assign-Eval-Arg}{$\hygEvalConf{R'}{\hygAssign{x}{2 + 40}} \;\to\; \hygEvalConf{R'}{\hygAssign{x}{42}}$} \UnaryInfCLab{R-Seq-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{2 + 40}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{42}; \\ \hygPrint{x} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 2$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygAssign{x}{2 + 40}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygAssign{x}{42}; \\ \hygPrint{x} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the fourth reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$ — but now, notice that:

in the scope of “$\hygLetMutNoInit{x}\ldots$”, there is an assignment that changes the value assigned to $x$ from $2$ to $42$;
correspondingly, we use rule $\ruleFmt{R-Assign-Res}$ to update the runtime enviromnent: we define $R''$ as a runtime environment equal to $R'$, except that $\envField{R''}{Mutables}$ maps $x$ to the newly-assigned value $42$;
besides its side effect (i.e. updating $R'$ into $R''$), the reduction of the assignment produces the assigned value $42$;
in the conclusion of this reduction, the original runtime environment $R$ is unchanged (because $x$ is not visible there). However, the original “$\hygLetMutInit{x}{2}\ldots$” has now become “$\hygLetMutInit{x}{42}\ldots$”: as a consequence, further reductions (that we explore below) will use the updated value of $x$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$\envField{R'}{Mutables}(x) = 2$} \AxiomC{$R'' = \left\{R' \text{ with } \text{Mutables} + (x \mapsto 42)\right\}$} \BinaryInfCLab{R-Assign-Res}{$\hygEvalConf{R'}{\hygAssign{x}{42}} \;\to\; \hygEvalConf{R''}{42}$} \UnaryInfCLab{R-Seq-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{42}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R''}{\boxed{ \begin{array}{@{}l@{}} 42; \\ \hygPrint{x} \end{array} }} $} \AxiomC{$\envField{R''}{Mutables}(x) = 42$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygAssign{x}{42}; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ 42; \\ \hygPrint{x} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the fifth reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and now we simplify the sequencing of expressions inside the scope of “$\hygLetMutNoInit{x}\ldots$”.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R'' = \cdots$} \AxiomC{} \UnaryInfCLab{R-Seq-Res}{$ \hygEvalConf{R''}{\boxed{ \begin{array}{@{}l@{}} 42; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R''}{\hygPrint{x}} $} \AxiomC{$\envField{R''}{Mutables}(x) = 42$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ 42; \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ \hygPrint{x} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the sixth reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and now we use (again) $\ruleFmt{R-Var-Res}$ to retrieve the current value of $x$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R'' = \cdots$} \AxiomC{$\envField{R''}{Mutables}(x) = 42$} \UnaryInfCLab{R-Var-Res}{$\hygEvalConf{R''}{x} \;\to\; \hygEvalConf{R''}{42}$} \UnaryInfCLab{R-Print-Eval-Arg}{$ \hygEvalConf{R''}{\hygPrint{x}} \;\to\; \hygEvalConf{R''}{\hygPrint{42}} $} \AxiomC{$\envField{R''}{Mutables}(x) = 42$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ \hygPrint{x} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ \hygPrint{42} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the seventh reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and now we reduce $\hygPrint{42}$ to the unit value (while printing 42 on the console).

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R'' = \cdots$} \AxiomC{$\envField{R''}{Printer}$ is defined} \UnaryInfCLab{R-Print-Res}{$ \hygEvalConf{R''}{ \begin{array}{@{}l@{}} \hygPrint{42} \end{array} } \;\to\; \hygEvalConf{R''}{ \begin{array}{@{}l@{}} () \end{array} } $} \AxiomC{$\envField{R''}{Mutables}(x) = 42$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ \hygPrint{42} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ () \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the eighth and last reduction, the only rule we can apply is $\ruleFmt{R-LetM-Res}$, which replaces the whole “$\hygLetMutNoInit{x}\ldots$” with the value in its scope, which is the unit value $()$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{} \UnaryInfCLab{R-LetM-Res}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{42} \\ () \end{array} }} \;\to\; \hygEvalConf{R}{ () } $} \end{prooftree} \end{array} \end{split}\]

Therefore, we were able to reduce the original program into a value, without getting stuck.

Exercise 24

Write the reductions of the following expression, in a runtime environment $R$. Show all reductions until the expression reduces into a value.

\[\begin{split} \begin{array}{l} \hygLetMutInit{x}{0} \\ \hygLetMutInit{y}{0} \\ \qquad\hygAssign{x}{\hygAssign{y}{1}}; \\ \qquad x + y \end{array} \end{split}\]

Exercise 25

Write the reductions of the following expression, in a runtime environment $R$. Show all reductions until the expression reduces into a value.

\[\begin{split} \begin{array}{l} \hygLetMutInit{x}{0}\\ \{\\ \qquad\hygLetMutInit{x}{1} \\ \qquad\hygAssign{x}{2} \\ \};\\ \hygAssert{x = 0} \end{array} \end{split}\]

Typing Rules#

We now extend the typing rules of Hygge0 to support the mutable variables introduced in Definition 13 according to the Design Considerations above. Our goal is to type-check programs that use the new assignment “$\hygAssign{x}{e}$”, but only when $x$ is in the scope of “$\hygLetMutNoInit{x}\ldots$”: this way, Hygge programmers can be sure that, if their code type-checks, then it does not accidentally modify any immutable variable. Also notice that, by the semantics in Definition 15, the runtime environment and expression $\hygEvalConf{R}{\hygAssign{x}{e}}$ gets stuck if $x$ is not a known mutable variables in $R$ — hence our typing rules should prevent the possibility of assigning a value to an unknown or immutable variable.

To achieve this result, we extend the typing environment $\Gamma$ in Definition 6 with a new entry, called “$\text{Mutables}$”, which keeps track of the known mutable variables in the current scope. Then, we add two new typing rules, and slightly tweak the existing rule for (immutable) let-binders.

Definition 16 (Typing Rules for Mutable Variable Binding and Assignment)

We extend the typing environment $\Gamma$ in Definition 6 by adding the following entry:

$\envField{\Gamma}{Mutables}$ is a set of variables.

Then, we define the typing rules of Hygge0 with mutable variable binding and assignment in two steps.

First, we extend Definition 11 with the following new rules:

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$\hygTypeCheckJ{\Gamma}{e_1}{T}$} \AxiomC{$\left\{ \Gamma \;\text{ with }\; \text{Vars} + (x \mapsto T) \;\text{ and }\; \text{Mutables} \cup \{x\} \right\} \vdash e_2 : T' $} \BinaryInfCLab{T-MLet}{$\hygTypeCheckJ{\Gamma}{\hygLetMut{x}{e_1}{e_2}}{T'}$} \end{prooftree} \\\\ \begin{prooftree} \AxiomC{$x \in \envField{\Gamma}{Mutables}$} \AxiomC{$\hygTypeCheckJ{\Gamma}{x}{T}$} \AxiomC{$\hygTypeCheckJ{\Gamma}{e}{T}$} \TrinaryInfCLab{T-Assign-Var}{$\hygTypeCheckJ{\Gamma}{\hygAssign{x}{e}}{T}$} \end{prooftree} \end{array} \end{split}\]

Then, we replace the rules $\ruleFmt{T-Let}$ and $\ruleFmt{T-Let-T}$ in Definition 8 with the following rules:

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$\Gamma \vdash e_1 : T$} \AxiomC{$\left\{\Gamma \text{ with } \text{Vars} + (x \mapsto T) \text{ and } \text{Mutables} \setminus \{x\} \right\} \vdash e_2 : T'$} \BinaryInfCLab{T-Let2}{$\Gamma \vdash \hygLetU{x}{e_1}{e_2} : T'$} \end{prooftree} \\\\ \begin{prooftree} \AxiomC{$\hygTypeResJ{\Gamma}{t}{T}$} \AxiomC{$\Gamma \vdash e_1 : T$} \AxiomC{$\left\{\Gamma \text{ with } \text{Vars} + (x \mapsto T) \text{ and } \text{Mutables} \setminus \{x\} \right\} \vdash e_2 : T'$} \TrinaryInfCLab{T-Let-T2}{$\Gamma \vdash \hygLet{x}{t}{e_1}{e_2} : T'$} \end{prooftree} \end{array} \end{split}\]

In Definition 16, the typing rule $\ruleFmt{T-MLet}$ is very similar to $\ruleFmt{T-Let}$ in Definition 8: the only difference is that, when type-checking the expression $e_2$ in the scope of “$\hygLetMutNoInit{x}\ldots$”, rule $\ruleFmt{T-MLet}$ also adds the variable $x$ to the set of known mutable variables in $\Gamma$.

The set of mutable variables in $\Gamma$ is used by rule $\ruleFmt{T-Assign-Var}$: it checks whether the variable $x$ (the target of the assignment) is mutable, and whether the type of $x$ matches the type of the expression $e$ being assigned to it. If all these conditions hold, then the whole assignment has type $T$ — because, as specified in Definition 15, it will produce the value being assigned.

Finally, we need to replace rules $\ruleFmt{T-Let}$ and $\ruleFmt{T-Let-T}$ in Definition 8 with the new rules $\ruleFmt{T-Let2}$ and $\ruleFmt{T-Let-T2}$: the only difference between the old and the new rules is that $\ruleFmt{T-Let2}$ and $\ruleFmt{T-Let-T2}$ remove the declared variables $x$ from the set of known mutable variables in the typing environment (using the set subtraction operation “$\setminus$”). This is necessary to address Example 32 below.

Example 32 (Shadowing Mutable Variables)

The following Hygge program declares a mutable variable x, and then shadows it with a regular (immutable) variable having the same name.

let mutable x = 0;
let x = 1;
x <- 2

We do not want this program to type-check, because it is attempting to use the assignment operator on a variable that has been (re-)defined as immutable by the inner “$\hygLetUNoInit{x}\ldots$”. For this reason, we use the new rule $\ruleFmt{T-Let2}$ to ensure that, whenever we introduce a regular (immutable) variable, we remove it from the known mutable variables in the typing environment.

Exercise 26 (Why We Need the Typing Rule [T-Let2])

Write a typing derivation for the program in Example 32 by using the “old” typing rule $\ruleFmt{T-Let}$ from Definition 8 (instead of $\ruleFmt{T-Let2}$ in Definition 16).

Then, try to write a typing derivation for the same program, now using $\ruleFmt{T-Let2}$ in Definition 16.

(Before trying this exercise, it may be helpful to have a look at the derivation in Example 33 below.)

Example 33 (Type-Checking a Program with Mutable Variables)

We now see how to type-check a program with mutable variables. To this purpose, let us define the following typing environments (with the extension introduced in Definition 16):

$\Gamma$ as the empty typing environment where:
- $\envField{\Gamma}{Vars} = \emptyset$;
- $\envField{\Gamma}{TypeVars} = \emptyset$;
- $\envField{\Gamma}{Mutables} = \emptyset$;
$\Gamma'$ as the typing environment obtained from $\Gamma$ by mapping $x$ to $\tInt$ in the field $\text{Vars}$, and adding $x$ to the field $\text{Mutables}$. Therefore, we have:
- $\envField{\Gamma'}{Vars} = \{x \mapsto \tInt\}$;
- $\envField{\Gamma'}{TypeVars} = \emptyset$;
- $\envField{\Gamma'}{Mutables} = \{x\}$.

Here is a typing derivation that type-checks the expression in Example 31, according to the rules in Definition 16, Definition 11, Definition 8, and Definition 7.

(Download this derivation as a PNG image.)

\[\begin{split}\begin{array}{c} \begin{prooftree} \AxiomC{1 is an integer} \UnaryInfCLab{T-Val-Int}{$\hygTypeCheckJ{\Gamma}{1}{\tInt}$} \AxiomC{$\cdots$} \BinaryInfCLab{T-Add}{$\hygTypeCheckJ{\Gamma}{1 + 1}{\tInt}$} \AxiomC{$\begin{prooftree} \AxiomC{$x \in \envField{\Gamma'}{Mutables}$} \AxiomC{$\envField{\Gamma'}{Vars}(x) = \tInt$} \UnaryInfCLab{T-Var}{$\hygTypeCheckJ{\Gamma'}{x}{\tInt}$} \AxiomC{$\envField{\Gamma'}{Vars}(x) = \tInt$} \UnaryInfCLab{T-Var}{$\hygTypeCheckJ{\Gamma'}{x}{\tInt}$} \AxiomC{40 is an integer} \UnaryInfCLab{T-Val-Int}{$\hygTypeCheckJ{\Gamma}{40}{\tInt}$} \BinaryInfCLab{T-Add}{$\hygTypeCheckJ{\Gamma'}{x + 40}{\tInt}$} \TrinaryInfCLab{T-Assign}{$\hygTypeCheckJ{\Gamma'}{\hygAssign{x}{x + 40}}{\tInt}$} \AxiomC{$\envField{\Gamma'}{Vars}(x) = \tInt$} \UnaryInfCLab{T-Var}{$\hygTypeCheckJ{\Gamma'}{x}{\tInt}$} \UnaryInfCLab{T-Print}{$\hygTypeCheckJ{\Gamma'}{\hygPrint{x}}{\tUnit}$} \BinaryInfCLab{T-Seq}{$ \hygTypeCheckJ{\Gamma'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{x + 40}; \\ \hygPrint{x} \end{array} }}{\tUnit} $} \end{prooftree}$} \BinaryInfCLab{T-LetM}{$ \hygTypeCheckJ{\Gamma}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{1 + 1} \\ \hygAssign{x}{x + 40}; \\ \hygPrint{x} \end{array} }}{\tUnit} $} \end{prooftree} \end{array}\end{split}\]

Exercise 27 (Type-Checking Mutable Variables and Assignments)

Write a typing derivation that type-checks the following expression:

\[\begin{split} \begin{array}{l} \hygLetInit{x}{\tFloat}{\text{2.0f}} \\ \hygLetMutInit{y}{\text{3.14f}} \\ \hygAssign{y}{x * y} \end{array} \end{split}\]

Implementation#

We now have a look at how hyggec is extended to implement mutable variables, according to the specification illustrated in the previous sections.

Tip

To see a summary of the changes described below, you can inspect the differences in the hyggec Git repositories between the tags hygge0 and mutable-vars.

Lexer, Parser, Interpreter, and Type Checking#

These parts of the hyggec compiler are extended along the lines of Example: Extending Hygge0 and hyggec with a Subtraction Operator.

We extend the data type Expr<'E,'T> (in AST.fs) with two new cases, according to Definition 13:
- LetMut for “$\hygLetMutNoInit{x}\ldots$”, and
- Assign for “$\hygAssign{e}{e'}$”.
We extend PrettyPrinter.fs to support the new expressions LetMut and Assign, and also to display the contents of the new typing context entry Mutables (see below).
We extend Lexer.fsl to support two new tokens:
- MUTABLE for the keyword mutable, and
- LARROW (left arrow) for the assignment operator <-.
We extend Parser.fsy to recognise the desired sequences of tokens according to Definition 13, and generate AST nodes for the new expressions LetMut and Assign.
We extend the function subst in ASTUtil.fs to support the new expressions LetMut and Assign, according to Definition 14.
We extend the function reduce in Interpreter.fs according to Definition 15:
- we add new cases for LetMut and Assign, and
- we add a new case for Var(x) that reduces a mutable variable x to its value taken from env.Mutables (therefore, if x is not present in the mapping env.Mutables, the expression Var(x) is stuck).
We extend Typechecker.fs according to Definition 16:
- we extend the definition of the record TypingEnv with a new entry called Mutables;
- we extend the function typer to support the new cases for:
  - LetMut (since their type-checking logic is very similar to Let, it is implemented in function called letTyper); and
  - Assign;
- we update the existing typing rule for Let to match the revised typing rule $\ruleFmt{T-Let2}$.
Besides, the type checking for Let and LetMut is very similar, so it is implemented in a common auxiliary function called letTyper.
We also add new tests; in particular, we add the tricky cases illustrated in Example 30 as tests for both the interpreter, and the Code Generation (described below).

Code Generation#

The code generation for the expression “$\hygLetMut{x}{e_1}{e_2}$” is not different from the immutable “$\hygLetUNoInit{x}\ldots$”: this is because the mutability (or immutability) of a variable is a concept that only exists in the Hygge programming language and typing system — whereas in RISC-V assembly (just like in most other assembly variants for other CPUs) registers and memory locations are generally mutable. Moreover, the code generation of “$\hygLetUNoInit{x}\ldots$” is already taking care of the correct scoping of variables — hence, it handles the tricky cases discussed in Example 30 out-of-the-box.

Therefore, in the function doCodegen (in the file RISCVCodegen.fs) we simply add a pattern matching case, that reuses the code generation already implemented for “$\hygLetUNoInit{x}\ldots$”:

let rec internal doCodegen (env: CodegenEnv) (node: TypedAST): Asm =
    match node.Expr with
    // ...
    | Let(name, init, scope)
    | LetT(name, _, init, scope)
    | LetMut(name, init, scope) ->  // We add this pattern matching case
        // ... The code generation for "let" is unchanged ...

The code generation for the expression “$\hygAssign{x}{e}$” is straighforward: after checking that the target of the assignment (called lhs) is a variable, it compiles expression $e$ (called rhs) using the current target register, and then moves (i.e. copies) the result of $e$ where the value of $x$ is stored (e.g. in a register). The only exception is when the expression $e$ has type $\tUnit$, hence it does not produce any value to assign. (The code snippet below omits some cases for clarity.)

    | Assign(lhs, rhs) ->
        match lhs.Expr with
        | Var(name) ->
            /// Code for the 'rhs', leaving its result in the target register
            let rhsCode = doCodegen env rhs
            match rhs.Type with
            | t when (isSubtypeOf rhs.Env t TUnit) ->
                rhsCode // No assignment to perform
            | _ ->
                match (env.VarStorage.TryFind name) with
                | Some(Storage.Reg(reg)) ->
                    rhsCode.AddText(RV.MV(reg, Reg.r(env.Target)),
                                    $"Assignment to variable %s{name}")
                | Some(Storage.FPReg(reg)) ->
                    rhsCode.AddText(RV.FMV_S(reg, FPReg.r(env.FPTarget)),
                                    $"Assignment to variable %s{name}")
                // ...
        | _ ->
            failwith ($"BUG: assignment to invalid target:%s{Util.nl}"
                      + $"%s{PrettyPrinter.prettyPrint lhs}")

Notice that the code snippet above does not check whether the target variable $x$ is mutable: it assumes that the type checking phase has already taken care of it.

“While” Loop#

We now extend the Hygge0 programming language with a “while” loop, in the style of most imperative programming languages (such as C, Java, Python, …). The “while” expression in Hygge is written “$\hygWhile{e_1}{e_2}$”, and it means that we want to repeat the execution of expression $e_2$ as long as $e_1$ is true.

Syntax#

The syntax of the “while” loop (Definition 17) is straightforward.

Definition 17 (While Loop)

We define the syntax of Hygge0 with while loops by extending Definition 1 with a new expressions:

\[\begin{split} \begin{array}{rrcll} \text{Expression} & e & ::= & \ldots \\ & & \mid & \hygWhile{e_1}{e_2} & \text{("While" loop)} \end{array} \end{split}\]

Operational Semantics#

To substitute variables in “$\hygWhile{e_1}{e_2}$” we simply propagate the substitution through the loop condition $e_1$ and loop body $e_2$, according to Definition 18 below.

Definition 18 (Substitution for “While” Loops)

We extend Definition 2 (substitution) with the following new case:

\[ \begin{array}{rcl} \subst{(\hygWhile{e_1}{e_2})}{x}{e'} & = & \hygWhile{(\subst{e_1}{x}{e'})}{(\subst{e_2}{x}{e'})} \end{array} \]

The reduction semantics of “$\hygWhile{e_1}{e_2}$” (Definition 19 below) realises the behaviour described in the beginning of this section by rewriting the “while” loop expression into the following expression:

\[ \hygCond{e_1}{ \{e_2;\; \hygWhile{e_1}{e_2}\} }{()} \]

In other words, the “while” loop becomes an “if” expression that (according to the semantics you should have defined as part of Exercise 14) behaves as follows:

the “if” semantics tries to reduce the loop condition $e_1$ into a value;
then, if the condition value is $\hygTrue$, the “if” expression executes the loop body $e_2$, followed by the “while” loop again;
otherwise, if the condition reduces to $\hygFalse$, the “if” expression produces the unit value $()$ (hence, it does not execute the loop body).

Definition 19 (Semantics of “While” Loops)

We define the semantics of Hygge0 with “while” loops by extending Definition 4 with the following rule:

\[ \begin{array}{c} \begin{prooftree} \AxiomC{} \UnaryInfCLab{R-While}{$ \hygEvalConf{R}{\hygWhile{e_1}{e_2}} \;\to\; \hygEvalConf{R}{ \hygCond{e_1}{ \{e_2;\; \hygWhile{e_1}{e_2}\} }{()} } $} \end{prooftree} \end{array} \]

Example 34 (A Program with a “While” Loop)

Let us examine the reductions of the following Hygge expression, according to the semantic rules in Definition 19, Definition 15 and Definition 4:

\[\begin{split} \begin{array}{l} \hygLetMutInit{x}{0} \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} \end{split}\]

Let us use a runtime environment $R$ where:

$\envField{R}{Mutables} = \emptyset$ (i.e. there are no known mutable variables in the current scope).

For the first reduction, the only rule we can apply is $\ruleFmt{R-LetM-Eval-Scope}$, which reduces the expression in the scope of “$\hygLetMutNoInit{x}\ldots$”. To this purpose, let us now define $R'$ as a runtime environment equal to $R$, except that $\envField{R}{Mutables}$ maps $x$ to the initialisation value $0$ (this is omitted with “$\cdots$” below). Observe that, to reduce the expression in the scope of “$\hygLetMutNoInit{x}\ldots$”, we use the new rule $\ruleFmt{R-While}$, which rewrites the “while” loop into an “if”.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{} \UnaryInfCLab{R-While}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygCondNoThenElse{x < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygCondNoThenElse{x < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the second reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$. Notice that:

to reduce the scope of the “$\hygLetMutNoInit{x}\ldots$” we use two rules that you should have defined as part of Exercise 14:
- one rule to reduce the “if” condition: let us call this rule $\ruleFmt{R-Cond-Eval}$;
- another rule to reduce the left-hand-side of a comparison: let us call this rule $\ruleFmt{R-Less-L}$;
we also use rule $\ruleFmt{R-Var-Res}$ from Definition 15 to access the current value of the mutable variable $x$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \UnaryInfCLab{R-Var-Res}{$ \hygEvalConf{R'}{x} \;\to\; \hygEvalConf{R'}{0} $} \UnaryInfCLab{R-Less-L}{$ \hygEvalConf{R'}{x < 2} \;\to\; \hygEvalConf{R'}{0 < 2} $} \UnaryInfCLab{R-Cond-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygCondNoThenElse{x < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygCondNoThenElse{0 < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygCondNoThenElse{x < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygCondNoThenElse{0 < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the third reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and we keep reducing the condition of the “if”. We use another rule that you should have defined as part of Exercise 14, to compare two values: let us call this rule $\ruleFmt{R-Less-Res}$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$0 < 2$ is true} \UnaryInfCLab{R-Less-Res}{$ \hygEvalConf{R'}{x < 2} \;\to\; \hygEvalConf{R'}{\hygTrue} $} \UnaryInfCLab{R-Cond-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygCondNoThenElse{0 < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygCondNoThenElse{\hygTrue} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygCondNoThenElse{0 < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygCondNoThenElse{\hygTrue} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the fourth reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and we now select the “then” branch of the “if”: to do this, we use another rule that you should have defined as part of Exercise 14, which we call $\ruleFmt{R-Cond-True}$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{} \UnaryInfCLab{R-Cond-True}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygCondNoThenElse{\hygTrue} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{x + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygCondNoThenElse{\hygTrue} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygAssign{x}{x + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the fifth reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and we now we replace the mutable variable $x$ (on the right-hand-side of the assignment) with its current value $0$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \UnaryInfCLab{R-Var-Res}{$ \hygEvalConf{R'}{x} \;\to\; \hygEvalConf{R'}{0} $} \UnaryInfCLab{R-Add-L}{$ \hygEvalConf{R'}{x + 1} \;\to\; \hygEvalConf{R'}{0 + 1} $} \UnaryInfCLab{R-Assign-Eval-Arg}{$ \hygEvalConf{R'}{\hygAssign{x}{x + 1}} \;\to\; \hygEvalConf{R'}{\hygAssign{x}{0 + 1}} $} \UnaryInfCLab{R-Seq-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{x + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{0 + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygAssign{x}{x + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygAssign{x}{0 + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the seventh reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and we now fully reduce the right-hand-side of the assignment into the value $1$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$0 + 1 = 1$} \UnaryInfCLab{R-Add-Res}{$ \hygEvalConf{R'}{0 + 1} \;\to\; \hygEvalConf{R'}{1} $} \UnaryInfCLab{R-Assign-Eval-Arg}{$ \hygEvalConf{R'}{\hygAssign{x}{0 + 1}} \;\to\; \hygEvalConf{R'}{\hygAssign{x}{1}} $} \UnaryInfCLab{R-Seq-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{0 + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygAssign{x}{0 + 1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygAssign{x}{1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the eighth reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and we now re-assign variable $x$, changing its value from $0$ to $1$. To this end, we use rule $\ruleFmt{R-Assign-Res}$ to update the runtime enviromnent: we define $R''$ as a runtime environment equal to $R'$, except that $\envField{R''}{Mutables}$ maps $x$ to the newly-assigned value $1$.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \AxiomC{$R'' = \left\{R' \text{ with } \text{Mutables} + (x \mapsto 1)\right\}$} \BinaryInfCLab{R-Assign-Res}{$ \hygEvalConf{R'}{\hygAssign{x}{1}} \;\to\; \hygEvalConf{R''}{1} $} \UnaryInfCLab{R-Seq-Eval}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygAssign{x}{1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} 1; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{0} \\ \hygAssign{x}{1}; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{1} \\ 1; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

For the ninth reduction, the only rule we can apply is (again) $\ruleFmt{R-LetM-Eval-Scope}$, and we now and now we simplify the sequencing of expressions inside the scope of “$\hygLetMutNoInit{x}\ldots$”.

\[\begin{split} \begin{array}{c} \begin{prooftree} \AxiomC{$R' = \cdots$} \AxiomC{} \UnaryInfCLab{R-Seq-Res}{$ \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} 1; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R'}{\boxed{ \begin{array}{@{}l@{}} \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \AxiomC{$\envField{R'}{Mutables}(x) = 0$} \TrinaryInfCLab{R-LetM-Eval-Scope}{$ \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{1} \\ 1; \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{1} \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} $} \end{prooftree} \end{array} \end{split}\]

We have now reached an expression that is very similar to the one at the beginning of this example — except that the mutable variable $x$ is now initialised with $1$ instead of $0$.

If we perform 9 more reductions similar to the ones above, we cause a further increment of variable $x$; then, we can again expand the “while” into an “if” (by rule $\ruleFmt{R-While}$) thus obtaining:

\[\begin{split} \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{1} \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \cdots \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygWhileNoBody{x < 2} \\ \qquad \hygAssign{x}{x + 1} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygCondNoThenElse{x < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \end{split}\]

This last expression now reduces by making the “if” condition false:

\[\begin{split} \begin{array}{c} \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygCondNoThenElse{x < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygCondNoThenElse{2 < 2} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygCondNoThenElse{\hygFalse} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \end{array} \end{split}\]

And now, the last expression takes the “else” branch of the “if” (using a rule that you should have defined as part of Exercise 14): therefore, it reduces into the final unit value $()$:

\[\begin{split} \begin{array}{c} \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ \hygCondNoThenElse{\hygFalse} \{ \\ \qquad \hygAssign{x}{x + 1}; \\ \qquad \hygWhileNoBody{x < 2} \\ \qquad\qquad \hygAssign{x}{x + 1} \\ \}\; \hygElse{()} \end{array} }} \;\to\; \hygEvalConf{R}{\boxed{ \begin{array}{@{}l@{}} \hygLetMutInit{x}{2} \\ () \end{array} }} \;\to\; \hygEvalConf{R}{ () } \end{array} \end{split}\]

Typing Rules#

We now extend the typing rules of Hygge0 to support the “while” loop introduced in Definition 17. This only requires a new typing rule, that is quite straightforward (see Definition 20 below): when type-checking “$\hygWhile{e_1}{e_2}$”, we make sure that $e_1$ has type $\tBool$, and $e_2$ is well-typed with some type $T$; if these premises hold, then the “while” loop has type $\tUnit$ (because whenever the loop terminates, it produces a unit value $()$, according to its semantics in Definition 19).

Definition 20 (Typing Rules for “While” Loops)

We define the typing rules of Hygge0 with “while” loops by extending Definition 11 with the following rule:

\[ \begin{array}{c} \begin{prooftree} \AxiomC{$\hygTypeCheckJ{\Gamma}{e_1}{\tBool}$} \AxiomC{$\hygTypeCheckJ{\Gamma}{e_2}{T}$} \BinaryInfCLab{T-While}{$\hygTypeCheckJ{\Gamma}{\hygWhile{e_1}{e_2}}{\tUnit}$} \end{prooftree} \end{array} \]

Exercise 28

Write a typing derivation that type-checks the following expression (giving to each operator its conventional mathematical precedence):

\[\begin{split} \begin{array}{l} \hygLetMutInit{x}{0} \\ \hygWhileNoBody{x * 2 < x + 4} \\ \qquad\hygAssign{x}{x * 2 + 1} \end{array} \end{split}\]

Implementation#

We now have a look at how hyggec can be extended to implement “while” loops, according to the specification illustrated in the previous sections.

Tip

To see a summary of the changes described below, you can inspect the differences in the hyggec Git repositories between the tags mutable-vars and while.

Lexer, Parser, Interpreter, and Type Checking#

These parts of the hyggec compiler are extended along the lines of Example: Extending Hygge0 and hyggec with a Subtraction Operator.

We extend the data type Expr<'E,'T> (in AST.fs) with a new named case While for “$\hygWhile{e_1}{e_2}$” (according to Definition 17).
We extend PrettyPrinter.fs to support the new expression While.
We extend Lexer.fsl to support two new tokens:
- WHILE for the keyword while, and
- DO for the keyword do.
We extend Parser.fsy to recognise the desired sequences of tokens according to Definition 17, and generate AST nodes for the new expression While.
We extend the function subst in ASTUtil.fs to support the new expressions LetMut and Assign, according to Definition 18.
We extend the function reduce in Interpreter.fs to support While, according to Definition 19.
We extend Typechecker.fs according to Definition 20.

Code Generation#

The RISC-V assembly code generated for the expression “$\hygWhile{e_1}{e_2}$” must mimic the semantics in Definition 19. Therefore, it must:

execute the assembly code generated for the condition expression $e_1$;
check the result produced by the code of $e_1$:
- if the result is 0 (false), the assembly code must jump to the end of the loop, and produce no result (corresponding to the unit value). Hence, we need to place an assembly label to mark the end of the loop;
- otherwise, the assembly code must:
  - execute the expression $e_2$ (i.e. the body of the loop); and
  - afterwards, re-evaluate the loop condition. To this purpose, the assembly code can jump back to point 1 above — hence, we need to place an assembly label to mark the beginning of the loop.

Therefore, in the function doCodegen (in the file RISCVCodegen.fs) we add the following pattern matching case.

let rec internal doCodegen (env: CodegenEnv) (node: TypedAST): Asm =
    match node.Expr with
    // ...
    | While(cond, body) ->
        /// Label to mark the beginning of the 'while' loop
        let whileBeginLabel = Util.genSymbol "while_loop_begin"
        /// Label to mark the end of the 'while' loop
        let whileEndLabel = Util.genSymbol "while_loop_end"
        // Check the 'while' condition, jump to 'whileEndLabel' if it is false
        Asm(RV.LABEL(whileBeginLabel))
            ++ (doCodegen env cond)
                .AddText(RV.BEQZ(Reg.r(env.Target), whileEndLabel),
                         "Jump if 'while' loop condition is false")
            ++ (doCodegen env body)
            .AddText([
                (RV.J(whileBeginLabel), "Next iteration of the 'while' loop")
                (RV.LABEL(whileEndLabel), "")
            ])

Project Ideas#

Here are some ideas for your group project.

Project Idea (Easy): C-Style Increment/Decrement Operators
Project Idea (Easy): C-Style Compute-Assign Operators
Project Idea (Easy): “Do…While” Loop
Project Idea (Easy): “For” Loop
Project Idea (Medium Difficulty): a Better “Do…While” Loop (which can replace the “do…while” project idea above)
Project Idea (Medium Difficulty): a “For” Loop with a Scoped Variable (which can replace the “for” loop project idea above)

Hint

There are several ways to implement the following project ideas. Depending on your approach, you may achieve the result without extending the interpreter, nor the code generation…

Note

If you have previously chosen Project Idea (Medium Difficulty): “And” and “Or” with Short-Circuit-Semantics, you can now use mutable variables to improve its tests. See the hints at the end of that project idea…

Project Idea (Easy): C-Style Increment/Decrement Operators#

Add increment or decrement operators to the Hygge0 language and to the hyggec compiler, by following the steps described in Example: Extending Hygge0 and hyggec with a Subtraction Operator. Choose at least two of the following.

Pre-increment expression “${+}{+}x$”, which increments the value of the mutable variable $x$ by 1, and reduces to the value of $x$ after the increment. The value assigned to variable $x$ can only be an integer or a float.
Post-increment expression “$x{+}{+}$”, which increments the value of the mutable variable $x$ by 1, and reduces to the value that $x$ had before the increment. The value assigned to variable $x$ can only be an integer or a float.
Pre-decrement expression “${-}{-}x$”, which decrements the value of the mutable variable $x$ by 1, and reduces to the value of $x$ after the decrement. The value assigned to variable $x$ can only be an integer or a float.
Post-increment expression “$x{-}{-}$”, which decrements the value of the mutable variable $x$ by 1, and reduces to the value that $x$ had before the decrement. The value assigned to variable $x$ can only be an integer or a float.

Hint

For the increment and decrement operators, you should define new tokens for the symbols ++ and/or -- (called e.g. PLUSPLUS and MINUSMINUS).
When modifying Parser.fsy, the increment and decrement operators should be placed in the syntactic category unaryExpr.
You will need to be careful with the precedence of the increment operators. For example, consider the following expression:
```
++ x ++
```
Shold it be parsed as “++ (x ++)” or as “(++ x) ++”?

To avoid ambiguities and select the first option (i.e. give higher precedence to the postfix increment), you could define parsing rules like:
```
unaryExpr:
  // ...
  | PLUSPLUS unaryExpr        { ... }
  | ascriptionExpr PLUSPLUS   { ... }

ascriptionExpr:
  // ...
```

Project Idea (Easy): C-Style Compute-Assign Operators#

Add compute-assign operators to the Hygge0 language and to the hyggec compiler, by following the steps described in Example: Extending Hygge0 and hyggec with a Subtraction Operator. Choose at least two of the following.

Add-assign expression “$x \mathrel{{+}{=}} e$”, which computes the value of $x + e$, assigns the result to the mutable variable $x$, and reduces to the updated value of $x$. This expression only reduces to a value when both $x$ and $e$ are integers or floats.
Minus-assign expression “$x \mathrel{{-}{=}} e$”, which computes the value of $x - e$, assigns the result to the mutable variable $x$, and reduces to the updated value of $x$. This expression only reduces to a value when both $x$ and $e$ are integers or floats.
Multiply-assign expression “$x \mathrel{{*}{=}} e$”, which computes the value of $x * e$, assigns the result to the mutable variable $x$, and reduces to the updated value of $x$. This expression only reduces to a value when both $x$ and $e$ are integers or floats.
Divide-assign expression “$x \mathrel{{/}{=}} e$”, which computes the value of $x / e$, assigns the result to the mutable variable $x$, and reduces to the updated value of $x$. This expression only reduces to a value when both $x$ and $e$ are integers or floats.
Modulo-assign expression “$x \mathrel{{\%}{=}} e$”, which computes the value of the modulo $x \mathbin{\%} e$ , assigns the result to the mutable variable $x$, and reduces to the updated value of $x$. This expression only reduces to a value when both $x$ and $e$ are integers.

Hint

To add these new assignment operators, you should define new tokens for their symbols — e.g. you could add a token for += called ADD_ASSIGN. These new assignment operators should have the same priority and associativity of the regular assignment, hence they can be added in Parser.fsy under the syntactic category simpleExpr.

Project Idea (Easy): “Do…While” Loop#

Add a “$\hygDoWhile{e_1}{e_2}$” expression to the Hygge0 language and to the hyggec compiler, by following the steps described in Example: Extending Hygge0 and hyggec with a Subtraction Operator. The semantics of “$\hygDoWhile{e_1}{e_2}$” is:

reduce $e_1$ into a value;
then, reduce the condition expression $e_2$ into a value:
- if $e_2$ is true, repeat from point 1;
- otherwise, reduce the whole “do…while” expression to the unit value $()$.

Project Idea (Easy): “For” Loop#

Add a C-style loop expression “$\hygFor{e_i}{e_c}{e_u}{e_b}$” to the Hygge0 language and to the hyggec compiler, by following the steps described in Example: Extending Hygge0 and hyggec with a Subtraction Operator. The behaviour of the expression is the following:

reduce the initialisation expression $e_i$ into a value;
reduce the condition expression $e_c$ into a value;
- if $e_c$ reduces to $\hygTrue$:
  - reduce the expression $e_b$ (the body of the loop) into a value;
  - execute the update expression $e_u$;
  - repeat from point 2;
- otherwise, if $e_c$ reduces to $\hygFalse$, reduce the whole for-loop expression into the unit value $()$.

Note

Unlike the “for” loop in C, the initialisation expression $e_i$ is not expected to introduce new variables that are also visible in $e_c$, $e_u$, and $e_b$. In other words, the “for” loop of this project idea should not act like a new binder in the style of “let”.

If you want to implement a more faithful C-style version of “for” loops, where $e_i$ can introduce new variables that are also visible in $e_c$, $e_u$, and $e_b$, see Project Idea (Medium Difficulty): a “For” Loop with a Scoped Variable.

Tip

To avoid parsing ambiguities, the expressions $e_i$, $e_c$, $e_u$, and $e_b$ should be in the category simpleExpr in the parser configuration file Parser.fsy.

Project Idea (Medium Difficulty): a Better “Do…While” Loop#

This project idea can be selected instead of the “do…while” Project Idea above.

Improve the specification of the “$\hygDoWhile{e_1}{e_2}$” loop outlined in the Project Idea above, as follows:

reduce $e_1$ into a value;
then, reduce the condition expression $e_2$ into a value:
- if $e_2$ reduces to $\hygTrue$, repeat from point 1;
- otherwise, reduce the whole “do…while” expression to the value produced by the last execution of $e_1$.

Define the semantics and typing rules that reflect this improved specification, and implement them in hyggec, together with the code generation.

Project Idea (Medium Difficulty): a “For” Loop with a Scoped Variable#

This project idea can be selected instead of the “for” Loop Project Idea above.

Add a C-style loop expression “$\hygFor{\hygLetMutNoInit{x}{e_i}}{e_c}{e_u}{e_b}$” to the Hygge0 language and to the hyggec compiler, by following the steps described in Example: Extending Hygge0 and hyggec with a Subtraction Operator. The behaviour of the expression is the following:

initialise the variable $x$ by reducing the initialisation expression $e_i$ into a value;
reduce the condition expression $e_c$ (which may refer to $x$) into a value;
- if $e_c$ reduces to $\hygTrue$:
  - reduce the expression $e_b$ (the body of the loop, which may refer to $x$) into a value;
  - execute the update expression $e_u$ (which may refer to $x$);
  - repeat from point 2;
- otherwise, if $e_c$ reduces to $\hygFalse$, reduce the whole for-loop expression into the unit value $()$.

Make sure that the variable $x$ is not visible outside the loop.

Define the semantics and typing rules that reflect this improved specification, and implement them in hyggec, together with the code generation.

Tip

To avoid parsing ambiguities, the expressions $e_i$, $e_c$, $e_u$, and $e_b$ should be in the category simpleExpr in the parser configuration file Parser.fsy.

02247 Compiler Construction — Spring 2024

Module 5: Mutability and Loops

Contents

Module 5: Mutability and Loops#

Overall Objective#

Mutable Variables#

Design Considerations#

Syntax#

Operational Semantics#

Typing Rules#

Implementation#

Lexer, Parser, Interpreter, and Type Checking#

Code Generation#

“While” Loop#

Syntax#

Operational Semantics#

Typing Rules#

Implementation#

Lexer, Parser, Interpreter, and Type Checking#

Code Generation#

Project Ideas#

Project Idea (Easy): C-Style Increment/Decrement Operators#

Project Idea (Easy): C-Style Compute-Assign Operators#

Project Idea (Easy): “Do…While” Loop#

Project Idea (Easy): “For” Loop#

Project Idea (Medium Difficulty): a Better “Do…While” Loop#

Project Idea (Medium Difficulty): a “For” Loop with a Scoped Variable#