Revert context extension notation

Author: rossberg

document/core/syntax/conventions.rst

@@ -41,9 +41,13 @@ The following conventions are adopted in defining grammar rules for abstract syn
 
 
 
+.. _notation-epsilon:
+.. _notation-length:
+.. _notation-index:
 .. _notation-slice:
 .. _notation-replace:
 .. _notation-record:
+.. _notation-project:
 .. _notation-concat:
 .. _notation-compose:
 

document/core/valid/conventions.rst

@@ -64,16 +64,18 @@ More concretely, contexts are defined as :ref:`records <notation-record>` :math:
      \end{array}
    \end{array}
 
+.. _notation-extend:
+
 In addition to field access written :math:`C.\K{field}` the following notation is adopted for manipulating contexts:
 
 * When spelling out a context, empty fields are omitted.
 
-* The notation :math:`\K{field}\,A^\ast, C` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence.
+* :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence.
 
 .. note::
-   The notation for context extension is only used in situations where the original :math:`C.\K{field}` is either empty
-   or :math:`\K{field}` is :math:`\K{labels}`.
-   It is reversed from usual conventions because it *prepends* not *appends*, in accordance with the use of relative indexing to look up a label in the context's label list.
+   We use :ref:`indexing notation <notation-index>` like :math:`C.\CLABELS[i]` to look up indices in their respective :ref:`index space <syntax-index>` in the context.
+   Context extension notation :math:`C,\K{field}\,A` is primarily used to locally extend *relative* index spaces, such as :ref:`label indices <syntax-labelidx>`.
+   Accordingly, the notation is defined to append at the *front* of the respective sequence, introducing a new relative index :math:`0` and shifting the existing ones.
 
 
 .. _valid-notation-textual:

document/core/valid/instructions.rst

@@ -477,12 +477,14 @@ Control Instructions
 
 .. math::
    \frac{
-     \CLABELS\,[t^?], C \vdashinstrseq \instr^\ast : [] \to [t^?]
+     C,\CLABELS\,[t^?] \vdashinstrseq \instr^\ast : [] \to [t^?]
    }{
      C \vdashinstr \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?]
    }
 
 .. note::
+   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others.
+
    The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the block was entered.
    This may be generalized in future versions of WebAssembly.
 
@@ -501,12 +503,14 @@ Control Instructions
 
 .. math::
    \frac{
-     \CLABELS\,[], C \vdashinstrseq \instr^\ast : [] \to [t^?]
+     C,\CLABELS\,[] \vdashinstrseq \instr^\ast : [] \to [t^?]
    }{
      C \vdashinstr \LOOP~[t^?]~\instr^\ast~\END : [] \to [t^?]
    }
 
 .. note::
+   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others.
+
    The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the loop was entered.
    This may be generalized in future versions of WebAssembly.
 
@@ -528,14 +532,16 @@ Control Instructions
 
 .. math::
    \frac{
-     \CLABELS\,[t^?], C \vdashinstrseq \instr_1^\ast : [] \to [t^?]
+     C,\CLABELS\,[t^?] \vdashinstrseq \instr_1^\ast : [] \to [t^?]
      \qquad
-     \CLABELS\,[t^?], C \vdashinstrseq \instr_2^\ast : [] \to [t^?]
+     C,\CLABELS\,[t^?] \vdashinstrseq \instr_2^\ast : [] \to [t^?]
    }{
      C \vdashinstr \IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [\I32] \to [t^?]
    }
 
 .. note::
+   The :ref:`notation <notation-extend>` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others.
+
    The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the conditional was entered.
    This may be generalized in future versions of WebAssembly.
 
@@ -559,6 +565,8 @@ Control Instructions
    }
 
 .. 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 |BR| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
 
@@ -580,6 +588,9 @@ Control Instructions
      C \vdashinstr \BRIF~l : [t^?~\I32] \to [t^?]
    }
 
+.. 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.
+
 
 .. _valid-br_table:
 
@@ -608,6 +619,8 @@ Control Instructions
    }
 
 .. 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_i]` performs a relative lookup as expected.
+
    The |BRTABLE| instruction is :ref:`stack-polymorphic <polymorphism>`.
 
 

document/core/valid/modules.rst

@@ -42,7 +42,7 @@ Functions :math:`\func` are classified by :ref:`function types <syntax-functype>
    \frac{
      C.\CTYPES[x] = [t_1^\ast] \to [t_2^?]
      \qquad
-     \CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?], C \vdashexpr \expr : [t_2^?]
+     C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?] \vdashexpr \expr : [t_2^?]
    }{
      C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^?]
    }