Modules — WebAssembly 2.0 + exception handling (Draft 2025-03-20) (original) (raw)

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\mathdef3414#1{{}}\mathdef3414{type index} & \href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{function index} & \href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{table index} & \href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{memory index} & \href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{tag index} & \href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\mathtt{32}}} &\Rightarrow& x \\&&|& v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& x & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{tags}}[x] = v) \\ \def\mathdef3414#1{{}}\mathdef3414{global index} & \href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{element index} & \href{../text/modules.html#text-elemidx}{\mathtt{elemidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{data index} & \href{../text/modules.html#text-dataidx}{\mathtt{dataidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{local index} & \href{../text/modules.html#text-localidx}{\mathtt{localidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{label index} & \href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I &::=& l{:}\href{../text/values.html#text-int}{\def\mathdef3439#1{{\mathtt{u}#1}}\mathdef3439{\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\mathdef3414#1{{}}\mathdef3414{type definition} & \href{../text/modules.html#text-typedef}{\mathtt{type}} &::=& \def\mathdef3453#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3453{(}~\def\mathdef3454#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3454{type}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef3455#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3455{)} &\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\mathdef3414#1{{}}\mathdef3414{type use} & \href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I &::=& \def\mathdef3456#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3456{(}~\def\mathdef3457#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3457{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3458#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3458{)} \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\mathdef3459#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3459{(}~\def\mathdef3460#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3460{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3461#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3461{)} ~~(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 local identifier context containing possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:

\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l} \mathrm{id}(\def\mathdef3462#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3462{(}~\def\mathdef3463#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3463{param}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3464#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3464{)}) &=& \href{../text/values.html#text-id}{\mathtt{id}}^? \\ \end{array}\end{split}\]

Note

Both productions overlap for the case that the function type is \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\). However, in that case, they also produce the same results, so that the choice is immaterial.

The well-formedness condition on \(I'\) ensures that the parameters do not contain duplicate identifiers.

Abbreviations

A \(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\) may also be replaced entirely by inline parameter and result declarations. In that case, a type index is automatically inserted:

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{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\mathdef3465#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3465{(}~\def\mathdef3466#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3466{type}~~x~\def\mathdef3467#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3467{)}~~\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\mathdef3468#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3468{(}~\def\mathdef3469#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3469{type}~~\def\mathdef3470#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3470{(}~\def\mathdef3471#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3471{func}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast~\def\mathdef3472#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3472{)}~\def\mathdef3473#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3473{)}\]

is inserted at the end of the module.

Abbreviations are expanded in the order they appear, such that previously inserted type definitions are reused by consecutive expansions.

Imports

The descriptors in imports can bind a symbolic function, table, memory, tag, or global identifier.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{import} & \href{../text/modules.html#text-import}{\mathtt{import}}_I &::=& \def\mathdef3474#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3474{(}~\def\mathdef3475#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3475{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\mathdef3476#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3476{)} \\ &&& \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\mathdef3414#1{{}}\mathdef3414{import description} & \href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I &::=& \def\mathdef3477#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3477{(}~\def\mathdef3478#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3478{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef3479#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3479{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x \\ &&|& \def\mathdef3480#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3480{(}~\def\mathdef3481#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3481{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3482#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3482{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\mathit{tt} \\ &&|& \def\mathdef3483#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3483{(}~\def\mathdef3484#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3484{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3485#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3485{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~~\mathit{mt} \\ &&|& \def\mathdef3486#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3486{(}~\def\mathdef3487#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3487{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/modules.html#text-tag}{\mathtt{tag}}~\def\mathdef3488#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3488{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{tag}}~\mathit{tt} \\ &&|& \def\mathdef3489#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3489{(}~\def\mathdef3490#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3490{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3491#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3491{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\mathit{gt} \\ \end{array}\end{split}\]

Abbreviations

As an abbreviation, imports may also be specified inline with function, table, memory, or global definitions; see the respective sections.

Functions

Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{function} & \href{../text/modules.html#text-func}{\mathtt{func}}_I &::=& \def\mathdef3492#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3492{(}~\def\mathdef3493#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3493{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\mathdef3494#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3494{)} \\ &&& \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} 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\mathdef3414#1{{}}\mathdef3414{local} & \href{../text/modules.html#text-local}{\mathtt{local}} &::=& \def\mathdef3495#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3495{(}~\def\mathdef3496#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3496{local}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~t{:}\href{../text/types.html#text-valtype}{\mathtt{valtype}}~\def\mathdef3497#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3497{)} \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\mathdef3498#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3498{(}~\def\mathdef3499#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3499{local}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3500#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3500{)}) &=& \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\mathdef3414#1{{}}\mathdef3414{local} & \def\mathdef3501#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3501{(}~~\def\mathdef3502#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3502{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}^\ast~~\def\mathdef3503#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3503{)} &\equiv& (\def\mathdef3504#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3504{(}~~\def\mathdef3505#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3505{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}~~\def\mathdef3506#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3506{)})^\ast \\ \end{array}\end{split}\]

Functions can be defined as imports or exports inline:

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3507#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3507{(}~\def\mathdef3508#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3508{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3509#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3509{(}~\def\mathdef3510#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3510{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3511#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3511{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3512#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3512{)} \quad\equiv \\ & \qquad \def\mathdef3513#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3513{(}~\def\mathdef3514#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3514{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3515#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3515{(}~\def\mathdef3516#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3516{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3517#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3517{)}~\def\mathdef3518#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3518{)} \\[1ex] & \def\mathdef3519#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3519{(}~\def\mathdef3520#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3520{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3521#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3521{(}~\def\mathdef3522#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3522{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3523#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3523{)}~~\dots~\def\mathdef3524#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3524{)} \quad\equiv \\ & \qquad \def\mathdef3525#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3525{(}~\def\mathdef3526#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3526{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3527#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3527{(}~\def\mathdef3528#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3528{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3529#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3529{)}~\def\mathdef3530#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3530{)}~~ \def\mathdef3531#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3531{(}~\def\mathdef3532#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3532{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3533#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3533{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\ \end{array}\end{split}\]

Note

The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a function declaration can contain any number of exports, possibly followed by an import.

Tables

Table definitions can bind a symbolic table identifier.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{table} & \href{../text/modules.html#text-table}{\mathtt{table}}_I &::=& \def\mathdef3534#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3534{(}~\def\mathdef3535#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3535{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3536#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3536{)} &\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\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3537#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3537{(}~\def\mathdef3538#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3538{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3539#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3539{(}~\def\mathdef3540#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3540{elem}~~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef3541#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3541{)}~\def\mathdef3542#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3542{)} \quad\equiv \\ & \qquad \def\mathdef3543#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3543{(}~\def\mathdef3544#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3544{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3545#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3545{)} \\ & \qquad \def\mathdef3546#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3546{(}~\def\mathdef3547#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3547{elem}~~\def\mathdef3548#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3548{(}~\def\mathdef3549#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3549{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3550#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3550{)}~~\def\mathdef3551#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3551{(}~\def\mathdef3552#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3552{i32.const}~~\def\mathdef3553#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3553{0}~\def\mathdef3554#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3554{)}~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef3555#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3555{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\ \end{array}\end{split}\]

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3556#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3556{(}~\def\mathdef3557#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3557{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3558#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3558{(}~\def\mathdef3559#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3559{elem}~~x^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef3560#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3560{)}~\def\mathdef3561#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3561{)} \quad\equiv \\ & \qquad \def\mathdef3562#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3562{(}~\def\mathdef3563#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3563{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3564#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3564{)} \\ & \qquad \def\mathdef3565#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3565{(}~\def\mathdef3566#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3566{elem}~~\def\mathdef3567#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3567{(}~\def\mathdef3568#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3568{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3569#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3569{)}~~\def\mathdef3570#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3570{(}~\def\mathdef3571#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3571{i32.const}~~\def\mathdef3572#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3572{0}~\def\mathdef3573#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3573{)}~~\def\mathdef3574#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3574{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef3575#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3575{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\ \end{array}\end{split}\]

Tables can be defined as imports or exports inline:

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3576#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3576{(}~\def\mathdef3577#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3577{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3578#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3578{(}~\def\mathdef3579#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3579{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3580#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3580{)}~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3581#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3581{)} \quad\equiv \\ & \qquad \def\mathdef3582#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3582{(}~\def\mathdef3583#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3583{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3584#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3584{(}~\def\mathdef3585#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3585{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3586#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3586{)}~\def\mathdef3587#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3587{)} \\[1ex] & \def\mathdef3588#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3588{(}~\def\mathdef3589#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3589{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3590#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3590{(}~\def\mathdef3591#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3591{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3592#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3592{)}~~\dots~\def\mathdef3593#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3593{)} \quad\equiv \\ & \qquad \def\mathdef3594#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3594{(}~\def\mathdef3595#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3595{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3596#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3596{(}~\def\mathdef3597#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3597{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3598#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3598{)}~\def\mathdef3599#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3599{)}~~ \def\mathdef3600#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3600{(}~\def\mathdef3601#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3601{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3602#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3602{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\ \end{array}\end{split}\]

Note

The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a table declaration can contain any number of exports, possibly followed by an import.

Memories

Memory definitions can bind a symbolic memory identifier.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{memory} & \href{../text/modules.html#text-mem}{\mathtt{mem}}_I &::=& \def\mathdef3603#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3603{(}~\def\mathdef3604#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3604{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3605#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3605{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-mem}{\mathsf{type}}~\mathit{mt} \} \\ \end{array}\end{split}\]

Abbreviations

A data segment can be given inline with a memory definition, in which case its offset is \(0\) and the limits of the memory type are inferred from the length of the data, rounded up to page size:

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3606#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3606{(}~\def\mathdef3607#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3607{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3608#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3608{(}~\def\mathdef3609#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3609{data}~~b^n{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3610#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3610{)}~~\def\mathdef3611#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3611{)} \quad\equiv \\ & \qquad \def\mathdef3612#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3612{(}~\def\mathdef3613#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3613{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~m~~m~\def\mathdef3614#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3614{)} \\ & \qquad \def\mathdef3615#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3615{(}~\def\mathdef3616#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3616{data}~~\def\mathdef3617#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3617{(}~\def\mathdef3618#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3618{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3619#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3619{)}~~\def\mathdef3620#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3620{(}~\def\mathdef3621#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3621{i32.const}~~\def\mathdef3622#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3622{0}~\def\mathdef3623#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3623{)}~~\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3624#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3624{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, 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\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3625#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3625{(}~\def\mathdef3626#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3626{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3627#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3627{(}~\def\mathdef3628#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3628{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3629#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3629{)}~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3630#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3630{)} \quad\equiv \\ & \qquad \def\mathdef3631#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3631{(}~\def\mathdef3632#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3632{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3633#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3633{(}~\def\mathdef3634#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3634{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3635#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3635{)}~\def\mathdef3636#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3636{)} \\[1ex] & \def\mathdef3637#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3637{(}~\def\mathdef3638#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3638{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3639#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3639{(}~\def\mathdef3640#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3640{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3641#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3641{)}~~\dots~\def\mathdef3642#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3642{)} \quad\equiv \\ & \qquad \def\mathdef3643#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3643{(}~\def\mathdef3644#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3644{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3645#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3645{(}~\def\mathdef3646#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3646{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3647#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3647{)}~\def\mathdef3648#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3648{)}~~ \def\mathdef3649#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3649{(}~\def\mathdef3650#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3650{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3651#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3651{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\ \end{array}\end{split}\]

Note

The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a memory declaration can contain any number of exports, possibly followed by an import.

Tags

An tag definition can bind a symbolic tag identifier.

\[\begin{split}\begin{array}{llcl} \def\mathdef3414#1{{}}\mathdef3414{tag} & \href{../text/modules.html#text-tag}{\mathtt{tag}}_I &::=& \def\mathdef3652#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3652{(}~\def\mathdef3653#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3653{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef3654#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3654{)} \\ &&& \qquad \Rightarrow\quad \{ \href{../syntax/modules.html#syntax-tag}{\mathsf{type}}~x \} \\ \end{array}\end{split}\]

Abbreviations

Tags can be defined as imports or exports inline:

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3655#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3655{(}~\def\mathdef3656#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3656{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3657#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3657{(}~\def\mathdef3658#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3658{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3659#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3659{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3660#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3660{)} \quad\equiv \\ & \qquad \def\mathdef3661#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3661{(}~\def\mathdef3662#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3662{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3663#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3663{(}~\def\mathdef3664#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3664{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3665#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3665{)}~\def\mathdef3666#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3666{)} \\[1ex] & \def\mathdef3667#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3667{(}~\def\mathdef3668#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3668{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3669#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3669{(}~\def\mathdef3670#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3670{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3671#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3671{)}~~\dots~\def\mathdef3672#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3672{)} \quad\equiv \\ & \qquad \def\mathdef3673#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3673{(}~\def\mathdef3674#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3674{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3675#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3675{(}~\def\mathdef3676#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3676{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3677#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3677{)}~\def\mathdef3678#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3678{)}~~ \def\mathdef3679#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3679{(}~\def\mathdef3680#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3680{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3681#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3681{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\ \end{array}\end{split}\]

Note

The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a memory declaration can contain any number of exports, possibly followed by an import.

Globals

Global definitions can bind a symbolic global identifier.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{global} & \href{../text/modules.html#text-global}{\mathtt{global}}_I &::=& \def\mathdef3682#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3682{(}~\def\mathdef3683#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3683{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\mathdef3684#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3684{)} &\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\mathdef3414#1{{}}\mathdef3414{module field} & \def\mathdef3685#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3685{(}~\def\mathdef3686#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3686{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3687#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3687{(}~\def\mathdef3688#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3688{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3689#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3689{)}~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3690#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3690{)} \quad\equiv \\ & \qquad \def\mathdef3691#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3691{(}~\def\mathdef3692#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3692{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3693#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3693{(}~\def\mathdef3694#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3694{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3695#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3695{)}~\def\mathdef3696#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3696{)} \\[1ex] & \def\mathdef3697#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3697{(}~\def\mathdef3698#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3698{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3699#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3699{(}~\def\mathdef3700#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3700{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3701#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3701{)}~~\dots~\def\mathdef3702#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3702{)} \quad\equiv \\ & \qquad \def\mathdef3703#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3703{(}~\def\mathdef3704#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3704{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3705#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3705{(}~\def\mathdef3706#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3706{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3707#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3707{)}~\def\mathdef3708#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3708{)}~~ \def\mathdef3709#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3709{(}~\def\mathdef3710#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3710{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3711#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3711{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}) \\ \end{array}\end{split}\]

Note

The latter abbreviation can be applied repeatedly, if “\(\dots\)” contains additional export clauses. Consequently, a global declaration can contain any number of exports, possibly followed by an import.

Exports

The syntax for exports mirrors their abstract syntax directly.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{export} & \href{../text/modules.html#text-export}{\mathtt{export}}_I &::=& \def\mathdef3712#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3712{(}~\def\mathdef3713#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3713{export}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I~\def\mathdef3714#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3714{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~d \} \\ \def\mathdef3414#1{{}}\mathdef3414{export description} & \href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I &::=& \def\mathdef3715#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3715{(}~\def\mathdef3716#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3716{func}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3717#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3717{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x \\ &&|& \def\mathdef3718#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3718{(}~\def\mathdef3719#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3719{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I~\def\mathdef3720#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3720{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x \\ &&|& \def\mathdef3721#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3721{(}~\def\mathdef3722#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3722{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I~\def\mathdef3723#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3723{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x \\ &&|& \def\mathdef3724#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3724{(}~\def\mathdef3725#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3725{tag}~~x{:}\href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}_I~\def\mathdef3726#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3726{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{tag}}~x \\&&|& \def\mathdef3727#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3727{(}~\def\mathdef3728#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3728{global}~~x{:}\href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I~\def\mathdef3729#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3729{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{global}}~x \\ \end{array}\end{split}\]

Abbreviations

As an abbreviation, exports may also be specified inline with function, table, memory, tag definitions, or global definitions; see the respective sections.

Start Function

A start function is defined in terms of its index.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{start function} & \href{../text/modules.html#text-start}{\mathtt{start}}_I &::=& \def\mathdef3730#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3730{(}~\def\mathdef3731#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3731{start}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3732#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3732{)} &\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\mathdef3414#1{{}}\mathdef3414{element segment} & \href{../text/modules.html#text-elem}{\mathtt{elem}}_I &::=& \def\mathdef3733#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3733{(}~\def\mathdef3734#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3734{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3735#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3735{)} \\ &&& \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\mathdef3736#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3736{(}~\def\mathdef3737#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3737{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I~~\def\mathdef3738#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3738{(}~\def\mathdef3739#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3739{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3740#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3740{)}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3741#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3741{)} \\ &&& \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\mathdef3742#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3742{(}~\def\mathdef3743#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3743{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3744#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3744{declare}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3745#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3745{)} \\ &&& \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\mathdef3414#1{{}}\mathdef3414{element list} & \href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I &::=& 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}{\mathtt{elemexpr}}_I) \qquad\Rightarrow\quad ( \href{../syntax/modules.html#syntax-elem}{\mathsf{type}}~t, \href{../syntax/modules.html#syntax-elem}{\mathsf{init}}~y^\ast ) \\ \def\mathdef3414#1{{}}\mathdef3414{element expression} & \href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}_I &::=& \def\mathdef3746#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3746{(}~\def\mathdef3747#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3747{item}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3748#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3748{)} \quad\Rightarrow\quad e \\ \def\mathdef3414#1{{}}\mathdef3414{table use} & \href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I &::=& \def\mathdef3749#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3749{(}~\def\mathdef3750#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3750{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I ~\def\mathdef3751#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3751{)} \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\mathdef3414#1{{}}\mathdef3414{element offset} & \def\mathdef3752#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3752{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3753#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3753{)} &\equiv& \def\mathdef3754#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3754{(}~\def\mathdef3755#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3755{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3756#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3756{)} \\ \def\mathdef3414#1{{}}\mathdef3414{element item} & \def\mathdef3757#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3757{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3758#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3758{)} &\equiv& \def\mathdef3759#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3759{(}~\def\mathdef3760#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3760{item}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3761#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3761{)} \\ \end{array}\end{split}\]

Also, the element list may be written as just a sequence of function indices:

\[\begin{array}{llcll} \def\mathdef3414#1{{}}\mathdef3414{element list} & \def\mathdef3762#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3762{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I) &\equiv& \def\mathdef3763#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3763{funcref}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\def\mathdef3764#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3764{(}~\def\mathdef3765#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3765{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3766#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3766{)}) \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\mathdef3767#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3767{func}\) keyword can be omitted as well.

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{table use} & \epsilon &\equiv& \def\mathdef3768#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3768{(}~\def\mathdef3769#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3769{table}~~\def\mathdef3770#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3770{0}~\def\mathdef3771#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3771{)} \\ \def\mathdef3414#1{{}}\mathdef3414{element segment} & \def\mathdef3772#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3772{(}~\def\mathdef3773#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3773{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3774#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3774{(}~\def\mathdef3775#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3775{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3776#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3776{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3777#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3777{)} &\equiv& \def\mathdef3778#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3778{(}~\def\mathdef3779#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3779{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3780#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3780{(}~\def\mathdef3781#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3781{table}~~\def\mathdef3782#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3782{0}~\def\mathdef3783#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3783{)}~~\def\mathdef3784#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3784{(}~\def\mathdef3785#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3785{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3786#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3786{)}~~\def\mathdef3787#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3787{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3788#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3788{)} \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\mathdef3414#1{{}}\mathdef3414{data segment} & \href{../text/modules.html#text-data}{\mathtt{data}}_I &::=& \def\mathdef3789#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3789{(}~\def\mathdef3790#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3790{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3791#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3791{)} \\ &&& \qquad \Rightarrow\quad \{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{passive}} \} \\ &&|& \def\mathdef3792#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3792{(}~\def\mathdef3793#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3793{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I~~\def\mathdef3794#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3794{(}~\def\mathdef3795#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3795{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3796#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3796{)}~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3797#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3797{)} \\ &&& \qquad \Rightarrow\quad \{ \href{../syntax/modules.html#syntax-data}{\mathsf{init}}~b^\ast, \href{../syntax/modules.html#syntax-data}{\mathsf{mode}}~\href{../syntax/modules.html#syntax-datamode}{\mathsf{active}}~\{ \href{../syntax/modules.html#syntax-data}{\mathsf{memory}}~x', \href{../syntax/modules.html#syntax-data}{\mathsf{offset}}~e \} \} \\ \def\mathdef3414#1{{}}\mathdef3414{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\mathdef3414#1{{}}\mathdef3414{memory use} & \href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I &::=& \def\mathdef3798#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3798{(}~\def\mathdef3799#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3799{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I ~\def\mathdef3800#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3800{)} \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\mathdef3414#1{{}}\mathdef3414{data offset} & \def\mathdef3801#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3801{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3802#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3802{)} &\equiv& \def\mathdef3803#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3803{(}~\def\mathdef3804#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3804{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3805#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3805{)} \end{array}\]

Also, a memory use can be omitted, defaulting to \(\mathtt{0}\).

\[\begin{split}\begin{array}{llclll} \def\mathdef3414#1{{}}\mathdef3414{memory use} & \epsilon &\equiv& \def\mathdef3806#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3806{(}~\def\mathdef3807#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3807{memory}~~\def\mathdef3808#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3808{0}~\def\mathdef3809#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3809{)} \\ \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.

\[\begin{split}\begin{array}{lll} \def\mathdef3414#1{{}}\mathdef3414{module} & \href{../text/modules.html#text-module}{\mathtt{module}} & \begin{array}[t]{@{}cllll} ::=& \def\mathdef3810#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3810{(}~\def\mathdef3811#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3811{module}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(m{:}\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I)^\ast~\def\mathdef3812#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3812{)} \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\mathdef3414#1{{}}\mathdef3414{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{tt}{:}\href{../text/modules.html#text-tag}{\mathtt{tag}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{tags}}~\mathit{tt}\} \\ |& \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

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, tag, 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\mathdef3813#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3813{(}~\def\mathdef3814#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3814{type}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef3815#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3815{)}) &=& \{\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\mathdef3816#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3816{(}~\def\mathdef3817#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3817{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3818#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3818{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3819#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3819{(}~\def\mathdef3820#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3820{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3821#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3821{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3822#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3822{(}~\def\mathdef3823#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3823{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3824#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3824{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3825#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3825{(}~\def\mathdef3826#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3826{tag}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3827#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3827{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tags}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3828#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3828{(}~\def\mathdef3829#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3829{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3830#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3830{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3831#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3831{(}~\def\mathdef3832#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3832{elem}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3833#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3833{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{elem}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3834#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3834{(}~\def\mathdef3835#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3835{data}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3836#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3836{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{data}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3837#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3837{(}~\def\mathdef3838#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3838{import}~\dots~\def\mathdef3839#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3839{(}~\def\mathdef3840#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3840{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3841#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3841{)}~\def\mathdef3842#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3842{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3843#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3843{(}~\def\mathdef3844#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3844{import}~\dots~\def\mathdef3845#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3845{(}~\def\mathdef3846#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3846{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3847#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3847{)}~\def\mathdef3848#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3848{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3849#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3849{(}~\def\mathdef3850#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3850{import}~\dots~\def\mathdef3851#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3851{(}~\def\mathdef3852#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3852{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3853#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3853{)}~\def\mathdef3854#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3854{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3855#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3855{(}~\def\mathdef3856#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3856{import}~\dots~\def\mathdef3857#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3857{(}~\def\mathdef3858#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3858{tag}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3859#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3859{)}~\def\mathdef3860#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3860{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tags}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3861#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3861{(}~\def\mathdef3862#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3862{import}~\dots~\def\mathdef3863#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3863{(}~\def\mathdef3864#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3864{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3865#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3865{)}~\def\mathdef3866#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3866{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3867#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3867{(}~\dots~\def\mathdef3868#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3868{)}) &=& \{\} \\ \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\mathdef3414#1{{}}\mathdef3414{module} & \href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast &\equiv& \def\mathdef3869#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3869{(}~\def\mathdef3870#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3870{module}~~\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast~\def\mathdef3871#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3871{)} \end{array}\]