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\mathdef3586#1{{}}\mathdef3586{type index} & \href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{function index} & \href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{table index} & \href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{memory index} & \href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{global index} & \href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{tag index} & \href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{element index} & \href{../text/modules.html#text-elemidx}{\mathtt{elemidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{data index} & \href{../text/modules.html#text-dataidx}{\mathtt{dataidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{local index} & \href{../text/modules.html#text-localidx}{\mathtt{localidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\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\mathdef3586#1{{}}\mathdef3586{label index} & \href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I &::=& l{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\mathtt{32}}} &\Rightarrow& l \\&&|& v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& l & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{labels}}[l] = v) \\ \def\mathdef3586#1{{}}\mathdef3586{field index} & \href{../text/modules.html#text-fieldidx}{\mathtt{fieldidx}}_{I,x} &::=& i{:}\href{../text/values.html#text-int}{\def\mathdef3616#1{{\mathtt{u}#1}}\mathdef3616{\mathtt{32}}} &\Rightarrow& i \\&&|& v{:}\href{../text/values.html#text-id}{\mathtt{id}} &\Rightarrow& i & (\mathrel{\mbox{if}} I.\href{../text/conventions.html#text-context}{\mathsf{fields}}[x][i] = v) \\ \end{array}\end{split}\]

Type Uses

A type use is a reference to a function type definition. It may optionally be augmented by explicit inlined parameter and result declarations. That allows binding symbolic identifiers to name the local indices of parameters. If inline declarations are given, then their types must match the referenced function type.

\[\begin{split}\begin{array}{llcllll} \def\mathdef3586#1{{}}\mathdef3586{type use} & \href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I &::=& \def\mathdef3630#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3630{(}~\def\mathdef3631#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3631{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3632#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3632{)} \quad\Rightarrow\quad x, I' \\ &&& \qquad (\mathrel{\mbox{if}} \begin{array}[t]{@{}l@{}} I.\href{../text/conventions.html#text-context}{\mathsf{typedefs}}[x] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}~(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^n] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]) \wedge I' = \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~(\epsilon)^n\}) \\ \end{array} \\[1ex] &&|& \def\mathdef3633#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3633{(}~\def\mathdef3634#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3634{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3635#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3635{)} ~~(t_1{:}\href{../text/types.html#text-functype}{\mathtt{param}})^\ast~~(t_2{:}\href{../text/types.html#text-functype}{\mathtt{result}})^\ast \quad\Rightarrow\quad x, I' \\ &&& \qquad (\mathrel{\mbox{if}} \begin{array}[t]{@{}l@{}} I.\href{../text/conventions.html#text-context}{\mathsf{typedefs}}[x] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}~(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]) \wedge I' = \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~\mathrm{id}(\href{../text/types.html#text-functype}{\mathtt{param}})^\ast\} ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\ \end{array} \\ \end{array}\end{split}\]

Note

If inline declarations are given, their types must be syntactically equal to the types from the indexed definition; possible type substitutions from other definitions that might make them equal are not taken into account. This is to simplify syntactic pre-processing.

The synthesized attribute of a \(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\) is a pair consisting of both the used type index and the local identifier context containing possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:

\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l} \mathrm{id}(\def\mathdef3636#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3636{(}~\def\mathdef3637#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3637{param}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3638#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3638{)}) &=& \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\mathdef3586#1{{}}\mathdef3586{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\mathdef3639#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3639{(}~\def\mathdef3640#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3640{type}~~x~\def\mathdef3641#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3641{)}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast \\ \end{array}\end{split}\]

where \(x\) is the smallest existing type index whose recursive type definition in the current module is of the form

\[\def\mathdef3642#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3642{(}~\def\mathdef3643#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3643{rec}~\def\mathdef3644#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3644{(}~\def\mathdef3645#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3645{type}~\def\mathdef3646#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3646{(}~\def\mathdef3647#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3647{sub}~\def\mathdef3648#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3648{final}~~\def\mathdef3649#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3649{(}~\def\mathdef3650#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3650{func}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast~\def\mathdef3651#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3651{)}~\def\mathdef3652#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3652{)}~\def\mathdef3653#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3653{)}~\def\mathdef3654#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3654{)}\]

If no such index exists, then a new recursive type of the same form is inserted at the end of the module.

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

Imports

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

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{import} & \href{../text/modules.html#text-import}{\mathtt{import}}_I &::=& \def\mathdef3655#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3655{(}~\def\mathdef3656#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3656{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\mathdef3657#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3657{)} \\ &&& \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\mathdef3586#1{{}}\mathdef3586{import description} & \href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I &::=& \def\mathdef3658#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3658{(}~\def\mathdef3659#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3659{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef3660#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3660{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x \\ &&|& \def\mathdef3661#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3661{(}~\def\mathdef3662#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3662{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}_I~\def\mathdef3663#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3663{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\mathit{tt} \\ &&|& \def\mathdef3664#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3664{(}~\def\mathdef3665#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3665{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}_I~\def\mathdef3666#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3666{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~~\mathit{mt} \\ &&|& \def\mathdef3667#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3667{(}~\def\mathdef3668#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3668{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}_I~\def\mathdef3669#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3669{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\mathit{gt} \\ &&|& \def\mathdef3670#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3670{(}~\def\mathdef3671#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3671{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/modules.html#text-tag}{\mathtt{tag}}~\def\mathdef3672#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3672{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{tag}}~\mathit{tt} \\ \end{array}\end{split}\]

Abbreviations

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

Functions

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

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{function} & \href{../text/modules.html#text-func}{\mathtt{func}}_I &::=& \def\mathdef3673#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3673{(}~\def\mathdef3674#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3674{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~~ (\mathit{loc}{:}\href{../text/modules.html#text-local}{\mathtt{local}}_I)^\ast~~(\mathit{in}{:}\href{../text/instructions.html#text-instr}{\mathtt{instr}}_{I''})^\ast~\def\mathdef3675#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3675{)} \\ &&& \qquad \Rightarrow\quad \{ \href{../syntax/modules.html#syntax-func}{\mathsf{type}}~x, \href{../syntax/modules.html#syntax-func}{\mathsf{locals}}~\mathit{loc}^\ast, \href{../syntax/modules.html#syntax-func}{\mathsf{body}}~\mathit{in}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \} \\ &&& \qquad\qquad\qquad (\mathrel{\mbox{if}} I'' = I \href{../syntax/conventions.html#notation-compose}{\oplus} I' \href{../syntax/conventions.html#notation-compose}{\oplus} \{\href{../text/conventions.html#text-context}{\mathsf{locals}}~\mathrm{id}(\href{../text/modules.html#text-local}{\mathtt{local}})^\ast\} ~\href{../text/conventions.html#text-context-wf}{\mbox{well-formed}}) \\[1ex] \def\mathdef3586#1{{}}\mathdef3586{local} & \href{../text/modules.html#text-local}{\mathtt{local}}_I &::=& \def\mathdef3676#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3676{(}~\def\mathdef3677#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3677{local}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~t{:}\href{../text/types.html#text-valtype}{\mathtt{valtype}}_I~\def\mathdef3678#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3678{)} \quad\Rightarrow\quad \{ \href{../syntax/modules.html#syntax-local}{\mathsf{type}}~t \} \\ \end{array}\end{split}\]

The definition of the local identifier context \(I''\) uses the following auxiliary function to extract optional identifiers from locals:

\[\begin{split}\begin{array}{lcl@{\qquad\qquad}l} \mathrm{id}(\def\mathdef3679#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3679{(}~\def\mathdef3680#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3680{local}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3681#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3681{)}) &=& \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\mathdef3586#1{{}}\mathdef3586{local} & \def\mathdef3682#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3682{(}~~\def\mathdef3683#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3683{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}^\ast~~\def\mathdef3684#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3684{)} &\equiv& (\def\mathdef3685#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3685{(}~~\def\mathdef3686#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3686{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}~~\def\mathdef3687#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3687{)})^\ast \\ \end{array}\end{split}\]

Functions can be defined as imports or exports inline:

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3688#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3688{(}~\def\mathdef3689#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3689{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3690#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3690{(}~\def\mathdef3691#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3691{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3692#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3692{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3693#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3693{)} \quad\equiv \\ & \qquad \def\mathdef3694#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3694{(}~\def\mathdef3695#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3695{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3696#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3696{(}~\def\mathdef3697#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3697{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3698#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3698{)}~\def\mathdef3699#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3699{)} \\[1ex] & \def\mathdef3700#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3700{(}~\def\mathdef3701#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3701{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3702#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3702{(}~\def\mathdef3703#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3703{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3704#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3704{)}~~\dots~\def\mathdef3705#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3705{)} \quad\equiv \\ & \qquad \def\mathdef3706#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3706{(}~\def\mathdef3707#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3707{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3708#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3708{(}~\def\mathdef3709#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3709{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3710#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3710{)}~\def\mathdef3711#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3711{)}~~ \def\mathdef3712#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3712{(}~\def\mathdef3713#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3713{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3714#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3714{)} \\ & \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\mathdef3586#1{{}}\mathdef3586{table} & \href{../text/modules.html#text-table}{\mathtt{table}}_I &::=& \def\mathdef3715#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3715{(}~\def\mathdef3716#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3716{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}_I~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3717#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3717{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\mathit{tt}, \href{../syntax/modules.html#syntax-table}{\mathsf{init}}~e \} \\ \end{array}\end{split}\]

Abbreviations

A table’s initialization expression can be omitted, in which case it defaults to \(\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}\):

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3718#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3718{(}~\def\mathdef3719#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3719{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3720#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3720{)} &\equiv& \def\mathdef3721#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3721{(}~\def\mathdef3722#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3722{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~~\def\mathdef3723#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3723{(}~\href{../syntax/instructions.html#syntax-instr-ref}{\mathsf{ref{.}null}}~\mathit{ht}~\def\mathdef3724#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3724{)}~\def\mathdef3725#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3725{)} \\ &&& \qquad\qquad (\mathrel{\mbox{if}} \href{../text/types.html#text-tabletype}{\mathtt{tabletype}} = \href{../text/types.html#text-limits}{\mathtt{limits}}~\def\mathdef3726#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3726{(}~\def\mathdef3727#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3727{ref}~\def\mathdef3728#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3728{null}^?~\mathit{ht}~\def\mathdef3729#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3729{)}) \\ \end{array}\end{split}\]

An element segment can be given inline with a table definition, in which case its offset is \(0\) and the limits of the table type are inferred from the length of the given segment:

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3730#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3730{(}~\def\mathdef3731#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3731{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3732#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3732{(}~\def\mathdef3733#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3733{elem}~~\href{../syntax/instructions.html#syntax-expr}{\mathit{expr}}^n{:}\href{../text/conventions.html#text-list}{\mathtt{list}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef3734#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3734{)}~\def\mathdef3735#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3735{)} \quad\equiv \\ & \qquad \def\mathdef3736#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3736{(}~\def\mathdef3737#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3737{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3738#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3738{)} \\ & \qquad \def\mathdef3739#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3739{(}~\def\mathdef3740#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3740{elem}~~\def\mathdef3741#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3741{(}~\def\mathdef3742#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3742{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3743#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3743{)}~~\def\mathdef3744#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3744{(}~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}'\def\mathdef3745#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3745{.const}~~\def\mathdef3746#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3746{0}~\def\mathdef3747#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3747{)}~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\href{../text/conventions.html#text-list}{\mathtt{list}}(\href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}})~\def\mathdef3748#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3748{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, \\ & \qquad\qquad \mathrel{\mbox{if}} \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}? \neq \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? \vee \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? = \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \def\mathdef3749#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3749{i32}) \\ \end{array}\end{split}\]
\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3750#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3750{(}~\def\mathdef3751#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3751{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3752#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3752{(}~\def\mathdef3753#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3753{elem}~~x^n{:}\href{../text/conventions.html#text-list}{\mathtt{list}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef3754#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3754{)}~\def\mathdef3755#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3755{)} \quad\equiv \\ & \qquad \def\mathdef3756#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3756{(}~\def\mathdef3757#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3757{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3758#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3758{)} \\ & \qquad \def\mathdef3759#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3759{(}~\def\mathdef3760#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3760{elem}~~\def\mathdef3761#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3761{(}~\def\mathdef3762#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3762{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3763#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3763{)}~~\def\mathdef3764#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3764{(}~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}'\def\mathdef3765#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3765{.const}~~\def\mathdef3766#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3766{0}~\def\mathdef3767#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3767{)}~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\href{../text/conventions.html#text-list}{\mathtt{list}}(\def\mathdef3768#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3768{(}~\def\mathdef3769#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3769{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}~\def\mathdef3770#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3770{)})~\def\mathdef3771#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3771{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, \\ & \qquad\qquad \mathrel{\mbox{if}} \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}? \neq \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? \vee \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? = \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \def\mathdef3772#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3772{i32}) \\ \end{array}\end{split}\]

Tables can be defined as imports or exports inline:

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3773#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3773{(}~\def\mathdef3774#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3774{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3775#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3775{(}~\def\mathdef3776#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3776{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3777#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3777{)}~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3778#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3778{)} \quad\equiv \\ & \qquad \def\mathdef3779#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3779{(}~\def\mathdef3780#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3780{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3781#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3781{(}~\def\mathdef3782#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3782{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3783#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3783{)}~\def\mathdef3784#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3784{)} \\[1ex] & \def\mathdef3785#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3785{(}~\def\mathdef3786#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3786{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3787#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3787{(}~\def\mathdef3788#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3788{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3789#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3789{)}~~\dots~\def\mathdef3790#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3790{)} \quad\equiv \\ & \qquad \def\mathdef3791#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3791{(}~\def\mathdef3792#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3792{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3793#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3793{(}~\def\mathdef3794#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3794{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3795#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3795{)}~\def\mathdef3796#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3796{)}~~ \def\mathdef3797#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3797{(}~\def\mathdef3798#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3798{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3799#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3799{)} \\ & \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\mathdef3586#1{{}}\mathdef3586{memory} & \href{../text/modules.html#text-mem}{\mathtt{mem}}_I &::=& \def\mathdef3800#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3800{(}~\def\mathdef3801#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3801{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}_I~\def\mathdef3802#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3802{)} &\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\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3803#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3803{(}~\def\mathdef3804#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3804{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~\def\mathdef3805#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3805{(}~\def\mathdef3806#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3806{data}~~b^n{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3807#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3807{)}~~\def\mathdef3808#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3808{)} \quad\equiv \\ & \qquad \def\mathdef3809#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3809{(}~\def\mathdef3810#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3810{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^?~~m~~m~\def\mathdef3811#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3811{)} \\ & \qquad \def\mathdef3812#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3812{(}~\def\mathdef3813#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3813{data}~~\def\mathdef3814#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3814{(}~\def\mathdef3815#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3815{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3816#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3816{)}~~\def\mathdef3817#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3817{(}~\href{../text/types.html#text-addrtype}{\mathtt{addrtype}}'\def\mathdef3818#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3818{.const}~~\def\mathdef3819#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3819{0}~\def\mathdef3820#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3820{)}~~\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3821#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3821{)} \\ & \qquad\qquad (\mathrel{\mbox{if}} \href{../text/values.html#text-id}{\mathtt{id}}^? \neq \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' = \href{../text/values.html#text-id}{\mathtt{id}}^? \vee \href{../text/values.html#text-id}{\mathtt{id}}^? = \epsilon \wedge \href{../text/values.html#text-id}{\mathtt{id}}' ~\href{../text/values.html#text-id-fresh}{\mbox{fresh}}, \\ & \qquad\qquad \mathrel{\mbox{if}} \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}? \neq \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? \vee \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}^? = \epsilon \wedge \href{../text/types.html#text-addrtype}{\mathtt{addrtype}}' = \def\mathdef3822#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3822{i32}, \\ & \qquad\qquad m = \mathrm{ceil}(n / 64\,\mathrm{Ki})) \\ \end{array}\end{split}\]

Memories can be defined as imports or exports inline:

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3823#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3823{(}~\def\mathdef3824#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3824{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3825#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3825{(}~\def\mathdef3826#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3826{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3827#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3827{)}~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3828#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3828{)} \quad\equiv \\ & \qquad \def\mathdef3829#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3829{(}~\def\mathdef3830#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3830{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3831#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3831{(}~\def\mathdef3832#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3832{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3833#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3833{)}~\def\mathdef3834#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3834{)} \\[1ex] & \def\mathdef3835#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3835{(}~\def\mathdef3836#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3836{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3837#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3837{(}~\def\mathdef3838#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3838{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3839#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3839{)}~~\dots~\def\mathdef3840#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3840{)} \quad\equiv \\ & \qquad \def\mathdef3841#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3841{(}~\def\mathdef3842#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3842{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3843#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3843{(}~\def\mathdef3844#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3844{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3845#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3845{)}~\def\mathdef3846#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3846{)}~~ \def\mathdef3847#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3847{(}~\def\mathdef3848#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3848{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3849#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3849{)} \\ & \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\mathdef3586#1{{}}\mathdef3586{global} & \href{../text/modules.html#text-global}{\mathtt{global}}_I &::=& \def\mathdef3850#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3850{(}~\def\mathdef3851#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3851{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}_I~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3852#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3852{)} &\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\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3853#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3853{(}~\def\mathdef3854#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3854{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3855#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3855{(}~\def\mathdef3856#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3856{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3857#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3857{)}~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3858#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3858{)} \quad\equiv \\ & \qquad \def\mathdef3859#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3859{(}~\def\mathdef3860#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3860{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3861#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3861{(}~\def\mathdef3862#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3862{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3863#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3863{)}~\def\mathdef3864#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3864{)} \\[1ex] & \def\mathdef3865#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3865{(}~\def\mathdef3866#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3866{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3867#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3867{(}~\def\mathdef3868#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3868{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3869#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3869{)}~~\dots~\def\mathdef3870#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3870{)} \quad\equiv \\ & \qquad \def\mathdef3871#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3871{(}~\def\mathdef3872#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3872{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3873#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3873{(}~\def\mathdef3874#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3874{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3875#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3875{)}~\def\mathdef3876#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3876{)}~~ \def\mathdef3877#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3877{(}~\def\mathdef3878#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3878{global}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3879#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3879{)} \\ & \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.

Tags

An tag definition can bind a symbolic tag identifier.

\[\begin{split}\begin{array}{llcl} \def\mathdef3586#1{{}}\mathdef3586{tag} & \href{../text/modules.html#text-tag}{\mathtt{tag}}_I &::=& \def\mathdef3880#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3880{(}~\def\mathdef3881#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3881{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef3882#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3882{)} \\ &&& \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\mathdef3586#1{{}}\mathdef3586{module field} & \def\mathdef3883#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3883{(}~\def\mathdef3884#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3884{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3885#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3885{(}~\def\mathdef3886#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3886{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3887#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3887{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3888#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3888{)} \quad\equiv \\ & \qquad \def\mathdef3889#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3889{(}~\def\mathdef3890#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3890{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3891#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3891{(}~\def\mathdef3892#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3892{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3893#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3893{)}~\def\mathdef3894#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3894{)} \\[1ex] & \def\mathdef3895#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3895{(}~\def\mathdef3896#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3896{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3897#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3897{(}~\def\mathdef3898#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3898{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3899#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3899{)}~~\dots~\def\mathdef3900#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3900{)} \quad\equiv \\ & \qquad \def\mathdef3901#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3901{(}~\def\mathdef3902#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3902{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3903#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3903{(}~\def\mathdef3904#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3904{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3905#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3905{)}~\def\mathdef3906#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3906{)}~~ \def\mathdef3907#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3907{(}~\def\mathdef3908#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3908{tag}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3909#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3909{)} \\ & \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.

Exports

The syntax for exports mirrors their abstract syntax directly.

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{export} & \href{../text/modules.html#text-export}{\mathtt{export}}_I &::=& \def\mathdef3910#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3910{(}~\def\mathdef3911#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3911{export}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{name}}~~d{:}\href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I~\def\mathdef3912#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3912{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-export}{\mathsf{name}}~\mathit{nm}, \href{../syntax/modules.html#syntax-export}{\mathsf{desc}}~d \} \\ \def\mathdef3586#1{{}}\mathdef3586{export description} & \href{../text/modules.html#text-exportdesc}{\mathtt{exportdesc}}_I &::=& \def\mathdef3913#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3913{(}~\def\mathdef3914#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3914{func}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3915#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3915{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{func}}~x \\ &&|& \def\mathdef3916#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3916{(}~\def\mathdef3917#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3917{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I~\def\mathdef3918#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3918{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{table}}~x \\ &&|& \def\mathdef3919#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3919{(}~\def\mathdef3920#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3920{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I~\def\mathdef3921#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3921{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{mem}}~x \\ &&|& \def\mathdef3922#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3922{(}~\def\mathdef3923#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3923{global}~~x{:}\href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I~\def\mathdef3924#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3924{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{global}}~x \\&&|& \def\mathdef3925#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3925{(}~\def\mathdef3926#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3926{tag}~~x{:}\href{../text/modules.html#text-tagidx}{\mathtt{tagidx}}_I~\def\mathdef3927#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3927{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{tag}}~x \\ \end{array}\end{split}\]

Abbreviations

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

Start Function

A start function is defined in terms of its index.

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{start function} & \href{../text/modules.html#text-start}{\mathtt{start}}_I &::=& \def\mathdef3928#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3928{(}~\def\mathdef3929#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3929{start}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3930#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3930{)} &\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\mathdef3586#1{{}}\mathdef3586{element segment} & \href{../text/modules.html#text-elem}{\mathtt{elem}}_I &::=& \def\mathdef3931#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3931{(}~\def\mathdef3932#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3932{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3933#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3933{)} \\ &&& \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\mathdef3934#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3934{(}~\def\mathdef3935#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3935{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I~~\def\mathdef3936#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3936{(}~\def\mathdef3937#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3937{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3938#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3938{)}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3939#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3939{)} \\ &&& \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\mathdef3940#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3940{(}~\def\mathdef3941#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3941{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3942#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3942{declare}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I~\def\mathdef3943#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3943{)} \\ &&& \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{declare}} \} \\ \def\mathdef3586#1{{}}\mathdef3586{element list} & \href{../text/modules.html#text-elemlist}{\mathtt{elemlist}}_I &::=& t{:}\href{../text/types.html#text-reftype}{\mathtt{reftype}}_I~~y^\ast{:}\href{../text/conventions.html#text-list}{\mathtt{list}}(\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\mathdef3586#1{{}}\mathdef3586{element expression} & \href{../text/modules.html#text-elemexpr}{\mathtt{elemexpr}}_I &::=& \def\mathdef3944#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3944{(}~\def\mathdef3945#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3945{item}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3946#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3946{)} \quad\Rightarrow\quad e \\ \def\mathdef3586#1{{}}\mathdef3586{table use} & \href{../text/modules.html#text-tableuse}{\mathtt{tableuse}}_I &::=& \def\mathdef3947#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3947{(}~\def\mathdef3948#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3948{table}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I ~\def\mathdef3949#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3949{)} \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\mathdef3586#1{{}}\mathdef3586{element offset} & \def\mathdef3950#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3950{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3951#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3951{)} &\equiv& \def\mathdef3952#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3952{(}~\def\mathdef3953#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3953{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3954#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3954{)} \\ \def\mathdef3586#1{{}}\mathdef3586{element item} & \def\mathdef3955#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3955{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3956#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3956{)} &\equiv& \def\mathdef3957#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3957{(}~\def\mathdef3958#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3958{item}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3959#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3959{)} \\ \end{array}\end{split}\]

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

\[\begin{array}{llcll} \def\mathdef3586#1{{}}\mathdef3586{element list} & \def\mathdef3960#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3960{func}~~\href{../text/conventions.html#text-list}{\mathtt{list}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I) &\equiv& \def\mathdef3961#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3961{(ref}~\def\mathdef3962#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3962{func)}~~\href{../text/conventions.html#text-list}{\mathtt{list}}(\def\mathdef3963#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3963{(}~\def\mathdef3964#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3964{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3965#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3965{)}) \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\mathdef3966#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3966{func}\) keyword can be omitted as well.

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{table use} & \epsilon &\equiv& \def\mathdef3967#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3967{(}~\def\mathdef3968#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3968{table}~~\def\mathdef3969#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3969{0}~\def\mathdef3970#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3970{)} \\ \def\mathdef3586#1{{}}\mathdef3586{element segment} & \def\mathdef3971#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3971{(}~\def\mathdef3972#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3972{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3973#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3973{(}~\def\mathdef3974#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3974{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3975#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3975{)}~~\href{../text/conventions.html#text-list}{\mathtt{list}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3976#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3976{)} &\equiv& \def\mathdef3977#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3977{(}~\def\mathdef3978#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3978{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3979#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3979{(}~\def\mathdef3980#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3980{table}~~\def\mathdef3981#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3981{0}~\def\mathdef3982#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3982{)}~~\def\mathdef3983#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3983{(}~\def\mathdef3984#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3984{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3985#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3985{)}~~\def\mathdef3986#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3986{func}~~\href{../text/conventions.html#text-list}{\mathtt{list}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3987#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3987{)} \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\mathdef3586#1{{}}\mathdef3586{data segment} & \href{../text/modules.html#text-data}{\mathtt{data}}_I &::=& \def\mathdef3988#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3988{(}~\def\mathdef3989#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3989{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3990#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3990{)} \\ &&& \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\mathdef3991#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3991{(}~\def\mathdef3992#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3992{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I~~\def\mathdef3993#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3993{(}~\def\mathdef3994#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3994{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3995#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3995{)}~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3996#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3996{)} \\ &&& \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\mathdef3586#1{{}}\mathdef3586{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}{\bigoplus}((b^\ast)^\ast) \\ \def\mathdef3586#1{{}}\mathdef3586{memory use} & \href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I &::=& \def\mathdef3997#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3997{(}~\def\mathdef3998#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3998{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I ~\def\mathdef3999#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3999{)} \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\mathdef3586#1{{}}\mathdef3586{data offset} & \def\mathdef4000#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4000{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4001#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4001{)} &\equiv& \def\mathdef4002#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4002{(}~\def\mathdef4003#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4003{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef4004#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4004{)} \end{array}\]

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

\[\begin{split}\begin{array}{llclll} \def\mathdef3586#1{{}}\mathdef3586{memory use} & \epsilon &\equiv& \def\mathdef4005#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4005{(}~\def\mathdef4006#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4006{memory}~~\def\mathdef4007#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4007{0}~\def\mathdef4008#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4008{)} \\ \end{array}\end{split}\]

As another abbreviation, data segments may also be specified inline with memory definitions; see the respective section.

Modules

A module consists of a sequence of fields that can occur in any order. All definitions and their respective bound identifiers scope over the entire module, including the text preceding them.

A module may optionally bind an identifier that names the module. The name serves a documentary role only.

Note

Tools may include the module name in the name section of the binary format.

\[\begin{split}\begin{array}{lll} \def\mathdef3586#1{{}}\mathdef3586{module} & \href{../text/modules.html#text-module}{\mathtt{module}} & \begin{array}[t]{@{}cllll} ::=& \def\mathdef4009#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4009{(}~\def\mathdef4010#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4010{module}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(m{:}\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I)^\ast~\def\mathdef4011#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4011{)} \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\mathdef3586#1{{}}\mathdef3586{module field} & \href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}_I & \begin{array}[t]{@{}clll} ::=& \mathit{ty}^\ast{:}\href{../text/types.html#text-rectype}{\mathtt{rectype}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{types}}~\mathit{ty}^\ast\} \\ |& \mathit{im}{:}\href{../text/modules.html#text-import}{\mathtt{import}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{imports}}~\mathit{im}\} \\ |& \mathit{fn}{:}\href{../text/modules.html#text-func}{\mathtt{func}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}}~\mathit{fn}\} \\ |& \mathit{ta}{:}\href{../text/modules.html#text-table}{\mathtt{table}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{tables}}~\mathit{ta}\} \\ |& \mathit{me}{:}\href{../text/modules.html#text-mem}{\mathtt{mem}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{mems}}~\mathit{me}\} \\ |& \mathit{gl}{:}\href{../text/modules.html#text-global}{\mathtt{global}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{globals}}~\mathit{gl}\} \\ |& \mathit{tg}{:}\href{../text/modules.html#text-tag}{\mathtt{tag}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{tags}}~\mathit{tg}\} \\ |& \mathit{el}{:}\href{../text/modules.html#text-elem}{\mathtt{elem}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{elems}}~\mathit{el}\} \\ |& \mathit{da}{:}\href{../text/modules.html#text-data}{\mathtt{data}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{datas}}~\mathit{da}\} \\ |& \mathit{st}{:}\href{../text/modules.html#text-start}{\mathtt{start}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{start}}~\mathit{st}\} \\ |& \mathit{ex}{:}\href{../text/modules.html#text-export}{\mathtt{export}}_I &\Rightarrow& \{\href{../syntax/modules.html#syntax-module}{\mathsf{exports}}~\mathit{ex}\} \\ \end{array} \end{array}\end{split}\]

The following restrictions are imposed on the composition of modules: \(m_1 \href{../syntax/conventions.html#notation-compose}{\oplus} m_2\) is defined if and only if

  • \(m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon \vee m_2.\href{../syntax/modules.html#syntax-module}{\mathsf{start}} = \epsilon\)

  • \(m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{funcs}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{tables}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{mems}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{globals}} = m_1.\href{../syntax/modules.html#syntax-module}{\mathsf{tags}} = \epsilon \vee m_2.\href{../syntax/modules.html#syntax-module}{\mathsf{imports}} = \epsilon\)

Note

The first condition ensures that there is at most one start function. The second condition enforces that all imports must occur before any regular definition of a function, table, memory, global, or tag, thereby maintaining the ordering of the respective index spaces.

The well-formedness condition on \(I\) in the grammar for \(\href{../text/modules.html#text-module}{\mathtt{module}}\) ensures that no namespace contains duplicate identifiers.

The definition of the initial identifier context \(I\) uses the following auxiliary definition which maps each relevant definition to a singular context with one (possibly empty) identifier:

\[\begin{split}\begin{array}{@{}lcl@{\qquad\qquad}l} \mathrm{idc}(\def\mathdef4012#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4012{(}~\def\mathdef4013#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4013{rec}~~\href{../text/types.html#text-typedef}{\mathtt{typedef}}^\ast~\def\mathdef4014#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4014{)}) &=& \href{../syntax/conventions.html#notation-compose}{\bigoplus} \mathrm{idc}(\href{../text/types.html#text-typedef}{\mathtt{typedef}})^\ast \\ \mathrm{idc}(\def\mathdef4015#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4015{(}~\def\mathdef4016#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4016{type}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\href{../text/types.html#text-subtype}{\mathtt{subtype}}~\def\mathdef4017#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4017{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{types}}~(v^?), \href{../text/conventions.html#text-context}{\mathsf{fields}}~\mathrm{idf}(\href{../text/types.html#text-subtype}{\mathtt{subtype}}), \href{../text/conventions.html#text-context}{\mathsf{typedefs}}~\mathit{st}\} \\ \mathrm{idc}(\def\mathdef4018#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4018{(}~\def\mathdef4019#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4019{func}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4020#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4020{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4021#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4021{(}~\def\mathdef4022#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4022{table}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4023#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4023{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4024#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4024{(}~\def\mathdef4025#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4025{memory}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4026#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4026{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4027#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4027{(}~\def\mathdef4028#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4028{global}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4029#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4029{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4030#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4030{(}~\def\mathdef4031#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4031{tag}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4032#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4032{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tags}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4033#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4033{(}~\def\mathdef4034#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4034{elem}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4035#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4035{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{elem}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4036#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4036{(}~\def\mathdef4037#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4037{data}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4038#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4038{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{data}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4039#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4039{(}~\def\mathdef4040#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4040{import}~\dots~\def\mathdef4041#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4041{(}~\def\mathdef4042#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4042{func}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4043#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4043{)}~\def\mathdef4044#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4044{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4045#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4045{(}~\def\mathdef4046#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4046{import}~\dots~\def\mathdef4047#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4047{(}~\def\mathdef4048#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4048{table}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4049#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4049{)}~\def\mathdef4050#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4050{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4051#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4051{(}~\def\mathdef4052#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4052{import}~\dots~\def\mathdef4053#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4053{(}~\def\mathdef4054#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4054{memory}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4055#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4055{)}~\def\mathdef4056#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4056{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4057#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4057{(}~\def\mathdef4058#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4058{import}~\dots~\def\mathdef4059#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4059{(}~\def\mathdef4060#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4060{global}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4061#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4061{)}~\def\mathdef4062#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4062{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(v^?)\} \\ \mathrm{idc}(\def\mathdef4063#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4063{(}~\dots~\def\mathdef4064#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4064{)}) &=& \{\} \\[2ex] \mathrm{idf}(\def\mathdef4065#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4065{(}~\def\mathdef4066#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4066{sub}~\dots~\href{../text/types.html#text-comptype}{\mathtt{comptype}}~\def\mathdef4067#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4067{)}) &=& \mathrm{idf}(\href{../text/types.html#text-comptype}{\mathtt{comptype}}) \\ \mathrm{idf}(\def\mathdef4068#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4068{(}~\def\mathdef4069#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4069{struct}~\mathit{Tfield}^\ast~\def\mathdef4070#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4070{)}) &=& \href{../syntax/conventions.html#notation-compose}{\bigoplus} \mathrm{idf}(\href{../text/types.html#text-structtype}{\mathtt{field}})^\ast \\ \mathrm{idf}(\def\mathdef4071#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4071{(}~\def\mathdef4072#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4072{array}~\dots~\def\mathdef4073#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4073{)}) &=& \epsilon \\ \mathrm{idf}(\def\mathdef4074#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4074{(}~\def\mathdef4075#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4075{func}~\dots~\def\mathdef4076#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4076{)}) &=& \epsilon \\ \mathrm{idf}(\def\mathdef4077#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4077{(}~\def\mathdef4078#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4078{field}~v^?{:}\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef4079#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4079{)}) &=& v^? \\ \end{array}\end{split}\]

Abbreviations

In a source file, the toplevel \(\mathtt{(module}~\dots\mathtt{)}\) surrounding the module body may be omitted.

\[\begin{array}{llcll} \def\mathdef3586#1{{}}\mathdef3586{module} & \href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast &\equiv& \def\mathdef4080#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4080{(}~\def\mathdef4081#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4081{module}~~\href{../text/modules.html#text-modulefield}{\mathtt{modulefield}}^\ast~\def\mathdef4082#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef4082{)} \end{array}\]