Add back lost text rule

WebAssembly · Nov 7, 2024 · d793168 · d793168
1 parent 0d9b985
commit d793168
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 5 deletions.
diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst
@@ -384,8 +384,8 @@ The *minimum* of two address types is defined as the address type whose :ref:`bi
 
 .. math::
    \begin{array}{llll}
-   \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_1 & (\iff |\X{at}_1| \leq |\X{at}_2|) \\
-   \atmin(\X{at}_1, \X{at}_2) &=& \X{at}_2 & (\otherwise) \\
+   \addrtypemin(\X{at}_1, \X{at}_2) &=& \X{at}_1 & (\iff |\X{at}_1| \leq |\X{at}_2|) \\
+   \addrtypemin(\X{at}_1, \X{at}_2) &=& \X{at}_2 & (\otherwise) \\
    \end{array}
 
 

diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst
@@ -304,6 +304,17 @@ A table's initialization :ref:`expression <text-expr>` can be omitted, in which
 
 An :ref:`element segment <text-elem>` can be given inline with a table definition, in which case its offset is :math:`0` and the :ref:`limits <text-limits>` of the :ref:`table type <text-tabletype>` are inferred from the length of the given segment:
 
+.. math::
+   \begin{array}{llclll}
+   \production{module field} &
+     \text{(}~\text{table}~~\Tid^?~~\Taddrtype^?~~\Treftype~~\text{(}~\text{elem}~~\expr^n{:}\Tvec(\Telemexpr)~\text{)}~\text{)} \quad\equiv \\ & \qquad
+       \text{(}~\text{table}~~\Tid'~~\Taddrtype^?~~n~~n~~\Treftype~\text{)} \\ & \qquad
+       \text{(}~\text{elem}~~\text{(}~\text{table}~~\Tid'~\text{)}~~\text{(}~\Taddrtype'\text{.const}~~\text{0}~\text{)}~~\Treftype~~\Tvec(\Telemexpr)~\text{)}
+       \\ & \qquad\qquad
+       (\iff \Tid^? \neq \epsilon \wedge \Tid' = \Tid^? \vee \Tid^? = \epsilon \wedge \Tid' \idfresh, \\ & \qquad\qquad
+        \iff \Taddrtype? \neq \epsilon \wedge \Taddrtype' = \Taddrtype^? \vee \Taddrtype^? = \epsilon \wedge \Taddrtype' = \text{i32}) \\
+   \end{array}
+
 .. math::
    \begin{array}{llclll}
    \production{module field} &

diff --git a/document/core/util/macros.def b/document/core/util/macros.def
@@ -301,6 +301,7 @@
 
 .. Types, meta functions
 
+.. |addrtypemin| mathdef:: \xref{syntax/types}{aux-addrtype-min}{\F{min}}
 .. |reftypediff| mathdef:: \xref{valid/conventions}{aux-reftypediff}{\setminus}
 
 .. |rollrt| mathdef:: \xref{valid/conventions}{aux-roll-rectype}{\F{roll}}
@@ -311,7 +312,6 @@
 .. |unrollht| mathdef:: \xref{appendix/properties}{aux-unroll-heaptype}{\F{unroll}}
 
 .. |unpacktype| mathdef:: \xref{syntax/types}{aux-unpacktype}{\F{unpack}}
-.. |atmin| mathdef:: \xref{syntax/types}{aux-addrtype-min}{\F{atmin}}
 
 .. |etfuncs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}}
 .. |ettables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}}

diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst
@@ -1510,7 +1510,7 @@ Table Instructions
      \qquad
      C \vdashreftypematch t_2 \matchesvaltype t_1
    }{
-     C \vdashinstr \TABLECOPY~x~y : [\X{at}_1~\X{at}_2~\atmin(\X{at}_1, \X{at}_2)] \to []
+     C \vdashinstr \TABLECOPY~x~y : [\X{at}_1~\X{at}_2~\addrtypemin(\X{at}_1, \X{at}_2)] \to []
    }
 
 
@@ -1898,7 +1898,7 @@ Memory Instructions
      \qquad
      C.\CMEMS[y] = \X{at}_y~\limits_y
    }{
-     C \vdashinstr \MEMORYCOPY~x~y : [\X{at}_x~\X{at}_y~\atmin(\X{at}_x, \X{at}_y)] \to []
+     C \vdashinstr \MEMORYCOPY~x~y : [\X{at}_x~\X{at}_y~\addrtypemin(\X{at}_x, \X{at}_y)] \to []
    }