Modules¶
Indices¶
Indices can be given either in raw numeric form or as symbolic identifiers when bound by a respective construct. Such identifiers are looked up in the suitable space of the identifier context \(I\).
\[\begin{split}\begin{array}{llcllllllll}
\def\mathdef4044#1{{}}\mathdef4044{type index} & \href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{types}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{function index} & \href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{funcs}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{table index} & \href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{tables}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{memory index} & \href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{mems}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{global index} & \href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{globals}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{tag index} & \href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{tags}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{element index} & \href{../text/modules.html#text-elemidx}{\mathtt{elemidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{elem}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{data index} & \href{../text/modules.html#text-dataidx}{\mathtt{dataidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{data}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{local index} & \href{../text/modules.html#text-localidx}{\mathtt{localidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& x \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{locals}}[x] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{label index} & \href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I &::=&
l{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& l \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& l & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{labels}}[l] = v) \\
\def\mathdef4044#1{{}}\mathdef4044{field index} & \href{../text/modules.html#text-fieldidx}{\mathtt{fieldidx}}_{I,x} &::=&
i{:}\href{../text/values.html#text-int}{\def\mathdef4070#1{{\mathtt{u}#1}}\mathdef4070{\mathtt{32}}} &\Rightarrow& i \\&&|&
v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& i & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{fields}}[x][i] = v) \\
\end{array}\end{split}\]
Type Uses¶
A type use is a reference to a function type definition. It may optionally be augmented by explicit inlined parameter and result declarations. That allows binding symbolic identifiers to name the local indices of parameters. If inline declarations are given, then their types must match the referenced function type.
\[\begin{split}\begin{array}{llcllll}
\def\mathdef4044#1{{}}\mathdef4044{type use} & \href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I &::=&
\def\mathdef4084#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4084{(}~\def\mathdef4085#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4085{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef4086#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4086{)}
\quad\Rightarrow\quad x, I' \\ &&& \qquad
(\mathrel{\mbox{if}} \begin{array}[t]{@{}l@{}}
I.\href{../text/conventions.html#text-context}{\mathsf{typedefs}}[x] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}~(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]) \wedge
I' = \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~(\epsilon)^n\}) \\
\end{array} \\[1ex] &&|&
\def\mathdef4087#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4087{(}~\def\mathdef4088#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4088{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef4089#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4089{)}
~~(t_1{:}\href{../text/types.html#text-functype}{\mathtt{param}})^\ast~~(t_2{:}\href{../text/types.html#text-functype}{\mathtt{result}})^\ast
\quad\Rightarrow\quad x, I' \\ &&& \qquad
(\mathrel{\mbox{if}} \begin{array}[t]{@{}l@{}}
I.\href{../text/conventions.html#text-context}{\mathsf{typedefs}}[x] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}~(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]) \wedge
I' = \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~\mathrm{id}(\href{../text/types.html#text-functype}{\mathtt{param}})^\ast\} ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\
\end{array} \\
\end{array}\end{split}\]
Note
If inline declarations are given, their types must be syntactically equal to the types from the indexed definition; possible type substitutions from other definitions that might make them equal are not taken into account. This is to simplify syntactic pre-processing.
The synthesized attribute of a \(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\) is a pair consisting of both the used type index and the local identifier context containing possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:
\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l}
\mathrm{id}(\def\mathdef4090#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4090{(}~\def\mathdef4091#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4091{param}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4092#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4092{)}) &=& \href{../text/values.html#text-id}{\mathtt{id}}^? \\
\end{array}\end{split}\]
Note
Both productions overlap for the case that the function type is \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\). However, in that case, they also produce the same results, so that the choice is immaterial.
The well-formedness condition on \(I'\) ensures that the parameters do not contain duplicate identifiers.
Abbreviations¶
A \(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\) may also be replaced entirely by inline parameter and result declarations. In that case, a type index is automatically inserted:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{type use} &
(t_1{:}\href{../text/types.html#text-functype}{\mathtt{param}})^\ast~~(t_2{:}\href{../text/types.html#text-functype}{\mathtt{result}})^\ast &\equiv&
\def\mathdef4093#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4093{(}~\def\mathdef4094#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4094{type}~~x~\def\mathdef4095#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4095{)}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast \\
\end{array}\end{split}\]
where \(x\) is the smallest existing type index whose recursive type definition in the current module is of the form
\[\def\mathdef4096#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4096{(}~\def\mathdef4097#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4097{rec}~\def\mathdef4098#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4098{(}~\def\mathdef4099#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4099{type}~\def\mathdef4100#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4100{(}~\def\mathdef4101#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4101{sub}~\def\mathdef4102#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4102{final}~~\def\mathdef4103#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4103{(}~\def\mathdef4104#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4104{func}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast~\def\mathdef4105#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4105{)}~\def\mathdef4106#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4106{)}~\def\mathdef4107#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4107{)}~\def\mathdef4108#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4108{)}\]
If no such index exists, then a new recursive type of the same form is inserted at the end of the module.
Abbreviations are expanded in the order they appear, such that previously inserted type definitions are reused by consecutive expansions.
Imports¶
The descriptors in imports can bind a symbolic function, table, memory, tag, or global identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{import} & \href{../text/modules.html#text-import}{\mathtt{import}}_I &::=&
\def\mathdef4109#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4109{(}~\def\mathdef4110#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4110{import}~~\mathit{mod}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I~\def\mathdef4111#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4111{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-import}{\mathsf{module}}~\mathit{mod}, \href{../syntax/modules.html#syntax-import}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-import}{\mathsf{desc}}~d \} \\[1ex]
\def\mathdef4044#1{{}}\mathdef4044{import description} & \href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I &::=&
\def\mathdef4112#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4112{(}~\def\mathdef4113#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4113{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef4114#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4114{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef4115#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4115{(}~\def\mathdef4116#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4116{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}_I~\def\mathdef4117#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4117{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\mathit{tt} \\ &&|&
\def\mathdef4118#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4118{(}~\def\mathdef4119#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4119{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}_I~\def\mathdef4120#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4120{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~~\mathit{mt} \\ &&|&
\def\mathdef4121#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4121{(}~\def\mathdef4122#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4122{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}_I~\def\mathdef4123#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4123{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\mathit{gt} \\ &&|&
\def\mathdef4124#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4124{(}~\def\mathdef4125#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4125{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/modules.html#text-tag}{\mathtt{tag}}~\def\mathdef4126#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4126{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{tag}}~\mathit{tt} \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, imports may also be specified inline with function, table, memory, global, or tag definitions; see the respective sections.
Functions¶
Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{function} & \href{../text/modules.html#text-func}{\mathtt{func}}_I &::=&
\def\mathdef4127#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4127{(}~\def\mathdef4128#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4128{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~~
(\mathit{loc}{:}\href{../text/modules.html#text-local}{\mathtt{local}}_I)^\ast~~(\mathit{in}{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I''})^\ast~\def\mathdef4129#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4129{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-func}{\mathsf{type}}~x, \href{../syntax/modules.html#syntax-func}{\mathsf{locals}}~\mathit{loc}^\ast, \href{../syntax/modules.html#syntax-func}{\mathsf{body}}~\mathit{in}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \} \\ &&& \qquad\qquad\qquad
(\mathrel{\mbox{if}} I'' = I \href{../syntax/conventions.html#notation-compose}{\oplus} I' \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~\mathrm{id}(\href{../text/modules.html#text-local}{\mathtt{local}})^\ast\} ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\[1ex]
\def\mathdef4044#1{{}}\mathdef4044{local} & \href{../text/modules.html#text-local}{\mathtt{local}}_I &::=&
\def\mathdef4130#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4130{(}~\def\mathdef4131#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4131{local}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~t{:}\href{../text/types.html#text-valtype}{\mathtt{valtype}}_I~\def\mathdef4132#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4132{)}
\quad\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-local}{\mathsf{type}}~t \} \\
\end{array}\end{split}\]
The definition of the local identifier context \(I''\) uses the following auxiliary function to extract optional identifiers from locals:
\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l}
\mathrm{id}(\def\mathdef4133#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4133{(}~\def\mathdef4134#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4134{local}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4135#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4135{)}) &=& \href{../text/values.html#text-id}{\mathtt{id}}^? \\
\end{array}\end{split}\]
Note
The well-formedness condition on \(I''\) ensures that parameters and locals do not contain duplicate identifiers.
Abbreviations¶
Multiple anonymous locals may be combined into a single declaration:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{local} &
\def\mathdef4136#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4136{(}~~\def\mathdef4137#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4137{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}^\ast~~\def\mathdef4138#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4138{)} &\equiv&
(\def\mathdef4139#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4139{(}~~\def\mathdef4140#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4140{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}~~\def\mathdef4141#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4141{)})^\ast \\
\end{array}\end{split}\]
Functions can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4142#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4142{(}~\def\mathdef4143#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4143{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4144#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4144{(}~\def\mathdef4145#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4145{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef4146#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4146{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef4147#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4147{)} \quad\equiv \\ & \qquad
\def\mathdef4148#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4148{(}~\def\mathdef4149#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4149{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef4150#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4150{(}~\def\mathdef4151#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4151{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef4152#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4152{)}~\def\mathdef4153#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4153{)} \\[1ex] &
\def\mathdef4154#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4154{(}~\def\mathdef4155#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4155{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4156#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4156{(}~\def\mathdef4157#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4157{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef4158#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4158{)}~~\dots~\def\mathdef4159#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4159{)} \quad\equiv \\ & \qquad
\def\mathdef4160#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4160{(}~\def\mathdef4161#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4161{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef4162#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4162{(}~\def\mathdef4163#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4163{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef4164#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4164{)}~\def\mathdef4165#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4165{)}~~
\def\mathdef4166#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4166{(}~\def\mathdef4167#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4167{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef4168#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4168{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a function declaration can contain any number of exports, possibly followed by an import.
Tables¶
Table definitions can bind a symbolic table identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{table} & \href{../text/modules.html#text-table}{\mathtt{table}}_I &::=&
\def\mathdef4169#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4169{(}~\def\mathdef4170#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4170{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}_I~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef4171#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4171{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\mathit{tt}, \href{../syntax/modules.html#syntax-table}{\mathsf{init}}~e \} \\
\end{array}\end{split}\]
Abbreviations¶
A table’s initialization expression can be omitted, in which case it defaults to \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}\):
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4172#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4172{(}~\def\mathdef4173#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4173{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef4174#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4174{)}
&\equiv&
\def\mathdef4175#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4175{(}~\def\mathdef4176#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4176{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~~\def\mathdef4177#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4177{(}~\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref.null}}~\mathit{ht}~\def\mathdef4178#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4178{)}~\def\mathdef4179#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4179{)}
\\ &&& \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/types.html#text-tabletype}{\mathtt{tabletype}} = \href{../text/types.html#text-limits}{\mathtt{limits}}~\def\mathdef4180#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4180{(}~\def\mathdef4181#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4181{ref}~\def\mathdef4182#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4182{null}^?~\mathit{ht}~\def\mathdef4183#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4183{)}) \\
\end{array}\end{split}\]
An element segment can be given inline with a table definition, in which case its offset is \(0\) and the limits of the table type are inferred from the length of the given segment:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4184#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4184{(}~\def\mathdef4185#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4185{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef4186#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4186{(}~\def\mathdef4187#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4187{elem}~~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef4188#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4188{)}~\def\mathdef4189#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4189{)} \quad\equiv \\ & \qquad
\def\mathdef4190#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4190{(}~\def\mathdef4191#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4191{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef4192#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4192{)} \\ & \qquad
\def\mathdef4193#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4193{(}~\def\mathdef4194#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4194{elem}~~\def\mathdef4195#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4195{(}~\def\mathdef4196#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4196{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef4197#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4197{)}~~\def\mathdef4198#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4198{(}~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}'\def\mathdef4199#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4199{.const}~~\def\mathdef4200#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4200{0}~\def\mathdef4201#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4201{)}~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef4202#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4202{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, \\ & \qquad\qquad
\mathrel{\mbox{if}} \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}? \neq \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? \vee \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? = \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \def\mathdef4203#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4203{i32}) \\
\end{array}\end{split}\]
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4204#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4204{(}~\def\mathdef4205#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4205{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef4206#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4206{(}~\def\mathdef4207#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4207{elem}~~x^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef4208#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4208{)}~\def\mathdef4209#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4209{)} \quad\equiv \\ & \qquad
\def\mathdef4210#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4210{(}~\def\mathdef4211#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4211{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef4212#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4212{)} \\ & \qquad
\def\mathdef4213#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4213{(}~\def\mathdef4214#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4214{elem}~~\def\mathdef4215#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4215{(}~\def\mathdef4216#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4216{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef4217#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4217{)}~~\def\mathdef4218#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4218{(}~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}'\def\mathdef4219#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4219{.const}~~\def\mathdef4220#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4220{0}~\def\mathdef4221#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4221{)}~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\def\mathdef4222#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4222{(}~\def\mathdef4223#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4223{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}~\def\mathdef4224#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4224{)})~\def\mathdef4225#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4225{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, \\ & \qquad\qquad
\mathrel{\mbox{if}} \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}? \neq \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? \vee \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? = \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \def\mathdef4226#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4226{i32}) \\
\end{array}\end{split}\]
Tables can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4227#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4227{(}~\def\mathdef4228#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4228{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4229#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4229{(}~\def\mathdef4230#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4230{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef4231#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4231{)}~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef4232#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4232{)} \quad\equiv \\ & \qquad
\def\mathdef4233#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4233{(}~\def\mathdef4234#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4234{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef4235#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4235{(}~\def\mathdef4236#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4236{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef4237#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4237{)}~\def\mathdef4238#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4238{)} \\[1ex] &
\def\mathdef4239#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4239{(}~\def\mathdef4240#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4240{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4241#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4241{(}~\def\mathdef4242#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4242{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef4243#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4243{)}~~\dots~\def\mathdef4244#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4244{)} \quad\equiv \\ & \qquad
\def\mathdef4245#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4245{(}~\def\mathdef4246#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4246{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef4247#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4247{(}~\def\mathdef4248#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4248{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef4249#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4249{)}~\def\mathdef4250#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4250{)}~~
\def\mathdef4251#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4251{(}~\def\mathdef4252#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4252{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef4253#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4253{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a table declaration can contain any number of exports, possibly followed by an import.
Memories¶
Memory definitions can bind a symbolic memory identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{memory} & \href{../text/modules.html#text-mem}{\mathtt{mem}}_I &::=&
\def\mathdef4254#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4254{(}~\def\mathdef4255#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4255{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}_I~\def\mathdef4256#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4256{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-mem}{\mathsf{type}}~\mathit{mt} \} \\
\end{array}\end{split}\]
Abbreviations¶
A data segment can be given inline with a memory definition, in which case its offset is \(0\) and the limits of the memory type are inferred from the length of the data, rounded up to page size:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4257#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4257{(}~\def\mathdef4258#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4258{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~\def\mathdef4259#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4259{(}~\def\mathdef4260#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4260{data}~~b^n{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef4261#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4261{)}~~\def\mathdef4262#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4262{)} \quad\equiv \\ & \qquad
\def\mathdef4263#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4263{(}~\def\mathdef4264#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4264{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~m~~m~\def\mathdef4265#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4265{)} \\ & \qquad
\def\mathdef4266#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4266{(}~\def\mathdef4267#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4267{data}~~\def\mathdef4268#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4268{(}~\def\mathdef4269#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4269{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef4270#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4270{)}~~\def\mathdef4271#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4271{(}~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}'\def\mathdef4272#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4272{.const}~~\def\mathdef4273#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4273{0}~\def\mathdef4274#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4274{)}~~\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef4275#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4275{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, \\ & \qquad\qquad
\mathrel{\mbox{if}} \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}? \neq \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? \vee \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? = \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \def\mathdef4276#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4276{i32}, \\ & \qquad\qquad
m = \mathrm{ceil}(n / 64\,\mathrm{Ki})) \\
\end{array}\end{split}\]
Memories can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4277#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4277{(}~\def\mathdef4278#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4278{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4279#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4279{(}~\def\mathdef4280#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4280{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef4281#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4281{)}~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef4282#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4282{)} \quad\equiv \\ & \qquad
\def\mathdef4283#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4283{(}~\def\mathdef4284#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4284{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef4285#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4285{(}~\def\mathdef4286#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4286{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef4287#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4287{)}~\def\mathdef4288#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4288{)}
\\[1ex] &
\def\mathdef4289#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4289{(}~\def\mathdef4290#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4290{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4291#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4291{(}~\def\mathdef4292#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4292{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef4293#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4293{)}~~\dots~\def\mathdef4294#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4294{)} \quad\equiv \\ & \qquad
\def\mathdef4295#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4295{(}~\def\mathdef4296#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4296{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef4297#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4297{(}~\def\mathdef4298#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4298{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef4299#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4299{)}~\def\mathdef4300#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4300{)}~~
\def\mathdef4301#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4301{(}~\def\mathdef4302#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4302{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef4303#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4303{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a memory declaration can contain any number of exports, possibly followed by an import.
Globals¶
Global definitions can bind a symbolic global identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{global} & \href{../text/modules.html#text-global}{\mathtt{global}}_I &::=&
\def\mathdef4304#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4304{(}~\def\mathdef4305#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4305{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}_I~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef4306#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4306{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-global}{\mathsf{type}}~\mathit{gt}, \href{../syntax/modules.html#syntax-global}{\mathsf{init}}~e \} \\
\end{array}\end{split}\]
Abbreviations¶
Globals can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{module field} &
\def\mathdef4307#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4307{(}~\def\mathdef4308#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4308{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4309#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4309{(}~\def\mathdef4310#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4310{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef4311#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4311{)}~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef4312#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4312{)} \quad\equiv \\ & \qquad
\def\mathdef4313#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4313{(}~\def\mathdef4314#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4314{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef4315#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4315{(}~\def\mathdef4316#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4316{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef4317#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4317{)}~\def\mathdef4318#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4318{)}
\\[1ex] &
\def\mathdef4319#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4319{(}~\def\mathdef4320#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4320{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4321#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4321{(}~\def\mathdef4322#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4322{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef4323#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4323{)}~~\dots~\def\mathdef4324#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4324{)} \quad\equiv \\ & \qquad
\def\mathdef4325#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4325{(}~\def\mathdef4326#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4326{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef4327#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4327{(}~\def\mathdef4328#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4328{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef4329#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4329{)}~\def\mathdef4330#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4330{)}~~
\def\mathdef4331#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4331{(}~\def\mathdef4332#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4332{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef4333#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4333{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
Note
The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a global declaration can contain any number of exports, possibly followed by an import.
Exports¶
The syntax for exports mirrors their abstract syntax directly.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{export} & \href{../text/modules.html#text-export}{\mathtt{export}}_I &::=&
\def\mathdef4364#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4364{(}~\def\mathdef4365#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4365{export}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I~\def\mathdef4366#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4366{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~d \} \\
\def\mathdef4044#1{{}}\mathdef4044{export description} & \href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I &::=&
\def\mathdef4367#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4367{(}~\def\mathdef4368#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4368{func}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef4369#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4369{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef4370#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4370{(}~\def\mathdef4371#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4371{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I~\def\mathdef4372#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4372{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x \\ &&|&
\def\mathdef4373#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4373{(}~\def\mathdef4374#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4374{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I~\def\mathdef4375#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4375{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x \\ &&|&
\def\mathdef4376#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4376{(}~\def\mathdef4377#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4377{global}~~x{:}\href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I~\def\mathdef4378#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4378{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{global}}~x \\&&|&
\def\mathdef4379#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4379{(}~\def\mathdef4380#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4380{tag}~~x{:}\href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}_I~\def\mathdef4381#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4381{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{tag}}~x \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, exports may also be specified inline with function, table, memory, global, or tag definitions; see the respective sections.
Start Function¶
A start function is defined in terms of its index.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{start function} & \href{../text/modules.html#text-start}{\mathtt{start}}_I &::=&
\def\mathdef4382#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4382{(}~\def\mathdef4383#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4383{start}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef4384#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4384{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-start}{\mathsf{func}}~x \} \\
\end{array}\end{split}\]
Note
At most one start function may occur in a module, which is ensured by a suitable side condition on the \(\href{../text/modules.html#text-module}{\mathtt{module}}\) grammar.
Element Segments¶
Element segments allow for an optional table index to identify the table to initialize.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{element segment} & \href{../text/modules.html#text-elem}{\mathtt{elem}}_I &::=&
\def\mathdef4385#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4385{(}~\def\mathdef4386#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4386{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef4387#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4387{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{passive}} \} \\ &&|&
\def\mathdef4388#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4388{(}~\def\mathdef4389#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4389{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I~~\def\mathdef4390#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4390{(}~\def\mathdef4391#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4391{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef4392#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4392{)}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef4393#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4393{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~e \} \} \\ &&&
\def\mathdef4394#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4394{(}~\def\mathdef4395#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4395{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4396#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4396{declare}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef4397#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4397{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{declarative}} \} \\
\def\mathdef4044#1{{}}\mathdef4044{element list} & \href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I &::=&
t{:}\href{../text/types.html#text-reftype}{\mathtt{reftype}}_I~~y^\ast{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}_I) \qquad\Rightarrow\quad ( \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~t, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast ) \\
\def\mathdef4044#1{{}}\mathdef4044{element expression} & \href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}_I &::=&
\def\mathdef4398#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4398{(}~\def\mathdef4399#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4399{item}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef4400#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4400{)}
\quad\Rightarrow\quad e \\
\def\mathdef4044#1{{}}\mathdef4044{table use} & \href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I &::=&
\def\mathdef4401#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4401{(}~\def\mathdef4402#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4402{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I ~\def\mathdef4403#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4403{)}
\quad\Rightarrow\quad x \\
\end{array}\end{split}\]
Abbreviations¶
As an abbreviation, a single instruction may occur in place of the offset of an active element segment or as an element expression:
\[\begin{split}\begin{array}{llcll}
\def\mathdef4044#1{{}}\mathdef4044{element offset} &
\def\mathdef4404#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4404{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4405#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4405{)} &\equiv&
\def\mathdef4406#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4406{(}~\def\mathdef4407#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4407{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4408#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4408{)} \\
\def\mathdef4044#1{{}}\mathdef4044{element item} &
\def\mathdef4409#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4409{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4410#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4410{)} &\equiv&
\def\mathdef4411#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4411{(}~\def\mathdef4412#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4412{item}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4413#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4413{)} \\
\end{array}\end{split}\]
Also, the element list may be written as just a sequence of function indices:
\[\begin{array}{llcll}
\def\mathdef4044#1{{}}\mathdef4044{element list} &
\def\mathdef4414#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4414{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I) &\equiv&
\def\mathdef4415#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4415{(ref}~\def\mathdef4416#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4416{func)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\def\mathdef4417#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4417{(}~\def\mathdef4418#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4418{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef4419#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4419{)})
\end{array}\]
A table use can be omitted, defaulting to \(\mathtt{0}\). Furthermore, for backwards compatibility with earlier versions of WebAssembly, if the table use is omitted, the \(\def\mathdef4420#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4420{func}\) keyword can be omitted as well.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{table use} &
\epsilon &\equiv& \def\mathdef4421#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4421{(}~\def\mathdef4422#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4422{table}~~\def\mathdef4423#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4423{0}~\def\mathdef4424#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4424{)} \\
\def\mathdef4044#1{{}}\mathdef4044{element segment} &
\def\mathdef4425#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4425{(}~\def\mathdef4426#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4426{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4427#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4427{(}~\def\mathdef4428#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4428{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef4429#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4429{)}~~\\ &
\qquad \href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef4430#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4430{)}
&\equiv&
\def\mathdef4431#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4431{(}~\def\mathdef4432#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4432{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef4433#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4433{(}~\def\mathdef4434#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4434{table}~~\def\mathdef4435#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4435{0}~\def\mathdef4436#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4436{)}~~\def\mathdef4437#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4437{(}~\def\mathdef4438#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4438{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef4439#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4439{)}~~\\ &
&&\qquad \def\mathdef4440#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4440{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef4441#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4441{)}
\end{array}\end{split}\]
As another abbreviation, element segments may also be specified inline with table definitions; see the respective section.
Data Segments¶
Data segments allow for an optional memory index to identify the memory to initialize. The data is written as a string, which may be split up into a possibly empty sequence of individual string literals.
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{data segment} & \href{../text/modules.html#text-data}{\mathtt{data}}_I &::=&
\def\mathdef4442#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4442{(}~\def\mathdef4443#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4443{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef4444#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4444{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}} \} \\ &&|&
\def\mathdef4445#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4445{(}~\def\mathdef4446#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4446{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I~~\def\mathdef4447#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4447{(}~\def\mathdef4448#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4448{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef4449#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4449{)}~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef4450#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4450{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~x, \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~e \} \} \\
\def\mathdef4044#1{{}}\mathdef4044{data string} & \href{../text/modules.html#text-datastring}{\mathtt{datastring}} &::=&
(b^\ast{:}\href{../text/values.html#text-string}{\mathtt{string}})^\ast \quad\Rightarrow\quad \href{../syntax/conventions.html#notation-concat}{\mathrm{concat}}((b^\ast)^\ast) \\
\def\mathdef4044#1{{}}\mathdef4044{memory use} & \href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I &::=&
\def\mathdef4451#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4451{(}~\def\mathdef4452#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4452{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I ~\def\mathdef4453#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4453{)}
\quad\Rightarrow\quad x \\
\end{array}\end{split}\]
Note
In the current version of WebAssembly, the only valid memory index is 0 or a symbolic memory identifier resolving to the same value.
Abbreviations¶
As an abbreviation, a single instruction may occur in place of the offset of an active data segment:
\[\begin{array}{llcll}
\def\mathdef4044#1{{}}\mathdef4044{data offset} &
\def\mathdef4454#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4454{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4455#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4455{)} &\equiv&
\def\mathdef4456#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4456{(}~\def\mathdef4457#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4457{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4458#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4458{)}
\end{array}\]
Also, a memory use can be omitted, defaulting to \(\mathtt{0}\).
\[\begin{split}\begin{array}{llclll}
\def\mathdef4044#1{{}}\mathdef4044{memory use} &
\epsilon &\equiv& \def\mathdef4459#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4459{(}~\def\mathdef4460#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4460{memory}~~\def\mathdef4461#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4461{0}~\def\mathdef4462#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4462{)} \\
\end{array}\end{split}\]
As another abbreviation, data segments may also be specified inline with memory definitions; see the respective section.
Modules¶
A module consists of a sequence of fields that can occur in any order. All definitions and their respective bound identifiers scope over the entire module, including the text preceding them.
A module may optionally bind an identifier that names the module. The name serves a documentary role only.
Note
Tools may include the module name in the name section of the binary format.
\[\begin{split}\begin{array}{lll}
\def\mathdef4044#1{{}}\mathdef4044{module} & \href{../text/modules.html#text-module}{\mathtt{module}} &
\begin{array}[t]{@{}cllll}
::=&
\def\mathdef4463#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4463{(}~\def\mathdef4464#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4464{module}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(m{:}\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I)^\ast~\def\mathdef4465#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4465{)}
\quad\Rightarrow\quad \href{../syntax/conventions.html#notation-compose}{\bigoplus} m^\ast \\
&\qquad (\mathrel{\mbox{if}} I = \href{../syntax/conventions.html#notation-compose}{\bigoplus} \mathrm{idc}(\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}})^\ast ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\
\end{array} \\[1ex]
\def\mathdef4044#1{{}}\mathdef4044{module field} & \href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I &
\begin{array}[t]{@{}clll}
::=&
\mathit{ty}^\ast{:}\href{../text/types.html#text-rectype}{\mathtt{rectype}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{types}}~\mathit{ty}^\ast\} \\ |&
\mathit{im}{:}\href{../text/modules.html#text-import}{\mathtt{import}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{imports}}~\mathit{im}\} \\ |&
\mathit{fn}{:}\href{../text/modules.html#text-func}{\mathtt{func}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}~\mathit{fn}\} \\ |&
\mathit{ta}{:}\href{../text/modules.html#text-table}{\mathtt{table}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}~\mathit{ta}\} \\ |&
\mathit{me}{:}\href{../text/modules.html#text-mem}{\mathtt{mem}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}~\mathit{me}\} \\ |&
\mathit{gl}{:}\href{../text/modules.html#text-global}{\mathtt{global}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}~\mathit{gl}\} \\ |&
\mathit{tg}{:}\href{../text/modules.html#text-tag}{\mathtt{tag}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{tags}}~\mathit{tg}\} \\ |&
\mathit{el}{:}\href{../text/modules.html#text-elem}{\mathtt{elem}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}~\mathit{el}\} \\ |&
\mathit{da}{:}\href{../text/modules.html#text-data}{\mathtt{data}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}~\mathit{da}\} \\ |&
\mathit{st}{:}\href{../text/modules.html#text-start}{\mathtt{start}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{start}}~\mathit{st}\} \\ |&
\mathit{ex}{:}\href{../text/modules.html#text-export}{\mathtt{export}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}~\mathit{ex}\} \\
\end{array}
\end{array}\end{split}\]
The following restrictions are imposed on the composition of modules: \(m_1 \href{../syntax/conventions.html#notation-compose}{\oplus} m_2\) is defined if and only if
\(m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon \vee m_2.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon\)
\(m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{tags}} = \epsilon \vee m_2.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}} = \epsilon\)
Note
The first condition ensures that there is at most one start function. The second condition enforces that all imports must occur before any regular definition of a function, table, memory, global, or tag, thereby maintaining the ordering of the respective index spaces.
The well-formedness condition on \(I\) in the grammar for \(\href{../text/modules.html#text-module}{\mathtt{module}}\) ensures that no namespace contains duplicate identifiers.
The definition of the initial identifier context \(I\) uses the following auxiliary definition which maps each relevant definition to a singular context with one (possibly empty) identifier:
\[\begin{split}\begin{array}{@{}lcl@{\qquad\qquad}l}
\mathrm{idc}(\def\mathdef4466#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4466{(}~\def\mathdef4467#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4467{rec}~~\href{../text/types.html#text-typedef}{\mathtt{typedef}}^\ast~\def\mathdef4468#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4468{)}) &=&
\href{../syntax/conventions.html#notation-compose}{\bigoplus} \mathrm{idc}(\href{../text/types.html#text-typedef}{\mathtt{typedef}})^\ast \\
\mathrm{idc}(\def\mathdef4469#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4469{(}~\def\mathdef4470#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4470{type}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\href{../text/types.html#text-subtype}{\mathtt{subtype}}~\def\mathdef4471#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4471{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{types}}~(v^?), \href{../text/conventions.html#text-context}{\mathsf{fields}}~\mathrm{idf}(\href{../text/types.html#text-subtype}{\mathtt{subtype}}), \href{../text/conventions.html#text-context}{\mathsf{typedefs}}~\mathit{st}\} \\
\mathrm{idc}(\def\mathdef4472#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4472{(}~\def\mathdef4473#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4473{func}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4474#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4474{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4475#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4475{(}~\def\mathdef4476#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4476{table}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4477#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4477{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4478#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4478{(}~\def\mathdef4479#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4479{memory}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4480#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4480{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4481#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4481{(}~\def\mathdef4482#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4482{global}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4483#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4483{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4484#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4484{(}~\def\mathdef4485#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4485{tag}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4486#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4486{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tags}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4487#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4487{(}~\def\mathdef4488#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4488{elem}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4489#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4489{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{elem}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4490#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4490{(}~\def\mathdef4491#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4491{data}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4492#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4492{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{data}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4493#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4493{(}~\def\mathdef4494#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4494{import}~\dots~\def\mathdef4495#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4495{(}~\def\mathdef4496#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4496{func}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4497#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4497{)}~\def\mathdef4498#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4498{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4499#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4499{(}~\def\mathdef4500#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4500{import}~\dots~\def\mathdef4501#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4501{(}~\def\mathdef4502#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4502{table}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4503#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4503{)}~\def\mathdef4504#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4504{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4505#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4505{(}~\def\mathdef4506#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4506{import}~\dots~\def\mathdef4507#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4507{(}~\def\mathdef4508#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4508{memory}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4509#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4509{)}~\def\mathdef4510#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4510{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4511#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4511{(}~\def\mathdef4512#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4512{import}~\dots~\def\mathdef4513#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4513{(}~\def\mathdef4514#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4514{global}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4515#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4515{)}~\def\mathdef4516#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4516{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(v^?)\} \\
\mathrm{idc}(\def\mathdef4517#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4517{(}~\dots~\def\mathdef4518#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4518{)}) &=&
\{\}
\\[2ex]
\mathrm{idf}(\def\mathdef4519#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4519{(}~\def\mathdef4520#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4520{sub}~\dots~\href{../text/types.html#text-comptype}{\mathtt{comptype}}~\def\mathdef4521#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4521{)}) &=&
\mathrm{idf}(\href{../text/types.html#text-comptype}{\mathtt{comptype}}) \\
\mathrm{idf}(\def\mathdef4522#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4522{(}~\def\mathdef4523#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4523{struct}~\mathit{Tfield}^\ast~\def\mathdef4524#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4524{)}) &=&
\href{../syntax/conventions.html#notation-compose}{\bigoplus} \mathrm{idf}(\href{../text/types.html#text-structtype}{\mathtt{field}})^\ast \\
\mathrm{idf}(\def\mathdef4525#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4525{(}~\def\mathdef4526#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4526{array}~\dots~\def\mathdef4527#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4527{)}) &=&
\epsilon \\
\mathrm{idf}(\def\mathdef4528#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4528{(}~\def\mathdef4529#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4529{func}~\dots~\def\mathdef4530#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4530{)}) &=&
\epsilon \\
\mathrm{idf}(\def\mathdef4531#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4531{(}~\def\mathdef4532#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4532{field}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4533#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4533{)}) &=&
v^? \\
\end{array}\end{split}\]
Abbreviations¶
In a source file, the toplevel \(\mathtt{(module}~\dots\mathtt{)}\) surrounding the module body may be omitted.
\[\begin{array}{llcll}
\def\mathdef4044#1{{}}\mathdef4044{module} &
\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast &\equiv&
\def\mathdef4534#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4534{(}~\def\mathdef4535#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4535{module}~~\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast~\def\mathdef4536#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4536{)}
\end{array}\]