Address additional review of #222, also fixing label types everywhere.

document/core/appendix/algorithm.rst

@@ -122,7 +122,7 @@ The control stack is likewise manipulated through auxiliary functions:
      ctrls.pop()
      return frame
 
-   func label_types(frame : ctrl_frame) : list(val_types) =
+   func label_types(frame : ctrl_frame) : list(val_type) =
      return (if frame.opcode == loop then frame.start_types else frame.end_types)
 
    func unreachable() =

document/core/appendix/properties.rst

@@ -655,7 +655,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
    \frac{
      S; C,\CLABELS\,[t^\ast] \vdashinstrseq \instr^\ast : [] \to [t^\ast]
      \qquad
-     C.\CLABELS[l] = [t_0^\ast]
+     C.\CLABELS[l] = \LCATCH^?~[t_0^\ast]
    }{
      S; C,\CLABELS\,[t^\ast] \vdashadmininstr \DELEGATEadm\{l\}~\instr^\ast~\END : [] \to [t^\ast]
    }
@@ -679,7 +679,6 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 * Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`.
 
-
 .. math::
    \frac{
      S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t_0^\ast]\to[]
@@ -716,7 +715,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 * The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid <valid-instr-seq>` with some type :math:`[t_1^n] \to [t_2^*]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_1^n]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_1^n]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t_2^*]`.

document/core/valid/instructions.rst

@@ -1234,7 +1234,7 @@ Memory Instructions
    }
 
 
-.. index:: control instructions, structured control, label, block, branch, block type, label index, function index, type index, tag index, vector, polymorphism, context
+.. index:: control instructions, structured control, label, block, branch, block type, label index, label type, function index, type index, tag index, vector, polymorphism, context
    pair: validation; instruction
    single: abstract syntax; instruction
 .. _valid-label:
@@ -1281,7 +1281,7 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
@@ -1308,7 +1308,7 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_1^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_1^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
@@ -1335,7 +1335,7 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
@@ -1368,23 +1368,25 @@ Control Instructions
 
 * The :ref:`block type <syntax-blocktype>` must be :ref:`valid <valid-blocktype>` as some :ref:`function type <syntax-functype>` :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]` prepended to the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_1^\ast] \to [t_2^\ast]`.
 
-* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label <exec-label>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.
+* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector.
 
-* For every :math:`(\CATCH~x~\instr_2^\ast)`:
+* For every :math:`x_i` and :math:`\instr_{2i}^\ast` in :math:`(\CATCH~x~\instr_2^\ast)^\ast`:
 
-  * The tag :math:`C.\CTAGS[x]` must be defined in the context :math:`C`.
+  * The tag :math:`C.\CTAGS[x_i]` must be defined in the context :math:`C`.
 
-  * Let :math:`[t^\ast] \to []` be its :ref:`tag type <syntax-tagtype>`.
+  * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type <syntax-tagtype>` :math:`C.\CTAGS[x_i]`.
+
+  * The :ref:`result type <syntax-resulttype>` :math:`[t_{4i}^\ast]` must be empty.
 
   * Under context :math:`C''`,
-    the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t^\ast] \to [t_2^\ast]`.
+    the instruction sequence :math:`\instr_{2i}^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[t_{3i}^\ast] \to [t_2^\ast]`.
 
-* If there is a :math:`(\CATCHALL~\instr_3^\ast)`, then:
+* If :math:`(\CATCHALL~\instr_3^\ast)^?` is not empty, then:
 
   * Under context :math:`C''`,
     the instruction sequence :math:`\instr_3^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t_2^\ast]`.
@@ -1460,9 +1462,9 @@ Control Instructions
 
 * The label :math:`C.\CLABELS[l]` must be defined in the context.
 
-* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type <labeltype>` :math:`C.\CLABELS[l]`.
+* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
-* The |LCATCH| must be present in the :ref:`label type <labeltype>` :math:`C.\CLABELS[l]`.
+* The |LCATCH| must be present in the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
 * Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of  :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
@@ -1487,19 +1489,19 @@ Control Instructions
 
 * The label :math:`C.\CLABELS[l]` must be defined in the context.
 
-* Let :math:`[t^\ast]` be the :ref:`result type <syntax-resulttype>` :math:`C.\CLABELS[l]`.
+* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
 * Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types <syntax-valtype>` :math:`t_1^\ast` and :math:`t_2^\ast`.
 
 .. math::
    \frac{
-     C.\CLABELS[l] = [t^\ast]
+     C.\CLABELS[l] = \LCATCH^?~[t^\ast]
    }{
      C \vdashinstr \BR~l : [t_1^\ast~t^\ast] \to [t_2^\ast]
    }
 
 .. note::
-   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label type first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
 
    The |BR| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
@@ -1511,19 +1513,19 @@ Control Instructions
 
 * The label :math:`C.\CLABELS[l]` must be defined in the context.
 
-* Let :math:`[t^\ast]` be the :ref:`result type <syntax-resulttype>` :math:`C.\CLABELS[l]`.
+* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[l]`.
 
 * Then the instruction is valid with type :math:`[t^\ast~\I32] \to [t^\ast]`.
 
 .. math::
    \frac{
-     C.\CLABELS[l] = [t^\ast]
+     C.\CLABELS[l] = \LCATCH^?~[t^\ast]
    }{
      C \vdashinstr \BRIF~l : [t^\ast~\I32] \to [t^\ast]
    }
 
 .. note::
-   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
+   The :ref:`label index <syntax-labelidx>` space in the :ref:`context <context>` :math:`C` contains the most recent label type first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected.
 
 
 .. _valid-br_table:

document/core/valid/modules.rst

@@ -29,7 +29,7 @@ Functions :math:`\func` are classified by :ref:`function types <syntax-functype>
 
   * |CLOCALS| set to the sequence of :ref:`value types <syntax-valtype>` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals,
 
-  * |CLABELS| set to the singular sequence containing only :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]`.
+  * |CLABELS| set to the singular sequence containing only :ref:`label type <syntax-labeltype>` :math:`[t_2^\ast]`.
 
   * |CRETURN| set to the :ref:`result type <syntax-resulttype>` :math:`[t_2^\ast]`.