Validation

Conventions

Contexts

The context is enriched with an additional flag on label types:

$$\begin{array}{r}\begin{array}{llll}& \mathit{labeltype}& ::=& {\mathsf{catch}}^{?}\mathit{resulttype}\\ & C& ::=& \{\dots ,\mathsf{labels}{\mathit{labeltype}}^{\ast },\dots \}\end{array}\end{array}$$

Existing typing rules are adjusted as follows:

• All rules that extend the context with new labels use an absent $\mathsf{catch}$ flag.

• All rules that inspect the context for a label ignore the presence of a $\mathsf{catch}$ flag.

Note

This flag is used to distinguish labels bound by catch clauses, which can be targeted by $\mathsf{rethrow}$.

Instructions

Control Instructions

$\mathsf{try}\mathit{blocktype}{\mathit{instr}}_1^{\ast }(\mathsf{catch}x{\mathit{instr}}_2^{\ast }{)}^{\ast }(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast }{)}^{?}\mathsf{end}$

• The block type must be valid as some function type $[t_1^{\ast }]\to [t_2^{\ast }]$.

• Let $C^{\prime }$ be the same context as $C$, but with the label type $[t_2^{\ast }]$ prepended to the $\mathsf{labels}$ vector.

• Under context $C^{\prime }$, the instruction sequence ${\mathit{instr}}_1^{\ast }$ must be valid with type $[t_1^{\ast }]\to [t_2^{\ast }]$.

• Let $C^{″}$ be the same context as $C$, but with the label type $\mathsf{catch}[t_2^{\ast }]$ prepended to the $\mathsf{labels}$ vector.

• For every $x_i$ and ${\mathit{instr}}_{2i}^{\ast }$ in $(\mathsf{catch}x{\mathit{instr}}_2^{\ast }{)}^{\ast }$:

  • The tag $C.\mathsf{tags}[x_i]$ must be defined in the context $C$.

  • Let $[t_{3i}^{\ast }]\to [t_{4i}^{\ast }]$ be the tag type $C.\mathsf{tags}[x_i]$.

  • The result type $[t_{4i}^{\ast }]$ must be empty.

  • Under context $C^{″}$, the instruction sequence ${\mathit{instr}}_{2i}^{\ast }$ must be valid with type $[t_{3i}^{\ast }]\to [t_2^{\ast }]$.

• If $(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast }{)}^{?}$ is not empty, then:

  • Under context $C^{″}$, the instruction sequence ${\mathit{instr}}_3^{\ast }$ must be valid with type $[]\to [t_2^{\ast }]$.

• Then the compound instruction is valid with type $[t_1^{\ast }]\to [t_2^{\ast }]$.

$$\begin{array}{r}\\ \frac{\begin{array}{c}C⊢\mathit{blocktype}:[t_1^{\ast }]\to [t_2^{\ast }]C,\mathsf{labels}[t_2^{\ast }]⊢{\mathit{instr}}_1^{\ast }:[t_1^{\ast }]\to [t_2^{\ast }]\\ (C.\mathsf{tags}[x]=[t^{\ast }]\to []{)}^{\ast }\\ C,\mathsf{labels}(\mathsf{catch}[t_2^{\ast }])⊢{\mathit{instr}}_2^{\ast }:[t^{\ast }]\to [t_2^{\ast }]{)}^{\ast }\\ (C,\mathsf{labels}(\mathsf{catch}[t_2^{\ast }])⊢{\mathit{instr}}_3^{\ast }:[]\to [t_2^{\ast }]{)}^{?}\end{array}}{C⊢\mathsf{try}\mathit{blocktype}{\mathit{instr}}_1^{\ast }(\mathsf{catch}x{\mathit{instr}}_2^{\ast }{)}^{\ast }(\mathsf{catch}\mathsf{\_}\mathsf{all}{\mathit{instr}}_3^{\ast }{)}^{?}\mathsf{end}:[t_1^{\ast }]\to [t_2^{\ast }]}\end{array}$$

Note

The notation $C,\mathsf{labels}(\mathsf{catch}[t^{\ast }])$ inserts the new label type at index $0$, shifting all others.

$\mathsf{try}\mathit{blocktype}{\mathit{instr}}^{\ast }\mathsf{delegate}l$

• The label $C.\mathsf{labels}[l]$ must be defined in the context.

• The block type must be valid as some function type $[t_1^{\ast }]\to [t_2^{\ast }]$.

• Let $C^{\prime }$ be the same context as $C$, but with the result type $[t_2^{\ast }]$ prepended to the $\mathsf{labels}$ vector.

• Under context $C^{\prime }$, the instruction sequence ${\mathit{instr}}^{\ast }$ must be valid with type $[t_1^{\ast }]\to [t_2^{\ast }]$.

• Then the compound instruction is valid with type $[t_1^{\ast }]\to [t_2^{\ast }]$.

$$\begin{array}{r}\\ \frac{C⊢\mathit{blocktype}:[t_1^{\ast }]\to [t_2^{\ast }]C,\mathsf{labels}[t_2^{\ast }]⊢{\mathit{instr}}^{\ast }:[t_1^{\ast }]\to [t_2^{\ast }]C.\mathsf{labels}[l]=[t_0^{\ast }]}{C⊢\mathsf{try}\mathit{blocktype}{\mathit{instr}}^{\ast }\mathsf{delegate}l:[t_1^{\ast }]\to [t_2^{\ast }]}\end{array}$$

Note

The label index space in the context $C$ contains the most recent label first, so that $C.\mathsf{labels}[l]$ performs a relative lookup as expected.

$\mathsf{rethrow}l$

• The label $C.\mathsf{labels}[l]$ must be defined in the context.

• Let $({\mathsf{catch}}^{?}[t^{\ast }])$ be the label type $C.\mathsf{labels}[l]$.

• The $\mathsf{catch}$ must be present in the label type $C.\mathsf{labels}[l]$.

• Then the instruction is valid with type $[t_1^{\ast }]\to [t_2^{\ast }]$, for any sequences of value types $t_1^{\ast }$ and $t_2^{\ast }$.

$$\begin{array}{r}\\ \frac{C.\mathsf{labels}[l]=\mathsf{catch}[t^{\ast }]}{C⊢\mathsf{rethrow}l:[t_1^{\ast }]\to [t_2^{\ast }]}\end{array}$$

Note

The $\mathsf{rethrow}$ instruction is stack-polymorphic.