模块

索引

索引Indices 可以以原始数字形式或符号标识符形式给出,前提是它们被相应的结构绑定。此类标识符将在相应的标识符上下文\(I\)的空间中查找。

\[\begin{split}\begin{array}{llcllllllll} \def\mathdef3386#1{{}}\mathdef3386{类型索引} & \href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{函数索引} & \href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{表索引} & \href{../text/modules.html#text-tableidx}{\mathtt{tableidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{内存索引} & \href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{全局索引} & \href{../text/modules.html#text-globalidx}{\mathtt{globalidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{元素索引} & \href{../text/modules.html#text-elemidx}{\mathtt{elemidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{数据索引} & \href{../text/modules.html#text-dataidx}{\mathtt{dataidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{局部索引} & \href{../text/modules.html#text-localidx}{\mathtt{localidx}}_I &::=& x{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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\mathdef3386#1{{}}\mathdef3386{标签索引} & \href{../text/modules.html#text-labelidx}{\mathtt{labelidx}}_I &::=& l{:}\href{../text/values.html#text-int}{\def\mathdef3411#1{{\mathtt{u}#1}}\mathdef3411{\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}\]

类型

类型定义可以绑定一个符号类型标识符

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{类型定义} & \href{../text/modules.html#text-typedef}{\mathtt{type}} &::=& \def\mathdef3425#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3425{(}~\def\mathdef3426#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3426{type}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef3427#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3427{)} &\Rightarrow& \mathit{ft} \\ \end{array}\end{split}\]

类型使用

类型使用是对类型定义的引用。它可以选择性地用显式内联参数结果声明进行增强。这允许将符号标识符绑定到参数的局部索引。如果给出了内联声明,则它们的类型必须与引用的函数类型匹配。

\[\begin{split}\begin{array}{llcllll} \def\mathdef3386#1{{}}\mathdef3386{类型使用} & \href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I &::=& \def\mathdef3428#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3428{(}~\def\mathdef3429#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3429{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3430#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3430{)} \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\mathdef3431#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3431{(}~\def\mathdef3432#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3432{type}~~x{:}\href{../text/modules.html#text-typeidx}{\mathtt{typeidx}}_I~\def\mathdef3433#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3433{)} ~~(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}\]

\(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\)的合成属性是一个对,由使用的类型索引和包含可能参数标识符的局部标识符上下文组成。以下辅助函数从参数中提取可选标识符

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

注意

两种生成规则对于函数类型为\([] \href{../syntax/types.html#syntax-functype}{\rightarrow} []\)的情况重叠。但是,在这种情况下,它们也会产生相同的结果,因此选择无关紧要。

\(I'\)良构性条件确保参数不包含重复的标识符。

缩写

\(\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}\)也可以完全替换为内联参数结果声明。在这种情况下,会自动插入类型索引

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{类型使用} & (t_1{:}\href{../text/types.html#text-functype}{\mathtt{param}})^\ast~~(t_2{:}\href{../text/types.html#text-functype}{\mathtt{result}})^\ast &\equiv& \def\mathdef3437#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3437{(}~\def\mathdef3438#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3438{type}~~x~\def\mathdef3439#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3439{)}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast \\ \end{array}\end{split}\]

其中\(x\)是最小的现有类型索引,其在当前模块中的定义是函数类型\([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\)。如果没有这样的索引存在,则会创建一个新的类型定义,其形式为

\[\def\mathdef3440#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3440{(}~\def\mathdef3441#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3441{type}~~\def\mathdef3442#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3442{(}~\def\mathdef3443#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3443{func}~~\href{../text/types.html#text-functype}{\mathtt{param}}^\ast~~\href{../text/types.html#text-functype}{\mathtt{result}}^\ast~\def\mathdef3444#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3444{)}~\def\mathdef3445#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3445{)}\]

插入到模块的末尾。

缩写按其出现的顺序展开,以便先前插入的类型定义可以被后续的展开重用。

导入

导入中的描述符可以绑定符号函数、表、内存或全局标识符

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{导入} & \href{../text/modules.html#text-import}{\mathtt{import}}_I &::=& \def\mathdef3446#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3446{(}~\def\mathdef3447#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3447{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\mathdef3448#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3448{)} \\ &&& \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\mathdef3386#1{{}}\mathdef3386{导入描述} & \href{../text/modules.html#text-importdesc}{\mathtt{importdesc}}_I &::=& \def\mathdef3449#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3449{(}~\def\mathdef3450#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3450{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x,I'{:}\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}_I~\def\mathdef3451#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3451{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{func}}~x \\ &&|& \def\mathdef3452#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3452{(}~\def\mathdef3453#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3453{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3454#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3454{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{table}}~\mathit{tt} \\ &&|& \def\mathdef3455#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3455{(}~\def\mathdef3456#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3456{memory}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{mt}{:}\href{../text/types.html#text-memtype}{\mathtt{memtype}}~\def\mathdef3457#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3457{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{mem}}~~\mathit{mt} \\ &&|& \def\mathdef3458#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3458{(}~\def\mathdef3459#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3459{global}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{globaltype}}~\def\mathdef3460#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3460{)} &\Rightarrow& \href{../syntax/modules.html#syntax-importdesc}{\mathsf{global}}~\mathit{gt} \\ \end{array}\end{split}\]

缩写

作为缩写,导入也可以与函数内存全局定义内联指定;请参阅各自的部分。

函数

函数定义可以绑定符号函数标识符,以及其参数和局部的局部标识符

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{函数} & \href{../text/modules.html#text-func}{\mathtt{func}}_I &::=& \def\mathdef3461#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3461{(}~\def\mathdef3462#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3462{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\mathdef3463#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3463{)} \\ &&& \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{如果}} 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{格式良好}}) \\[1ex] \def\mathdef3386#1{{}}\mathdef3386{局部变量} & \href{../text/modules.html#text-local}{\mathtt{local}} &::=& \def\mathdef3464#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3464{(}~\def\mathdef3465#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3465{local}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~t{:}\href{../text/types.html#text-valtype}{\mathtt{valtype}}~\def\mathdef3466#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3466{)} \quad\Rightarrow\quad t \\ \end{array}\end{split}\]

局部变量的 标识符上下文 \(I''\) 的定义使用以下辅助函数从局部变量中提取可选标识符

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

注意

\(I''\)格式良好性 条件确保参数和局部变量不包含重复的标识符。

缩写

多个匿名局部变量可以合并到一个声明中

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{局部变量} & \def\mathdef3470#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3470{(}~~\def\mathdef3471#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3471{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}^\ast~~\def\mathdef3472#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3472{)} &\equiv& (\def\mathdef3473#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3473{(}~~\def\mathdef3474#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3474{local}~~\href{../text/types.html#text-valtype}{\mathtt{valtype}}~~\def\mathdef3475#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3475{)})^\ast \\ \end{array}\end{split}\]

函数可以定义为 导入导出 内联

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{模块字段} & \def\mathdef3476#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3476{(}~\def\mathdef3477#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3477{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3478#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3478{(}~\def\mathdef3479#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3479{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3480#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3480{)}~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3481#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3481{)} \quad\equiv \\ & \qquad \def\mathdef3482#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3482{(}~\def\mathdef3483#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3483{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3484#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3484{(}~\def\mathdef3485#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3485{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/modules.html#text-typeuse}{\mathtt{typeuse}}~\def\mathdef3486#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3486{)}~\def\mathdef3487#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3487{)} \\[1ex] & \def\mathdef3488#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3488{(}~\def\mathdef3489#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3489{func}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3490#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3490{(}~\def\mathdef3491#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3491{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3492#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3492{)}~~\dots~\def\mathdef3493#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3493{)} \quad\equiv \\ & \qquad \def\mathdef3494#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3494{(}~\def\mathdef3495#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3495{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3496#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3496{(}~\def\mathdef3497#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3497{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3498#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3498{)}~\def\mathdef3499#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3499{)}~~ \def\mathdef3500#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3500{(}~\def\mathdef3501#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3501{func}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3502#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3502{)} \\ & \qquad\qquad (\mathrel{\mbox{如果}} \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{新的}}) \\ \end{array}\end{split}\]

注意

如果“\(\dots\)”包含其他导出子句,则可以重复应用后一个缩写。因此,函数声明可以包含任意数量的导出,之后可能紧跟着一个导入。

表格

表格定义可以绑定一个符号 表格标识符

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{表格} & \href{../text/modules.html#text-table}{\mathtt{table}}_I &::=& \def\mathdef3503#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3503{(}~\def\mathdef3504#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3504{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{tt}{:}\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3505#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3505{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-table}{\mathsf{type}}~\mathit{tt} \} \\ \end{array}\end{split}\]

缩写

一个 元素段 可以与表格定义一起内联给出,在这种情况下,其偏移量为 \(0\),并且 表格类型限制 从给定段的长度推断得出

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{模块字段} & \def\mathdef3506#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3506{(}~\def\mathdef3507#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3507{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3508#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3508{(}~\def\mathdef3509#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3509{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\mathdef3510#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3510{)}~\def\mathdef3511#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3511{)} \quad\equiv \\ & \qquad \def\mathdef3512#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3512{(}~\def\mathdef3513#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3513{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3514#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3514{)} \\ & \qquad \def\mathdef3515#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3515{(}~\def\mathdef3516#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3516{elem}~~\def\mathdef3517#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3517{(}~\def\mathdef3518#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3518{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3519#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3519{)}~~\def\mathdef3520#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3520{(}~\def\mathdef3521#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3521{i32.const}~~\def\mathdef3522#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3522{0}~\def\mathdef3523#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3523{)}~~\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\mathdef3524#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3524{)} \\ & \qquad\qquad (\mathrel{\mbox{如果}} \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{新的}}) \\ \end{array}\end{split}\]
\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{模块字段} & \def\mathdef3525#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3525{(}~\def\mathdef3526#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3526{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~~\def\mathdef3527#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3527{(}~\def\mathdef3528#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3528{elem}~~x^n{:}\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef3529#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3529{)}~\def\mathdef3530#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3530{)} \quad\equiv \\ & \qquad \def\mathdef3531#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3531{(}~\def\mathdef3532#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3532{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~n~~n~~\href{../text/types.html#text-reftype}{\mathtt{reftype}}~\def\mathdef3533#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3533{)} \\ & \qquad \def\mathdef3534#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3534{(}~\def\mathdef3535#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3535{elem}~~\def\mathdef3536#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3536{(}~\def\mathdef3537#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3537{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3538#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3538{)}~~\def\mathdef3539#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3539{(}~\def\mathdef3540#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3540{i32.const}~~\def\mathdef3541#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3541{0}~\def\mathdef3542#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3542{)}~~\def\mathdef3543#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3543{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}})~\def\mathdef3544#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3544{)} \\ & \qquad\qquad (\mathrel{\mbox{如果}} \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{新的}}) \\ \end{array}\end{split}\]

表格可以定义为 导入导出 内联

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{模块字段} & \def\mathdef3545#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3545{(}~\def\mathdef3546#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3546{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3547#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3547{(}~\def\mathdef3548#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3548{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~\def\mathdef3549#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3549{)}~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3550#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3550{)} \quad\equiv \\ & \qquad \def\mathdef3551#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3551{(}~\def\mathdef3552#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3552{import}~~\href{../text/values.html#text-name}{\mathtt{name}}_1~~\href{../text/values.html#text-name}{\mathtt{name}}_2~~\def\mathdef3553#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3553{(}~\def\mathdef3554#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3554{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-tabletype}{\mathtt{tabletype}}~\def\mathdef3555#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3555{)}~\def\mathdef3556#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3556{)} \\[1ex] & \def\mathdef3557#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3557{(}~\def\mathdef3558#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3558{table}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3559#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3559{(}~\def\mathdef3560#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3560{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~\def\mathdef3561#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3561{)}~~\dots~\def\mathdef3562#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3562{)} \quad\equiv \\ & \qquad \def\mathdef3563#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3563{(}~\def\mathdef3564#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3564{export}~~\href{../text/values.html#text-name}{\mathtt{name}}~~\def\mathdef3565#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3565{(}~\def\mathdef3566#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3566{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3567#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3567{)}~\def\mathdef3568#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3568{)}~~ \def\mathdef3569#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3569{(}~\def\mathdef3570#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3570{table}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3571#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3571{)} \\ & \qquad\qquad (\mathrel{\mbox{如果}} \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{新的}}) \\ \end{array}\end{split}\]

注意

如果“\(\dots\)”包含其他导出子句,则可以重复应用后一个缩写。因此,表格声明可以包含任意数量的导出,之后可能紧跟着一个导入。

内存

内存定义可以绑定一个符号 内存标识符

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

缩写

一个 数据段 可以与内存定义一起内联给出,在这种情况下,其偏移量为 \(0\),并且 内存类型限制 从数据长度推断得出,向上舍入到 页面大小

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{模块字段} & \def\mathdef3575#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3575{(}~\def\mathdef3576#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3576{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3577#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3577{(}~\def\mathdef3578#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3578{数据}~~b^n{:}\href{../text/modules.html#text-datastring}{\mathtt{数据字符串}}~\def\mathdef3579#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3579{)}~~\def\mathdef3580#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3580{)} \quad\equiv \\ & \qquad \def\mathdef3581#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3581{(}~\def\mathdef3582#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3582{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~m~~m~\def\mathdef3583#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3583{)} \\ & \qquad \def\mathdef3584#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3584{(}~\def\mathdef3585#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3585{数据}~~\def\mathdef3586#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3586{(}~\def\mathdef3587#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3587{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3588#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3588{)}~~\def\mathdef3589#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3589{(}~\def\mathdef3590#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3590{i32.const}~~\def\mathdef3591#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3591{0}~\def\mathdef3592#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3592{)}~~\href{../text/modules.html#text-datastring}{\mathtt{数据字符串}}~\def\mathdef3593#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3593{)} \\ & \qquad\qquad (\mathrel{\mbox{如果}} \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{新值}}, m = \mathrm{ceil}(n / 64\,\mathrm{Ki})) \\ \end{array}\end{split}\]

内存可以定义为导入导出内联

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{模块字段} & \def\mathdef3594#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3594{(}~\def\mathdef3595#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3595{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3596#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3596{(}~\def\mathdef3597#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3597{导入}~~\href{../text/values.html#text-name}{\mathtt{名称}}_1~~\href{../text/values.html#text-name}{\mathtt{名称}}_2~\def\mathdef3598#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3598{)}~~\href{../text/types.html#text-memtype}{\mathtt{内存类型}}~\def\mathdef3599#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3599{)} \quad\equiv \\ & \qquad \def\mathdef3600#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3600{(}~\def\mathdef3601#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3601{导入}~~\href{../text/values.html#text-name}{\mathtt{名称}}_1~~\href{../text/values.html#text-name}{\mathtt{名称}}_2~~\def\mathdef3602#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3602{(}~\def\mathdef3603#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3603{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-memtype}{\mathtt{内存类型}}~\def\mathdef3604#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3604{)}~\def\mathdef3605#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3605{)} \\[1ex] & \def\mathdef3606#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3606{(}~\def\mathdef3607#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3607{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3608#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3608{(}~\def\mathdef3609#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3609{导出}~~\href{../text/values.html#text-name}{\mathtt{名称}}~\def\mathdef3610#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3610{)}~~\dots~\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{导出}~~\href{../text/values.html#text-name}{\mathtt{名称}}~~\def\mathdef3614#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3614{(}~\def\mathdef3615#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3615{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3616#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3616{)}~\def\mathdef3617#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3617{)}~~ \def\mathdef3618#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3618{(}~\def\mathdef3619#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3619{内存}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3620#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3620{)} \\ & \qquad\qquad (\mathrel{\mbox{如果}} \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{新值}}) \\ \end{array}\end{split}\]

注意

后一种缩写可以重复应用,如果“\(\dots\)”包含额外的导出子句。因此,内存声明可以包含任意数量的导出,可能后面跟着一个导入。

全局变量

全局变量定义可以绑定一个符号化的全局标识符

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{全局变量} & \href{../text/modules.html#text-global}{\mathtt{全局变量}}_I &::=& \def\mathdef3621#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3621{(}~\def\mathdef3622#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3622{全局变量}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\mathit{gt}{:}\href{../text/types.html#text-globaltype}{\mathtt{全局变量类型}}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{表达式}}_I~\def\mathdef3623#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3623{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-global}{\mathsf{类型}}~\mathit{gt}, \href{../syntax/modules.html#syntax-global}{\mathsf{初始化}}~e \} \\ \end{array}\end{split}\]

缩写

全局变量可以定义为导入导出内联

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{模块字段} & \def\mathdef3624#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3624{(}~\def\mathdef3625#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3625{全局变量}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3626#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3626{(}~\def\mathdef3627#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3627{导入}~~\href{../text/values.html#text-name}{\mathtt{名称}}_1~~\href{../text/values.html#text-name}{\mathtt{名称}}_2~\def\mathdef3628#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3628{)}~~\href{../text/types.html#text-globaltype}{\mathtt{全局变量类型}}~\def\mathdef3629#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3629{)} \quad\equiv \\ & \qquad \def\mathdef3630#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3630{(}~\def\mathdef3631#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3631{导入}~~\href{../text/values.html#text-name}{\mathtt{名称}}_1~~\href{../text/values.html#text-name}{\mathtt{名称}}_2~~\def\mathdef3632#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3632{(}~\def\mathdef3633#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3633{全局变量}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\href{../text/types.html#text-globaltype}{\mathtt{全局变量类型}}~\def\mathdef3634#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3634{)}~\def\mathdef3635#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3635{)} \\[1ex] & \def\mathdef3636#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3636{(}~\def\mathdef3637#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3637{全局变量}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3638#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3638{(}~\def\mathdef3639#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3639{导出}~~\href{../text/values.html#text-name}{\mathtt{名称}}~\def\mathdef3640#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3640{)}~~\dots~\def\mathdef3641#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3641{)} \quad\equiv \\ & \qquad \def\mathdef3642#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3642{(}~\def\mathdef3643#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3643{导出}~~\href{../text/values.html#text-name}{\mathtt{名称}}~~\def\mathdef3644#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3644{(}~\def\mathdef3645#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3645{全局变量}~~\href{../text/values.html#text-id}{\mathtt{id}}'~\def\mathdef3646#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3646{)}~\def\mathdef3647#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3647{)}~~ \def\mathdef3648#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3648{(}~\def\mathdef3649#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3649{全局变量}~~\href{../text/values.html#text-id}{\mathtt{id}}'~~\dots~\def\mathdef3650#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3650{)} \\ & \qquad\qquad (\mathrel{\mbox{如果}} \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{新值}}) \\ \end{array}\end{split}\]

注意

后一种缩写可以重复应用,如果“\(\dots\)”包含额外的导出子句。因此,全局变量声明可以包含任意数量的导出,可能后面跟着一个导入。

导出

导出的语法直接反映了它们的抽象语法

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{导出} & \href{../text/modules.html#text-export}{\mathtt{导出}}_I &::=& \def\mathdef3651#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3651{(}~\def\mathdef3652#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3652{导出}~~\mathit{nm}{:}\href{../text/values.html#text-name}{\mathtt{名称}}~~d{:}\href{../text/modules.html#text-exportdesc}{\mathtt{导出描述}}_I~\def\mathdef3653#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3653{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-export}{\mathsf{名称}}~\mathit{nm}, \href{../syntax/modules.html#syntax-export}{\mathsf{描述}}~d \} \\ \def\mathdef3386#1{{}}\mathdef3386{导出描述} & \href{../text/modules.html#text-exportdesc}{\mathtt{导出描述}}_I &::=& \def\mathdef3654#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3654{(}~\def\mathdef3655#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3655{函数}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{函数索引}}_I~\def\mathdef3656#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3656{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{函数}}~x \\ &&|& \def\mathdef3657#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3657{(}~\def\mathdef3658#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3658{表}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{表索引}}_I~\def\mathdef3659#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3659{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{表}}~x \\ &&|& \def\mathdef3660#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3660{(}~\def\mathdef3661#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3661{内存}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{内存索引}}_I~\def\mathdef3662#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3662{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{内存}}~x \\ &&|& \def\mathdef3663#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3663{(}~\def\mathdef3664#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3664{全局变量}~~x{:}\href{../text/modules.html#text-globalidx}{\mathtt{全局变量索引}}_I~\def\mathdef3665#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3665{)} &\Rightarrow& \href{../syntax/modules.html#syntax-exportdesc}{\mathsf{全局变量}}~x \\ \end{array}\end{split}\]

缩写

作为缩写,导出也可以与函数内存全局变量定义内联指定;请参阅各个部分。

起始函数

一个起始函数根据其索引定义。

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{起始函数} & \href{../text/modules.html#text-start}{\mathtt{起始}}_I &::=& \def\mathdef3666#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3666{(}~\def\mathdef3667#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3667{起始}~~x{:}\href{../text/modules.html#text-funcidx}{\mathtt{函数索引}}_I~\def\mathdef3668#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3668{)} &\Rightarrow& \{ \href{../syntax/modules.html#syntax-start}{\mathsf{函数}}~x \} \\ \end{array}\end{split}\]

注意

一个模块中最多只能出现一个起始函数,这由\(\href{../text/modules.html#text-module}{\mathtt{模块}}\)语法的适当的附加条件来确保。

元素段

元素段允许使用可选的表索引来标识要初始化的表。

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{元素段} & \href{../text/modules.html#text-elem}{\mathtt{元素}}_I &::=& \def\mathdef3669#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3669{(}~\def\mathdef3670#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3670{元素}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{元素列表}}_I~\def\mathdef3671#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3671{)} \\ &&& \qquad \Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{类型}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{初始化}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{模式}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{被动}} \} \\ &&|& \def\mathdef3672#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3672{(}~\def\mathdef3673#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3673{元素}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-tableuse}{\mathtt{表使用}}_I~~\def\mathdef3674#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3674{(}~\def\mathdef3675#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3675{偏移量}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{表达式}}_I~\def\mathdef3676#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3676{)}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{元素列表}}_I~\def\mathdef3677#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3677{)} \\ &&& \qquad \Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{类型}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{初始化}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{模式}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{主动}}~\{ \href{../syntax/modules.html#syntax-elem}{\mathsf{表}}~x, \href{../syntax/modules.html#syntax-elem}{\mathsf{偏移量}}~e \} \} \\ &&& \def\mathdef3678#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3678{(}~\def\mathdef3679#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3679{元素}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3680#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3680{声明}~~(et, y^\ast){:}\href{../text/modules.html#text-elemlist}{\mathtt{元素列表}}_I~\def\mathdef3681#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3681{)} \\ &&& \qquad \Rightarrow\quad \{ \href{../syntax/modules.html#syntax-elem}{\mathsf{类型}}~et, \href{../syntax/modules.html#syntax-elem}{\mathsf{初始化}}~y^\ast, \href{../syntax/modules.html#syntax-elem}{\mathsf{模式}}~\href{../syntax/modules.html#syntax-elemmode}{\mathsf{声明式}} \} \\ \def\mathdef3386#1{{}}\mathdef3386{元素列表} & \href{../text/modules.html#text-elemlist}{\mathtt{元素列表}}_I &::=& t{:}\href{../text/types.html#text-reftype}{\mathtt{引用类型}}~~y^\ast{:}\href{../text/conventions.html#text-vec}{\mathtt{向量}}(\href{../text/modules.html#text-elemexpr}{\mathtt{元素表达式}}_I) \qquad\Rightarrow\quad ( \href{../syntax/modules.html#syntax-elem}{\mathsf{类型}}~t, \href{../syntax/modules.html#syntax-elem}{\mathsf{初始化}}~y^\ast ) \\ \def\mathdef3386#1{{}}\mathdef3386{元素表达式} & \href{../text/modules.html#text-elemexpr}{\mathtt{元素表达式}}_I &::=& \def\mathdef3682#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3682{(}~\def\mathdef3683#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3683{项}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{表达式}}_I~\def\mathdef3684#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3684{)} \quad\Rightarrow\quad e \\ \def\mathdef3386#1{{}}\mathdef3386{表使用} & \href{../text/modules.html#text-tableuse}{\mathtt{表使用}}_I &::=& \def\mathdef3685#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3685{(}~\def\mathdef3686#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3686{表}~~x{:}\href{../text/modules.html#text-tableidx}{\mathtt{表索引}}_I ~\def\mathdef3687#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3687{)} \quad\Rightarrow\quad x \\ \end{array}\end{split}\]

缩写

作为缩写,单个指令可以代替活动元素段的偏移量或作为元素表达式。

\[\begin{split}\begin{array}{llcll} \def\mathdef3386#1{{}}\mathdef3386{元素偏移量} & \def\mathdef3688#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3688{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3689#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3689{)} &\equiv& \def\mathdef3690#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3690{(}~\def\mathdef3691#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3691{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3692#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3692{)} \\ \def\mathdef3386#1{{}}\mathdef3386{元素项} & \def\mathdef3693#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3693{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3694#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3694{)} &\equiv& \def\mathdef3695#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3695{(}~\def\mathdef3696#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3696{item}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3697#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3697{)} \\ \end{array}\end{split}\]

此外,元素列表可以写成一系列函数索引

\[\begin{array}{llcll} \def\mathdef3386#1{{}}\mathdef3386{元素列表} & \def\mathdef3698#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3698{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I) &\equiv& \def\mathdef3699#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3699{funcref}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\def\mathdef3700#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3700{(}~\def\mathdef3701#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3701{ref.func}~~\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I~\def\mathdef3702#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3702{)}) \end{array}\]

可以省略表格使用,默认为\(\mathtt{0}\)。此外,为了与早期版本的 WebAssembly 保持向后兼容性,如果省略了表格使用,则也可以省略\(\def\mathdef3703#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3703{func}\)关键字。

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{表格使用} & \epsilon &\equiv& \def\mathdef3704#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3704{(}~\def\mathdef3705#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3705{table}~~\def\mathdef3706#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3706{0}~\def\mathdef3707#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3707{)} \\ \def\mathdef3386#1{{}}\mathdef3386{元素段} & \def\mathdef3708#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3708{(}~\def\mathdef3709#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3709{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3710#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3710{(}~\def\mathdef3711#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3711{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3712#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3712{)}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3713#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3713{)} &\equiv& \def\mathdef3714#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3714{(}~\def\mathdef3715#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3715{elem}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~\def\mathdef3716#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3716{(}~\def\mathdef3717#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3717{table}~~\def\mathdef3718#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3718{0}~\def\mathdef3719#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3719{)}~~\def\mathdef3720#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3720{(}~\def\mathdef3721#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3721{offset}~~\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3722#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3722{)}~~\def\mathdef3723#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3723{func}~~\href{../text/conventions.html#text-vec}{\mathtt{vec}}(\href{../text/modules.html#text-funcidx}{\mathtt{funcidx}}_I)~\def\mathdef3724#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3724{)} \end{array}\end{split}\]

作为另一种缩写,元素段也可以在表格定义中内联指定;请参阅相应部分。

数据段

数据段允许使用可选的内存索引来识别要初始化的内存。数据被写成字符串,可以将其拆分为一个可能为空的单个字符串文字序列。

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{数据段} & \href{../text/modules.html#text-data}{\mathtt{data}}_I &::=& \def\mathdef3725#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3725{(}~\def\mathdef3726#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3726{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3727#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3727{)} \\ &&& \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\mathdef3728#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3728{(}~\def\mathdef3729#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3729{data}~~\href{../text/values.html#text-id}{\mathtt{id}}^?~~x{:}\href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I~~\def\mathdef3730#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3730{(}~\def\mathdef3731#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3731{offset}~~e{:}\href{../text/instructions.html#text-expr}{\mathtt{expr}}_I~\def\mathdef3732#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3732{)}~~b^\ast{:}\href{../text/modules.html#text-datastring}{\mathtt{datastring}}~\def\mathdef3733#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3733{)} \\ &&& \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\mathdef3386#1{{}}\mathdef3386{数据字符串} & \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\mathdef3386#1{{}}\mathdef3386{内存使用} & \href{../text/modules.html#text-memuse}{\mathtt{memuse}}_I &::=& \def\mathdef3734#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3734{(}~\def\mathdef3735#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3735{memory}~~x{:}\href{../text/modules.html#text-memidx}{\mathtt{memidx}}_I ~\def\mathdef3736#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3736{)} \quad\Rightarrow\quad x \\ \end{array}\end{split}\]

注意

在当前版本的 WebAssembly 中,唯一有效的内存索引是 0 或解析为相同值的符号内存标识符

缩写

作为缩写,单个指令可以代替活动数据段的偏移量。

\[\begin{array}{llcll} \def\mathdef3386#1{{}}\mathdef3386{数据偏移量} & \def\mathdef3737#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3737{(}~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3738#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3738{)} &\equiv& \def\mathdef3739#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3739{(}~\def\mathdef3740#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3740{offset}~~\href{../text/instructions.html#text-instr}{\mathtt{instr}}~\def\mathdef3741#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3741{)} \end{array}\]

此外,可以省略内存使用,默认为\(\mathtt{0}\)

\[\begin{split}\begin{array}{llclll} \def\mathdef3386#1{{}}\mathdef3386{内存使用} & \epsilon &\equiv& \def\mathdef3742#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3742{(}~\def\mathdef3743#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3743{memory}~~\def\mathdef3744#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3744{0}~\def\mathdef3745#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3745{)} \\ \end{array}\end{split}\]

作为另一种缩写,数据段也可以在内存定义中内联指定;请参阅相应部分。

模块

模块由一系列可以按任意顺序出现的字段组成。所有定义及其各自绑定的标识符的作用域覆盖整个模块,包括其前面的文本。

模块可以选择性地绑定一个标识符来命名模块。名称仅起文档作用。

注意

工具可能会在名称段中包含模块名称二进制格式

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

模块的组合施加以下限制:\(m_1 \href{../syntax/conventions.html#notation-compose}{\oplus} m_2\) 定义当且仅当

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

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

注意

第一个条件确保最多只有一个开始函数。第二个条件强制所有导入必须出现在函数表格内存全局变量的任何常规定义之前,从而保持各自索引空间的顺序。

\(\href{../text/modules.html#text-module}{\mathtt{module}}\)语法中关于\(I\)良好形式条件确保没有命名空间包含重复的标识符。

初始标识符上下文\(I\)的定义使用以下辅助定义,该定义将每个相关定义映射到具有一个(可能为空)标识符的单个上下文

\[\begin{split}\begin{array}{@{}lcl@{\qquad\qquad}l} \mathrm{idc}(\def\mathdef3749#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3749{(}~\def\mathdef3750#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3750{type}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\mathit{ft}{:}\href{../text/types.html#text-functype}{\mathtt{functype}}~\def\mathdef3751#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3751{)}) &=& \{\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\mathdef3752#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3752{(}~\def\mathdef3753#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3753{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3754#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3754{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3755#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3755{(}~\def\mathdef3756#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3756{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3757#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3757{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3758#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3758{(}~\def\mathdef3759#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3759{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3760#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3760{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3761#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3761{(}~\def\mathdef3762#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3762{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3763#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3763{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3764#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3764{(}~\def\mathdef3765#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3765{elem}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3766#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3766{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{elem}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3767#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3767{(}~\def\mathdef3768#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3768{data}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3769#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3769{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{data}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3770#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3770{(}~\def\mathdef3771#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3771{import}~\dots~\def\mathdef3772#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3772{(}~\def\mathdef3773#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3773{func}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3774#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3774{)}~\def\mathdef3775#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3775{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{funcs}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3776#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3776{(}~\def\mathdef3777#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3777{import}~\dots~\def\mathdef3778#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3778{(}~\def\mathdef3779#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3779{table}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3780#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3780{)}~\def\mathdef3781#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3781{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{tables}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3782#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3782{(}~\def\mathdef3783#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3783{import}~\dots~\def\mathdef3784#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3784{(}~\def\mathdef3785#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3785{memory}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3786#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3786{)}~\def\mathdef3787#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3787{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{mems}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3788#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3788{(}~\def\mathdef3789#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3789{import}~\dots~\def\mathdef3790#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3790{(}~\def\mathdef3791#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3791{global}~\href{../text/values.html#text-id}{\mathtt{id}}^?~\dots~\def\mathdef3792#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3792{)}~\def\mathdef3793#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3793{)}) &=& \{\href{../text/conventions.html#text-context}{\mathsf{globals}}~(\href{../text/values.html#text-id}{\mathtt{id}}^?)\} \\ \mathrm{idc}(\def\mathdef3794#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3794{(}~\dots~\def\mathdef3795#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef3795{)}) &=& \{\} \\ \end{array}\end{split}\]

缩写

在源文件中,围绕模块体的顶级 \(\mathtt{(module}~\dots\mathtt{)}\) 可以省略。

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