Skip to content

Commit 119d3b2

Browse files
rossbergrossberg
authored
[spec] Layout improvements (WebAssembly#1307)
1 parent c2ec899 commit 119d3b2

File tree

5 files changed

+87
-59
lines changed

5 files changed

+87
-59
lines changed

‎document/core/appendix/properties.rst‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -360,7 +360,8 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
360360

361361
* Let :math:`\globaltype^\ast` be the concatenation of all :math:`\globaltype_i` in order.
362362

363-
* Then the module instance is valid with :ref:`context <context>` :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CGLOBALS~\globaltype^\ast\}`.
363+
* | Then the module instance is valid with :ref:`context <context>`
364+
| :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CGLOBALS~\globaltype^\ast\}`.
364365
365366
.. math::
366367
~\\[-1ex]

‎document/core/binary/modules.rst‎

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -328,21 +328,29 @@ It decodes into a vector of :ref:`element segments <syntax-elem>` that represent
328328
\X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\
329329
\production{element segment} & \Belem &::=&
330330
\hex{00}~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx)
331-
&\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
331+
&\Rightarrow& \\&&&\quad
332+
\{ \ETYPE~\FUNCREF, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
332333
\hex{01}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
333-
&\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
334+
&\Rightarrow& \\&&&\quad
335+
\{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EPASSIVE \} \\ &&|&
334336
\hex{02}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
335-
&\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
337+
&\Rightarrow& \\&&&\quad
338+
\{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
336339
\hex{03}~~\X{et}:\Belemkind~~y^\ast{:}\Bvec(\Bfuncidx)
337-
&\Rightarrow& \{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
340+
&\Rightarrow& \\&&&\quad
341+
\{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
338342
\hex{04}~~e{:}\Bexpr~~\X{el}^\ast{:}\Bvec(\Bexpr)
339-
&\Rightarrow& \{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
343+
&\Rightarrow& \\&&&\quad
344+
\{ \ETYPE~\FUNCREF, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
340345
\hex{05}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
341-
&\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&
346+
&\Rightarrow& \\&&&\quad
347+
\{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EPASSIVE \} \\ &&|&
342348
\hex{06}~~x{:}\Btableidx~~e{:}\Bexpr~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
343-
&\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
349+
&\Rightarrow& \\&&&\quad
350+
\{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
344351
\hex{07}~~\X{et}:\Breftype~~\X{el}^\ast{:}\Bvec(\Bexpr)
345-
&\Rightarrow& \{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\
352+
&\Rightarrow& \\&&&\quad
353+
\{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\
346354
\production{element kind} & \Belemkind &::=&
347355
\hex{00} &\Rightarrow& \FUNCREF \\
348356
\end{array}

‎document/core/exec/instructions.rst‎

Lines changed: 38 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -607,7 +607,7 @@ Table Instructions
607607
\begin{array}[t]{@{}r@{~}l@{}}
608608
(\iff & F.\AMODULE.\MITABLES[x] = a \\
609609
\wedge & \X{sz} = |S.\STABLES[a].\TIELEM| \\
610-
\wedge & S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n, \val)) \\
610+
\wedge & S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n, \val)) \\[1ex]
611611
\end{array}
612612
\\[1ex]
613613
\begin{array}{lcl@{\qquad}l}
@@ -659,17 +659,17 @@ Table Instructions
659659

660660
a. Return.
661661

662-
13. Push the value :math:`\I32.CONST~i` to the stack.
662+
13. Push the value :math:`\I32.\CONST~i` to the stack.
663663

664664
14. Push the value :math:`\val` to the stack.
665665

666666
15. Execute the instruction :math:`\TABLESET~x`.
667667

668-
16. Push the value :math:`\I32.CONST~(i+1)` to the stack.
668+
16. Push the value :math:`\I32.\CONST~(i+1)` to the stack.
669669

670670
17. Push the value :math:`\val` to the stack.
671671

672-
18. Push the value :math:`\I32.CONST~(n-1)` to the stack.
672+
18. Push the value :math:`\I32.\CONST~(n-1)` to the stack.
673673

674674
19. Execute the instruction :math:`\TABLEFILL~x`.
675675

@@ -679,7 +679,7 @@ Table Instructions
679679
\quad\stepto\quad S; F; \TRAP
680680
\\ \qquad
681681
\begin{array}[t]{@{}r@{~}l@{}}
682-
(\iff & i + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\
682+
(\iff & i + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex]
683683
\end{array}
684684
\\[1ex]
685685
S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~0)~(\TABLEFILL~x)
@@ -688,7 +688,8 @@ Table Instructions
688688
(\otherwise)
689689
\\[1ex]
690690
S; F; (\I32.\CONST~i)~\val~(\I32.\CONST~n+1)~(\TABLEFILL~x)
691-
\quad\stepto\quad S; F;
691+
\quad\stepto
692+
\\ \qquad S; F;
692693
\begin{array}[t]{@{}l@{}}
693694
(\I32.\CONST~i)~\val~(\TABLESET~x) \\
694695
(\I32.\CONST~i+1)~\val~(\I32.\CONST~n)~(\TABLEFILL~x) \\
@@ -789,7 +790,7 @@ Table Instructions
789790
\\ \qquad
790791
\begin{array}[t]{@{}r@{~}l@{}}
791792
(\iff & s + n > |S.\STABLES[F.\AMODULE.\MITABLES[y]].\TIELEM| \\
792-
\vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\
793+
\vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex]
793794
\end{array}
794795
\\[1ex]
795796
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLECOPY~x~y)
@@ -798,7 +799,8 @@ Table Instructions
798799
(\otherwise)
799800
\\[1ex]
800801
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLECOPY~x~y)
801-
\quad\stepto\quad S; F;
802+
\quad\stepto
803+
\\ \qquad S; F;
802804
\begin{array}[t]{@{}l@{}}
803805
(\I32.\CONST~d)~(\I32.\CONST~s)~(\TABLEGET~y)~(\TABLESET~x) \\
804806
(\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\
@@ -807,7 +809,8 @@ Table Instructions
807809
(\otherwise, \iff d \leq s)
808810
\\[1ex]
809811
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLECOPY~x~y)
810-
\quad\stepto\quad S; F;
812+
\quad\stepto
813+
\\ \qquad S; F;
811814
\begin{array}[t]{@{}l@{}}
812815
(\I32.\CONST~d+n-1)~(\I32.\CONST~s+n-1)~(\TABLEGET~y)~(\TABLESET~x) \\
813816
(\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n)~(\TABLECOPY~x~y) \\
@@ -888,7 +891,7 @@ Table Instructions
888891
\\ \qquad
889892
\begin{array}[t]{@{}r@{~}l@{}}
890893
(\iff & s + n > |S.\SELEMS[F.\AMODULE.\MIELEMS[y]].\EIELEM| \\
891-
\vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\
894+
\vee & d + n > |S.\STABLES[F.\AMODULE.\MITABLES[x]].\TIELEM|) \\[1ex]
892895
\end{array}
893896
\\[1ex]
894897
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\TABLEINIT~x~y)
@@ -897,7 +900,8 @@ Table Instructions
897900
(\otherwise)
898901
\\[1ex]
899902
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\TABLEINIT~x~y)
900-
\quad\stepto\quad S; F;
903+
\quad\stepto
904+
\\ \qquad S; F;
901905
\begin{array}[t]{@{}l@{}}
902906
(\I32.\CONST~d)~\val~(\TABLESET~x) \\
903907
(\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\TABLEINIT~x~y) \\
@@ -1004,7 +1008,7 @@ Memory Instructions
10041008
\begin{array}[t]{@{}r@{~}l@{}}
10051009
(\iff & \X{ea} = i + \memarg.\OFFSET \\
10061010
\wedge & \X{ea} + |t|/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\
1007-
\wedge & \bytes_t(c) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice |t|/8])
1011+
\wedge & \bytes_t(c) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice |t|/8]) \\[1ex]
10081012
\end{array}
10091013
\\[1ex]
10101014
\begin{array}{lcl@{\qquad}l}
@@ -1015,7 +1019,7 @@ Memory Instructions
10151019
\begin{array}[t]{@{}r@{~}l@{}}
10161020
(\iff & \X{ea} = i + \memarg.\OFFSET \\
10171021
\wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\
1018-
\wedge & \bytes_{\iN}(n) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8])
1022+
\wedge & \bytes_{\iN}(n) = S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8]) \\[1ex]
10191023
\end{array}
10201024
\\[1ex]
10211025
\begin{array}{lcl@{\qquad}l}
@@ -1082,7 +1086,7 @@ Memory Instructions
10821086
\begin{array}[t]{@{}r@{~}l@{}}
10831087
(\iff & \X{ea} = i + \memarg.\OFFSET \\
10841088
\wedge & \X{ea} + |t|/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\
1085-
\wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice |t|/8] = \bytes_t(c))
1089+
\wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice |t|/8] = \bytes_t(c)) \\[1ex]
10861090
\end{array}
10871091
\\[1ex]
10881092
\begin{array}{lcl@{\qquad}l}
@@ -1092,7 +1096,7 @@ Memory Instructions
10921096
\begin{array}[t]{@{}r@{~}l@{}}
10931097
(\iff & \X{ea} = i + \memarg.\OFFSET \\
10941098
\wedge & \X{ea} + N/8 \leq |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\
1095-
\wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\wrap_{|t|,N}(c))
1099+
\wedge & S' = S \with \SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA[\X{ea} \slice N/8] = \bytes_{\iN}(\wrap_{|t|,N}(c)) \\[1ex]
10961100
\end{array}
10971101
\\[1ex]
10981102
\begin{array}{lcl@{\qquad}l}
@@ -1173,7 +1177,7 @@ Memory Instructions
11731177
\begin{array}[t]{@{}r@{~}l@{}}
11741178
(\iff & F.\AMODULE.\MIMEMS[0] = a \\
11751179
\wedge & \X{sz} = |S.\SMEMS[a].\MIDATA|/64\,\F{Ki} \\
1176-
\wedge & S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\
1180+
\wedge & S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\[1ex]
11771181
\end{array}
11781182
\\[1ex]
11791183
\begin{array}{lcl@{\qquad}l}
@@ -1247,15 +1251,16 @@ Memory Instructions
12471251
S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n)~\MEMORYFILL
12481252
\quad\stepto\quad S; F; \TRAP
12491253
\\ \qquad
1250-
(\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\
1254+
(\iff d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|)
12511255
\\[1ex]
12521256
S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~0)~\MEMORYFILL
12531257
\quad\stepto\quad S; F; \epsilon
12541258
\\ \qquad
12551259
(\otherwise)
12561260
\\[1ex]
12571261
S; F; (\I32.\CONST~d)~\val~(\I32.\CONST~n+1)~\MEMORYFILL
1258-
\quad\stepto\quad S; F;
1262+
\quad\stepto
1263+
\\ \qquad S; F;
12591264
\begin{array}[t]{@{}l@{}}
12601265
(\I32.\CONST~d)~\val~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\
12611266
(\I32.\CONST~d+1)~\val~(\I32.\CONST~n)~\MEMORYFILL \\
@@ -1348,7 +1353,7 @@ Memory Instructions
13481353
\\ \qquad
13491354
\begin{array}[t]{@{}r@{~}l@{}}
13501355
(\iff & s + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| \\
1351-
\vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|) \\
1356+
\vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA|) \\[1ex]
13521357
\end{array}
13531358
\\[1ex]
13541359
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~\MEMORYCOPY
@@ -1357,7 +1362,8 @@ Memory Instructions
13571362
(\otherwise)
13581363
\\[1ex]
13591364
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\MEMORYCOPY
1360-
\quad\stepto\quad S; F;
1365+
\quad\stepto
1366+
\\ \qquad S; F;
13611367
\begin{array}[t]{@{}l@{}}
13621368
(\I32.\CONST~d) \\
13631369
(\I32.\CONST~s)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\
@@ -1368,7 +1374,8 @@ Memory Instructions
13681374
(\otherwise, \iff d \leq s)
13691375
\\[1ex]
13701376
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~\MEMORYCOPY
1371-
\quad\stepto\quad S; F;
1377+
\quad\stepto
1378+
\\ \qquad S; F;
13721379
\begin{array}[t]{@{}l@{}}
13731380
(\I32.\CONST~d+n-1) \\
13741381
(\I32.\CONST~s+n-1)~(\I32\K{.}\LOAD\K{8\_u}~\{ \OFFSET~0, \ALIGN~0 \}) \\
@@ -1451,7 +1458,7 @@ Memory Instructions
14511458
\\ \qquad
14521459
\begin{array}[t]{@{}r@{~}l@{}}
14531460
(\iff & s + n > |S.\SDATAS[F.\AMODULE.\MIDATAS[x]].\DIDATA| \\
1454-
\vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\
1461+
\vee & d + n > |S.\SMEMS[F.\AMODULE.\MIMEMS[x]].\MIDATA|) \\[1ex]
14551462
\end{array}
14561463
\\[1ex]
14571464
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~0)~(\MEMORYINIT~x)
@@ -1460,7 +1467,8 @@ Memory Instructions
14601467
(\otherwise)
14611468
\\[1ex]
14621469
S; F; (\I32.\CONST~d)~(\I32.\CONST~s)~(\I32.\CONST~n+1)~(\MEMORYINIT~x)
1463-
\quad\stepto\quad S; F;
1470+
\quad\stepto
1471+
\\ \qquad S; F;
14641472
\begin{array}[t]{@{}l@{}}
14651473
(\I32.\CONST~d)~(\I32.\CONST~b)~(\I32\K{.}\STORE\K{8}~\{ \OFFSET~0, \ALIGN~0 \}) \\
14661474
(\I32.\CONST~d+1)~(\I32.\CONST~s+1)~(\I32.\CONST~n)~(\MEMORYINIT~x) \\
@@ -1550,10 +1558,10 @@ Control Instructions
15501558

15511559
.. math::
15521560
~\\[-1ex]
1553-
\begin{array}{lcl@{\qquad}l}
1561+
\begin{array}{lcl}
15541562
F; \val^m~\BLOCK~\X{bt}~\instr^\ast~\END &\stepto&
15551563
F; \LABEL_n\{\epsilon\}~\val^m~\instr^\ast~\END
1556-
& (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n])
1564+
\\&&\quad (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n])
15571565
\end{array}
15581566
15591567
@@ -1576,10 +1584,10 @@ Control Instructions
15761584

15771585
.. math::
15781586
~\\[-1ex]
1579-
\begin{array}{lcl@{\qquad}l}
1587+
\begin{array}{lcl}
15801588
F; \val^m~\LOOP~\X{bt}~\instr^\ast~\END &\stepto&
15811589
F; \LABEL_m\{\LOOP~\X{bt}~\instr^\ast~\END\}~\val^m~\instr^\ast~\END
1582-
& (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n])
1590+
\\&&\quad (\iff \expand_F(\X{bt}) = [t_1^m] \to [t_2^n])
15831591
\end{array}
15841592
15851593
@@ -1612,13 +1620,13 @@ Control Instructions
16121620

16131621
.. math::
16141622
~\\[-1ex]
1615-
\begin{array}{lcl@{\qquad}l}
1623+
\begin{array}{lcl}
16161624
F; \val^m~(\I32.\CONST~c)~\IF~\X{bt}~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto&
16171625
F; \LABEL_n\{\epsilon\}~\val^m~\instr_1^\ast~\END
1618-
& (\iff c \neq 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\
1626+
\\&&\quad (\iff c \neq 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\
16191627
F; \val^m~(\I32.\CONST~c)~\IF~\X{bt}~\instr_1^\ast~\ELSE~\instr_2^\ast~\END &\stepto&
16201628
F; \LABEL_n\{\epsilon\}~\val^m~\instr_2^\ast~\END
1621-
& (\iff c = 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\
1629+
\\&&\quad (\iff c = 0 \wedge \expand_F(\X{bt}) = [t_1^m] \to [t_2^n]) \\
16221630
\end{array}
16231631
16241632

‎document/core/exec/modules.rst‎

Lines changed: 27 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -516,7 +516,13 @@ and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element
516516
where:
517517

518518
.. math::
519-
\begin{array}{rlll}
519+
\begin{array}{@{}rlll@{}}
520+
\table^\ast &=& \module.\MTABLES \\
521+
\mem^\ast &=& \module.\MMEMS \\
522+
\global^\ast &=& \module.\MGLOBALS \\
523+
\elem^\ast &=& \module.\MELEMS \\
524+
\data^\ast &=& \module.\MDATAS \\
525+
\export^\ast &=& \module.\MEXPORTS \\[1ex]
520526
\moduleinst &=& \{~
521527
\begin{array}[t]{@{}l@{}}
522528
\MITYPES~\module.\MTYPES, \\
@@ -528,28 +534,29 @@ where:
528534
\MIDATAS~\dataaddr^\ast, \\
529535
\MIEXPORTS~\exportinst^\ast ~\}
530536
\end{array} \\[1ex]
531-
S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\
532-
S_2, \tableaddr^\ast &=& \alloctable^\ast(S_1, (\table.\TTYPE)^\ast, \REFNULL~t)
533-
\qquad\qquad\qquad~ (\where \table^\ast = \module.\MTABLES \\ &&
534-
\qquad\qquad\qquad~~ \wedge (\table.\TTYPE)^\ast = (\limits~t)^\ast) \\
535-
S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast)
536-
\qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\
537-
S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast)
538-
\qquad\quad~ (\where \global^\ast = \module.\MGLOBALS) \\
539-
S_5, \elemaddr^\ast &=& \allocelem^\ast(S_4, (\elem.\ETYPE)^\ast, (\reff^\ast)^\ast) \\
540-
\qquad\quad~ (\where \elem^\ast = \module.\MELEMS) \\
541-
S', \dataaddr^\ast &=& \allocdata^\ast(S_5, (\data.\DINIT)^\ast)
542-
\qquad\qquad\qquad~ (\where \data^\ast = \module.\MDATAS) \\
543-
\exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast
544-
\quad (\where \export^\ast = \module.\MEXPORTS) \\[1ex]
537+
S_1, \funcaddr^\ast &=&
538+
\allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\
539+
S_2, \tableaddr^\ast &=&
540+
\alloctable^\ast(S_1, (\table.\TTYPE)^\ast, (\REFNULL~t)^\ast)
541+
\quad (\where (\table.\TTYPE)^\ast = (\limits~t)^\ast) \\
542+
S_3, \memaddr^\ast &=&
543+
\allocmem^\ast(S_2, (\mem.\MTYPE)^\ast) \\
544+
S_4, \globaladdr^\ast &=&
545+
\allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast) \\
546+
S_5, \elemaddr^\ast &=&
547+
\allocelem^\ast(S_4, (\elem.\ETYPE)^\ast, (\reff^\ast)^\ast) \\
548+
S', \dataaddr^\ast &=&
549+
\allocdata^\ast(S_5, (\data.\DINIT)^\ast) \\
550+
\exportinst^\ast &=&
551+
\{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \\[1ex]
545552
\evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast
546-
\qquad~ (\where x^\ast = \edfuncs(\module.\MEXPORTS)) \\
553+
\qquad~ (\where x^\ast = \edfuncs(\export^\ast)) \\
547554
\evtables(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MITABLES[x])^\ast
548-
\qquad (\where x^\ast = \edtables(\module.\MEXPORTS)) \\
555+
\qquad (\where x^\ast = \edtables(\export^\ast)) \\
549556
\evmems(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIMEMS[x])^\ast
550-
\qquad (\where x^\ast = \edmems(\module.\MEXPORTS)) \\
557+
\qquad (\where x^\ast = \edmems(\export^\ast)) \\
551558
\evglobals(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast
552-
\qquad\!\!\! (\where x^\ast = \edglobals(\module.\MEXPORTS)) \\
559+
\qquad\!\!\! (\where x^\ast = \edglobals(\export^\ast)) \\
553560
\end{array}
554561
555562
.. scratch
@@ -571,7 +578,7 @@ Here, the notation :math:`\F{allocx}^\ast` is shorthand for multiple :ref:`alloc
571578
S_{i+1}, a^n[i] &=& \F{allocx}(S_i, X^n[i], \dots)
572579
\end{array}
573580
574-
Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals), then the elements of this sequence are passed to the allocation function pointwise.
581+
Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals or tables), then the elements of this sequence are passed to the allocation function pointwise.
575582

576583
.. note::
577584
The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance :math:`\moduleinst` is passed to the function allocator as an argument, in order to form the necessary closures.

‎document/core/static/custom.css‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,10 @@ div.admonition p.admonition-title {
4141
font-weight: bold;
4242
}
4343

44+
div.math {
45+
background-color: #F0F0F0;
46+
padding: 3px 0 3px 0;
47+
}
4448

4549
div.relations {
4650
display: block;

0 commit comments

Comments
 (0)