Validation¶

Conventions¶

Contexts¶

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

\[\begin{split}\begin{array}{llll} \def\mathdef293#1{{}}\mathdef293{labeltype} & \href{../valid/conventions.html#context}{\mathit{labeltype}} & ::= & \href{../valid/conventions.html#context}{\mathsf{catch}}^?~\href{../syntax/types.html#syntax-resulttype}{\mathit{resulttype}} \\ \def\mathdef293#1{{}}\mathdef293{context} & C &::=& \{ \dots, \href{../valid/conventions.html#context}{\mathsf{labels}}~\href{../valid/conventions.html#context}{\mathit{labeltype}}^\ast, \dots \} \end{array}\end{split}\]

Existing typing rules are adjusted as follows:

All rules that extend the context with new labels use an absent \(\href{../valid/conventions.html#context}{\mathsf{catch}}\) flag.
All rules that inspect the context for a label ignore the presence of a \(\href{../valid/conventions.html#context}{\mathsf{catch}}\) flag.

Note

This flag is used to distinguish labels bound by catch clauses, which can be targeted by \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{rethrow}}\).

Instructions¶

Control Instructions¶

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast)^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)^?~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)¶

The block type must be valid as some function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
Let \(C'\) be the same context as \(C\), but with the label type \([t_2^\ast]\) prepended to the \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) vector.
Under context \(C'\), the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast\) must be valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
Let \(C''\) be the same context as \(C\), but with the label type \(\href{../valid/conventions.html#context}{\mathsf{catch}}~[t_2^\ast]\) prepended to the \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) vector.
For every \(x_i\) and \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_{2i}^\ast\) in \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast)^\ast\):
- The tag \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x_i]\) must be defined in the context \(C\).
- Let \([t_{3i}^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_{4i}^\ast]\) be the tag type \(C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x_i]\).
- The result type \([t_{4i}^\ast]\) must be empty.
- Under context \(C''\), the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_{2i}^\ast\) must be valid with type \([t_{3i}^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
If \((\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)^?\) is not empty, then:
- Under context \(C''\), the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast\) must be valid with type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
Then the compound instruction is valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

\[\begin{split}~\\ \frac{ \begin{array}{c} C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_2^\ast] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \\ (C.\href{../valid/conventions.html#context}{\mathsf{tags}}[x] = [t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [])^\ast \\ C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,(\href{../valid/conventions.html#context}{\mathsf{catch}}~[t_2^\ast]) \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast : [t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast])^\ast \\ (C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,(\href{../valid/conventions.html#context}{\mathsf{catch}}~[t_2^\ast]) \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast])^? \end{array} }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_1^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_2^\ast)^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}_3^\ast)^?~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\end{split}\]

Note

The notation \(C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,(\href{../valid/conventions.html#context}{\mathsf{catch}}~[t^\ast])\) inserts the new label type at index \(0\), shifting all others.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l\)¶

The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.
The block type must be valid as some function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
Let \(C'\) be the same context as \(C\), but with the result type \([t_2^\ast]\) prepended to the \(\href{../valid/conventions.html#context}{\mathsf{labels}}\) vector.
Under context \(C'\), the instruction sequence \(\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast\) must be valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).
Then the compound instruction is valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

\[\begin{split}~\\ \frac{ C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}} : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \qquad C,\href{../valid/conventions.html#context}{\mathsf{labels}}\,[t_2^\ast] \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast : [t_1^\ast]\href{../syntax/types.html#syntax-functype}{\rightarrow}[t_2^\ast] \qquad C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l] = [t_0^\ast] }{ C \href{../valid/instructions.html#valid-instr-seq}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\href{../syntax/instructions.html#syntax-blocktype}{\mathit{blocktype}}~\href{../syntax/instructions.html#syntax-instr}{\mathit{instr}}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l : [t_1^\ast]\href{../syntax/types.html#syntax-functype}{\rightarrow}[t_2^\ast] }\end{split}\]

Note

The label index space in the context \(C\) contains the most recent label first, so that \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) performs a relative lookup as expected.

\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{rethrow}}~l\)¶

The label \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\) must be defined in the context.
Let \((\href{../valid/conventions.html#context}{\mathsf{catch}}^?~[t^\ast])\) be the label type \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\).
The \(\href{../valid/conventions.html#context}{\mathsf{catch}}\) must be present in the label type \(C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l]\).
Then the instruction is valid with type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\), for any sequences of value types \(t_1^\ast\) and \(t_2^\ast\).

\[\begin{split}~\\ \frac{ C.\href{../valid/conventions.html#context}{\mathsf{labels}}[l] = \href{../valid/conventions.html#context}{\mathsf{catch}}~[t^\ast] }{ C \href{../valid/instructions.html#valid-instr}{\vdash} \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{rethrow}}~l : [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] }\end{split}\]

Note

The \(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{rethrow}}\) instruction is stack-polymorphic.