Text Format

Instructions

Control Instructions

The label identifier on a structured control instruction may optionally be repeated after the corresponding \(\mathtt{end}\), \(\mathtt{else}\), \(\mathtt{catch}\), \(\mathtt{catch\_all}\), and \(\mathtt{delegate}\) pseudo instructions, to indicate the matching delimiters.

\[\begin{split}\begin{array}{@{}llclll} \def\mathdef247#1{{}}\mathdef247{block instruction} & \href{../text/instructions.html#text-blockinstr}{\mathtt{blockinstr}}_I &::=& \dots \\ &&|& \def\mathdef286#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef286{try}~~I'{:}\href{../text/instructions.html#text-label}{\mathtt{label}}_I~~\mathit{bt}{:}\href{../text/instructions.html#text-blocktype}{\mathtt{blocktype}}~~(\mathit{in}_1{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I'})^\ast~~\\&&& (\def\mathdef287#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef287{catch}~~\href{../text/values.html#text-id}{\mathtt{id}}_1^?~~x{:}\href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}_I~~(\mathit{in}_2{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I'})^\ast)^\ast~~ \\&&& (\def\mathdef288#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef288{catch\_all}~~\href{../text/values.html#text-id}{\mathtt{id}}_1^?~~(\mathit{in}_3{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I'})^\ast)^?~~ \\&&& \def\mathdef289#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef289{end}~~\href{../text/values.html#text-id}{\mathtt{id}}_2^? \\ &&&\qquad \Rightarrow\quad \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\mathit{bt}~\mathit{in}_1^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch}}~x~\mathit{in}_2^\ast)^\ast~(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{catch\_all}}~\mathit{in}_3^\ast)^?~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&&\qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}_1^? = \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}_1^? = \href{../text/instructions.html#text-label}{\mathtt{label}}, \href{../text/values.html#text-id}{\mathtt{id}}_2^? = \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}_2^? = \href{../text/instructions.html#text-label}{\mathtt{label}}) \\ &&|& \def\mathdef290#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef290{try}~~I'{:}\href{../text/instructions.html#text-label}{\mathtt{label}}_I~~\mathit{bt}{:}\href{../text/instructions.html#text-blocktype}{\mathtt{blocktype}}~~(\mathit{in}_1{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I'})^\ast~~ \\&&& \def\mathdef291#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef291{delegate}~~l{:}\href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I~~\mathit{l}{:}\href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I \\ &&&\qquad \Rightarrow\quad \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{try}}~\mathit{bt}~\mathit{in}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{delegate}}~l \qquad\quad~~ (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \href{../text/instructions.html#text-label}{\mathtt{label}}) \\ \def\mathdef247#1{{}}\mathdef247{plain instruction} & \href{../text/instructions.html#text-plaininstr}{\mathtt{plaininstr}}_I &::=& \dots \\ &&|& \def\mathdef292#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef292{rethrow}~~l{:}\href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I \quad\Rightarrow\quad \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{rethrow}}~l \\ \end{array}\end{split}\]