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\mathdef2221#1{{}}\mathdef2221{type index} & \href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{function index} & \href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{table index} & \href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{memory index} & \href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{global index} & \href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{element index} & \href{../text/modules.html#text-elemidx}{\mathtt{elemidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{data index} & \href{../text/modules.html#text-dataidx}{\mathtt{dataidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{local index} & \href{../text/modules.html#text-localidx}{\mathtt{localidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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\mathdef2221#1{{}}\mathdef2221{label index} & \href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I &::=&
l{:}\href{../text/values.html#text-int}{\def\mathdef2246#1{{\mathtt{u}#1}}\mathdef2246{\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) \\
\end{array}\end{split}\]
Types¶
Type definitions can bind a symbolic type identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{type definition} & \href{../text/modules.html#text-typedef}{\mathtt{type}} &::=&
\def\mathdef2258#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2258{(}~\def\mathdef2259#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2259{type}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef2260#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2260{)}
&\Rightarrow& \mathit{ft} \\
\end{array}\end{split}\]
Type Uses¶
A type use is a reference to a 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\mathdef2221#1{{}}\mathdef2221{type use} & \href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I &::=&
\def\mathdef2261#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2261{(}~\def\mathdef2262#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2262{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef2263#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2263{)}
\quad\Rightarrow\quad x, I' \\ &&& \qquad
(\mathrel{\mbox{if}} \begin{array}[t]{@{}l@{}}
I.\href{../text/conventions.html#text-context}{\mathsf{typedefs}}[x] = [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\mathdef2264#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2264{(}~\def\mathdef2265#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2265{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef2266#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2266{)}
~~(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] = [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}\]
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 updated identifier context including possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:
\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l}
\mathrm{id}(\def\mathdef2267#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2267{(}~\def\mathdef2268#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2268{param}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2269#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2269{)}) &=& \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 identifier.
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\mathdef2221#1{{}}\mathdef2221{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\mathdef2270#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2270{(}~\def\mathdef2271#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2271{type}~~x~\def\mathdef2272#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2272{)}~~\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 definition in the current module is the function type \([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\). If no such index exists, then a new type definition of the form
\[\def\mathdef2273#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2273{(}~\def\mathdef2274#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2274{type}~~\def\mathdef2275#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2275{(}~\def\mathdef2276#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2276{func}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast~\def\mathdef2277#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2277{)}~\def\mathdef2278#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2278{)}\]
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, or global identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{import} & \href{../text/modules.html#text-import}{\mathtt{import}}_I &::=&
\def\mathdef2279#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2279{(}~\def\mathdef2280#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2280{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\mathdef2281#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2281{)} \\ &&& \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\mathdef2221#1{{}}\mathdef2221{import description} & \href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I &::=&
\def\mathdef2282#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2282{(}~\def\mathdef2283#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2283{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef2284#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2284{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef2285#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2285{(}~\def\mathdef2286#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2286{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2287#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2287{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\mathit{tt} \\ &&|&
\def\mathdef2288#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2288{(}~\def\mathdef2289#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2289{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2290#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2290{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~~\mathit{mt} \\ &&|&
\def\mathdef2291#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2291{(}~\def\mathdef2292#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2292{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef2293#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2293{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\mathit{gt} \\
\end{array}\end{split}\]
Functions¶
Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{function} & \href{../text/modules.html#text-func}{\mathtt{func}}_I &::=&
\def\mathdef2294#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2294{(}~\def\mathdef2295#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2295{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~~
(t{:}\href{../text/modules.html#text-local}{\mathtt{local}})^\ast~~(\mathit{in}{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I''})^\ast~\def\mathdef2296#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2296{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-func}{\mathsf{type}}~x, \href{../syntax/modules.html#syntax-func}{\mathsf{locals}}~t^\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} \{\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\mathdef2221#1{{}}\mathdef2221{local} & \href{../text/modules.html#text-local}{\mathtt{local}} &::=&
\def\mathdef2297#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2297{(}~\def\mathdef2298#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2298{local}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~t{:}\href{../text/types.html#text-valtype}{\mathtt{valtype}}~\def\mathdef2299#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2299{)}
\quad\Rightarrow\quad 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\mathdef2300#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2300{(}~\def\mathdef2301#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2301{local}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2302#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2302{)}) &=& \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\mathdef2221#1{{}}\mathdef2221{local} &
\def\mathdef2303#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2303{(}~~\def\mathdef2304#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2304{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}^\ast~~\def\mathdef2305#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2305{)} &\equiv&
(\def\mathdef2306#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2306{(}~~\def\mathdef2307#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2307{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}~~\def\mathdef2308#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2308{)})^\ast \\
\end{array}\end{split}\]
Functions can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{module field} &
\def\mathdef2309#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2309{(}~\def\mathdef2310#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2310{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2311#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2311{(}~\def\mathdef2312#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2312{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2313#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2313{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef2314#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2314{)} \quad\equiv \\ & \qquad
\def\mathdef2315#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2315{(}~\def\mathdef2316#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2316{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2317#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2317{(}~\def\mathdef2318#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2318{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef2319#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2319{)}~\def\mathdef2320#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2320{)} \\[1ex] &
\def\mathdef2321#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2321{(}~\def\mathdef2322#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2322{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2323#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2323{(}~\def\mathdef2324#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2324{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2325#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2325{)}~~\dots~\def\mathdef2326#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2326{)} \quad\equiv \\ & \qquad
\def\mathdef2327#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2327{(}~\def\mathdef2328#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2328{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2329#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2329{(}~\def\mathdef2330#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2330{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2331#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2331{)}~\def\mathdef2332#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2332{)}~~
\def\mathdef2333#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2333{(}~\def\mathdef2334#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2334{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2335#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2335{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export.
Tables¶
Table definitions can bind a symbolic table identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{table} & \href{../text/modules.html#text-table}{\mathtt{table}}_I &::=&
\def\mathdef2336#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2336{(}~\def\mathdef2337#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2337{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2338#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2338{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\mathit{tt} \} \\
\end{array}\end{split}\]
Abbreviations¶
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\mathdef2221#1{{}}\mathdef2221{module field} &
\def\mathdef2339#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2339{(}~\def\mathdef2340#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2340{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef2341#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2341{(}~\def\mathdef2342#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2342{elem}~~\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}~\def\mathdef2343#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2343{)} \quad\equiv \\ & \qquad
\def\mathdef2344#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2344{(}~\def\mathdef2345#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2345{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef2346#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2346{)}~~
\def\mathdef2347#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2347{(}~\def\mathdef2348#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2348{elem}~~\def\mathdef2349#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2349{(}~\def\mathdef2350#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2350{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2351#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2351{)}~~\def\mathdef2352#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2352{(}~\def\mathdef2353#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2353{i32.const}~~\def\mathdef2354#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2354{0}~\def\mathdef2355#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2355{)}~~\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}~\def\mathdef2356#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2356{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{module field} &
\def\mathdef2357#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2357{(}~\def\mathdef2358#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2358{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef2359#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2359{(}~\def\mathdef2360#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2360{elem}~~x^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/instructions.html#text-expr}{\mathtt{expr}})~\def\mathdef2361#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2361{)}~~\def\mathdef2362#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2362{)} \quad\equiv \\ & \qquad
\def\mathdef2363#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2363{(}~\def\mathdef2364#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2364{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef2365#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2365{)}~~
\def\mathdef2366#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2366{(}~\def\mathdef2367#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2367{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\def\mathdef2368#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2368{(}~\def\mathdef2369#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2369{i32.const}~~\def\mathdef2370#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2370{0}~\def\mathdef2371#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2371{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/instructions.html#text-expr}{\mathtt{expr}})~\def\mathdef2372#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2372{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
Tables can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{module field} &
\def\mathdef2373#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2373{(}~\def\mathdef2374#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2374{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2375#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2375{(}~\def\mathdef2376#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2376{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2377#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2377{)}~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2378#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2378{)} \quad\equiv \\ & \qquad
\def\mathdef2379#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2379{(}~\def\mathdef2380#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2380{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2381#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2381{(}~\def\mathdef2382#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2382{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2383#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2383{)}~\def\mathdef2384#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2384{)} \\[1ex] &
\def\mathdef2385#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2385{(}~\def\mathdef2386#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2386{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2387#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2387{(}~\def\mathdef2388#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2388{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2389#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2389{)}~~\dots~\def\mathdef2390#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2390{)} \quad\equiv \\ & \qquad
\def\mathdef2391#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2391{(}~\def\mathdef2392#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2392{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2393#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2393{(}~\def\mathdef2394#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2394{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2395#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2395{)}~\def\mathdef2396#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2396{)}~~
\def\mathdef2397#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2397{(}~\def\mathdef2398#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2398{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2399#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2399{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export or an inline elements segment.
Memories¶
Memory definitions can bind a symbolic memory identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{memory} & \href{../text/modules.html#text-mem}{\mathtt{mem}}_I &::=&
\def\mathdef2400#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2400{(}~\def\mathdef2401#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2401{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2402#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2402{)}
&\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\) 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\mathdef2221#1{{}}\mathdef2221{module field} &
\def\mathdef2403#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2403{(}~\def\mathdef2404#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2404{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2405#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2405{(}~\def\mathdef2406#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2406{data}~~b^n{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef2407#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2407{)}~~\def\mathdef2408#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2408{)} \quad\equiv \\ & \qquad
\def\mathdef2409#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2409{(}~\def\mathdef2410#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2410{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~m~~m~\def\mathdef2411#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2411{)}~~
\def\mathdef2412#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2412{(}~\def\mathdef2413#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2413{data}~~\def\mathdef2414#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2414{(}~\def\mathdef2415#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2415{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2416#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2416{)}~~\def\mathdef2417#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2417{(}~\def\mathdef2418#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2418{i32.const}~~\def\mathdef2419#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2419{0}~\def\mathdef2420#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2420{)}~~\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef2421#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2421{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, 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\mathdef2221#1{{}}\mathdef2221{module field} &
\def\mathdef2422#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2422{(}~\def\mathdef2423#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2423{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2424#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2424{(}~\def\mathdef2425#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2425{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2426#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2426{)}~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2427#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2427{)} \quad\equiv \\ & \qquad
\def\mathdef2428#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2428{(}~\def\mathdef2429#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2429{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2430#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2430{(}~\def\mathdef2431#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2431{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2432#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2432{)}~\def\mathdef2433#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2433{)}
\\[1ex] &
\def\mathdef2434#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2434{(}~\def\mathdef2435#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2435{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2436#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2436{(}~\def\mathdef2437#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2437{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2438#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2438{)}~~\dots~\def\mathdef2439#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2439{)} \quad\equiv \\ & \qquad
\def\mathdef2440#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2440{(}~\def\mathdef2441#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2441{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2442#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2442{(}~\def\mathdef2443#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2443{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2444#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2444{)}~\def\mathdef2445#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2445{)}~~
\def\mathdef2446#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2446{(}~\def\mathdef2447#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2447{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2448#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2448{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export or an inline data segment.
Globals¶
Global definitions can bind a symbolic global identifier.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{global} & \href{../text/modules.html#text-global}{\mathtt{global}}_I &::=&
\def\mathdef2449#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2449{(}~\def\mathdef2450#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2450{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2451#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2451{)}
&\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\mathdef2221#1{{}}\mathdef2221{module field} &
\def\mathdef2452#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2452{(}~\def\mathdef2453#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2453{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2454#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2454{(}~\def\mathdef2455#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2455{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2456#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2456{)}~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef2457#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2457{)} \quad\equiv \\ & \qquad
\def\mathdef2458#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2458{(}~\def\mathdef2459#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2459{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2460#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2460{(}~\def\mathdef2461#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2461{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef2462#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2462{)}~\def\mathdef2463#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2463{)}
\\[1ex] &
\def\mathdef2464#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2464{(}~\def\mathdef2465#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2465{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2466#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2466{(}~\def\mathdef2467#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2467{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2468#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2468{)}~~\dots~\def\mathdef2469#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2469{)} \quad\equiv \\ & \qquad
\def\mathdef2470#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2470{(}~\def\mathdef2471#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2471{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2472#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2472{(}~\def\mathdef2473#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2473{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2474#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2474{)}~\def\mathdef2475#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2475{)}~~
\def\mathdef2476#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2476{(}~\def\mathdef2477#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2477{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2478#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2478{)}
\\ & \qquad\qquad
(\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \vee \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\
\end{array}\end{split}\]
The latter abbreviation can be applied repeatedly, with “\(\dots\)” containing another import or export.
Exports¶
The syntax for exports mirrors their abstract syntax directly.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{export} & \href{../text/modules.html#text-export}{\mathtt{export}}_I &::=&
\def\mathdef2479#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2479{(}~\def\mathdef2480#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2480{export}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I~\def\mathdef2481#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2481{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~d \} \\
\def\mathdef2221#1{{}}\mathdef2221{export description} & \href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I &::=&
\def\mathdef2482#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2482{(}~\def\mathdef2483#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2483{func}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef2484#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2484{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef2485#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2485{(}~\def\mathdef2486#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2486{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I~\def\mathdef2487#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2487{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x \\ &&|&
\def\mathdef2488#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2488{(}~\def\mathdef2489#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2489{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I~\def\mathdef2490#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2490{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x \\ &&|&
\def\mathdef2491#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2491{(}~\def\mathdef2492#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2492{global}~~x{:}\href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I~\def\mathdef2493#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2493{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{global}}~x \\
\end{array}\end{split}\]
Start Function¶
A start function is defined in terms of its index.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{start function} & \href{../text/modules.html#text-start}{\mathtt{start}}_I &::=&
\def\mathdef2494#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2494{(}~\def\mathdef2495#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2495{start}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef2496#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2496{)}
&\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\mathdef2221#1{{}}\mathdef2221{element segment} & \href{../text/modules.html#text-elem}{\mathtt{elem}}_I &::=&
\def\mathdef2497#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2497{(}~\def\mathdef2498#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2498{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}~\def\mathdef2499#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2499{)} \\ &&& \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\mathdef2500#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2500{(}~\def\mathdef2501#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2501{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I~~\def\mathdef2502#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2502{(}~\def\mathdef2503#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2503{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2504#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2504{)}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}~\def\mathdef2505#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2505{)} \\ &&& \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\mathdef2506#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2506{(}~\def\mathdef2507#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2507{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2508#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2508{declare}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}~\def\mathdef2509#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2509{)} \\ &&& \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\mathdef2221#1{{}}\mathdef2221{element list} & \href{../text/modules.html#text-elemlist}{\mathtt{elemlist}} &::=&
t{:}\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~y^\ast{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathit{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\mathdef2221#1{{}}\mathdef2221{element expression} & \href{../text/modules.html#text-elemexpr}{\mathit{elemexpr}} &::=&
\def\mathdef2510#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2510{(}~\def\mathdef2511#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2511{item}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}~\def\mathdef2512#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2512{)}
\quad\Rightarrow\quad e \\
\def\mathdef2221#1{{}}\mathdef2221{table use} & \href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I &::=&
\def\mathdef2513#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2513{(}~\def\mathdef2514#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2514{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I ~\def\mathdef2515#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2515{)}
\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\mathdef2221#1{{}}\mathdef2221{element offset} &
\href{../text/instructions.html#text-instr}{\mathtt{instr}} &\equiv&
\def\mathdef2516#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2516{(}~\def\mathdef2517#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2517{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef2518#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2518{)} \\
\def\mathdef2221#1{{}}\mathdef2221{element item} &
\href{../text/instructions.html#text-instr}{\mathtt{instr}} &\equiv&
\def\mathdef2519#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2519{(}~\def\mathdef2520#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2520{item}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef2521#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2521{)} \\
\end{array}\end{split}\]
Also, the element list may be written as just a sequence of function indices:
\[\begin{array}{llcll}
\def\mathdef2221#1{{}}\mathdef2221{element list} &
\def\mathdef2522#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2522{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I) &\equiv&
\def\mathdef2523#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2523{funcref}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\def\mathdef2524#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2524{(}~\def\mathdef2525#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2525{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef2526#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2526{)})
\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\mathdef2527#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2527{func}\) keyword can be omitted as well.
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{table use} &
\epsilon &\equiv& \def\mathdef2528#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2528{(}~\def\mathdef2529#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2529{table}~~\def\mathdef2530#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2530{0}~\def\mathdef2531#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2531{)} \\
\def\mathdef2221#1{{}}\mathdef2221{element segment} &
\def\mathdef2532#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2532{(}~\def\mathdef2533#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2533{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2534#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2534{(}~\def\mathdef2535#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2535{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2536#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2536{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef2537#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2537{)}
&\equiv&
\def\mathdef2538#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2538{(}~\def\mathdef2539#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2539{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2540#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2540{(}~\def\mathdef2541#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2541{table}~~\def\mathdef2542#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2542{0}~\def\mathdef2543#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2543{)}~~\def\mathdef2544#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2544{(}~\def\mathdef2545#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2545{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2546#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2546{)}~~\def\mathdef2547#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2547{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef2548#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2548{)}
\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\mathdef2221#1{{}}\mathdef2221{data segment} & \href{../text/modules.html#text-data}{\mathtt{data}}_I &::=&
\def\mathdef2549#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2549{(}~\def\mathdef2550#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2550{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef2551#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2551{)} \\ &&& \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-data}{\mathsf{passive}} \} \\ &&|&
\def\mathdef2552#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2552{(}~\def\mathdef2553#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2553{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I~~\def\mathdef2554#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2554{(}~\def\mathdef2555#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2555{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2556#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2556{)}~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef2557#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2557{)} \\ &&& \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-data}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~x', \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~e \} \} \\
\def\mathdef2221#1{{}}\mathdef2221{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\mathdef2221#1{{}}\mathdef2221{memory use} & \href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I &::=&
\def\mathdef2558#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2558{(}~\def\mathdef2559#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2559{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I ~\def\mathdef2560#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2560{)}
\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\mathdef2221#1{{}}\mathdef2221{data offset} &
\href{../text/instructions.html#text-instr}{\mathtt{instr}} &\equiv&
\def\mathdef2561#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2561{(}~\def\mathdef2562#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2562{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef2563#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2563{)}
\end{array}\]
Also, a memory use can be omitted, defaulting to \(\mathtt{0}\).
\[\begin{split}\begin{array}{llclll}
\def\mathdef2221#1{{}}\mathdef2221{memory use} &
\epsilon &\equiv& \def\mathdef2564#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2564{(}~\def\mathdef2565#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2565{memory}~~\def\mathdef2566#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2566{0}~\def\mathdef2567#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2567{)} \\
\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\mathdef2221#1{{}}\mathdef2221{module} & \href{../text/modules.html#text-module}{\mathtt{module}} &
\begin{array}[t]{@{}cllll}
::=&
\def\mathdef2568#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2568{(}~\def\mathdef2569#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2569{module}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(m{:}\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I)^\ast~\def\mathdef2570#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2570{)}
\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\mathdef2221#1{{}}\mathdef2221{module field} & \href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I &
\begin{array}[t]{@{}clll}
::=&
\mathit{ty}{:}\href{../text/modules.html#text-typedef}{\mathtt{type}} &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{types}}~\mathit{ty}\} \\ |&
\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{ex}{:}\href{../text/modules.html#text-export}{\mathtt{export}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}~\mathit{ex}\} \\ |&
\mathit{st}{:}\href{../text/modules.html#text-start}{\mathtt{start}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{start}}~\mathit{st}\} \\ |&
\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}\} \\
\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}} = \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, or global, 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\mathdef2571#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2571{(}~\def\mathdef2572#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2572{type}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef2573#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2573{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{types}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?), \href{../text/conventions.html#text-context}{\mathsf{typedefs}}~\mathit{ft}\} \\
\mathrm{idc}(\def\mathdef2574#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2574{(}~\def\mathdef2575#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2575{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2576#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2576{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2577#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2577{(}~\def\mathdef2578#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2578{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2579#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2579{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2580#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2580{(}~\def\mathdef2581#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2581{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2582#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2582{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2583#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2583{(}~\def\mathdef2584#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2584{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2585#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2585{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2586#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2586{(}~\def\mathdef2587#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2587{elem}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2588#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2588{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{elem}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2589#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2589{(}~\def\mathdef2590#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2590{data}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2591#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2591{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{data}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2592#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2592{(}~\def\mathdef2593#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2593{import}~\dots~\def\mathdef2594#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2594{(}~\def\mathdef2595#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2595{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2596#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2596{)}~\def\mathdef2597#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2597{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2598#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2598{(}~\def\mathdef2599#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2599{import}~\dots~\def\mathdef2600#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2600{(}~\def\mathdef2601#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2601{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2602#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2602{)}~\def\mathdef2603#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2603{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2604#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2604{(}~\def\mathdef2605#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2605{import}~\dots~\def\mathdef2606#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2606{(}~\def\mathdef2607#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2607{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2608#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2608{)}~\def\mathdef2609#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2609{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2610#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2610{(}~\def\mathdef2611#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2611{import}~\dots~\def\mathdef2612#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2612{(}~\def\mathdef2613#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2613{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2614#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2614{)}~\def\mathdef2615#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2615{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2616#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2616{(}~\dots~\def\mathdef2617#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2617{)}) &=&
\{\} \\
\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\mathdef2221#1{{}}\mathdef2221{module} &
\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast &\equiv&
\def\mathdef2618#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2618{(}~\def\mathdef2619#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2619{module}~~\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast~\def\mathdef2620#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2620{)}
\end{array}\]