deploy: 6becba4

core/appendix/properties.html

@@ -517,8 +517,8 @@ <h3><a class="reference internal" href="../exec/runtime.html#syntax-result"><spa
   S \href{../appendix/properties.html#valid-globalinst}{\vdash} \{ \href{../exec/runtime.html#syntax-globalinst}{\mathsf{type}}~(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t), \href{../exec/runtime.html#syntax-globalinst}{\mathsf{value}}~\href{../exec/runtime.html#syntax-val}{\mathit{val}} \} : \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~t
 }\]</div>
 </section>
-<section id="element-instances-xref-exec-runtime-syntax-eleminst-mathsf-elem-mathit-fa-ast">
-<span id="valid-eleminst"></span><span id="index-12"></span><h3><a class="reference internal" href="../exec/runtime.html#syntax-eleminst"><span class="std std-ref">Element Instances</span></a> <span class="math notranslate nohighlight">\(\{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\mathit{fa}^\ast \}\)</span><a class="headerlink" href="#element-instances-xref-exec-runtime-syntax-eleminst-mathsf-elem-mathit-fa-ast" title="Permalink to this heading">¶</a></h3>
+<section id="element-instances-xref-exec-runtime-syntax-eleminst-mathsf-type-t-xref-exec-runtime-syntax-eleminst-mathsf-elem-xref-exec-runtime-syntax-ref-mathit-ref-ast">
+<span id="valid-eleminst"></span><span id="index-12"></span><h3><a class="reference internal" href="../exec/runtime.html#syntax-eleminst"><span class="std std-ref">Element Instances</span></a> <span class="math notranslate nohighlight">\(\{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{type}}~t, \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^\ast \}\)</span><a class="headerlink" href="#element-instances-xref-exec-runtime-syntax-eleminst-mathsf-type-t-xref-exec-runtime-syntax-eleminst-mathsf-elem-xref-exec-runtime-syntax-ref-mathit-ref-ast" title="Permalink to this heading">¶</a></h3>
 <ul class="simple">
 <li><p>The <a class="reference internal" href="../syntax/types.html#syntax-reftype"><span class="std std-ref">reference type</span></a> <span class="math notranslate nohighlight">\(t\)</span> must be <a class="reference internal" href="../valid/types.html#valid-reftype"><span class="std std-ref">valid</span></a> under the empty <a class="reference internal" href="../valid/conventions.html#context"><span class="std std-ref">context</span></a>.</p></li>
 <li><p>For each <a class="reference internal" href="../exec/runtime.html#syntax-ref"><span class="std std-ref">reference</span></a> <span class="math notranslate nohighlight">\(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}_i\)</span> in the elements <span class="math notranslate nohighlight">\(\href{../exec/runtime.html#syntax-ref}{\mathit{ref}}^n\)</span>:</p>

core/binary/conventions.html

@@ -123,7 +123,8 @@ <h3 id="searchlabel">Quick search</h3>
 (This is a shorthand for <span class="math notranslate nohighlight">\(B^n\)</span> used where <span class="math notranslate nohighlight">\(n\)</span> is not relevant.)</p></li>
 <li><p><span class="math notranslate nohighlight">\(B^?\)</span> is an optional occurrence of <span class="math notranslate nohighlight">\(B\)</span>.
 (This is a shorthand for <span class="math notranslate nohighlight">\(B^n\)</span> where <span class="math notranslate nohighlight">\(n \leq 1\)</span>.)</p></li>
-<li><p><span class="math notranslate nohighlight">\(x{:}B\)</span> denotes the same language as the nonterminal <span class="math notranslate nohighlight">\(B\)</span>, but also binds the variable <span class="math notranslate nohighlight">\(x\)</span> to the attribute synthesized for <span class="math notranslate nohighlight">\(B\)</span>.</p></li>
+<li><p><span class="math notranslate nohighlight">\(x{:}B\)</span> denotes the same language as the nonterminal <span class="math notranslate nohighlight">\(B\)</span>, but also binds the variable <span class="math notranslate nohighlight">\(x\)</span> to the attribute synthesized for <span class="math notranslate nohighlight">\(B\)</span>.
+A pattern may also be used instead of a variable, e.g., <span class="math notranslate nohighlight">\(7{:}B\)</span>.</p></li>
 <li><p>Productions are written <span class="math notranslate nohighlight">\(\mathtt{sym} ::= B_1 \Rightarrow A_1 ~|~ \dots ~|~ B_n \Rightarrow A_n\)</span>, where each <span class="math notranslate nohighlight">\(A_i\)</span> is the attribute that is synthesized for <span class="math notranslate nohighlight">\(\mathtt{sym}\)</span> in the given case, usually from attribute variables bound in <span class="math notranslate nohighlight">\(B_i\)</span>.</p></li>
 <li><p>Some productions are augmented by side conditions in parentheses, which restrict the applicability of the production. They provide a shorthand for a combinatorial expansion of the production into many separate cases.</p></li>
 <li><p>If the same meta variable or non-terminal symbol appears multiple times in a production (in the syntax or in an attribute), then all those occurrences must have the same instantiation.

core/binary/modules.html

@@ -116,7 +116,7 @@ <h1>Modules<a class="headerlink" href="#modules" title="Permalink to this headin
 <ul class="simple">
 <li><p>a one-byte section <em>id</em>,</p></li>
 <li><p>the <span class="math notranslate nohighlight">\(\href{../syntax/values.html#syntax-int}{\mathit{u32}}\)</span> <em>size</em> of the contents, in bytes,</p></li>
-<li><p>the actual <em>contents</em>, whose structure is depended on the section id.</p></li>
+<li><p>the actual <em>contents</em>, whose structure is dependent on the section id.</p></li>
 </ul>
 <p>Every section is optional; an omitted section is equivalent to the section being present with empty contents.</p>
 <p>The following parameterized grammar rule defines the generic structure of a section with id <span class="math notranslate nohighlight">\(N\)</span> and contents described by the grammar <span class="math notranslate nohighlight">\(\mathtt{B}\)</span>.</p>

core/exec/instructions.html

@@ -2304,7 +2304,7 @@ <h3><span class="math notranslate nohighlight">\(t_2\mathsf{x}N\mathsf{.}\href{.
 <li><p>Assert: due to <a class="reference internal" href="../valid/instructions.html#valid-elem-drop"><span class="std std-ref">validation</span></a>, <span class="math notranslate nohighlight">\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[x]\)</span> exists.</p></li>
 <li><p>Let <span class="math notranslate nohighlight">\(a\)</span> be the <a class="reference internal" href="runtime.html#syntax-elemaddr"><span class="std std-ref">element address</span></a> <span class="math notranslate nohighlight">\(F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[x]\)</span>.</p></li>
 <li><p>Assert: due to <a class="reference internal" href="../valid/instructions.html#valid-elem-drop"><span class="std std-ref">validation</span></a>, <span class="math notranslate nohighlight">\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[a]\)</span> exists.</p></li>
-<li><p>Replace <span class="math notranslate nohighlight">\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[a]\)</span> with the <a class="reference internal" href="runtime.html#syntax-eleminst"><span class="std std-ref">element instance</span></a> <span class="math notranslate nohighlight">\(\{\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\epsilon\}\)</span>.</p></li>
+<li><p>Replace <span class="math notranslate nohighlight">\(S.\href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[a].\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}\)</span> with <span class="math notranslate nohighlight">\(\epsilon\)</span>.</p></li>
 </ol>
 <div class="math notranslate nohighlight">
 \[\begin{split}~\\[-1ex]
@@ -2313,7 +2313,7 @@ <h3><span class="math notranslate nohighlight">\(t_2\mathsf{x}N\mathsf{.}\href{.
 S; F; (\href{../syntax/instructions.html#syntax-instr-table}{\mathsf{elem.drop}}~x) &amp;\href{../exec/conventions.html#formal-notation}{\hookrightarrow}&amp; S'; F; \epsilon
 \end{array}
 \\ \qquad
-  (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[x]] = \{ \href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}}~\epsilon \}) \\
+  (\mathrel{\mbox{if}} S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{elems}}[F.\href{../exec/runtime.html#syntax-frame}{\mathsf{module}}.\href{../exec/runtime.html#syntax-moduleinst}{\mathsf{elemaddrs}}[x]].\href{../exec/runtime.html#syntax-eleminst}{\mathsf{elem}} = \epsilon) \\
 \end{array}\end{split}\]</div>
 </section>
 </section>

core/syntax/instructions.html

@@ -683,7 +683,7 @@ <h3 id="searchlabel">Quick search</h3>
 </section>
 <section id="expressions">
 <span id="syntax-expr"></span><span id="index-10"></span><h2>Expressions<a class="headerlink" href="#expressions" title="Permalink to this heading">¶</a></h2>
-<p><a class="reference internal" href="modules.html#syntax-func"><span class="std std-ref">Function</span></a> bodies, initialization values for <a class="reference internal" href="modules.html#syntax-global"><span class="std std-ref">globals</span></a>, and offsets of <a class="reference internal" href="modules.html#syntax-elem"><span class="std std-ref">element</span></a> or <a class="reference internal" href="modules.html#syntax-data"><span class="std std-ref">data</span></a> segments are given as expressions, which are sequences of <a class="reference internal" href="#syntax-instr"><span class="std std-ref">instructions</span></a> terminated by an <span class="math notranslate nohighlight">\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)</span> marker.</p>
+<p><a class="reference internal" href="modules.html#syntax-func"><span class="std std-ref">Function</span></a> bodies, initialization values for <a class="reference internal" href="modules.html#syntax-global"><span class="std std-ref">globals</span></a>, elements and offsets of <a class="reference internal" href="modules.html#syntax-elem"><span class="std std-ref">element</span></a> segments, and offsets of <a class="reference internal" href="modules.html#syntax-data"><span class="std std-ref">data</span></a> segments are given as expressions, which are sequences of <a class="reference internal" href="#syntax-instr"><span class="std std-ref">instructions</span></a> terminated by an <span class="math notranslate nohighlight">\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}}\)</span> marker.</p>
 <div class="math notranslate nohighlight">
 \[\begin{split}\begin{array}{llrl}
 \def\mathdef2803#1{{}}\mathdef2803{expression} &amp; \href{../syntax/instructions.html#syntax-expr}{\mathit{expr}} &amp;::=&amp;

core/text/conventions.html

@@ -115,7 +115,8 @@ <h3 id="searchlabel">Quick search</h3>
 (This is a shorthand for <span class="math notranslate nohighlight">\(T^n\)</span> where <span class="math notranslate nohighlight">\(n \geq 1\)</span>.)</p></li>
 <li><p><span class="math notranslate nohighlight">\(T^?\)</span> is an optional occurrence of <span class="math notranslate nohighlight">\(T\)</span>.
 (This is a shorthand for <span class="math notranslate nohighlight">\(T^n\)</span> where <span class="math notranslate nohighlight">\(n \leq 1\)</span>.)</p></li>
-<li><p><span class="math notranslate nohighlight">\(x{:}T\)</span> denotes the same language as the nonterminal <span class="math notranslate nohighlight">\(T\)</span>, but also binds the variable <span class="math notranslate nohighlight">\(x\)</span> to the attribute synthesized for <span class="math notranslate nohighlight">\(T\)</span>.</p></li>
+<li><p><span class="math notranslate nohighlight">\(x{:}T\)</span> denotes the same language as the nonterminal <span class="math notranslate nohighlight">\(T\)</span>, but also binds the variable <span class="math notranslate nohighlight">\(x\)</span> to the attribute synthesized for <span class="math notranslate nohighlight">\(T\)</span>.
+A pattern may also be used instead of a variable, e.g., <span class="math notranslate nohighlight">\((x,y){:}T\)</span>.</p></li>
 <li><p>Productions are written <span class="math notranslate nohighlight">\(\mathtt{sym} ::= T_1 \Rightarrow A_1 ~|~ \dots ~|~ T_n \Rightarrow A_n\)</span>, where each <span class="math notranslate nohighlight">\(A_i\)</span> is the attribute that is synthesized for <span class="math notranslate nohighlight">\(\mathtt{sym}\)</span> in the given case, usually from attribute variables bound in <span class="math notranslate nohighlight">\(T_i\)</span>.</p></li>
 <li><p>Some productions are augmented by side conditions in parentheses, which restrict the applicability of the production. They provide a shorthand for a combinatorial expansion of the production into many separate cases.</p></li>
 <li><p>If the same meta variable or non-terminal symbol appears multiple times in a production (in the syntax or in an attribute), then all those occurrences must have the same instantiation.</p></li>