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

@@ -68,12 +68,12 @@ In addition to field access written :math:`C.\K{field}` the following notation i
 
 * 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[x]` 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,7 +477,7 @@ 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^?]
    }
@@ -501,7 +501,7 @@ 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^?]
    }
@@ -528,9 +528,9 @@ 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^?]
    }

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^?]
    }