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\mathdef1990#1{{}}\mathdef1990{type index} & \href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2014#1{{\mathtt{u}#1}}\mathdef2014{\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\mathdef1990#1{{}}\mathdef1990{function index} & \href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2014#1{{\mathtt{u}#1}}\mathdef2014{\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\mathdef1990#1{{}}\mathdef1990{table index} & \href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2014#1{{\mathtt{u}#1}}\mathdef2014{\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\mathdef1990#1{{}}\mathdef1990{memory index} & \href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2014#1{{\mathtt{u}#1}}\mathdef2014{\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\mathdef1990#1{{}}\mathdef1990{global index} & \href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2014#1{{\mathtt{u}#1}}\mathdef2014{\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\mathdef1990#1{{}}\mathdef1990{local index} & \href{../text/modules.html#text-localidx}{\mathtt{localidx}}_I &::=&
x{:}\href{../text/values.html#text-int}{\def\mathdef2014#1{{\mathtt{u}#1}}\mathdef2014{\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\mathdef1990#1{{}}\mathdef1990{label index} & \href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I &::=&
l{:}\href{../text/values.html#text-int}{\def\mathdef2014#1{{\mathtt{u}#1}}\mathdef2014{\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\mathdef1990#1{{}}\mathdef1990{type definition} & \href{../text/modules.html#text-typedef}{\mathtt{type}} &::=&
\def\mathdef2026#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2026{(}~\def\mathdef2027#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2027{type}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef2028#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2028{)}
&\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\mathdef1990#1{{}}\mathdef1990{type use} & \href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I &::=&
\def\mathdef2029#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2029{(}~\def\mathdef2030#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2030{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef2031#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2031{)}
\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\mathdef2032#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2032{(}~\def\mathdef2033#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2033{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef2034#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2034{)}
~~(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\mathdef2035#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2035{(}~\def\mathdef2036#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2036{param}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2037#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2037{)}) &=& \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\mathdef1990#1{{}}\mathdef1990{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\mathdef2038#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2038{(}~\def\mathdef2039#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2039{type}~~x~\def\mathdef2040#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2040{)}~~\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\mathdef2041#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2041{(}~\def\mathdef2042#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2042{type}~~\def\mathdef2043#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2043{(}~\def\mathdef2044#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2044{func}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}~\def\mathdef2045#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2045{)}~\def\mathdef2046#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2046{)}\]
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\mathdef1990#1{{}}\mathdef1990{import} & \href{../text/modules.html#text-import}{\mathtt{import}}_I &::=&
\def\mathdef2047#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2047{(}~\def\mathdef2048#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2048{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\mathdef2049#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2049{)} \\ &&& \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\mathdef1990#1{{}}\mathdef1990{import description} & \href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I &::=&
\def\mathdef2050#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2050{(}~\def\mathdef2051#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2051{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef2052#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2052{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef2053#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2053{(}~\def\mathdef2054#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2054{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2055#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2055{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\mathit{tt} \\ &&|&
\def\mathdef2056#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2056{(}~\def\mathdef2057#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2057{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2058#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2058{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~~\mathit{mt} \\ &&|&
\def\mathdef2059#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2059{(}~\def\mathdef2060#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2060{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef2061#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2061{)}
&\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\mathdef1990#1{{}}\mathdef1990{function} & \href{../text/modules.html#text-func}{\mathtt{func}}_I &::=&
\def\mathdef2062#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2062{(}~\def\mathdef2063#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2063{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\mathdef2064#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2064{)} \\ &&& \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\mathdef1990#1{{}}\mathdef1990{local} & \href{../text/modules.html#text-local}{\mathtt{local}} &::=&
\def\mathdef2065#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2065{(}~\def\mathdef2066#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2066{local}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~t{:}\href{../text/types.html#text-valtype}{\mathtt{valtype}}~\def\mathdef2067#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2067{)}
\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\mathdef2068#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2068{(}~\def\mathdef2069#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2069{local}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2070#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2070{)}) &=& \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\mathdef1990#1{{}}\mathdef1990{local} &
\def\mathdef2071#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2071{(}~~\def\mathdef2072#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2072{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}^\ast~~\def\mathdef2073#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2073{)} &\equiv&
(\def\mathdef2074#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2074{(}~~\def\mathdef2075#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2075{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}~~\def\mathdef2076#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2076{)})^\ast \\
\end{array}\end{split}\]
Functions can be defined as imports or exports inline:
\[\begin{split}\begin{array}{llclll}
\def\mathdef1990#1{{}}\mathdef1990{module field} &
\def\mathdef2077#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2077{(}~\def\mathdef2078#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2078{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2079#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2079{(}~\def\mathdef2080#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2080{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2081#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2081{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef2082#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2082{)} \quad\equiv \\ & \qquad
\def\mathdef2083#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2083{(}~\def\mathdef2084#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2084{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2085#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2085{(}~\def\mathdef2086#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2086{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef2087#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2087{)}~\def\mathdef2088#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2088{)} \\[1ex] &
\def\mathdef2089#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2089{(}~\def\mathdef2090#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2090{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2091#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2091{(}~\def\mathdef2092#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2092{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2093#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2093{)}~~\dots~\def\mathdef2094#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2094{)} \quad\equiv \\ & \qquad
\def\mathdef2095#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2095{(}~\def\mathdef2096#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2096{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2097#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2097{(}~\def\mathdef2098#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2098{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2099#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2099{)}~\def\mathdef2100#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2100{)}~~
\def\mathdef2101#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2101{(}~\def\mathdef2102#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2102{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2103#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2103{)}
\\ & \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\mathdef1990#1{{}}\mathdef1990{table} & \href{../text/modules.html#text-table}{\mathtt{table}}_I &::=&
\def\mathdef2104#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2104{(}~\def\mathdef2105#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2105{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2106#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2106{)}
&\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\mathdef1990#1{{}}\mathdef1990{module field} &
\def\mathdef2107#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2107{(}~\def\mathdef2108#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2108{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-elemtype}{\mathtt{elemtype}}~~\def\mathdef2109#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2109{(}~\def\mathdef2110#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2110{elem}~~x^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef2111#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2111{)}~~\def\mathdef2112#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2112{)} \quad\equiv \\ & \qquad
\def\mathdef2113#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2113{(}~\def\mathdef2114#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2114{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-elemtype}{\mathtt{elemtype}}~\def\mathdef2115#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2115{)}~~
\def\mathdef2116#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2116{(}~\def\mathdef2117#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2117{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\def\mathdef2118#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2118{(}~\def\mathdef2119#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2119{i32.const}~~\def\mathdef2120#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2120{0}~\def\mathdef2121#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2121{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef2122#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2122{)}
\\ & \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\mathdef1990#1{{}}\mathdef1990{module field} &
\def\mathdef2123#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2123{(}~\def\mathdef2124#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2124{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2125#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2125{(}~\def\mathdef2126#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2126{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2127#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2127{)}~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2128#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2128{)} \quad\equiv \\ & \qquad
\def\mathdef2129#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2129{(}~\def\mathdef2130#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2130{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2131#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2131{(}~\def\mathdef2132#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2132{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef2133#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2133{)}~\def\mathdef2134#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2134{)} \\[1ex] &
\def\mathdef2135#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2135{(}~\def\mathdef2136#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2136{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2137#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2137{(}~\def\mathdef2138#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2138{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2139#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2139{)}~~\dots~\def\mathdef2140#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2140{)} \quad\equiv \\ & \qquad
\def\mathdef2141#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2141{(}~\def\mathdef2142#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2142{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2143#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2143{(}~\def\mathdef2144#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2144{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2145#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2145{)}~\def\mathdef2146#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2146{)}~~
\def\mathdef2147#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2147{(}~\def\mathdef2148#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2148{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2149#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2149{)}
\\ & \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\mathdef1990#1{{}}\mathdef1990{memory} & \href{../text/modules.html#text-mem}{\mathtt{mem}}_I &::=&
\def\mathdef2150#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2150{(}~\def\mathdef2151#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2151{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2152#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2152{)}
&\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\mathdef1990#1{{}}\mathdef1990{module field} &
\def\mathdef2153#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2153{(}~\def\mathdef2154#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2154{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2155#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2155{(}~\def\mathdef2156#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2156{data}~~b^n{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef2157#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2157{)}~~\def\mathdef2158#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2158{)} \quad\equiv \\ & \qquad
\def\mathdef2159#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2159{(}~\def\mathdef2160#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2160{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~m~~m~\def\mathdef2161#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2161{)}~~
\def\mathdef2162#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2162{(}~\def\mathdef2163#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2163{data}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\def\mathdef2164#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2164{(}~\def\mathdef2165#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2165{i32.const}~~\def\mathdef2166#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2166{0}~\def\mathdef2167#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2167{)}~~\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef2168#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2168{)}
\\ & \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\mathdef1990#1{{}}\mathdef1990{module field} &
\def\mathdef2169#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2169{(}~\def\mathdef2170#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2170{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2171#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2171{(}~\def\mathdef2172#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2172{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2173#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2173{)}~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2174#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2174{)} \quad\equiv \\ & \qquad
\def\mathdef2175#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2175{(}~\def\mathdef2176#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2176{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2177#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2177{(}~\def\mathdef2178#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2178{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef2179#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2179{)}~\def\mathdef2180#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2180{)}
\\[1ex] &
\def\mathdef2181#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2181{(}~\def\mathdef2182#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2182{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2183#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2183{(}~\def\mathdef2184#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2184{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2185#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2185{)}~~\dots~\def\mathdef2186#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2186{)} \quad\equiv \\ & \qquad
\def\mathdef2187#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2187{(}~\def\mathdef2188#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2188{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2189#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2189{(}~\def\mathdef2190#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2190{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2191#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2191{)}~\def\mathdef2192#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2192{)}~~
\def\mathdef2193#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2193{(}~\def\mathdef2194#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2194{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2195#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2195{)}
\\ & \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\mathdef1990#1{{}}\mathdef1990{global} & \href{../text/modules.html#text-global}{\mathtt{global}}_I &::=&
\def\mathdef2196#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2196{(}~\def\mathdef2197#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2197{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\mathdef2198#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2198{)}
&\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\mathdef1990#1{{}}\mathdef1990{module field} &
\def\mathdef2199#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2199{(}~\def\mathdef2200#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2200{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2201#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2201{(}~\def\mathdef2202#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2202{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef2203#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2203{)}~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef2204#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2204{)} \quad\equiv \\ & \qquad
\def\mathdef2205#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2205{(}~\def\mathdef2206#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2206{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef2207#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2207{(}~\def\mathdef2208#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2208{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef2209#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2209{)}~\def\mathdef2210#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2210{)}
\\[1ex] &
\def\mathdef2211#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2211{(}~\def\mathdef2212#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2212{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef2213#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2213{(}~\def\mathdef2214#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2214{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef2215#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2215{)}~~\dots~\def\mathdef2216#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2216{)} \quad\equiv \\ & \qquad
\def\mathdef2217#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2217{(}~\def\mathdef2218#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2218{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef2219#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2219{(}~\def\mathdef2220#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2220{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef2221#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2221{)}~\def\mathdef2222#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2222{)}~~
\def\mathdef2223#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2223{(}~\def\mathdef2224#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2224{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef2225#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2225{)}
\\ & \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\mathdef1990#1{{}}\mathdef1990{export} & \href{../text/modules.html#text-export}{\mathtt{export}}_I &::=&
\def\mathdef2226#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2226{(}~\def\mathdef2227#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2227{export}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I~\def\mathdef2228#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2228{)}
&\Rightarrow& \{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~d \} \\
\def\mathdef1990#1{{}}\mathdef1990{export description} & \href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I &::=&
\def\mathdef2229#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2229{(}~\def\mathdef2230#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2230{func}~~x{:}\href{../binary/modules.html#binary-funcidx}{\mathtt{funcidx}}_I~\def\mathdef2231#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2231{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x \\ &&|&
\def\mathdef2232#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2232{(}~\def\mathdef2233#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2233{table}~~x{:}\href{../binary/modules.html#binary-tableidx}{\mathtt{tableidx}}_I~\def\mathdef2234#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2234{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x \\ &&|&
\def\mathdef2235#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2235{(}~\def\mathdef2236#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2236{memory}~~x{:}\href{../binary/modules.html#binary-memidx}{\mathtt{memidx}}_I~\def\mathdef2237#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2237{)}
&\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x \\ &&|&
\def\mathdef2238#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2238{(}~\def\mathdef2239#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2239{global}~~x{:}\href{../binary/modules.html#binary-globalidx}{\mathtt{globalidx}}_I~\def\mathdef2240#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2240{)}
&\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\mathdef1990#1{{}}\mathdef1990{start function} & \href{../text/modules.html#text-start}{\mathtt{start}}_I &::=&
\def\mathdef2241#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2241{(}~\def\mathdef2242#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2242{start}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef2243#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2243{)}
&\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\mathdef1990#1{{}}\mathdef1990{element segment} & \href{../text/modules.html#text-elem}{\mathtt{elem}}_I &::=&
\def\mathdef2244#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2244{(}~\def\mathdef2245#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2245{elem}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I~~\def\mathdef2246#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2246{(}~\def\mathdef2247#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2247{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2248#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2248{)}~~y^\ast{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef2249#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2249{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{table}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{offset}}~e, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast \} \\
\end{array}\end{split}\]
Note
In the current version of WebAssembly, the only valid table index is 0 or a symbolic table identifier resolving to the same value.
Abbreviations¶
As an abbreviation, a single instruction may occur in place of the offset:
\[\begin{array}{llcll}
\def\mathdef1990#1{{}}\mathdef1990{element offset} &
\href{../text/instructions.html#text-instr}{\mathtt{instr}} &\equiv&
\def\mathdef2250#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2250{(}~\def\mathdef2251#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2251{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef2252#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2252{)}
\end{array}\]
Also, the table index can be omitted, defaulting to \(\mathtt{0}\).
\[\begin{array}{llclll}
\def\mathdef1990#1{{}}\mathdef1990{element segment} &
\def\mathdef2253#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2253{(}~\def\mathdef2254#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2254{elem}~~\def\mathdef2255#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2255{(}~\def\mathdef2256#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2256{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2257#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2257{)}~~\dots~\def\mathdef2258#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2258{)}
&\equiv&
\def\mathdef2259#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2259{(}~\def\mathdef2260#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2260{elem}~~0~~\def\mathdef2261#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2261{(}~\def\mathdef2262#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2262{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2263#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2263{)}~~\dots~\def\mathdef2264#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2264{)}
\end{array}\]
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\mathdef1990#1{{}}\mathdef1990{data segment} & \href{../text/modules.html#text-data}{\mathtt{data}}_I &::=&
\def\mathdef2265#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2265{(}~\def\mathdef2266#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2266{data}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I~~\def\mathdef2267#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2267{(}~\def\mathdef2268#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2268{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2269#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2269{)}~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef2270#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2270{)} \\ &&& \qquad
\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-data}{\mathsf{data}}~x', \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~e, \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast \} \\[1ex]
\def\mathdef1990#1{{}}\mathdef1990{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) \\
\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:
\[\begin{array}{llcll}
\def\mathdef1990#1{{}}\mathdef1990{data offset} &
\href{../text/instructions.html#text-instr}{\mathtt{instr}} &\equiv&
\def\mathdef2271#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2271{(}~\def\mathdef2272#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2272{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef2273#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2273{)}
\end{array}\]
Also, the memory index can be omitted, defaulting to \(\mathtt{0}\).
\[\begin{array}{llclll}
\def\mathdef1990#1{{}}\mathdef1990{data segment} &
\def\mathdef2274#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2274{(}~\def\mathdef2275#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2275{data}~~\def\mathdef2276#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2276{(}~\def\mathdef2277#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2277{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2278#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2278{)}~~\dots~\def\mathdef2279#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2279{)}
&\equiv&
\def\mathdef2280#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2280{(}~\def\mathdef2281#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2281{data}~~0~~\def\mathdef2282#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2282{(}~\def\mathdef2283#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2283{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef2284#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2284{)}~~\dots~\def\mathdef2285#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2285{)}
\end{array}\]
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\mathdef1990#1{{}}\mathdef1990{module} & \href{../text/modules.html#text-module}{\mathtt{module}} &
\begin{array}[t]{@{}cllll}
::=&
\def\mathdef2286#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2286{(}~\def\mathdef2287#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2287{module}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(m{:}\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I)^\ast~\def\mathdef2288#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2288{)}
\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\mathdef1990#1{{}}\mathdef1990{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{elem}}~\mathit{el}\} \\ |&
\mathit{da}{:}\href{../text/modules.html#text-data}{\mathtt{data}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{data}}~\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\mathdef2289#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2289{(}~\def\mathdef2290#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2290{type}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef2291#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2291{)}) &=&
\{\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\mathdef2292#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2292{(}~\def\mathdef2293#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2293{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2294#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2294{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2295#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2295{(}~\def\mathdef2296#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2296{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2297#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2297{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2298#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2298{(}~\def\mathdef2299#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2299{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2300#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2300{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2301#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2301{(}~\def\mathdef2302#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2302{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2303#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2303{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2304#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2304{(}~\def\mathdef2305#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2305{import}~\dots~\def\mathdef2306#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2306{(}~\def\mathdef2307#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2307{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2308#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2308{)}~\def\mathdef2309#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2309{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2310#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2310{(}~\def\mathdef2311#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2311{import}~\dots~\def\mathdef2312#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2312{(}~\def\mathdef2313#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2313{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2314#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2314{)}~\def\mathdef2315#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2315{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2316#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2316{(}~\def\mathdef2317#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2317{import}~\dots~\def\mathdef2318#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2318{(}~\def\mathdef2319#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2319{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2320#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2320{)}~\def\mathdef2321#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2321{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2322#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2322{(}~\def\mathdef2323#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2323{import}~\dots~\def\mathdef2324#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2324{(}~\def\mathdef2325#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2325{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef2326#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2326{)}~\def\mathdef2327#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2327{)}) &=&
\{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\
\mathrm{idc}(\def\mathdef2328#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2328{(}~\dots~\def\mathdef2329#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2329{)}) &=&
\{\} \\
\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\mathdef1990#1{{}}\mathdef1990{module} &
\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast &\equiv&
\def\mathdef2330#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2330{(}~\def\mathdef2331#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2331{module}~~\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast~\def\mathdef2332#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2332{)}
\end{array}\]