rework definitions

Author: Guy Bedford

document/core/appendix/embedding.rst

@@ -163,11 +163,11 @@ Modules
 
 .. math::
    \begin{array}{lclll}
-   \F{module\_extern\_subtype}(\externtype_1, \externtype_2) &=& \TRUE && (\iff \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2) \\
+   \F{module\_extern\_subtype}(\externtype_1, \externtype_2) &\iff& \vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2 \\
    \end{array}
 
 .. note::
-   This function encapsulates the external type matching relation defined in the core specification. It allows for checking compatibility of external types when linking modules or validating imports against exports. The current implementation uses the exact matching rules from the core specification, but this function provides a single point for potential future extensions to the type system.
+   This function encapsulates the external type matching relation defined in the :ref:`Import Subtyping <match>` of the validation section, where the :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2` judgment establishes compatibility between external types. This allows for explicit checking of type compatibility when linking modules or validating imports against exports.
 
 .. index:: instantiation, module instance
 .. _embed-module-instantiate:
@@ -263,16 +263,20 @@ Modules
 
 4. For each :math:`\export_i` in :math:`\export^\ast` and corresponding :math:`\externtype'_i` in :math:`{\externtype'}^\ast`, do:
 
-   a. If :math:`\isdirectexport(\module, \export_i.\EDESC)`, then append the pair :math:`(\export_i.\ENAME, \externtype'_i)` to :math:`\X{result}`.
+  a. Let :math:`\import_j = \exportimport(\module, \export_i.\EDESC)`.
+
+  b. If :math:`\import_j = \epsilon`, then append the pair :math:`(\export_i.\ENAME, \externtype'_i)` to :math:`\X{result}`.
 
 5. Return :math:`\X{result}`.
 
 .. math::
    ~ \\
    \begin{array}{lclll}
    \F{module\_direct\_exports}(m) &=& (\X{ex}.\ENAME, \externtype')^\ast \\
-   && \qquad (\iff \X{ex} \in m.\MEXPORTS \wedge \externtype' \in {\externtype'}^\ast \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast \\
-   && \qquad\quad \wedge \isdirectexport(m, \X{ex}.\EDESC)) \\
+     && \qquad (\iff \X{ex}^\ast = m.\MEXPORTS \\
+     && \qquad\quad \wedge~\exportimport(m, \X{ex}.\EDESC) = \epsilon \\
+     && \qquad\quad \wedge~\vdashmodule m : \externtype^\ast \to {\externtype'}^\ast \\
+     && \qquad\quad \wedge~\externtype' = \X{ex}.\EDESC) \\
    \end{array}
 
 
@@ -292,20 +296,22 @@ Modules
 
 5. For each :math:`\export_i` in :math:`\export^\ast`, do:
 
-   a. If :math:`\isindirectexport(\module, \export_i.\EDESC)`, then:
+  a. Let :math:`\import_j = \exportimport(\module, \export_i.\EDESC)`.
 
-      i. Let :math:`\import_j` be the import corresponding to the index in :math:`\export_i.\EDESC`.
+  b. If :math:`\import_j \neq \epsilon`, then:
 
-      ii. Append the triple :math:`(\export_i.\ENAME, \import_j.\IMODULE, \import_j.\INAME)` to :math:`\X{result}`.
+     i. Append the triple :math:`(\export_i.\ENAME, \import_j.\IMODULE, \import_j.\INAME)` to :math:`\X{result}`.
 
 6. Return :math:`\X{result}`.
 
 .. math::
    ~ \\
    \begin{array}{lclll}
    \F{module\_indirect\_exports}(m) &=& (\X{ex}.\ENAME, \X{im}.\IMODULE, \X{im}.\INAME)^\ast \\
-   && \qquad (\iff \X{ex} \in m.\MEXPORTS \wedge \X{im} \in m.\MIMPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast \\
-   && \qquad\quad \wedge \isindirectexport(m, \X{ex}.\EDESC) \wedge \X{im} = \importforexport(m, \X{ex}.\EDESC)) \\
+     && \qquad (\iff \X{ex}^\ast = m.\MEXPORTS \\
+     && \qquad\quad \wedge~\X{im} = \exportimport(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

@@ -356,32 +356,26 @@ Each export is labeled by a unique :ref:`name <syntax-name>`.
 Exportable definitions are :ref:`functions <syntax-func>`, :ref:`tables <syntax-table>`, :ref:`memories <syntax-mem>`, and :ref:`globals <syntax-global>`,
 which are referenced through a respective descriptor.
 
-A *direct export* is one where the export references a function, table, memory, or global instance that is defined within the module itself rather than being imported.
+A *direct export* is one where the export references a function, table, memory, or global instance that is defined within the module itself rather than being imported. 
 
 An *indirect export* (or *re-export*) is one where the export references a function, table, memory, or global that the module imports.
 
-The import corresponding to an export description is given by:
+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:
 
 .. math::
-   \begin{array}{lllll}
-   \production{import for export} & \importforexport(m, \exportdesc) &=&
-     \begin{cases}
-       m.\MIMPORTS[\X{idx}] & (\iff \exportdesc = \EDFUNC~\X{idx} \wedge \X{idx} < |\etfuncs(m.\MIMPORTS)|) \\
-       m.\MIMPORTS[\X{fidx} + \X{idx}] & (\iff \exportdesc = \EDTABLE~\X{idx} \wedge \X{idx} < |\ettables(m.\MIMPORTS)| \\
-       & \quad \wedge \X{fidx} = |\etfuncs(m.\MIMPORTS)|) \\
-       m.\MIMPORTS[\X{fidx} + \X{tidx} + \X{idx}] & (\iff \exportdesc = \EDMEM~\X{idx} \wedge \X{idx} < |\etmems(m.\MIMPORTS)| \\
-       & \quad \wedge \X{fidx} = |\etfuncs(m.\MIMPORTS)| \wedge \X{tidx} = |\ettables(m.\MIMPORTS)|) \\
-       m.\MIMPORTS[\X{fidx} + \X{tidx} + \X{midx} + \X{idx}] & (\iff \exportdesc = \EDGLOBAL~\X{idx} \wedge \X{idx} < |\etglobals(m.\MIMPORTS)| \\
-       & \quad \wedge \X{fidx} = |\etfuncs(m.\MIMPORTS)| \wedge \X{tidx} = |\ettables(m.\MIMPORTS)| \\
-       & \quad \wedge \X{midx} = |\etmems(m.\MIMPORTS)|) \\
-       \epsilon & (\otherwise) \\
-     \end{cases} \\
+   \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 \\
+   \F{exportimport}(m, \exportdesc) &=& m.\MIMPORTS[i] && (\iff \exportdesc = \EDTABLE~\tableidx \\
+     &&&& \quad \wedge~\exists~i~\colon \ m.\MIMPORTS[i].\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 \\
+   \F{exportimport}(m, \exportdesc) &=& m.\MIMPORTS[i] && (\iff \exportdesc = \EDGLOBAL~\globalidx \\
+     &&&& \quad \wedge~\exists~i~\colon \ m.\MIMPORTS[i].\IDESC = \IDGLOBAL~\globaltype \\
+   \F{exportimport}(m, \exportdesc) &=& \epsilon && (\otherwise) \\
    \end{array}
 
-For embedder convenience, we also define:
-
-* :math:`\isdirectexport(m, \exportdesc) = (\importforexport(m, \exportdesc) = \epsilon)`
-* :math:`\isindirectexport(m, \exportdesc) = (\importforexport(m, \exportdesc) \neq \epsilon)`
 
 Conventions
 ...........

document/core/util/macros.def

@@ -346,9 +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}}
-.. |importforexport| mathdef:: \xref{syntax/modules}{syntax-export}{\F{import\_for\_export}}
-.. |isdirectexport| mathdef:: \xref{syntax/modules}{syntax-export}{\F{is\_direct\_export}}
-.. |isindirectexport| mathdef:: \xref{syntax/modules}{syntax-export}{\F{is\_indirect\_export}}
+.. |exportimport| mathdef:: \xref{syntax/modules}{syntax-export}{\F{import\_for\_export}}
 
 
 .. Instructions, terminals