From 78c18fb16daa4d8d12344462f02a2e5c5d668912 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 25 Aug 2022 18:36:53 +0200 Subject: [PATCH] [spec] Correct use of opdtype and stacktype (#1524) --- document/core/valid/instructions.rst | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index ac4b34a82c..384a651377 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -48,7 +48,7 @@ This is extended to stack types in a point-wise manner. consuming two |I32| values and producing one. Typing extends to :ref:`instruction sequences ` :math:`\instr^\ast`. -Such a sequence has a :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]` if the accumulative effect of executing the instructions is consuming values of types :math:`t_1^\ast` off the operand stack and pushing new values of types :math:`t_2^\ast`. +Such a sequence has a :ref:`stack type ` :math:`[t_1^\ast] \to [t_2^\ast]` if the accumulative effect of executing the instructions is consuming values of types :math:`t_1^\ast` off the operand stack and pushing new values of types :math:`t_2^\ast`. .. _polymorphism: @@ -63,7 +63,7 @@ Two degrees of polymorphism can be distinguished: * *stack-polymorphic*: - the entire (or most of the) :ref:`function type ` :math:`[t_1^\ast] \to [t_2^\ast]` of the instruction is unconstrained. + the entire (or most of the) :ref:`stack type ` :math:`[t_1^\ast] \to [t_2^\ast]` of the instruction is unconstrained. That is the case for all :ref:`control instructions ` that perform an *unconditional control transfer*, such as |UNREACHABLE|, |BR|, |BRTABLE|, and |RETURN|. In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program. @@ -81,7 +81,7 @@ In both cases, the unconstrained types or type sequences can be chosen arbitrari are valid, with :math:`t` in the typing of |SELECT| being instantiated to |I32| or |F64|, respectively. - The |UNREACHABLE| instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]` for any possible sequences of value types :math:`t_1^\ast` and :math:`t_2^\ast`. + The |UNREACHABLE| instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]` for any possible sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`. Consequently, .. math:: @@ -258,7 +258,7 @@ Reference Instructions Vector Instructions ~~~~~~~~~~~~~~~~~~~ -Vector instructions can have a prefix to describe the :ref:`shape ` of the operand. Packed numeric types, |I8| and |I16|, are not :ref:`value type `, we define an auxiliary function to map such packed types into value types: +Vector instructions can have a prefix to describe the :ref:`shape ` of the operand. Packed numeric types, |I8| and |I16|, are not :ref:`value types `. An auxiliary function maps such packed types to value types: .. math:: \begin{array}{lll@{\qquad}l} @@ -598,7 +598,7 @@ Parametric Instructions :math:`\DROP` ............. -* The instruction is valid with type :math:`[t] \to []`, for any :ref:`value type ` :math:`t`. +* The instruction is valid with type :math:`[t] \to []`, for any :ref:`operand type ` :math:`t`. .. math:: \frac{ @@ -1267,7 +1267,7 @@ Control Instructions :math:`\UNREACHABLE` .................... -* 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`. +* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ @@ -1374,7 +1374,7 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result 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`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ @@ -1422,14 +1422,14 @@ Control Instructions * For all :math:`l_i` in :math:`l^\ast`, the label :math:`C.\CLABELS[l_i]` must be defined in the context. -* There must be a :ref:`result type ` :math:`[t^\ast]`, such that: +* There must be a sequence :math:`t^\ast` of :ref:`operand types `, such that: * For each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{Nj}` in :math:`C.\CLABELS[l_N]`, :math:`t_j` :ref:`matches ` :math:`t'_{Nj}`. * For all :math:`l_i` in :math:`l^\ast`, and for each :ref:`operand type ` :math:`t_j` in :math:`t^\ast` and corresponding type :math:`t'_{ij}` in :math:`C.\CLABELS[l_i]`, :math:`t_j` :ref:`matches ` :math:`t'_{ij}`. -* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast~\I32] \to [t_2^\ast]`, for any sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ @@ -1455,7 +1455,7 @@ Control Instructions * Let :math:`[t^\ast]` be the :ref:`result type ` of :math:`C.\CRETURN`. -* 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`. +* Then the instruction is valid with type :math:`[t_1^\ast~t^\ast] \to [t_2^\ast]`, for any sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ @@ -1542,12 +1542,12 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` ............................................................ * The instruction sequence :math:`\instr^\ast` must be valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, - for some sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. + for some sequences of :ref:`operand types ` :math:`t_1^\ast` and :math:`t_2^\ast`. * The instruction :math:`\instr_N` must be valid with type :math:`[t^\ast] \to [t_3^\ast]`, - for some sequences of :ref:`value types ` :math:`t^\ast` and :math:`t_3^\ast`. + for some sequences of :ref:`operand types ` :math:`t^\ast` and :math:`t_3^\ast`. -* There must be a sequence of :ref:`value types ` :math:`t_0^\ast`, +* There must be a sequence of :ref:`operand types ` :math:`t_0^\ast`, such that :math:`t_2^\ast = t_0^\ast~{t'}^\ast` where the type sequence :math:`{t'}^\ast` is as long as :math:`t^\ast`. * For each :ref:`operand type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`.