Skip to content

Commit

Permalink
Module syntax section
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed May 23, 2024
1 parent b9b4c13 commit 93ca858
Show file tree
Hide file tree
Showing 33 changed files with 2,339 additions and 2,037 deletions.
4 changes: 2 additions & 2 deletions document/core/binary/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -353,7 +353,7 @@ It decodes into a list of :ref:`element segments <syntax-elem>` that represent t
\{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
3{:}\Bu32~~\X{et}:\Belemkind~~y^\ast{:}\Blist(\Bfuncidx)
&\Rightarrow& \\&&&\quad
\{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARATIVE \} \\ &&|&
\{ \ETYPE~\X{et}, \EINIT~((\REFFUNC~y)~\END)^\ast, \EMODE~\EDECLARE \} \\ &&|&
4{:}\Bu32~~e{:}\Bexpr~~\X{el}^\ast{:}\Blist(\Bexpr)
&\Rightarrow& \\&&&\quad
\{ \ETYPE~(\REF~\NULL~\FUNC), \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~0, \EOFFSET~e \} \} \\ &&|&
Expand All @@ -365,7 +365,7 @@ It decodes into a list of :ref:`element segments <syntax-elem>` that represent t
\{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EACTIVE~\{ \ETABLE~x, \EOFFSET~e \} \} \\ &&|&
7{:}\Bu32~~\X{et}:\Breftype~~\X{el}^\ast{:}\Blist(\Bexpr)
&\Rightarrow& \\&&&\quad
\{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARATIVE \} \\
\{ \ETYPE~et, \EINIT~\X{el}^\ast, \EMODE~\EDECLARE \} \\
\production{element kind} & \Belemkind &::=&
\hex{00} &\Rightarrow& (\REF~\FUNC) \\
\end{array}
Expand Down
12 changes: 6 additions & 6 deletions document/core/exec/modules.rst
Original file line number Diff line number Diff line change
Expand Up @@ -420,13 +420,13 @@ where:
\exportinst^\ast &=&
\{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \\[1ex]
\funcsxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast
\qquad~ (\where x^\ast = \funcsed(\export^\ast)) \\
\qquad~ (\where x^\ast = \funcsxx(\export^\ast)) \\
\tablesxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MITABLES[x])^\ast
\qquad (\where x^\ast = \tablesed(\export^\ast)) \\
\qquad (\where x^\ast = \tablesxx(\export^\ast)) \\
\memsxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIMEMS[x])^\ast
\qquad (\where x^\ast = \memsed(\export^\ast)) \\
\qquad (\where x^\ast = \memsxx(\export^\ast)) \\
\globalsxv(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIGLOBALS[x])^\ast
\qquad\!\!\! (\where x^\ast = \globalsed(\export^\ast)) \\
\qquad\!\!\! (\where x^\ast = \globalsxx(\export^\ast)) \\
\end{array}
.. scratch
Expand Down Expand Up @@ -571,7 +571,7 @@ It is up to the :ref:`embedder <embedder>` to define how such conditions are rep

f. :ref:`Execute <exec-elem.drop>` the instruction :math:`\ELEMDROP~i`.

13. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EDECLARATIVE`, do:
13. For each :ref:`element segment <syntax-elem>` :math:`\elem_i` in :math:`\module.\MELEMS` whose :ref:`mode <syntax-elemmode>` is of the form :math:`\EDECLARE`, do:

a. :ref:`Execute <exec-elem.drop>` the instruction :math:`\ELEMDROP~i`.

Expand Down Expand Up @@ -636,7 +636,7 @@ where:
\F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\expr^n, \EMODE~\EPASSIVE\}) \quad=\quad \epsilon \\
\F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\expr^n, \EMODE~\EACTIVE \{\ETABLE~x, \EOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad
\instr^\ast~(\I32.\CONST~0)~(\I32.\CONST~n)~(\TABLEINIT~x~i)~(\ELEMDROP~i) \\
\F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\expr^n, \EMODE~\EDECLARATIVE\}) \quad=\\ \qquad
\F{runelem}_i(\{\ETYPE~\X{et}, \EINIT~\expr^n, \EMODE~\EDECLARE\}) \quad=\\ \qquad
(\ELEMDROP~i) \\[1ex]
\F{rundata}_i(\{\DINIT~b^n, \DMODE~\DPASSIVE\}) \quad=\\ \qquad \epsilon \\
\F{rundata}_i(\{\DINIT~b^n, \DMODE~\DACTIVE \{\DMEM~0, \DOFFSET~\instr^\ast~\END\}\}) \quad=\\ \qquad
Expand Down
8 changes: 4 additions & 4 deletions document/core/intro/overview.rst
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ This language is structured around the following concepts.
WebAssembly provides only four basic *number types*.
These are integers and |IEEE754|_ numbers,
each in 32 and 64 bit width.
32 bit integers also serve as Booleans and as memory addresses.
32-bit integers also serve as Booleans and as memory addresses.
The usual operations on these types are available,
including the full matrix of conversions between them.
There is no distinction between signed and unsigned integer types.
Expand All @@ -25,10 +25,10 @@ This language is structured around the following concepts.

In addition to these basic number types, there is a single 128 bit wide
vector type representing different types of packed data.
The supported representations are 4 32-bit, or 2 64-bit
The supported representations are four 32-bit, or two 64-bit
|IEEE754|_ numbers, or different widths of packed integer values,
specifically 2 64-bit integers, 4 32-bit integers, 8
16-bit integers, or 16 8-bit integers.
specifically two 64-bit integers, four 32-bit integers, eight
16-bit integers, or sixteen 8-bit integers.

Finally, values can consist of opaque *references* that represent pointers towards different sorts of entities.
Unlike with other types, their size or representation is not observable.
Expand Down
30 changes: 12 additions & 18 deletions document/core/syntax/conventions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ When dealing with syntactic constructs the following notation is also used:

* ${:s[i : n]} denotes the sub-sequence ${:s[i]...s[i+n-1]} of a sequence ${:s}.

* ${-:s[[i]=A]} denotes the same sequence as ${:s},
* ${:s[[i]=A]} denotes the same sequence as ${:s},
except that the ${:i}-th element is replaced with ${-:A}.

* ${:s[[i : n] = A^n]} denotes the same sequence as ${:s},
Expand All @@ -88,41 +88,35 @@ Moreover, the following conventions are employed:
This implicitly expresses a form of mapping syntactic constructions over a sequence.


Productions of the following form are interpreted as *records* that map a fixed set of fields ${-:FIELD_ i} to "values" ${:A_i}, respectively:
Productions of the following form are interpreted as *records* that map a fixed set of fields ${:FIELD_ i} to "values" ${:A_i}, respectively:

$${syntax-: record}
${syntax-ignore: recorddots}

The following notation is adopted for manipulating such records:

* ${-:r.FIELD} denotes the contents of the ${-:FIELD} component of ${:r}.
* ${:r.FIELD} denotes the contents of the ${:FIELD} component of ${:r}.

* ${-:r[.FIELD = A]} denotes the same record as ${:r},
except that the contents of the ${-:FIELD} component is replaced with ${:A}.
* ${:r[.FIELD = A]} denotes the same record as ${:r},
except that the contents of the ${:FIELD} component is replaced with ${:A}.

* ${-:r[.FIELD =.. A^n]} denotes the same record as ${:r},
except that ${:A^n} is appended to the sequence of the ${-:FIELD} component,
i.e, it is short for ${-:r[.FIELD = r.FIELD A^n]}.
* ${:r[.FIELD =.. A^n]} denotes the same record as ${:r},
except that ${:A^n} is appended to the sequence of the ${:FIELD} component,
i.e, it is short for ${:r[.FIELD = r.FIELD A^n]}.

* ${:r_1++r_2} denotes the composition of two records with the same fields of sequences by appending each sequence point-wise:

$${-:
{FIELD_ 1 A_1*, FIELD_ 2 A_2*, `... !%} `++ \
{FIELD_ 1 B_1*, FIELD_ 2 B_2*, `... !%} `= \
{FIELD_ 1 A_1* B_1*, FIELD_ 2 A_2* B_2*, `... !%}
$${:
`{FIELD_ 1 A_1*, FIELD_ 2 A_2*, `...} ++ `{FIELD_ 1 B_1*, FIELD_ 2 B_2*, `...} = `{FIELD_ 1 A_1* B_1*, FIELD_ 2 A_2* B_2*, `...}
}

* ${:(++) r*} denotes the composition of a sequence of records, respectively; if the sequence is empty, then all fields of the resulting record are empty.

The update notation for sequences and records generalizes recursively to nested components accessed by "paths" ${syntax-: pth}:

* ${-:s[.I_PTH = A]} is short for ${-:s[[i] = (s[i][.PTH = A])]},
* ${:s[$(`[i]#pth = A)]} is short for ${:s[[i] = s[i][pth = A]]},

* ${-:r[.FIELD_PTH = A]} is short for ${-:r[.FIELD = (s.FIELD[.PTH = A])]},

where ${-:r[.DOT_FIELD_PTH = A]} is shortened to ${-:r[.FIELD = A]}.

${syntax-ignore: pthaux}
* ${:r[$(!%.FIELD pth = A)]} is short for ${:r[.FIELD = r.FIELD[pth = A]]}.



Expand Down
Loading

0 comments on commit 93ca858

Please sign in to comment.