Merge remote-tracking branch 'upstream/main' into HEAD

.github/workflows/ci-interpreter.yml

@@ -23,7 +23,7 @@ jobs:
         with:
           ocaml-compiler: 4.12.x
       - name: Setup OCaml tools
-        run: opam install --yes ocamlbuild.0.14.0 ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0
+        run: opam install --yes ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0
       - name: Setup Node.js
         uses: actions/setup-node@v2
         with:

document/core/appendix/embedding.rst

@@ -323,7 +323,7 @@ Tables
 
 .. _embed-table-alloc:
 
-:math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr, \reff)`
+:math:`\F{table\_alloc}(\store, \tabletype, \reff) : (\store, \tableaddr)`
 ..........................................................................
 
 1. Pre-condition: :math:`\tabletype` is :ref:`valid <valid-tabletype>`.

document/core/appendix/index-instructions.py

@@ -54,8 +54,7 @@ def RefWrap(s, kind):
 
 def Instruction(name, opcode, type=None, validation=None, execution=None, operator=None):
     if operator:
-        execution_str = ', '.join([RefWrap(execution, 'execution'),
-                                   RefWrap(operator, 'operator')])
+        execution_str = RefWrap(execution, 'execution') + ' (' + RefWrap(operator, 'operator') + ')'
     else:
         execution_str = RefWrap(execution, 'execution')
 
@@ -431,8 +430,8 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
     Instruction(r'\V128.\STORE\K{16\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{59}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
     Instruction(r'\V128.\STORE\K{32\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5A}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
     Instruction(r'\V128.\STORE\K{64\_lane}~\memarg~\laneidx', r'\hex{FD}~~\hex{5B}', r'[\I32~\V128] \to []', r'valid-store-lane', r'exec-store-lane'),
-    Instruction(r'\V128.\LOAD\K{32\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
-    Instruction(r'\V128.\LOAD\K{64\_zero}~\memarg~\laneidx', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
+    Instruction(r'\V128.\LOAD\K{32\_zero}~\memarg', r'\hex{FD}~~\hex{5C}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
+    Instruction(r'\V128.\LOAD\K{64\_zero}~\memarg', r'\hex{FD}~~\hex{5D}', r'[\I32] \to [\V128]', r'valid-load-zero', r'exec-load-zero'),
     Instruction(r'\F32X4.\VDEMOTE\K{\_f64x2\_zero}', r'\hex{FD}~~\hex{5E}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-demote'),
     Instruction(r'\F64X2.\VPROMOTE\K{\_low\_f32x4}', r'\hex{FD}~~\hex{5F}', r'[\V128] \to [\V128]', r'valid-vcvtop', r'exec-vcvtop', r'op-promote'),
     Instruction(r'\I8X16.\VABS', r'\hex{FD}~~\hex{60}', r'[\V128] \to [\V128]', r'valid-vunop', r'exec-vunop', r'op-iabs'),

document/core/appendix/properties.rst

@@ -278,8 +278,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 .. index:: element instance, reference
 .. _valid-eleminst:
 
-:ref:`Element Instances <syntax-eleminst>` :math:`\{ \EIELEM~\X{fa}^\ast \}`
-............................................................................
+:ref:`Element Instances <syntax-eleminst>` :math:`\{ \EITYPE~t, \EIELEM~\reff^\ast \}`
+......................................................................................
 
 * For each :ref:`reference <syntax-ref>` :math:`\reff_i` in the elements :math:`\reff^n`:
 
@@ -665,9 +665,9 @@ a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'
 
 * For each :ref:`global instance <syntax-globalinst>` :math:`\globalinst_i` in the original :math:`S.\SGLOBALS`, the new global instance must be an :ref:`extension <extend-globalinst>` of the old.
 
-* For each :ref:`element instance <syntax-eleminst>` :math:`\eleminst_i` in the original :math:`S.\SELEMS`, the new global instance must be an :ref:`extension <extend-eleminst>` of the old.
+* For each :ref:`element instance <syntax-eleminst>` :math:`\eleminst_i` in the original :math:`S.\SELEMS`, the new element instance must be an :ref:`extension <extend-eleminst>` of the old.
 
-* For each :ref:`data instance <syntax-datainst>` :math:`\datainst_i` in the original :math:`S.\SDATAS`, the new global instance must be an :ref:`extension <extend-datainst>` of the old.
+* For each :ref:`data instance <syntax-datainst>` :math:`\datainst_i` in the original :math:`S.\SDATAS`, the new data instance must be an :ref:`extension <extend-datainst>` of the old.
 
 .. math::
    \frac{

document/core/binary/conventions.rst

@@ -54,6 +54,7 @@ In order to distinguish symbols of the binary syntax from symbols of the abstrac
   (This is a shorthand for :math:`B^n` where :math:`n \leq 1`.)
 
 * :math:`x{:}B` denotes the same language as the nonterminal :math:`B`, but also binds the variable :math:`x` to the attribute synthesized for :math:`B`.
+  A pattern may also be used instead of a variable, e.g., :math:`7{:}B`.
 
 * Productions are written :math:`\B{sym} ::= B_1 \Rightarrow A_1 ~|~ \dots ~|~ B_n \Rightarrow A_n`, where each :math:`A_i` is the attribute that is synthesized for :math:`\B{sym}` in the given case, usually from attribute variables bound in :math:`B_i`.
 

document/core/binary/modules.rst

@@ -60,7 +60,7 @@ Each section consists of
 
 * a one-byte section *id*,
 * the |U32| *size* of the contents, in bytes,
-* the actual *contents*, whose structure is depended on the section id.
+* the actual *contents*, whose structure is dependent on the section id.
 
 Every section is optional; an omitted section is equivalent to the section being present with empty contents.