diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst index d03882b9..8269bb21 100644 --- a/document/core/appendix/algorithm.rst +++ b/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() = diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index 837ecb8c..c2a9c792 100644 --- a/document/core/appendix/properties.rst +++ b/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 ` with some type :math:`[t_1^n] \to [t_2^*]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_1^n]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_1^n]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^*]`. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index dc5efe55..b7799f33 100644 --- a/document/core/valid/instructions.rst +++ b/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 ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1308,7 +1308,7 @@ Control Instructions * The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_1^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_1^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1335,7 +1335,7 @@ Control Instructions * The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. @@ -1368,23 +1368,25 @@ Control Instructions * The :ref:`block type ` must be :ref:`valid ` as some :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :math:`[t_2^\ast]` prepended to the |CLABELS| vector. * Under context :math:`C'`, the instruction sequence :math:`\instr_1^\ast` must be :ref:`valid ` with type :math:`[t_1^\ast] \to [t_2^\ast]`. -* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the :ref:`label ` :math:`\LCATCH~[t_2^\ast]` prepended to the |CLABELS| vector. +* Let :math:`C''` be the same :ref:`context ` as :math:`C`, but with the :ref:`label type ` :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 `. + * Let :math:`[t_{3i}^\ast] \to [t_{4i}^\ast]` be the :ref:`tag type ` :math:`C.\CTAGS[x_i]`. + + * The :ref:`result type ` :math:`[t_{4i}^\ast]` must be empty. * Under context :math:`C''`, - the instruction sequence :math:`\instr_2^\ast` must be :ref:`valid ` with type :math:`[t^\ast] \to [t_2^\ast]`. + the instruction sequence :math:`\instr_{2i}^\ast` must be :ref:`valid ` 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 ` 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 ` :math:`C.\CLABELS[l]`. +* Let :math:`(\LCATCH^?~[t^\ast])` be the :ref:`label type ` :math:`C.\CLABELS[l]`. -* The |LCATCH| must be present in the :ref:`label type ` :math:`C.\CLABELS[l]`. +* The |LCATCH| must be present in the :ref:`label type ` :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 ` :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 ` :math:`C.\CLABELS[l]`. +* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type ` :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 ` :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 ` space in the :ref:`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 ` space in the :ref:`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 `. @@ -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 ` :math:`C.\CLABELS[l]`. +* Let :math:`\LCATCH^?~[t^\ast]` be the :ref:`label type ` :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 ` space in the :ref:`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 ` space in the :ref:`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: diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 71a8b1ef..ddf2815c 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -29,7 +29,7 @@ Functions :math:`\func` are classified by :ref:`function types * |CLOCALS| set to the sequence of :ref:`value types ` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals, - * |CLABELS| set to the singular sequence containing only :ref:`result type ` :math:`[t_2^\ast]`. + * |CLABELS| set to the singular sequence containing only :ref:`label type ` :math:`[t_2^\ast]`. * |CRETURN| set to the :ref:`result type ` :math:`[t_2^\ast]`.