= Solution
Let `expr(e)` generate <postfix code> that evaluates a <program expression> once, leaving one value above an otherwise unchanged evaluation <stack>. Let `stmt(s)` preserve the evaluation <stack>'s height. Use `EQ` to pop two <integers> and push their <Boolean> <equality> result; `JZ L` pops that result and jumps to `L` when it is false. `JMP` is unconditional. All labels returned by `fresh()` are distinct, including labels inside recursively generated bodies.
``
generateCase(Case(control, arms)):
done := fresh()
emit expr(control)
for (labelExpression, body) in arms, in source order:
next := fresh()
emit DUP
emit expr(labelExpression)
emit EQ
emit JZ next
emit POP
emit stmt(body)
emit JMP done
emit LABEL next
emit POP
emit LABEL done
``
To verify the <stack invariant>, write the incoming evaluation <stack> as $sigma$. Immediately before any label test it is $sigma,v$, where $v$ is the controlling value. `DUP`, evaluation of the label with value $w$, and `EQ` change this to $sigma,v,[v=w]$. `JZ` removes the <Boolean>. On failure the surviving $v$ is available for the next label; on success `POP` removes it before the body runs. The body therefore starts and ends with $sigma$ and jumps past every remaining label. If every label fails, the final `POP` restores $sigma$.
\b[The controlling expression is evaluated once, each reached label is evaluated once, and no later label or arm is evaluated after a match.] Keeping $v$ on the evaluation <stack> also preserves its original value if a label evaluation has a <side effect> that changes a variable appearing in the controlling <program expression>. A nested `Case` uses the same <stack invariant> relative to whatever <stack> it receives. The concise contract is
$$
\boxed{N_{\mathrm{control}}=1,\quad N_{\mathrm{reached\ label}}=1,\quad \Delta h_{\mathrm{stack}}=0.}
$$
Back to article page
