You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<h2>Conventions<aclass="headerlink" href="#conventions" title="Link to this heading">¶</a></h2>
98
98
<p>A profile modification is specified by decorating selected rules in the main body of this specification with a <em>profile annotation</em> that defines them as conditional on the choice of profile.</p>
99
-
<p>For that purpose, every profile defines a <em>profile marker</em>, an alphanumeric short-hand like <spanclass="math notranslate nohighlight">\(\def\mathdef1448#1{{\small{\mathrm{#1}}}}\mathdef1448{ABC}\)</span>.
100
-
A profile annotation of the form <spanclass="math notranslate nohighlight">\(\def\mathdef1449#1{{{}^{\small{[{!}#1]}}}}\mathdef1449{\mathrm{ABC}~\mathrm{XYZ}}\)</span> on a rule indicates that this rule is <em>excluded</em> for either of the profiles whose marker is <spanclass="math notranslate nohighlight">\(\def\mathdef1450#1{{\small{\mathrm{#1}}}}\mathdef1450{ABC}\)</span> or <spanclass="math notranslate nohighlight">\(\def\mathdef1451#1{{\small{\mathrm{#1}}}}\mathdef1451{XYZ}\)</span>.</p>
99
+
<p>For that purpose, every profile defines a <em>profile marker</em>, an alphanumeric short-hand like <spanclass="math notranslate nohighlight">\(\def\mathdef1451#1{{\small{\mathrm{#1}}}}\mathdef1451{ABC}\)</span>.
100
+
A profile annotation of the form <spanclass="math notranslate nohighlight">\(\def\mathdef1452#1{{{}^{\small{[{!}#1]}}}}\mathdef1452{\mathrm{ABC}~\mathrm{XYZ}}\)</span> on a rule indicates that this rule is <em>excluded</em> for either of the profiles whose marker is <spanclass="math notranslate nohighlight">\(\def\mathdef1453#1{{\small{\mathrm{#1}}}}\mathdef1453{ABC}\)</span> or <spanclass="math notranslate nohighlight">\(\def\mathdef1454#1{{\small{\mathrm{#1}}}}\mathdef1454{XYZ}\)</span>.</p>
101
101
<p>There are two ways of subsetting the language in a profile:</p>
102
102
<ulclass="simple">
103
103
<li><p><em>Syntactic</em>, by <em>omitting</em> a feature, in which case certain constructs are removed from the syntax altogether.</p></li>
<p>The overall effect is that the respective construct is no longer part of the language under a respective profile.</p>
115
115
<divclass="admonition note">
116
116
<pclass="admonition-title">Note</p>
117
-
<p>For example, a “busy” profile marked <spanclass="math notranslate nohighlight">\(\def\mathdef1452#1{{\small{\mathrm{#1}}}}\mathdef1452{BUSY}\)</span> could rule out the <spanclass="math notranslate nohighlight">\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}}\)</span> instruction by marking the production for it in the abstract syntax as follows:</p>
117
+
<p>For example, a “busy” profile marked <spanclass="math notranslate nohighlight">\(\def\mathdef1455#1{{\small{\mathrm{#1}}}}\mathdef1455{BUSY}\)</span> could rule out the <spanclass="math notranslate nohighlight">\(\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}}\)</span> instruction by marking the production for it in the abstract syntax as follows:</p>
118
118
<divclass="math notranslate nohighlight">
119
119
\[\begin{split}\begin{array}{llcl}
120
-
\def\mathdef1417#1{{}}\mathdef1417{instruction} & \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} &::=&
120
+
\def\mathdef1420#1{{}}\mathdef1420{instruction} & \href{../syntax/instructions.html#syntax-instr}{\mathit{instr}} &::=&
121
121
\dots \\
122
-
& \def\mathdef1453#1{{{}^{\small{[{!}#1]}}}}\mathdef1453{\mathrm{BUSY}} &|& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} \\
122
+
& \def\mathdef1456#1{{{}^{\small{[{!}#1]}}}}\mathdef1456{\mathrm{BUSY}} &|& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} \\
123
123
& &|& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}} \\
124
124
\end{array}\end{split}\]</div>
125
125
<p>A rule may be annotated by multiple markers, which could be the case if a construct is in the intersection of multiple features.</p>
<p>This has the consequence that the respective rule is no longer applicable under the given profile.</p>
132
132
<divclass="admonition note">
133
133
<pclass="admonition-title">Note</p>
134
-
<p>For example, an “infinite” profile marked <spanclass="math notranslate nohighlight">\(\def\mathdef1454#1{{\small{\mathrm{#1}}}}\mathdef1454{INF}\)</span> could define that growing memory never fails:</p>
134
+
<p>For example, an “infinite” profile marked <spanclass="math notranslate nohighlight">\(\def\mathdef1457#1{{\small{\mathrm{#1}}}}\mathdef1457{INF}\)</span> could define that growing memory never fails:</p>
135
135
<divclass="math notranslate nohighlight">
136
136
\[\begin{split}\begin{array}{llcl@{\qquad}l}
137
137
& S; F; (\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}grow}}~x &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S'; F; (\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\mathit{sz})
\wedge & S' = S \href{../syntax/conventions.html#notation-replace}{\mathrel{\mbox{with}}} \href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a] = \href{../exec/modules.html#grow-mem}{\mathrm{growmem}}(S.\href{../exec/runtime.html#syntax-store}{\mathsf{mems}}[a], n)) \\[1ex]
143
143
\end{array}
144
144
\\[1ex]
145
-
\def\mathdef1455#1{{{}^{\small{[{!}#1]}}}}\mathdef1455{\mathrm{INF}} & S; F; (\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}grow}}~x &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{32}^{-1}(-1))
145
+
\def\mathdef1458#1{{{}^{\small{[{!}#1]}}}}\mathdef1458{\mathrm{INF}} & S; F; (\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~n)~\href{../syntax/instructions.html#syntax-instr-memory}{\mathsf{memory{.}grow}}~x &\href{../exec/conventions.html#exec-notation}{\hookrightarrow}& S; F; (\href{../syntax/types.html#syntax-numtype}{\mathsf{i\scriptstyle32}}.\href{../syntax/instructions.html#syntax-instr-numeric}{\mathsf{const}}~\href{../exec/numerics.html#aux-signed}{\mathrm{signed}}_{32}^{-1}(-1))
146
146
\end{array}\end{split}\]</div>
147
147
</div>
148
148
</section>
@@ -176,7 +176,7 @@ <h2>Defined Profiles<a class="headerlink" href="#defined-profiles" title="Link t
<spanid="profile-deterministic"></span><spanid="index-2"></span><h3>Deterministic Profile (<spanclass="math notranslate nohighlight">\({\small{\mathrm{DET}}}\)</span>)<aclass="headerlink" href="#deterministic-profile-small-mathrm-det" title="Link to this heading">¶</a></h3>
179
-
<p>The <em>deterministic</em> profile excludes all rules marked <spanclass="math notranslate nohighlight">\(\def\mathdef1456#1{{{}^{\small{[{!}#1]}}}}\mathdef1456{\href{../appendix/profiles.html#profile-deterministic}{\mathrm{DET}}}\)</span>.
179
+
<p>The <em>deterministic</em> profile excludes all rules marked <spanclass="math notranslate nohighlight">\(\def\mathdef1459#1{{{}^{\small{[{!}#1]}}}}\mathdef1459{\href{../appendix/profiles.html#profile-deterministic}{\mathrm{DET}}}\)</span>.
180
180
It defines a sub-language that does not exhibit any incidental non-deterministic behaviour:</p>
181
181
<ulclass="simple">
182
182
<li><p>All <aclass="reference internal" href="../syntax/values.html#syntax-nan"><spanclass="std std-ref">NaN</span></a> values <aclass="reference internal" href="../exec/numerics.html#aux-nans"><spanclass="std std-ref">generated</span></a> by <aclass="reference internal" href="../syntax/instructions.html#syntax-instr-numeric"><spanclass="std std-ref">floating-point instructions</span></a> are canonical and positive.</p></li>
the <aclass="reference internal" href="../valid/conventions.html#context"><spanclass="std std-ref">context</span></a> is locally extended with an additional component that records the <aclass="reference internal" href="../syntax/types.html#syntax-subtype"><spanclass="std std-ref">sub type</span></a> corresponding to each <aclass="reference internal" href="../valid/conventions.html#syntax-rectypeidx"><spanclass="std std-ref">recursive type index</span></a> within the current <aclass="reference internal" href="../syntax/types.html#syntax-rectype"><spanclass="std std-ref">recursive type</span></a>:</p>
109
109
<divclass="math notranslate nohighlight">
110
110
\[\begin{split}\begin{array}{llll}
111
-
\def\mathdef1457#1{{}}\mathdef1457{context} & C &::=&
111
+
\def\mathdef1460#1{{}}\mathdef1460{context} & C &::=&
<p>Technically, the <aclass="reference internal" href="../syntax/modules.html#syntax-type"><spanclass="std std-ref">syntax</span></a> of <aclass="reference internal" href="../syntax/types.html#syntax-heaptype"><spanclass="std std-ref">heap</span></a>, <aclass="reference internal" href="../syntax/types.html#syntax-valtype"><spanclass="std std-ref">value</span></a>, and <aclass="reference internal" href="../syntax/types.html#syntax-resulttype"><spanclass="std std-ref">result</span></a> types can be enriched with type variables as follows:</p>
1275
1275
<divclass="math notranslate nohighlight">
1276
1276
\[\begin{split}\begin{array}{llll}
1277
-
\def\mathdef1457#1{{}}\mathdef1457{nullability} & \mathit{null} &::=&
1277
+
\def\mathdef1460#1{{}}\mathdef1460{nullability} & \mathit{null} &::=&
<p>where each <spanclass="math notranslate nohighlight">\(\alpha_{\mathit{xyz}}\)</span> ranges over a set of type variables for syntactic class <spanclass="math notranslate nohighlight">\(\mathit{xyz}\)</span>, respectively.
0 commit comments