fix exportimport descriptor

Author: Guy Bedford

document/core/appendix/embedding.rst

@@ -263,7 +263,7 @@ Modules
 
 4. For each :math:`\export_i` in :math:`\export^\ast` and corresponding :math:`\externtype'_i` in :math:`{\externtype'}^\ast`, do:
 
-  a. Let :math:`\import_j = \exportimport(\module, \export_i.\EDESC)`.
+  a. Let :math:`\import_j = \edexportimport(\module, \export_i.\EDESC)`.
 
   b. If :math:`\import_j = \epsilon`, then append the pair :math:`(\export_i.\ENAME, \externtype'_i)` to :math:`\X{result}`.
 
@@ -274,7 +274,7 @@ Modules
    \begin{array}{lclll}
    \F{module\_direct\_exports}(m) &=& (\X{ex}.\ENAME, \externtype')^\ast \\
      && \qquad (\iff \X{ex}^\ast = m.\MEXPORTS \\
-     && \qquad\quad \wedge~\exportimport(m, \X{ex}.\EDESC) = \epsilon \\
+     && \qquad\quad \wedge~\edexportimport(m, \X{ex}.\EDESC) = \epsilon \\
      && \qquad\quad \wedge~\vdashmodule m : \externtype^\ast \to {\externtype'}^\ast \\
      && \qquad\quad \wedge~\externtype' = \X{ex}.\EDESC) \\
    \end{array}
@@ -296,7 +296,7 @@ Modules
 
 5. For each :math:`\export_i` in :math:`\export^\ast`, do:
 
-  a. Let :math:`\import_j = \exportimport(\module, \export_i.\EDESC)`.
+  a. Let :math:`\import_j = \edexportimport(\module, \export_i.\EDESC)`.
 
   b. If :math:`\import_j \neq \epsilon`, then:
 
@@ -309,7 +309,7 @@ Modules
    \begin{array}{lclll}
    \F{module\_indirect\_exports}(m) &=& (\X{ex}.\ENAME, \X{im}.\IMODULE, \X{im}.\INAME)^\ast \\
      && \qquad (\iff \X{ex}^\ast = m.\MEXPORTS \\
-     && \qquad\quad \wedge~\X{im} = \exportimport(m, \X{ex}.\EDESC) \\
+     && \qquad\quad \wedge~\X{im} = \edexportimport(m, \X{ex}.\EDESC) \\
      && \qquad\quad \wedge~\X{im} \neq \epsilon \\
      && \qquad\quad \wedge~\vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\
    \end{array}

document/core/syntax/modules.rst

@@ -360,19 +360,23 @@ A *direct export* is one where the export references a function, table, memory,
 
 An *indirect export* (or *re-export*) is one where the export references a function, table, memory, or global that the module imports.
 
-For an export :math:`\export` in module :math:`m`, the export is direct when :math:`\exportimport(m, \export.\EDESC) = \epsilon` and indirect otherwise, where
-the import corresponding to an export description is defined by:
+For an export :math:`\export` in module :math:`m`, the export is direct when :math:`\edexportimport(m, \export.\EDESC) = \epsilon` and indirect otherwise, where
+the import corresponding to an export descriptor is defined by:
 
 .. math::
    \begin{array}{lclll}
    \F{exportimport}(m, \exportdesc) &=& m.\MIMPORTS[i] && (\iff \exportdesc = \EDFUNC~\funcidx \\
-     &&&& \quad \wedge~\exists~i~\colon \ m.\MIMPORTS[i].\IDESC = \IDFUNC~\typeidx \\
+     &&&& \quad \wedge~\exists~i~\colon~\funcidx = |\{j ~|~ j < i \\
+     &&&& \quad \quad \wedge~m.\MIMPORTS[j].\IDESC = \IDFUNC~\typeidx' \}|) \\
    \F{exportimport}(m, \exportdesc) &=& m.\MIMPORTS[i] && (\iff \exportdesc = \EDTABLE~\tableidx \\
-     &&&& \quad \wedge~\exists~i~\colon \ m.\MIMPORTS[i].\IDESC = \IDTABLE~\tabletype \\
+     &&&& \quad \wedge~\exists~i~\colon~\tableidx = |\{j ~|~ j < i \\
+     &&&& \quad \quad \wedge~m.\MIMPORTS[j].\IDESC = \IDTABLE~\tabletype' \}|) \\
    \F{exportimport}(m, \exportdesc) &=& m.\MIMPORTS[i] && (\iff \exportdesc = \EDMEM~\memidx \\
-     &&&& \quad \wedge~\exists~i~\colon \ m.\MIMPORTS[i].\IDESC = \IDMEM~\memtype \\
+     &&&& \quad \wedge~\exists~i~\colon~\memidx = |\{j ~|~ j < i \\
+     &&&& \quad \quad \wedge~m.\MIMPORTS[j].\IDESC = \IDMEM~\memtype' \}|) \\
    \F{exportimport}(m, \exportdesc) &=& m.\MIMPORTS[i] && (\iff \exportdesc = \EDGLOBAL~\globalidx \\
-     &&&& \quad \wedge~\exists~i~\colon \ m.\MIMPORTS[i].\IDESC = \IDGLOBAL~\globaltype \\
+     &&&& \quad \wedge~\exists~i~\colon~\globalidx = |\{j ~|~ j < i \\
+     &&&& \quad \quad \wedge~m.\MIMPORTS[j].\IDESC = \IDGLOBAL~\globaltype' \}|) \\
    \F{exportimport}(m, \exportdesc) &=& \epsilon && (\otherwise) \\
    \end{array}
 

document/core/util/macros.def

@@ -346,7 +346,7 @@
 .. |edtables| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{tables}}
 .. |edmems| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{mems}}
 .. |edglobals| mathdef:: \xref{syntax/modules}{syntax-exportdesc}{\F{globals}}
-.. |exportimport| mathdef:: \xref{syntax/modules}{syntax-export}{\F{import\_for\_export}}
+.. |edexportimport| mathdef:: \xref{syntax/modules}{syntax-export}{\F{exportimport}}
 
 
 .. Instructions, terminals