[spec] Tweaks

Author: rossberg

document/core/appendix/properties.rst

@@ -27,7 +27,7 @@ Contexts
 ~~~~~~~~
 
 In order to check :ref:`rolled up <aux-roll-rectype>` recursive types,
-the :ref:`context <context>` is locally extended with an additional component that records the :ref:`sub type <syntax-subtype>` corresponding to each :ref:`recursive type index <syntax-rectypeidx>` within the current :ref:`recursive type <syntax-rectype>`:
+the :ref:`context <context>` is locally extended with an additional component that records the :ref:`sub type <syntax-subtype>` corresponding to each :ref:`recursive type index <syntax-rectypeidx>` within the current group of :ref:`recursive types <syntax-rectype>`:
 
 $${syntax: context/sem}
 

document/core/valid/conventions.rst

@@ -218,7 +218,6 @@ Validity of an individual definition is specified relative to a *context*,
 which collects relevant information about the surrounding :ref:`module <syntax-module>` and the definitions in scope:
 
 * *Types*: the list of :ref:`types <syntax-type>` defined in the current module.
-.. * *Recursive Types*: the list of :ref:`sub types <syntax-subtype>` in the current group of recursive types.
 * *Functions*: the list of :ref:`functions <syntax-func>` declared in the current module, represented by a :ref:`defined type <syntax-deftype>` that :ref:`expands <aux-expand-deftype>` to their :ref:`function type <syntax-functype>`.
 * *Tables*: the list of :ref:`tables <syntax-table>` declared in the current module, represented by their :ref:`table type <syntax-tabletype>`.
 * *Memories*: the list of :ref:`memories <syntax-mem>` declared in the current module, represented by their :ref:`memory type <syntax-memtype>`.
@@ -241,7 +240,7 @@ More concretely, contexts are defined as :ref:`records <notation-record>` ${:C}
 $${syntax: context/syn}
 
 .. note::
-   The definition of contexts is :ref:`extended <context-ext>` with additional fields for the purpose of proving :ref:`type soundness <soundness>`.
+   The definition of contexts needs to be :ref:`extended <context-ext>` with additional fields for the purpose of proving :ref:`type soundness <soundness>`.
 
 
 .. index:: ! type closure

specification/wasm-3.0/2.0-validation.contexts.spectec

@@ -21,9 +21,8 @@ var it : instrtype
 
 ;; Contexts
 
-syntax context hint(desc "context") hint(macro "%" "C%") =
+syntax context/syn hint(desc "context") hint(macro "%" "C%") =
   { TYPES deftype*          hint(desc "type"),
-    RECS subtype*           hint(desc "recursive type"),
     TAGS tagtype*           hint(desc "tag"),
     GLOBALS globaltype*     hint(desc "global"),
     MEMS memtype*           hint(desc "memory"),
@@ -34,9 +33,13 @@ syntax context hint(desc "context") hint(macro "%" "C%") =
     LOCALS localtype*       hint(desc "local"),
     LABELS resulttype*      hint(desc "label"),
     RETURN resulttype?      hint(desc "result"),
-    REFS funcidx*
+    REFS funcidx*           hint(desc "references"),
+    ...
   }
 
+syntax context/sem hint(macro "%" "C%") =
+  { ..., RECS subtype*      hint(desc "recursive type") }
+
 var C : context
 
 

specification/wasm-latest/2.0-validation.contexts.spectec

@@ -38,9 +38,7 @@ syntax context/syn hint(desc "context") hint(macro "%" "C%") =
   }
 
 syntax context/sem hint(macro "%" "C%") =
-  { ...,
-    RECS subtype*           hint(desc "recursive type")
-  }
+  { ..., RECS subtype*      hint(desc "recursive type") }
 
 var C : context