mirror of
https://github.com/ganelson/inform.git
synced 2024-07-08 18:14:21 +03:00
2520 lines
276 KiB
HTML
2520 lines
276 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>Compile Deferred Propositions</title>
|
|
<meta name="viewport" content="width=device-width initial-scale=1">
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<meta http-equiv="Content-Language" content="en-gb">
|
|
<link href="../inweb.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
|
|
</head>
|
|
<body>
|
|
<nav role="navigation">
|
|
<h1><a href="../index.html">
|
|
<img src="../docs-src/Figures/Inform.png" height=72">
|
|
</a></h1>
|
|
<ul><li><a href="../compiler.html">compiler tools</a></li>
|
|
<li><a href="../other.html">other tools</a></li>
|
|
<li><a href="../extensions.html">extensions and kits</a></li>
|
|
<li><a href="../units.html">unit test tools</a></li>
|
|
</ul><h2>Compiler Webs</h2><ul>
|
|
<li><a href="../inbuild/index.html">inbuild</a></li>
|
|
<li><a href="../inform7/index.html">inform7</a></li>
|
|
<li><a href="../inter/index.html">inter</a></li>
|
|
</ul><h2>Inbuild Modules</h2><ul>
|
|
<li><a href="../supervisor-module/index.html">supervisor</a></li>
|
|
</ul><h2>Inform7 Modules</h2><ul>
|
|
<li><a href="index.html"><span class="selectedlink">core</span></a></li>
|
|
<li><a href="../inflections-module/index.html">inflections</a></li>
|
|
<li><a href="../linguistics-module/index.html">linguistics</a></li>
|
|
<li><a href="../kinds-module/index.html">kinds</a></li>
|
|
<li><a href="../if-module/index.html">if</a></li>
|
|
<li><a href="../multimedia-module/index.html">multimedia</a></li>
|
|
<li><a href="../problems-module/index.html">problems</a></li>
|
|
<li><a href="../index-module/index.html">index</a></li>
|
|
</ul><h2>Inter Modules</h2><ul>
|
|
<li><a href="../bytecode-module/index.html">bytecode</a></li>
|
|
<li><a href="../building-module/index.html">building</a></li>
|
|
<li><a href="../codegen-module/index.html">codegen</a></li>
|
|
</ul><h2>Shared Modules</h2><ul>
|
|
<li><a href="../arch-module/index.html">arch</a></li>
|
|
<li><a href="../syntax-module/index.html">syntax</a></li>
|
|
<li><a href="../words-module/index.html">words</a></li>
|
|
<li><a href="../html-module/index.html">html</a></li>
|
|
<li><a href="../../../inweb/docs/foundation-module/index.html">foundation</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
|
|
<!--Weave of 'Compile Deferred Propositions' generated by 7-->
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../compiler.html">Inform7 Modules</a></li><li><a href="index.html">core</a></li><li><a href="index.html#12">Chapter 12: Use of Propositions</a></li><li><b>Compile Deferred Propositions</b></li></ul><p class="purpose">To compile the I6 routines needed to perform the tests or tasks deferred as being too difficult in their original contexts.</p>
|
|
|
|
<ul class="toc"><li><a href="12-cdp.html#SP1">§1. Comment</a></li><li><a href="12-cdp.html#SP2">§2. Preliminaries</a></li><li><a href="12-cdp.html#SP2_1_6_1_1">§2.1.6.1.1. The Search</a></li><li><a href="12-cdp.html#SP2_1_6_1_2_1">§2.1.6.1.2.1. The R-stack</a></li><li><a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3. Compiling the search</a></li><li><a href="12-cdp.html#SP2_1_6_1_2_3_1">§2.1.6.1.2.3.1. Predicate runs and their negations</a></li><li><a href="12-cdp.html#SP2_1_6_1_2_3_5">§2.1.6.1.2.3.5. Quantifiers and the Q-stack</a></li><li><a href="12-cdp.html#SP2_1_6_1_2_3_8">§2.1.6.1.2.3.8. The C-stack</a></li><li><a href="12-cdp.html#SP2_1_5_1">§2.1.5.1. Adaptations</a></li><li><a href="12-cdp.html#SP2_1_6_1_3">§2.1.6.1.3. Adaptation to CONDITION</a></li><li><a href="12-cdp.html#SP2_1_6_1_5">§2.1.6.1.5. Adaptation to NUMBER</a></li><li><a href="12-cdp.html#SP2_1_6_1_8">§2.1.6.1.8. Adaptation to LIST</a></li><li><a href="12-cdp.html#SP2_1_6_1_10">§2.1.6.1.10. Adaptation to RANDOM</a></li><li><a href="12-cdp.html#SP2_1_6_1_12">§2.1.6.1.12. Adaptation to TOTAL</a></li><li><a href="12-cdp.html#SP2_1_6_1_14">§2.1.6.1.14. Adaptation to EXTREMAL</a></li><li><a href="12-cdp.html#SP2_1_6_1_16">§2.1.6.1.16. Adaptation to LOOP</a></li><li><a href="12-cdp.html#SP3">§3. Compiling loop headers</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="inwebparagraph"><a id="SP1"></a><b>§1. Comment. </b>The following compiles an I6 comment noting the reason for a deferral.
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="reserved">void</span><span class="plain"> </span><span class="functiontext">Calculus::Propositions::Deferred::compile_comment_about_deferral_reason<button class="popup" onclick="togglePopup('usagePopup839')">...<span class="popuptext" id="usagePopup839">Usage of <b>Calculus::Propositions::Deferred::compile_comment_about_deferral_reason</b>:<br><a href="12-cdp.html#SP2_1_6">§2.1.6</a></span></button></span><span class="plain">(</span><span class="reserved">int</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain">) {</span>
|
|
<span class="reserved">switch</span><span class="plain">(</span><span class="identifier">reason</span><span class="plain">) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">CONDITION_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! True or false?"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NOW_ASSERTION_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! Force this to be true via 'now':"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">EXTREMAL_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! Find the extremal x satisfying:"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LOOP_DOMAIN_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! Find next x satisfying:"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LIST_OF_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! Construct a list of x satisfying:"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NUMBER_OF_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! How many x satisfy this?"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">TOTAL_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! Find a total property value over all x satisfying:"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">RANDOM_OF_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! Find a random x satisfying:"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">MULTIPURPOSE_DEFER:</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::code_comment</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"! Abstraction for set of x such that:"</span><span class="plain">); </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="identifier">default:</span><span class="plain"> </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"Unknown proposition deferral reason"</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2"></a><b>§2. Preliminaries. </b>We have seen that propositions are deferred for diverse reasons. Here we
|
|
take our medicine, and actually compile the deferred propositions into
|
|
routines. This is part of the phrase-compilation-coroutine process because
|
|
funny things can happen when we compile: we can create new text substitutions
|
|
which create routines which... and so on.
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="reserved">void</span><span class="plain"> </span><span class="functiontext">Calculus::Propositions::Deferred::compile_remaining_deferred<button class="popup" onclick="togglePopup('usagePopup840')">...<span class="popuptext" id="usagePopup840">Usage of <b>Calculus::Propositions::Deferred::compile_remaining_deferred</b>:<br>How To Compile - <a href="1-htc.html#SP2_8">§2.8</a></span></button></span><span class="plain">(</span><span class="reserved">void</span><span class="plain">) {</span>
|
|
<span class="functiontext"><a href="12-cdp.html#SP2">Calculus::Propositions::Deferred::compilation_coroutine</a></span><span class="plain">();</span>
|
|
<span class="plain">}</span>
|
|
|
|
<span class="reserved">pcalc_prop_deferral</span><span class="plain"> *</span><span class="identifier">latest_pcd</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="functiontext">Calculus::Propositions::Deferred::compilation_coroutine<button class="popup" onclick="togglePopup('usagePopup841')">...<span class="popuptext" id="usagePopup841">Usage of <b>Calculus::Propositions::Deferred::compilation_coroutine</b>:<br>Construction Sequence - <a href="22-cs.html#SP14">§14</a></span></button></span><span class="plain">(</span><span class="reserved">void</span><span class="plain">) {</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">N</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">TRUE</span><span class="plain">) {</span>
|
|
<span class="reserved">pcalc_prop_deferral</span><span class="plain"> *</span><span class="identifier">pdef</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">latest_pcd</span><span class="plain"> == </span><span class="identifier">NULL</span><span class="plain">)</span>
|
|
<span class="identifier">pdef</span><span class="plain"> = </span><span class="identifier">FIRST_OBJECT</span><span class="plain">(</span><span class="reserved">pcalc_prop_deferral</span><span class="plain">);</span>
|
|
<span class="reserved">else</span><span class="plain"> </span><span class="identifier">pdef</span><span class="plain"> = </span><span class="identifier">NEXT_OBJECT</span><span class="plain">(</span><span class="identifier">latest_pcd</span><span class="plain">, </span><span class="reserved">pcalc_prop_deferral</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pdef</span><span class="plain"> == </span><span class="identifier">NULL</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="identifier">latest_pcd</span><span class="plain"> = </span><span class="identifier">pdef</span><span class="plain">;</span>
|
|
<<span class="cwebmacro">Compile an individual deferred proposition</span> <span class="cwebmacronumber">2.1</span>><span class="plain">;</span>
|
|
<span class="identifier">N</span><span class="plain">++;</span>
|
|
<span class="plain">}</span>
|
|
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">N</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1"></a><b>§2.1. </b>The basic structure of a proposition routine is the same for all
|
|
of the various reasons, but with considerable variations affecting (mainly)
|
|
the initial setup and the returned value.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Note that the unchecked array bounds of 26 are safe here because
|
|
propositions may only use 26 different variables at most (<code class="display"><span class="extract">x</span></code>, <code class="display"><span class="extract">y</span></code>, <code class="display"><span class="extract">z</span></code>,
|
|
<code class="display"><span class="extract">a</span></code>, ..., <code class="display"><span class="extract">w</span></code>). There therefore can't be more than 26 callings, or 26
|
|
quantifiers, either.
|
|
</p>
|
|
|
|
|
|
<pre class="definitions">
|
|
<span class="definitionkeyword">define</span> <span class="constant">MAX_QC_VARIABLES</span><span class="plain"> </span><span class="constant">100</span>
|
|
</pre>
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile an individual deferred proposition</span> <span class="cwebmacronumber">2.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">pcalc_prop_deferral</span><span class="plain"> *</span><span class="identifier">save_current_pdef</span><span class="plain"> = </span><span class="identifier">current_pdef</span><span class="plain">;</span>
|
|
<span class="identifier">current_pdef</span><span class="plain"> = </span><span class="identifier">pdef</span><span class="plain">;</span>
|
|
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">ct_locals_problem_thrown</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">negated_quantifier_found</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
|
|
<span class="identifier">current_sentence</span><span class="plain"> = </span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">deferred_from</span><span class="plain">;</span>
|
|
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="11-pr.html#SP14">Calculus::Propositions::copy</a></span><span class="plain">(</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">proposition_to_defer</span><span class="plain">);</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">multipurpose_routine</span><span class="plain"> = (</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">reason</span><span class="plain"> == </span><span class="constant">MULTIPURPOSE_DEFER</span><span class="plain">)?</span><span class="identifier">TRUE:FALSE</span><span class="plain">;</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">CONDITION_DEFER</span><span class="plain">; </span><span class="comment"> redundant assignment to appease <code class="display"><span class="extract">gcc -O2</span></code></span>
|
|
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">reason_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">var_s</span><span class="plain">[26], *</span><span class="identifier">var_ix_s</span><span class="plain">[26];</span>
|
|
<span class="reserved">local_variable</span><span class="plain"> *</span><span class="identifier">var_ix_lv</span><span class="plain">[26];</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">qcy_s</span><span class="plain">[</span><span class="constant">MAX_QC_VARIABLES</span><span class="plain">], *</span><span class="identifier">qcn_s</span><span class="plain">[</span><span class="constant">MAX_QC_VARIABLES</span><span class="plain">];</span>
|
|
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">best_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">best_with_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">counter_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">list_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">selection_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">strong_kind_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">total_s</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
|
|
<span class="identifier">inter_symbol</span><span class="plain"> *</span><span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="constant">MULTIPURPOSE_DEFER</span><span class="plain">+1];</span>
|
|
<span class="reserved">for</span><span class="plain"> (</span><span class="reserved">int</span><span class="plain"> </span><span class="identifier">r</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">; </span><span class="identifier">r</span><span class="plain"> < </span><span class="constant">MULTIPURPOSE_DEFER</span><span class="plain">+1; </span><span class="identifier">r</span><span class="plain">++) </span><span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="identifier">r</span><span class="plain">] = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
|
|
<<span class="cwebmacro">Simplify the proposition by flipping negated quantifiers, if possible</span> <span class="cwebmacronumber">2.1.2</span>><span class="plain">;</span>
|
|
|
|
<span class="identifier">LOGIF</span><span class="plain">(</span><span class="identifier">PREDICATE_CALCULUS</span><span class="plain">, </span><span class="string">"Compiling deferred proposition: %d: reason %d: $D\n"</span><span class="plain">,</span>
|
|
<span class="identifier">pdef</span><span class="plain">-></span><span class="identifier">allocation_id</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">reason</span><span class="plain">, </span><span class="identifier">proposition</span><span class="plain">);</span>
|
|
|
|
<span class="identifier">packaging_state</span><span class="plain"> </span><span class="identifier">save</span><span class="plain"> = </span><span class="functiontext"><a href="26-rt.html#SP1">Routines::begin</a></span><span class="plain">(</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">ppd_iname</span><span class="plain">);</span>
|
|
|
|
<span class="constant">BEGIN_COMPILATION_MODE</span><span class="plain">;</span>
|
|
<span class="identifier">COMPILATION_MODE_EXIT</span><span class="plain">(</span><span class="constant">DEREFERENCE_POINTERS_CMODE</span><span class="plain">);</span>
|
|
<<span class="cwebmacro">Declare the I6 local variables which will be needed by this deferral routine</span> <span class="cwebmacronumber">2.1.5</span>><span class="plain">;</span>
|
|
<<span class="cwebmacro">Compile the code inside this deferral routine</span> <span class="cwebmacronumber">2.1.6</span>><span class="plain">;</span>
|
|
<<span class="cwebmacro">Issue a problem message if the table-lookup locals were needed</span> <span class="cwebmacronumber">2.1.3</span>><span class="plain">;</span>
|
|
<<span class="cwebmacro">Issue a problem message if a negated quantifier was needed</span> <span class="cwebmacronumber">2.1.4</span>><span class="plain">;</span>
|
|
<span class="constant">END_COMPILATION_MODE</span><span class="plain">;</span>
|
|
|
|
<span class="functiontext"><a href="26-rt.html#SP4">Routines::end</a></span><span class="plain">(</span><span class="identifier">save</span><span class="plain">);</span>
|
|
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pdef</span><span class="plain">-></span><span class="identifier">rtp_iname</span><span class="plain">) </span><<span class="cwebmacro">Compile the constant origin text for run-time problem use</span> <span class="cwebmacronumber">2.1.1</span>><span class="plain">;</span>
|
|
<span class="identifier">current_pdef</span><span class="plain"> = </span><span class="identifier">save_current_pdef</span><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2">§2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_1"></a><b>§2.1.1. </b>We compile the following only in cases where it seems possible that a
|
|
run-time problem message may be needed; compiling it for every deferred
|
|
proposition would be wasteful of space in the Z-machine.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile the constant origin text for run-time problem use</span> <span class="cwebmacronumber">2.1.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">TEMPORARY_TEXT</span><span class="plain">(</span><span class="identifier">COTT</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pdef</span><span class="plain">-></span><span class="identifier">deferred_from</span><span class="plain">)</span>
|
|
<span class="identifier">WRITE_TO</span><span class="plain">(</span><span class="identifier">COTT</span><span class="plain">, </span><span class="string">"%~W"</span><span class="plain">, </span><span class="identifier">ParseTree::get_text</span><span class="plain">(</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">deferred_from</span><span class="plain">));</span>
|
|
<span class="reserved">else</span>
|
|
<span class="identifier">WRITE_TO</span><span class="plain">(</span><span class="identifier">COTT</span><span class="plain">, </span><span class="string">"not sure where this came from"</span><span class="plain">);</span>
|
|
<span class="functiontext"><a href="27-em.html#SP3">Emit::named_string_constant</a></span><span class="plain">(</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">rtp_iname</span><span class="plain">, </span><span class="identifier">COTT</span><span class="plain">);</span>
|
|
<span class="identifier">DISCARD_TEXT</span><span class="plain">(</span><span class="identifier">COTT</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1">§2.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_2"></a><b>§2.1.2. </b>Just in case this hasn't already been done:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Simplify the proposition by flipping negated quantifiers, if possible</span> <span class="cwebmacronumber">2.1.2</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">changed</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="11-sm.html#SP5">Calculus::Simplifications::negated_determiners</a></span><span class="plain">(</span><span class="identifier">proposition</span><span class="plain">, &</span><span class="identifier">changed</span><span class="plain">, </span><span class="identifier">TRUE</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">changed</span><span class="plain">) {</span>
|
|
<span class="identifier">LOGIF</span><span class="plain">(</span><span class="identifier">PREDICATE_CALCULUS</span><span class="plain">, </span><span class="string">"Calculus::Simplifications::negated_determiners: $D\n"</span><span class="plain">, </span><span class="identifier">proposition</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1">§2.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_3"></a><b>§2.1.3. </b>While unfortunate in a way, this is for the best, because a successful
|
|
match on a condition looking up a table would record the table and row
|
|
in local variables within the deferred proposition: they would then be
|
|
wrong in the calling routine, where they are needed.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Issue a problem message if the table-lookup locals were needed</span> <span class="cwebmacronumber">2.1.3</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> ((</span><span class="functiontext"><a href="24-lv.html#SP22">LocalVariables::are_we_using_table_lookup</a></span><span class="plain">()) && (!</span><span class="identifier">ct_locals_problem_thrown</span><span class="plain">)) {</span>
|
|
<span class="identifier">ct_locals_problem_thrown</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="identifier">Problems::Issue::sentence_problem</span><span class="plain">(</span><span class="functiontext"><a href="1-wtc.html#SP5">Task::syntax_tree</a></span><span class="plain">(), </span><span class="identifier">_p_</span><span class="plain">(</span><span class="identifier">PM_CantLookUpTableInDeferred</span><span class="plain">),</span>
|
|
<span class="string">"I am not able to look up table entries in this complicated "</span>
|
|
<span class="string">"condition"</span><span class="plain">,</span>
|
|
<span class="string">"which seems to involve making a potentially large number "</span>
|
|
<span class="string">"of checks in rather few words (and may perhaps result from "</span>
|
|
<span class="string">"a misunderstanding such as writing the name of a kind where "</span>
|
|
<span class="string">"an individual object is intended?)."</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1">§2.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_4"></a><b>§2.1.4. </b>This looks like a horrible restriction, but in fact propositions are
|
|
built and simplified in such a way that it never bites. (Quantifiers are
|
|
always moved outside of negation where possible, and it is almost always
|
|
possible.)
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Issue a problem message if a negated quantifier was needed</span> <span class="cwebmacronumber">2.1.4</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">negated_quantifier_found</span><span class="plain">) {</span>
|
|
<span class="identifier">Problems::Issue::sentence_problem</span><span class="plain">(</span><span class="functiontext"><a href="1-wtc.html#SP5">Task::syntax_tree</a></span><span class="plain">(), </span><span class="identifier">_p_</span><span class="plain">(</span><span class="identifier">BelievedImpossible</span><span class="plain">),</span>
|
|
<span class="string">"this involves a very complicated negative thought"</span><span class="plain">,</span>
|
|
<span class="string">"which I'm not able to untangle. Perhaps you could rephrase "</span>
|
|
<span class="string">"this more simply, or split it into more than one sentence?"</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1">§2.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_5"></a><b>§2.1.5. </b>Recall that an I6 function header consists of a <code class="display"><span class="extract">[</span></code>, then an identifier
|
|
name for the function — in this case always <code class="display"><span class="extract">Prop_N</span></code> for some number <code class="display"><span class="extract">N</span></code> —
|
|
and then a space-delimited list of local variable names, the initial of
|
|
which are used to receive function arguments. The order of the variables
|
|
is: any cinders (constants evaluated back at deferral time and being
|
|
handed forward on the stack as function arguments); then any variables
|
|
in the predicate calculus sense, of which the first may or may not be
|
|
being used as a function argument, depending on whether or not it is
|
|
bound; then the enumeration variables needed to compile generalised
|
|
quantifiers, if any; and finally any oddball variables needed by code
|
|
specific to particular deferral reasons.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Declare the I6 local variables which will be needed by this deferral routine</span> <span class="cwebmacronumber">2.1.5</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">j</span><span class="plain">, </span><span class="identifier">var_states</span><span class="plain">[26], </span><span class="identifier">no_extras</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">multipurpose_routine</span><span class="plain">)</span>
|
|
<span class="identifier">reason_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_named_call_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"reason"</span><span class="plain">); </span><span class="comment"> no cinders exist here</span>
|
|
<span class="reserved">else</span>
|
|
<span class="functiontext"><a href="12-cad.html#SP5">Calculus::Deferrals::Cinders::declare</a></span><span class="plain">(</span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
|
|
<<span class="cwebmacro">Declare the I6 call parameters needed by adaptations to particular deferral cases</span> <span class="cwebmacronumber">2.1.5.2</span>><span class="plain">;</span>
|
|
|
|
<span class="functiontext"><a href="11-bas.html#SP4">Calculus::Variables::determine_status</a></span><span class="plain">(</span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">var_states</span><span class="plain">, </span><span class="identifier">NULL</span><span class="plain">);</span>
|
|
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">j</span><span class="plain">=0; </span><span class="identifier">j</span><span class="plain"><26; </span><span class="identifier">j</span><span class="plain">++)</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">var_states</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] != </span><span class="constant">UNUSED_VST</span><span class="plain">) {</span>
|
|
<span class="identifier">TEMPORARY_TEXT</span><span class="plain">(</span><span class="identifier">letter_var</span><span class="plain">);</span>
|
|
<span class="identifier">PUT_TO</span><span class="plain">(</span><span class="identifier">letter_var</span><span class="plain">, </span><span class="identifier">pcalc_vars</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]);</span>
|
|
<span class="identifier">var_s</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">letter_var</span><span class="plain">);</span>
|
|
<span class="identifier">WRITE_TO</span><span class="plain">(</span><span class="identifier">letter_var</span><span class="plain">, </span><span class="string">"_ix"</span><span class="plain">);</span>
|
|
<span class="identifier">var_ix_s</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol_noting</a></span><span class="plain">(</span><span class="identifier">letter_var</span><span class="plain">, &(</span><span class="identifier">var_ix_lv</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">]));</span>
|
|
<span class="identifier">DISCARD_TEXT</span><span class="plain">(</span><span class="identifier">letter_var</span><span class="plain">);</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="identifier">var_s</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">var_ix_s</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="identifier">var_ix_lv</span><span class="plain">[</span><span class="identifier">j</span><span class="plain">] = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
|
|
<span class="identifier">no_extras</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
|
|
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">proposition</span><span class="plain">)</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">element</span><span class="plain"> == </span><span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">) {</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">no_extras</span><span class="plain"> >= </span><span class="constant">MAX_QC_VARIABLES</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="identifier">TEMPORARY_TEXT</span><span class="plain">(</span><span class="identifier">q_var</span><span class="plain">);</span>
|
|
<span class="identifier">WRITE_TO</span><span class="plain">(</span><span class="identifier">q_var</span><span class="plain">, </span><span class="string">"qcy_%d"</span><span class="plain">, </span><span class="identifier">no_extras</span><span class="plain">);</span>
|
|
<span class="identifier">qcy_s</span><span class="plain">[</span><span class="identifier">no_extras</span><span class="plain">] = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">q_var</span><span class="plain">);</span>
|
|
<span class="identifier">Str::clear</span><span class="plain">(</span><span class="identifier">q_var</span><span class="plain">);</span>
|
|
<span class="identifier">WRITE_TO</span><span class="plain">(</span><span class="identifier">q_var</span><span class="plain">, </span><span class="string">"qcn_%d"</span><span class="plain">, </span><span class="identifier">no_extras</span><span class="plain">);</span>
|
|
<span class="identifier">qcn_s</span><span class="plain">[</span><span class="identifier">no_extras</span><span class="plain">] = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">q_var</span><span class="plain">);</span>
|
|
<span class="identifier">DISCARD_TEXT</span><span class="plain">(</span><span class="identifier">q_var</span><span class="plain">);</span>
|
|
<span class="identifier">no_extras</span><span class="plain">++;</span>
|
|
<span class="plain">}</span>
|
|
|
|
<<span class="cwebmacro">Declare the I6 locals needed by adaptations to particular deferral cases</span> <span class="cwebmacronumber">2.1.5.1</span>><span class="plain">;</span>
|
|
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1">§2.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6"></a><b>§2.1.6. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Compile the code inside this deferral routine</span> <span class="cwebmacronumber">2.1.6</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">multipurpose_routine</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">reason_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">reason_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">reason_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, (</span><span class="identifier">inter_t</span><span class="plain">) </span><span class="constant">CONDITION_DUSAGE</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">SWITCH_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">reason_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">safety_copy</span><span class="plain"> = </span><span class="functiontext"><a href="11-pr.html#SP14">Calculus::Propositions::copy</a></span><span class="plain">(</span><span class="identifier">proposition</span><span class="plain">);</span>
|
|
<span class="reserved">for</span><span class="plain"> (</span><span class="reserved">int</span><span class="plain"> </span><span class="identifier">use</span><span class="plain"> = </span><span class="constant">EXTREMAL_DUSAGE</span><span class="plain">; </span><span class="identifier">use</span><span class="plain"> <= </span><span class="constant">CONDITION_DUSAGE</span><span class="plain">; </span><span class="identifier">use</span><span class="plain">++) {</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">use</span><span class="plain"> > </span><span class="constant">EXTREMAL_DUSAGE</span><span class="plain">) </span><span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="11-pr.html#SP14">Calculus::Propositions::copy</a></span><span class="plain">(</span><span class="identifier">safety_copy</span><span class="plain">);</span>
|
|
<span class="reserved">switch</span><span class="plain"> (</span><span class="identifier">use</span><span class="plain">) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">CONDITION_DUSAGE:</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">CONDITION_DEFER</span><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LOOP_DOMAIN_DUSAGE:</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">LOOP_DOMAIN_DEFER</span><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LIST_OF_DUSAGE:</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">LIST_OF_DEFER</span><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NUMBER_OF_DUSAGE:</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">NUMBER_OF_DEFER</span><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">RANDOM_OF_DUSAGE:</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">RANDOM_OF_DEFER</span><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">TOTAL_DUSAGE:</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">TOTAL_DEFER</span><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">EXTREMAL_DUSAGE:</span><span class="plain"> </span><span class="identifier">reason</span><span class="plain"> = </span><span class="constant">EXTREMAL_DEFER</span><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">CASE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, (</span><span class="identifier">inter_t</span><span class="plain">) </span><span class="identifier">use</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="functiontext"><a href="12-cdp.html#SP1">Calculus::Propositions::Deferred::compile_comment_about_deferral_reason</a></span><span class="plain">(</span><span class="identifier">reason</span><span class="plain">);</span>
|
|
<<span class="cwebmacro">Compile body of deferred proposition for the given reason</span> <span class="cwebmacronumber">2.1.6.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="identifier">reason</span><span class="plain"> = </span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">reason</span><span class="plain">;</span>
|
|
<<span class="cwebmacro">Compile body of deferred proposition for the given reason</span> <span class="cwebmacronumber">2.1.6.1</span>><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1">§2.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1"></a><b>§2.1.6.1. </b>From here on, we compile the body of a routine to handle the deferral case
|
|
in the variable <code class="display"><span class="extract">reason</span></code>.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">What these different cases have in common is that each is basically a search
|
|
of all possible values of the bound variables in the expression. There will
|
|
be some initialisation, something to do with each successfully found
|
|
combination, and eventually some winding-up code. For example, "number of..."
|
|
initialises by setting <code class="display"><span class="extract">counter</span></code> to 0, on each success it performs <code class="display"><span class="extract">counter++</span></code>,
|
|
and at the end of the search it performs <code class="display"><span class="extract">return counter</span></code>.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile body of deferred proposition for the given reason</span> <span class="cwebmacronumber">2.1.6.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">property</span><span class="plain"> *</span><span class="identifier">prn</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="reserved">property</span><span class="plain"> *</span><span class="identifier">def_prn</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">def_prn_sign</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">OL</span><span class="plain"> = </span><span class="identifier">Produce::level</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="reserved">switch</span><span class="plain">(</span><span class="identifier">reason</span><span class="plain">) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NOW_ASSERTION_DEFER:</span><span class="plain"> </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">CONDITION_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Initialisation before CONDITION search</span> <span class="cwebmacronumber">2.1.6.1.3</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">EXTREMAL_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Initialisation before EXTREMAL search</span> <span class="cwebmacronumber">2.1.6.1.14</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LOOP_DOMAIN_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Initialisation before LOOP search</span> <span class="cwebmacronumber">2.1.6.1.17</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NUMBER_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Initialisation before NUMBER search</span> <span class="cwebmacronumber">2.1.6.1.5</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LIST_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Initialisation before LIST search</span> <span class="cwebmacronumber">2.1.6.1.8</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">TOTAL_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Initialisation before TOTAL search</span> <span class="cwebmacronumber">2.1.6.1.12</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">RANDOM_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Initialisation before RANDOM search</span> <span class="cwebmacronumber">2.1.6.1.10</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<<span class="cwebmacro">Compile code to search for valid combinations of variables</span> <span class="cwebmacronumber">2.1.6.1.2</span>><span class="plain">;</span>
|
|
|
|
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">reason</span><span class="plain"> != </span><span class="constant">NOW_ASSERTION_DEFER</span><span class="plain">) && (</span><span class="identifier">reason</span><span class="plain"> != </span><span class="constant">CONDITION_DEFER</span><span class="plain">)) {</span>
|
|
<<span class="cwebmacro">Place next outer loop label</span> <span class="cwebmacronumber">2.1.6.1.6</span>><span class="plain">;</span>
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">Produce::level</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">()) > </span><span class="identifier">OL</span><span class="plain">) </span><span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">}</span>
|
|
|
|
<span class="reserved">switch</span><span class="plain">(</span><span class="identifier">reason</span><span class="plain">) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NOW_ASSERTION_DEFER:</span><span class="plain"> </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">CONDITION_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Winding-up after CONDITION search</span> <span class="cwebmacronumber">2.1.6.1.4</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">EXTREMAL_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Winding-up after EXTREMAL search</span> <span class="cwebmacronumber">2.1.6.1.15</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LOOP_DOMAIN_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Winding-up after LOOP search</span> <span class="cwebmacronumber">2.1.6.1.18</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NUMBER_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Winding-up after NUMBER search</span> <span class="cwebmacronumber">2.1.6.1.7</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LIST_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Winding-up after LIST search</span> <span class="cwebmacronumber">2.1.6.1.9</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">TOTAL_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Winding-up after TOTAL search</span> <span class="cwebmacronumber">2.1.6.1.13</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">RANDOM_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Winding-up after RANDOM search</span> <span class="cwebmacronumber">2.1.6.1.11</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6">§2.1.6</a> (twice).</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_1"></a><b>§2.1.6.1.1. The Search. </b>We can now begin the real work. Given \(\phi\), we compile I6 code which
|
|
contains a magic position M (for "match") such that M is visited exactly
|
|
once for every combination of possible substitutions into the bound
|
|
variables such that \(\phi\) is true. For example,
|
|
$$ \exists x: {\it door}(x)\land{\it open}(x)\land \exists y: {\it room}(y)\land{\it in}(x, y) $$
|
|
might compile to code in the form:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">blah, blah, blah {</span>
|
|
<span class="plain">M</span>
|
|
<span class="plain">} rhubarb, rhubarb</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">such that execution reaches <code class="display"><span class="extract">M</span></code> exactly once for each combination of open
|
|
door \(x\) and room \(y\) such that \(x\) is in \(y\). (Position <code class="display"><span class="extract">M</span></code> is where we
|
|
will place the case-dependent code for what to do on a successful match.)
|
|
In the language of model theory, this is a loop over all interpretations
|
|
in which \(\phi\) is true.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">We will do this by compiling the proposition from left to right. If there
|
|
are \(k\) atoms in \(\phi\), then there are \(k+1\) positions between atoms,
|
|
counting the start and the end. Then:
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Invariant.\quad Let \(\psi\) be any syntactically valid subproposition
|
|
of \(\phi\) (that is, a contiguous sequence of atoms from \(\psi\) which would
|
|
be a valid proposition in its own right). Then there are before and after
|
|
positions <code class="display"><span class="extract">B</span></code> and <code class="display"><span class="extract">A</span></code> in the compiled I6 code for searching \(\phi\) such that
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) <code class="display"><span class="extract">A</span></code> cannot be reached except from <code class="display"><span class="extract">B</span></code>, and
|
|
</li><li>(b) at execution time, on every occasion <code class="display"><span class="extract">B</span></code> is reached, <code class="display"><span class="extract">A</span></code> is then reached
|
|
exactly once for each combination of possible substitutions into the
|
|
\(\exists\)-bound variables of \(\psi\) such that \(\psi\) is then true.
|
|
</li></ul>
|
|
<p class="inwebparagraph">In particular, in the case when \(\psi = \phi\), <code class="display"><span class="extract">B</span></code> is the start of our
|
|
compiled I6 code (before anything is done) and <code class="display"><span class="extract">A</span></code> is the magic match
|
|
position <code class="display"><span class="extract">M</span></code>.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">The restriction to syntactically valid subpropositions is important. Suppose
|
|
\(\phi\) arises from "all doors are open" and is stored in memory as:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">Forall x IN[ door(x) IN] open(x)</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">Then <code class="display"><span class="extract">door(x)</span></code> and <code class="display"><span class="extract">Forall x IN[ door(x) IN]</span></code> are valid, for instance, but
|
|
<code class="display"><span class="extract">IN] open(x)</span></code> is not.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Lemma.\quad If the Invariant holds for two adjacent syntactically valid
|
|
subpropositions \(\mu\) and \(\nu\), then it holds for the subproposition \(\mu\nu\).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Proof.\quad There are now three positions in the code: <code class="display"><span class="extract">B1</span></code>, before \(\mu\);
|
|
<code class="display"><span class="extract">B2</span></code>, before \(\nu\), which is the same position as after \(\mu\); and <code class="display"><span class="extract">A</span></code>, after
|
|
\(\nu\). Execution reaches <code class="display"><span class="extract">B2</span></code> \(m\) times for each visit to <code class="display"><span class="extract">B1</span></code>, where \(m\)
|
|
is the number of combinations of viable bound variable values in \(\mu\).
|
|
Execution reaches <code class="display"><span class="extract">A</span></code> \(n\) times for each visit to <code class="display"><span class="extract">B2</span></code>, where \(n\) is the
|
|
similar number for \(\nu\). Therefore execution reaches <code class="display"><span class="extract">A</span></code> a total of \(nm\)
|
|
times for each visit to <code class="display"><span class="extract">B1</span></code>, the product of the number of variable combinations
|
|
in \(\mu\) and \(\nu\), which is exactly the number of combinations in total.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Corollary.\quad If the Invariant holds for subpropositions in each of
|
|
the following forms, then it will hold overall.
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) <code class="display"><span class="extract">Exists v</span></code>, for some variable \(v\), or <code class="display"><span class="extract">Q v IN[ ... IN]</span></code>, for some quantifier other than \(\exists\).
|
|
</li><li>(b) <code class="display"><span class="extract">NOT[ ... NOT]</span></code>.
|
|
</li><li>(c) any single predicate-like atom.
|
|
</li></ul>
|
|
<p class="inwebparagraph">Proof.\quad Because all valid subpropositions are concatenations of
|
|
these, and we then apply the Lemma.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">It follows that if we can prove our algorithm maintains the invariant in
|
|
cases (a) to (d), we can be sure it will correctly construct code leading
|
|
to the match point <code class="display"><span class="extract">M</span></code>.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2"></a><b>§2.1.6.1.2. </b>We will make use of three stacks:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(a) The R-stack, which holds the current "reason": the goal being pursued
|
|
by the I6 code currently being compiled.
|
|
</li><li>(b) The Q-stack, which holds details of quantifiers being searched on.
|
|
</li><li>(c) The C-stack, which holds details of callings of variables.
|
|
</li></ul>
|
|
<p class="inwebparagraph">Since each is tied to a quantifier, each of which is tied to a distinct
|
|
variable, and there are at most 26 variables, we need a worst-case
|
|
capacity of 27 slots on the R-stack (counting the initial <code class="display"><span class="extract">reason</span></code>) and
|
|
26 on the Q-stack and C-stack.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile code to search for valid combinations of variables</span> <span class="cwebmacronumber">2.1.6.1.2</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">block_nesting</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">; </span><span class="comment"> how many <code class="display"><span class="extract">{</span></code> ... <code class="display"><span class="extract">}</span></code> blocks are open in I6 code being compiled</span>
|
|
|
|
<span class="comment"> The R-stack</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">R_stack_reason</span><span class="plain">[27];</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">R_stack_parity</span><span class="plain">[27];</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">R_sp</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
|
|
<span class="comment"> The Q-stack</span>
|
|
<span class="identifier">quantifier</span><span class="plain"> *</span><span class="identifier">Q_stack_quantifier</span><span class="plain">[26];</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">Q_stack_parameter</span><span class="plain">[26];</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">Q_stack_C_stack_level</span><span class="plain">[26];</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">Q_stack_block_nesting</span><span class="plain">[26];</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">Q_sp</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
|
|
<span class="comment"> The C-stack</span>
|
|
<span class="reserved">pcalc_term</span><span class="plain"> </span><span class="identifier">C_stack_term</span><span class="plain">[26]; </span><span class="comment"> the term to which a called-name is being given</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">C_stack_index</span><span class="plain">[26]; </span><span class="comment"> its index in the <code class="display"><span class="extract">deferred_calling_list</span></code></span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">C_sp</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
|
|
<span class="comment"> The L-stack</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">L_stack_level</span><span class="plain">[26]; </span><span class="comment"> emission level at start of block</span>
|
|
<span class="comment"> block_nesting serves at stack pointer here</span>
|
|
|
|
<<span class="cwebmacro">Push initial reason onto the R-stack</span> <span class="cwebmacronumber">2.1.6.1.2.1</span>><span class="plain">;</span>
|
|
<span class="comment"> we now begin compiling the search code</span>
|
|
<<span class="cwebmacro">Compile the proposition into a search algorithm</span> <span class="cwebmacronumber">2.1.6.1.2.3</span>><span class="plain">;</span>
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">Q_sp</span><span class="plain"> > </span><span class="constant">0</span><span class="plain">) </span><<span class="cwebmacro">Pop the Q-stack</span> <span class="cwebmacronumber">2.1.6.1.2.4</span>><span class="plain">;</span>
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">C_sp</span><span class="plain"> > </span><span class="constant">0</span><span class="plain">) </span><<span class="cwebmacro">Pop the C-stack</span> <span class="cwebmacronumber">2.1.6.1.2.5</span>><span class="plain">;</span>
|
|
<span class="comment"> we are now at the magic match point <code class="display"><span class="extract">M</span></code> in the search code</span>
|
|
<<span class="cwebmacro">Pop the R-stack</span> <span class="cwebmacronumber">2.1.6.1.2.2</span>><span class="plain">;</span>
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">block_nesting</span><span class="plain"> > </span><span class="constant">0</span><span class="plain">)</span>
|
|
<<span class="cwebmacro">Close a block in the I6 code compiled to perform the search</span> <span class="cwebmacronumber">2.1.6.1.2.6</span>><span class="plain">;</span>
|
|
<span class="comment"> we have now finished compiling the search code</span>
|
|
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">R_sp</span><span class="plain"> != </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"R-stack failure"</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">Q_sp</span><span class="plain"> != </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"Q-stack failure"</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">C_sp</span><span class="plain"> != </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"C-stack failure"</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_1"></a><b>§2.1.6.1.2.1. The R-stack. </b>This is a sort of "split goals into sub-goals" mechanism. In order to
|
|
determine
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>if all but one of the closed doors are unlocked, ...</p>
|
|
|
|
</blockquote>
|
|
|
|
<p class="inwebparagraph">our main goal is to determine the truth of the "are unlocked" part. This
|
|
is reason <code class="display"><span class="extract">CONDITION_DEFER</span></code>, and it is pushed onto the R-stack at the
|
|
start of the compilation:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Push initial reason onto the R-stack</span> <span class="cwebmacronumber">2.1.6.1.2.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">R_stack_reason</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">] = </span><span class="identifier">reason</span><span class="plain">;</span>
|
|
<span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">] = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="identifier">R_sp</span><span class="plain">++;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2">§2.1.6.1.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP_1"></a><b>§.1. </b>But in order to work this out, we have to work out which doors are
|
|
closed, and this is a subgoal to which we give the pseudo-reason
|
|
<code class="display"><span class="extract">FILTER_DEFER</span></code>. We push this new sub-goal onto the R-stack, leaving the
|
|
original to be resumed when we're done.
|
|
</p>
|
|
|
|
|
|
<pre class="definitions">
|
|
<span class="definitionkeyword">define</span> <span class="constant">FILTER_DEFER</span><span class="plain"> </span><span class="constant">10000</span><span class="plain"> </span><span class="comment"> pseudo-reason value used only inside this routine</span>
|
|
</pre>
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Push domain-opening onto the R-stack</span> <span class="cwebmacronumber">.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">R_stack_reason</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">] = </span><span class="constant">FILTER_DEFER</span><span class="plain">;</span>
|
|
<span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">] = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="identifier">R_sp</span><span class="plain">++;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2"></a><b>§2.1.6.1.2.2. </b>The R-stack is then popped when the goal is accomplished (or rather, when
|
|
the I6 code we are compiling has reached a point which will be executed when
|
|
its goal has been accomplished).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">In the case of <code class="display"><span class="extract">FILTER_DEFER</span></code>, when scanning domains of quantifiers, we
|
|
increment the count of the domain set size — the number of closed doors,
|
|
in the above example. (See below.)
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Pop the R-stack</span> <span class="cwebmacronumber">2.1.6.1.2.2</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">R_sp</span><span class="plain">--; </span><span class="reserved">if</span><span class="plain"> (</span><span class="identifier">R_sp</span><span class="plain"> < </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"R stack underflow"</span><span class="plain">);</span>
|
|
|
|
<span class="reserved">switch</span><span class="plain">(</span><span class="identifier">R_stack_reason</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">]) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">FILTER_DEFER:</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">POSTINCREMENT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">qcn_s</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">-1]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NOW_ASSERTION_DEFER:</span><span class="plain"> </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">CONDITION_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Act on successful match in CONDITION search</span> <span class="cwebmacronumber">2.1.6.1.2.2.1</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">EXTREMAL_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Act on successful match in EXTREMAL search</span> <span class="cwebmacronumber">2.1.6.1.2.2.6</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LOOP_DOMAIN_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Act on successful match in LOOP search</span> <span class="cwebmacronumber">2.1.6.1.2.2.7</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NUMBER_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Act on successful match in NUMBER search</span> <span class="cwebmacronumber">2.1.6.1.2.2.2</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LIST_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Act on successful match in LIST search</span> <span class="cwebmacronumber">2.1.6.1.2.2.3</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">TOTAL_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Act on successful match in TOTAL search</span> <span class="cwebmacronumber">2.1.6.1.2.2.5</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">RANDOM_OF_DEFER:</span><span class="plain"> </span><<span class="cwebmacro">Act on successful match in RANDOM search</span> <span class="cwebmacronumber">2.1.6.1.2.2.4</span>><span class="plain">; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2">§2.1.6.1.2</a>, <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3"></a><b>§2.1.6.1.2.3. Compiling the search. </b>In the following we run through the proposition from left to right, compiling
|
|
I6 code as we go, but preserving the Invariant.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile the proposition into a search algorithm</span> <span class="cwebmacronumber">2.1.6.1.2.3</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">run_of_conditions</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">no_deferred_callings</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">; </span><span class="comment"> how many <code class="display"><span class="extract">CALLED</span></code> atoms have been found to date</span>
|
|
|
|
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">proposition</span><span class="plain">) {</span>
|
|
<span class="reserved">switch</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">element</span><span class="plain">) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NEGATION_OPEN_ATOM:</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NEGATION_CLOSE_ATOM:</span>
|
|
<<span class="cwebmacro">End a run of predicate-like conditions, if one is under way</span> <span class="cwebmacronumber">2.1.6.1.2.3.3</span>><span class="plain">;</span>
|
|
<span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] = (</span><span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1])?</span><span class="identifier">FALSE:TRUE</span><span class="plain">; </span><span class="comment"> reverse parity</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">QUANTIFIER_ATOM:</span>
|
|
<<span class="cwebmacro">End a run of predicate-like conditions, if one is under way</span> <span class="cwebmacronumber">2.1.6.1.2.3.3</span>><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] == </span><span class="identifier">FALSE</span><span class="plain">) </span><span class="identifier">negated_quantifier_found</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="identifier">quantifier</span><span class="plain"> *</span><span class="identifier">quant</span><span class="plain"> = </span><span class="identifier">RETRIEVE_POINTER_quantifier</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">predicate</span><span class="plain">);</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">param</span><span class="plain"> = </span><span class="functiontext"><a href="11-ap.html#SP9">Calculus::Atoms::get_quantification_parameter</a></span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">quant</span><span class="plain"> != </span><span class="identifier">exists_quantifier</span><span class="plain">) </span><<span class="cwebmacro">Push the Q-stack</span> <span class="cwebmacronumber">2.1.6.1.2.3.7</span>><span class="plain">;</span>
|
|
<<span class="cwebmacro">Compile a loop through possible values of the variable quantified</span> <span class="cwebmacronumber">2.1.6.1.2.3.5</span>><span class="plain">;</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">DOMAIN_OPEN_ATOM:</span>
|
|
<<span class="cwebmacro">End a run of predicate-like conditions, if one is under way</span> <span class="cwebmacronumber">2.1.6.1.2.3.3</span>><span class="plain">;</span>
|
|
<<span class="cwebmacro">Push domain-opening onto the R-stack</span> <span class="cwebmacronumber">.1</span>><span class="plain">;</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">DOMAIN_CLOSE_ATOM:</span>
|
|
<<span class="cwebmacro">End a run of predicate-like conditions, if one is under way</span> <span class="cwebmacronumber">2.1.6.1.2.3.3</span>><span class="plain">;</span>
|
|
<<span class="cwebmacro">Pop the R-stack</span> <span class="cwebmacronumber">2.1.6.1.2.2</span>><span class="plain">;</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">CALLED_ATOM:</span>
|
|
<<span class="cwebmacro">Push the C-stack</span> <span class="cwebmacronumber">2.1.6.1.2.3.8</span>><span class="plain">;</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="identifier">default:</span><span class="plain"> {</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">R_stack_reason</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] == </span><span class="constant">NOW_ASSERTION_DEFER</span><span class="plain">)</span>
|
|
<<span class="cwebmacro">Compile code to force the atom</span> <span class="cwebmacronumber">2.1.6.1.2.3.4</span>>
|
|
<span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">last_in_run</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">, </span><span class="identifier">first_in_run</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">run_of_conditions</span><span class="plain">++ > </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">first_in_run</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
|
|
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">ex</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-></span><span class="element">next</span><span class="plain">;</span>
|
|
<span class="reserved">while</span><span class="plain"> ((</span><span class="identifier">ex</span><span class="plain">) && (</span><span class="identifier">ex</span><span class="plain">-></span><span class="element">element</span><span class="plain"> == </span><span class="constant">CALLED_ATOM</span><span class="plain">)) </span><span class="identifier">ex</span><span class="plain"> = </span><span class="identifier">ex</span><span class="plain">-></span><span class="element">next</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">ex</span><span class="plain">) {</span>
|
|
<span class="reserved">switch</span><span class="plain">(</span><span class="identifier">ex</span><span class="plain">-></span><span class="identifier">element</span><span class="plain">) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NEGATION_OPEN_ATOM:</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NEGATION_CLOSE_ATOM:</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">QUANTIFIER_ATOM:</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">DOMAIN_OPEN_ATOM:</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">DOMAIN_CLOSE_ATOM:</span>
|
|
<span class="identifier">last_in_run</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="identifier">default:</span>
|
|
<span class="identifier">last_in_run</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<<span class="cwebmacro">Compile code to test the atom</span> <span class="cwebmacronumber">2.1.6.1.2.3.2</span>><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<<span class="cwebmacro">End a run of predicate-like conditions, if one is under way</span> <span class="cwebmacronumber">2.1.6.1.2.3.3</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2">§2.1.6.1.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_1"></a><b>§2.1.6.1.2.3.1. Predicate runs and their negations. </b>Or, cheating Professor de Morgan.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">If we have a run of predicate-like atoms — say X, Y, Z — then this amounts
|
|
to a conjunction: \(X\land Y\land Z\). The obvious way to compile code for this
|
|
would be to take one term at a time:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">if (X)</span>
|
|
<span class="plain">if (Y)</span>
|
|
<span class="plain">if (Z)</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">That satisfies the Invariant, and is clearly correct. But we want to use the
|
|
same mechanism when looking at a negation, and then it would go wrong.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Note that if \(\phi\) contains \(\lnot(\psi)\) then \(\psi\) must be a
|
|
conjunction of predicate-like atoms. (Otherwise a problem message would be
|
|
issued and in that case it doesn't matter what code we compile, so long as
|
|
we don't crash: it will never be run.) Thus we can assume that between
|
|
<code class="display"><span class="extract">NEGATION_OPEN_ATOM</span></code> and <code class="display"><span class="extract">NEGATION_CLOSE_ATOM</span></code> is a predicate run.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Between negation brackets, then, we must interpret X, Y, Z as
|
|
\(\lnot(X\land Y\land Z)\), and we need to compile that to
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">if (~~(X && Y && Z))</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">rather than
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">if (~~X)</span>
|
|
<span class="plain">if (~~Y)</span>
|
|
<span class="plain">if (~~Z)</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">which gets de Morgan's laws wrong.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_2"></a><b>§2.1.6.1.2.3.2. </b>That means a little fancy footwork to start and finish the compound <code class="display"><span class="extract">if</span></code>
|
|
statement properly:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile code to test the atom</span> <span class="cwebmacronumber">2.1.6.1.2.3.2</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">first_in_run</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] == </span><span class="identifier">FALSE</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">NOT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">last_in_run</span><span class="plain"> == </span><span class="identifier">FALSE</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">AND_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">}</span>
|
|
<span class="functiontext"><a href="12-ca.html#SP5">Calculus::Atoms::Compile::emit</a></span><span class="plain">(</span><span class="constant">TEST_ATOM_TASK</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">TRUE</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_3"></a><b>§2.1.6.1.2.3.3. </b><code class="display">
|
|
<<span class="cwebmacrodefn">End a run of predicate-like conditions, if one is under way</span> <span class="cwebmacronumber">2.1.6.1.2.3.3</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">run_of_conditions</span><span class="plain"> > </span><span class="constant">0</span><span class="plain">) {</span>
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">run_of_conditions</span><span class="plain"> > </span><span class="constant">1</span><span class="plain">) { </span><span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">()); </span><span class="identifier">run_of_conditions</span><span class="plain">--; }</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] == </span><span class="identifier">FALSE</span><span class="plain">) { </span><span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">()); }</span>
|
|
<span class="identifier">run_of_conditions</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">;</span>
|
|
<<span class="cwebmacro">Open a block in the I6 code compiled to perform the search, if variant</span> <span class="cwebmacronumber">2.1.6.1.2.3.3.1</span>><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a> (five times).</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_4"></a><b>§2.1.6.1.2.3.4. </b>The <code class="display"><span class="extract">NOW_ASSERTION_DEFER</span></code> reason is different from all of the others,
|
|
because rather than searching for a given situation it tries force it to
|
|
happen (or not to). Forcing rather than testing is easy here: we just supply
|
|
a different task when calling <code class="display"><span class="extract">Calculus::Atoms::Compile::compile</span></code>.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">In the negated case, we again cheat de Morgan, by falsifying \(\phi\) more
|
|
aggressively than we need: we force \(\lnot(X)\land\lnot(Y)\land\lnot(Z)\) to
|
|
be true, though strictly speaking it would be enough to falsify X alone.
|
|
(We do it that way for consistency with the same convention when asserting
|
|
about the model world.)
|
|
</p>
|
|
|
|
<p class="inwebparagraph">We don't need to consider runs of predicates for that; we can take the atoms
|
|
one at a time.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile code to force the atom</span> <span class="cwebmacronumber">2.1.6.1.2.3.4</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="functiontext"><a href="12-ca.html#SP5">Calculus::Atoms::Compile::emit</a></span><span class="plain">((</span><span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1])?</span><span class="identifier">NOW_ATOM_TRUE_TASK:NOW_ATOM_FALSE_TASK</span><span class="plain">, </span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">TRUE</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_5"></a><b>§2.1.6.1.2.3.5. Quantifiers and the Q-stack. </b>It remains to deal with quantifiers, and to show that the Invariant is
|
|
preserved by them. There are two cases: \(\exists\), and everything else.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">The existence case is the easiest. Given \(\exists v: \psi(v)\) we compile
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">loop header for v to run through its domain set {</span>
|
|
<span class="plain">...</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">and note that execution reaches the start of the loop body once for each
|
|
possible choice of \(v\), as required by the Invariant — indeed the Invariant
|
|
pretty much requires that this is what we compile.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Compile a loop through possible values of the variable quantified</span> <span class="cwebmacronumber">2.1.6.1.2.3.5</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">level_back_to</span><span class="plain"> = </span><span class="identifier">Produce::level</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">pl</span><span class="plain"> = </span><span class="functiontext"><a href="12-cdp.html#SP5">Calculus::Propositions::Deferred::compile_loop_header</a></span><span class="plain">(</span>
|
|
<span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">, </span><span class="identifier">var_ix_lv</span><span class="plain">[</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain">],</span>
|
|
<span class="identifier">pl</span><span class="plain">,</span>
|
|
<span class="plain">(</span><span class="identifier">R_stack_reason</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] == </span><span class="constant">NOW_ASSERTION_DEFER</span><span class="plain">)?</span><span class="identifier">TRUE:FALSE</span><span class="plain">,</span>
|
|
<span class="plain">(</span><span class="identifier">quant</span><span class="plain"> != </span><span class="identifier">exists_quantifier</span><span class="plain">)?</span><span class="identifier">TRUE:FALSE</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
<<span class="cwebmacro">Open a block in the I6 code compiled to perform the search</span> <span class="cwebmacronumber">2.1.6.1.2.3.5.1</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_6"></a><b>§2.1.6.1.2.3.6. </b>Generalised quantifiers — "at least three", "all but four", and
|
|
so on — make quantitative statements about the number of valid or invalid
|
|
cases over a domain set. These need more elaborate code. Suppose we have
|
|
\(\phi = Q v\in\lbrace v\mid\psi(v)\rbrace: \theta(v)\), which in memory
|
|
looks like this:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">QUANTIFIER --> DOMAIN_OPEN --> psi --> DOMAIN_CLOSE --> theta</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">We compile that to code in the following shape:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">set count of domain size to 0</span>
|
|
<span class="plain">set count of valid cases to 0</span>
|
|
<span class="plain">loop header for v to run through its domain set {</span>
|
|
<span class="plain">if psi holds {</span>
|
|
<span class="plain">increment count of domain size</span>
|
|
<span class="plain">if theta holds {</span>
|
|
<span class="plain">increment count of valid cases</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">if the counts are such that the quantifier is satisfied {</span>
|
|
<span class="plain">...</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">We don't always need both counts. For instance, to handle "at least three
|
|
doors are unlocked" we count both the domain size (the number of doors)
|
|
and the number of valid cases (the number of unlocked doors), but only need
|
|
the latter. This might be worth optimising some day, to save local variables.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_7"></a><b>§2.1.6.1.2.3.7. </b>The domain size and valid case counts are stored in locals called <code class="display"><span class="extract">qcn_N</span></code>
|
|
and <code class="display"><span class="extract">qcy_N</span></code> respectively, where <code class="display"><span class="extract">N</span></code> is the index of the quantifier — 0 for
|
|
the first one in the proposition, 1 for the second and so on.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">On reading a non-existence <code class="display"><span class="extract">QUANTIFIER</span></code> atom, we compile code to zero the
|
|
counts, and push details of the quantifier onto the Q-stack, so that we
|
|
can recover them later. We then compile a loop header exactly as above.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">The test of \(\psi\), which acts as a filter on the domain set — e.g.,
|
|
only doors, not all objects — is handled by pushing a suitable goal onto
|
|
the R-stack, but we don't need to do anything to make that happen here,
|
|
because the <code class="display"><span class="extract">DOMAIN_OPEN</span></code> atom does it.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Push the Q-stack</span> <span class="cwebmacronumber">2.1.6.1.2.3.7</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">R_stack_reason</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] == </span><span class="constant">NOW_ASSERTION_DEFER</span><span class="plain">)</span>
|
|
<<span class="cwebmacro">Handle "not exists" as "for all not"</span> <span class="cwebmacronumber">2.1.6.1.2.3.7.1</span>><span class="plain">;</span>
|
|
|
|
<span class="identifier">Q_stack_quantifier</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">] = </span><span class="identifier">quant</span><span class="plain">;</span>
|
|
<span class="identifier">Q_stack_parameter</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">] = </span><span class="identifier">param</span><span class="plain">;</span>
|
|
<span class="identifier">Q_stack_block_nesting</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">] = </span><span class="identifier">block_nesting</span><span class="plain">;</span>
|
|
<span class="identifier">Q_stack_C_stack_level</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">] = </span><span class="identifier">C_sp</span><span class="plain">;</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">qcy_s</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">]);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">qcn_s</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">]);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Q_sp</span><span class="plain">++;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_7_1"></a><b>§2.1.6.1.2.3.7.1. </b>It is always true that \(\not\exists x: \psi(x)\) is equivalent to \(\forall x:
|
|
\lnot(\phi(x))\(, so the following seems pointless. We do this, in the case
|
|
of "now" only, in order to make \(\not\exists\) legal in a "now", which
|
|
it otherwise wouldn't be. Most quantifiers aren't, because they are too vague:
|
|
"now fewer than six doors are open", for instance, is not allowed. But we
|
|
do want to allow "now nobody likes Mr Wickham", say, which asserts
|
|
\(\not\exists x: {\it person}(x)\land{\it likes}(x, W)\).
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Handle "not exists" as "for all not"</span> <span class="cwebmacronumber">2.1.6.1.2.3.7.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">quant</span><span class="plain"> == </span><span class="identifier">not_exists_quantifier</span><span class="plain">) {</span>
|
|
<span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1] = (</span><span class="identifier">R_stack_parity</span><span class="plain">[</span><span class="identifier">R_sp</span><span class="plain">-1])?</span><span class="identifier">FALSE:TRUE</span><span class="plain">;</span>
|
|
<span class="identifier">quant</span><span class="plain"> = </span><span class="identifier">for_all_quantifier</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3_7">§2.1.6.1.2.3.7</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_4"></a><b>§2.1.6.1.2.4. </b>To resume the narrative of what happens when we read:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">QUANTIFIER --> DOMAIN_OPEN --> psi --> DOMAIN_CLOSE --> theta</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">We zeroed the counters, compiled the loop headers and pushed details to the
|
|
Q-stack at the <code class="display"><span class="extract">QUANTIFIER</span></code> atom; pushed a filtering goal onto the R-stack
|
|
at the <code class="display"><span class="extract">DOMAIN_OPEN</span></code> atom; popped it again as accomplished at <code class="display"><span class="extract">DOMAIN_CLOSE</span></code>,
|
|
compiling a line which increments the domain size to celebrate; and then
|
|
compiled code to test \(\theta\).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Now we are at the end of the line, and still have the quantifier code
|
|
half-done, as we know because the Q-stack is not empty. We first compile
|
|
an increment of the valid cases count, because if execution of the I6
|
|
code gets to the end of testing \(\theta\) then it must have found a valid
|
|
case: in the "at least three doors are unlocked" example, it will have
|
|
found an unlocked one among the doors making up the domain. We then need
|
|
to record any "called" values for later retrieval by whoever called
|
|
this proposition routine: see below. That leaves just this part:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">if the counts are such that the quantifier is satisfied {</span>
|
|
<span class="plain">...</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">left to compile, and we will be done: execution will reach the <code class="display"><span class="extract">...</span></code> if and
|
|
only if it is true at run-time that three or more of the doors is unlocked.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Thus this elaborate generalised-quantifier case satisfies the Invariant
|
|
because it transfers execution from before to <code class="display"><span class="extract">...</span></code> either 0 times (if the
|
|
counts don't satisfy us), or once. Unlike in the \(\exists v\) case, it's
|
|
not a question of enumerating which \(v\) work and which do not; the whole
|
|
thing works, or doesn't, and is more like testing a single <code class="display"><span class="extract">if</span></code>.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Pop the Q-stack</span> <span class="cwebmacronumber">2.1.6.1.2.4</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Q_sp</span><span class="plain">--; </span><span class="reserved">if</span><span class="plain"> (</span><span class="identifier">Q_sp</span><span class="plain"> < </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"Q stack underflow"</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">POSTINCREMENT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">qcy_s</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">C_sp</span><span class="plain"> > </span><span class="identifier">Q_stack_C_stack_level</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">])</span>
|
|
<<span class="cwebmacro">Pop the C-stack</span> <span class="cwebmacronumber">2.1.6.1.2.5</span>><span class="plain">;</span>
|
|
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">block_nesting</span><span class="plain"> > </span><span class="identifier">Q_stack_block_nesting</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">])</span>
|
|
<<span class="cwebmacro">Close a block in the I6 code compiled to perform the search</span> <span class="cwebmacronumber">2.1.6.1.2.6</span>><span class="plain">;</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Quantifiers::emit_test</span><span class="plain">(</span><span class="identifier">Q_stack_quantifier</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">], </span><span class="identifier">Q_stack_parameter</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">], </span><span class="identifier">qcy_s</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">], </span><span class="identifier">qcn_s</span><span class="plain">[</span><span class="identifier">Q_sp</span><span class="plain">]);</span>
|
|
<<span class="cwebmacro">Open a block in the I6 code compiled to perform the search, if variant</span> <span class="cwebmacronumber">2.1.6.1.2.3.3.1</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2">§2.1.6.1.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_8"></a><b>§2.1.6.1.2.3.8. The C-stack. </b>When a CALLED atom in the proposition gives a name to a variable, we have to
|
|
transcribe that to the <code class="display"><span class="extract">deferred_calling_list</span></code> for the benefit of the code
|
|
calling this proposition routine. Each time we discover that a term \(t\) is
|
|
to be given a name, we stack it up. These are not always variables:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>if a person (called the dupe) is in a dark room (called the lair), ...</p>
|
|
|
|
</blockquote>
|
|
|
|
<p class="inwebparagraph">gives names to \(x\) ("dupe") and \(f_{\it in}(x)\) ("lair"), because
|
|
simplification has eliminated the variable \(y\) which appears to be being
|
|
given a name.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Push the C-stack</span> <span class="cwebmacronumber">2.1.6.1.2.3.8</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">C_stack_term</span><span class="plain">[</span><span class="identifier">C_sp</span><span class="plain">] = </span><span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[0];</span>
|
|
<span class="identifier">C_stack_index</span><span class="plain">[</span><span class="identifier">C_sp</span><span class="plain">] = </span><span class="identifier">no_deferred_callings</span><span class="plain">++;</span>
|
|
<span class="identifier">C_sp</span><span class="plain">++;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_5"></a><b>§2.1.6.1.2.5. </b>When does the compiled search code record values into <code class="display"><span class="extract">deferred_calling_list</span></code>?
|
|
In two situations:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(a) when a domain-search has successfully found a viable case for a quantifier,
|
|
the values of any variables called in that domain are recorded;
|
|
</li><li>(b) and otherwise the values of called variables are recorded just before
|
|
point <code class="display"><span class="extract">M</span></code>, that is, immediately before acting on a successful match.
|
|
</li></ul>
|
|
<p class="inwebparagraph">For example, when reading:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>if a person (called the dupe) is in a lighted room which is adjacent to exactly one dark room (called the lair), ...</p>
|
|
|
|
</blockquote>
|
|
|
|
<p class="inwebparagraph">the value of "dupe" is transferred just before <code class="display"><span class="extract">M</span></code>, but the value of "lair"
|
|
is transferred as soon as a dark room is found. The code looks like this:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">set count of domain size to 1</span>
|
|
<span class="plain">loop through domain (i.e., dark rooms adjacent to the person's location) {</span>
|
|
<span class="plain">increment count of domain size</span>
|
|
<span class="plain">record the lair value</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">if the count of domain size is 1 {</span>
|
|
<span class="plain">record the dupe value</span>
|
|
<span class="plain">M</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">If we waited until point <code class="display"><span class="extract">M</span></code> to record the lair value, it would have disappeared,
|
|
because <code class="display"><span class="extract">M</span></code> is outside the loop which searches the domain of the "exactly one"
|
|
quantifier.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Pop the C-stack</span> <span class="cwebmacronumber">2.1.6.1.2.5</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">C_sp</span><span class="plain">--; </span><span class="reserved">if</span><span class="plain"> (</span><span class="identifier">C_sp</span><span class="plain"> < </span><span class="constant">0</span><span class="plain">) </span><span class="identifier">internal_error</span><span class="plain">(</span><span class="string">"C stack underflow"</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">LOOKUPREF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">DEFERRED_CALLING_LIST_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, (</span><span class="identifier">inter_t</span><span class="plain">) </span><span class="identifier">C_stack_index</span><span class="plain">[</span><span class="identifier">C_sp</span><span class="plain">]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="functiontext"><a href="11-tr.html#SP10">Calculus::Terms::emit</a></span><span class="plain">(</span><span class="identifier">C_stack_term</span><span class="plain">[</span><span class="identifier">C_sp</span><span class="plain">]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2">§2.1.6.1.2</a>, <a href="12-cdp.html#SP2_1_6_1_2_4">§2.1.6.1.2.4</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_5_1"></a><b>§2.1.6.1.2.3.5.1. </b>That just leaves the blocking, which follows the One True Brace Style. Thus:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Open a block in the I6 code compiled to perform the search</span> <span class="cwebmacronumber">2.1.6.1.2.3.5.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">L_stack_level</span><span class="plain">[</span><span class="identifier">block_nesting</span><span class="plain">] = </span><span class="identifier">level_back_to</span><span class="plain">;</span>
|
|
<span class="identifier">block_nesting</span><span class="plain">++;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3_5">§2.1.6.1.2.3.5</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_3_3_1"></a><b>§2.1.6.1.2.3.3.1. </b>Not for a loop body:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Open a block in the I6 code compiled to perform the search, if variant</span> <span class="cwebmacronumber">2.1.6.1.2.3.3.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">L_stack_level</span><span class="plain">[</span><span class="identifier">block_nesting</span><span class="plain">] = </span><span class="identifier">Produce::level</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">())-1;</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">block_nesting</span><span class="plain">++;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_3_3">§2.1.6.1.2.3.3</a>, <a href="12-cdp.html#SP2_1_6_1_2_4">§2.1.6.1.2.4</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_6"></a><b>§2.1.6.1.2.6. </b>and:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Close a block in the I6 code compiled to perform the search</span> <span class="cwebmacronumber">2.1.6.1.2.6</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">while</span><span class="plain"> (</span><span class="identifier">Produce::level</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">()) > </span><span class="identifier">L_stack_level</span><span class="plain">[</span><span class="identifier">block_nesting</span><span class="plain">-1]) </span><span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">block_nesting</span><span class="plain">--;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2">§2.1.6.1.2</a>, <a href="12-cdp.html#SP2_1_6_1_2_4">§2.1.6.1.2.4</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_5_1"></a><b>§2.1.5.1. Adaptations. </b>That completes the general pattern of searching according to the proposition's
|
|
instructions. It remains to adapt it to different needs, by providing, in
|
|
each case, some setting-up code; some code to execute when a viable set
|
|
of variable values is found; and some winding-up code.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">In some of the cases, additional local variables are needed within the
|
|
<code class="display"><span class="extract">Prop_N</span></code> routine, to keep track of counters or totals. These are they:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Declare the I6 locals needed by adaptations to particular deferral cases</span> <span class="cwebmacronumber">2.1.5.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">multipurpose_routine</span><span class="plain">) {</span>
|
|
<span class="identifier">total_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"total"</span><span class="plain">);</span>
|
|
<span class="identifier">counter_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"counter"</span><span class="plain">);</span>
|
|
<span class="identifier">selection_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"selection"</span><span class="plain">);</span>
|
|
<span class="identifier">best_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"best"</span><span class="plain">);</span>
|
|
<span class="identifier">best_with_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"best_with"</span><span class="plain">);</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="reserved">switch</span><span class="plain"> (</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">reason</span><span class="plain">) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">NUMBER_OF_DEFER:</span>
|
|
<span class="identifier">counter_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"counter"</span><span class="plain">);</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">RANDOM_OF_DEFER:</span>
|
|
<span class="identifier">counter_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"counter"</span><span class="plain">);</span>
|
|
<span class="identifier">selection_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"selection"</span><span class="plain">);</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">TOTAL_DEFER:</span>
|
|
<span class="identifier">total_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"total"</span><span class="plain">);</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">LIST_OF_DEFER:</span>
|
|
<span class="identifier">counter_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"counter"</span><span class="plain">);</span>
|
|
<span class="identifier">total_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"total"</span><span class="plain">);</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">EXTREMAL_DEFER:</span>
|
|
<span class="identifier">best_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"best"</span><span class="plain">);</span>
|
|
<span class="identifier">best_with_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_internal_local_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"best_with"</span><span class="plain">);</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_5">§2.1.5</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_5_2"></a><b>§2.1.5.2. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Declare the I6 call parameters needed by adaptations to particular deferral cases</span> <span class="cwebmacronumber">2.1.5.2</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> ((!</span><span class="identifier">multipurpose_routine</span><span class="plain">) && (</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">reason</span><span class="plain"> == </span><span class="constant">LIST_OF_DEFER</span><span class="plain">)) {</span>
|
|
<span class="identifier">list_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_named_call_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"list"</span><span class="plain">);</span>
|
|
<span class="identifier">strong_kind_s</span><span class="plain"> = </span><span class="functiontext"><a href="24-lv.html#SP11">LocalVariables::add_named_call_as_symbol</a></span><span class="plain">(</span><span class="identifier">I</span><span class="string">"strong_kind"</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_5">§2.1.5</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_3"></a><b>§2.1.6.1.3. Adaptation to CONDITION. </b>The first and simplest of our cases to understand: where \(\phi\) is a sentence,
|
|
with all variables bound, and we have to return <code class="display"><span class="extract">true</span></code> if it is true and
|
|
<code class="display"><span class="extract">false</span></code> if it is false. There is no initialisation:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Initialisation before CONDITION search</span> <span class="cwebmacronumber">2.1.6.1.3</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_1"></a><b>§2.1.6.1.2.2.1. </b>As soon as we find any valid combination of the variables, we return <code class="display"><span class="extract">true</span></code>:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Act on successful match in CONDITION search</span> <span class="cwebmacronumber">2.1.6.1.2.2.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::rtrue</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_4"></a><b>§2.1.6.1.4. </b>So we only reach winding-up if every case failed, and then we return <code class="display"><span class="extract">false</span></code>:
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Winding-up after CONDITION search</span> <span class="cwebmacronumber">2.1.6.1.4</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::rfalse</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_5"></a><b>§2.1.6.1.5. Adaptation to NUMBER. </b>In the remaining cases, \(\phi\) has variable \(x\) (only) left free, but the use
|
|
we want to make will be a loop over all objects \(x\), and we compile this
|
|
"outer loop" here: the loop opens in the initialisation code, closes in
|
|
the winding-up code, and therefore completely encloses the code generated
|
|
by the searching mechanism above.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">In the first case, we want to count the number of \(x\) for which \(\phi(x)\)
|
|
is true. The local <code class="display"><span class="extract">counter</span></code> holds the count so far; it starts out automatically
|
|
at 0, since all I6 locals do.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Initialisation before NUMBER search</span> <span class="cwebmacronumber">2.1.6.1.5</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="12-cdp.html#SP5">Calculus::Propositions::Deferred::compile_loop_header</a></span><span class="plain">(0, </span><span class="identifier">var_ix_lv</span><span class="plain">[0], </span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_2"></a><b>§2.1.6.1.2.2.2. </b>Recall that we get here for each possible way that \(\phi(x)\) could
|
|
be true, that is, once for each viable set of values of bound variables in
|
|
\(\phi\). But we only want to increment <code class="display"><span class="extract">counter</span></code> once, so having done so, we
|
|
exit the searching code and continue the outer loop.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">The <code class="display"><span class="extract">jump</span></code> to a label is forced on us since I6, unlike, say, Perl, has no
|
|
syntax to break or continue a loop other than the innermost one.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Act on successful match in NUMBER search</span> <span class="cwebmacronumber">2.1.6.1.2.2.2</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">POSTINCREMENT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<<span class="cwebmacro">Jump to next outer loop for this reason</span> <span class="cwebmacronumber">2.1.6.1.2.2.2.1</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_2_1"></a><b>§2.1.6.1.2.2.2.1. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Jump to next outer loop for this reason</span> <span class="cwebmacronumber">2.1.6.1.2.2.2.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="identifier">reason</span><span class="plain">] == </span><span class="identifier">NULL</span><span class="plain">) {</span>
|
|
<span class="identifier">TEMPORARY_TEXT</span><span class="plain">(</span><span class="identifier">L</span><span class="plain">);</span>
|
|
<span class="identifier">WRITE_TO</span><span class="plain">(</span><span class="identifier">L</span><span class="plain">, </span><span class="string">".NextOuterLoop_%d"</span><span class="plain">, </span><span class="identifier">reason</span><span class="plain">);</span>
|
|
<span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="identifier">reason</span><span class="plain">] = </span><span class="identifier">Produce::reserve_label</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">L</span><span class="plain">);</span>
|
|
<span class="identifier">DISCARD_TEXT</span><span class="plain">(</span><span class="identifier">L</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">JUMP_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::lab</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="identifier">reason</span><span class="plain">]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2_2">§2.1.6.1.2.2.2</a>, <a href="12-cdp.html#SP2_1_6_1_2_2_3">§2.1.6.1.2.2.3</a>, <a href="12-cdp.html#SP2_1_6_1_2_2_4">§2.1.6.1.2.2.4</a>, <a href="12-cdp.html#SP2_1_6_1_2_2_5">§2.1.6.1.2.2.5</a>, <a href="12-cdp.html#SP2_1_6_1_17">§2.1.6.1.17</a> (twice).</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_6"></a><b>§2.1.6.1.6. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Place next outer loop label</span> <span class="cwebmacronumber">2.1.6.1.6</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="identifier">reason</span><span class="plain">] == </span><span class="identifier">NULL</span><span class="plain">) {</span>
|
|
<span class="identifier">TEMPORARY_TEXT</span><span class="plain">(</span><span class="identifier">L</span><span class="plain">);</span>
|
|
<span class="identifier">WRITE_TO</span><span class="plain">(</span><span class="identifier">L</span><span class="plain">, </span><span class="string">".NextOuterLoop_%d"</span><span class="plain">, </span><span class="identifier">reason</span><span class="plain">);</span>
|
|
<span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="identifier">reason</span><span class="plain">] = </span><span class="identifier">Produce::reserve_label</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">L</span><span class="plain">);</span>
|
|
<span class="identifier">DISCARD_TEXT</span><span class="plain">(</span><span class="identifier">L</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">Produce::place_label</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">NextOuterLoop_labels</span><span class="plain">[</span><span class="identifier">reason</span><span class="plain">]);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_7"></a><b>§2.1.6.1.7. </b>The continue-outer-loop labels are marked with the reason number so that
|
|
if code is compiled for each reason in turn within a single routine — which
|
|
is what we do for multipurpose deferred propositions — the labels do
|
|
not have clashing names.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Winding-up after NUMBER search</span> <span class="cwebmacronumber">2.1.6.1.7</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_8"></a><b>§2.1.6.1.8. Adaptation to LIST. </b>In the next case, we want to form the list of all \(x\) for which \(\phi(x)\)
|
|
is true. The local <code class="display"><span class="extract">list</span></code> holds the list so far, and already exists.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Initialisation before LIST search</span> <span class="cwebmacronumber">2.1.6.1.8</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_call_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">BLKVALUEWRITE_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">list_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">LIST_ITEM_KOV_F_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">strong_kind_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_call_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">LIST_OF_TY_GETLENGTH_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">list_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="12-cdp.html#SP5">Calculus::Propositions::Deferred::compile_loop_header</a></span><span class="plain">(0, </span><span class="identifier">var_ix_lv</span><span class="plain">[0], </span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_3"></a><b>§2.1.6.1.2.2.3. </b>Recall that we get here for each possible way that \(\phi(x)\) could
|
|
be true, that is, once for each viable set of values of bound variables in
|
|
\(\phi\). But we only want to increment <code class="display"><span class="extract">counter</span></code> once, so having done so, we
|
|
exit the searching code and continue the outer loop.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">The <code class="display"><span class="extract">jump</span></code> to a label is forced on us since I6, unlike, say, Perl, has no
|
|
syntax to break or continue a loop other than the innermost one.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Act on successful match in LIST search</span> <span class="cwebmacronumber">2.1.6.1.2.2.3</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">POSTINCREMENT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">PLUS_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">TIMES_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">3</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">DIVIDE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">2</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">8</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_call_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">LIST_OF_TY_SETLENGTH_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">list_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_call_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">BLKVALUEWRITE_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">list_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">MINUS_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">PLUS_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">LIST_ITEM_BASE_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">1</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<<span class="cwebmacro">Jump to next outer loop for this reason</span> <span class="cwebmacronumber">2.1.6.1.2.2.2.1</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_9"></a><b>§2.1.6.1.9. </b>The continue-outer-loop labels are marked with the reason number so that
|
|
if code is compiled for each reason in turn within a single routine — which
|
|
is what we do for multipurpose deferred propositions — the labels do
|
|
not have clashing names.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Winding-up after LIST search</span> <span class="cwebmacronumber">2.1.6.1.9</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_call_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">LIST_OF_TY_SETLENGTH_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">list_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">list_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_10"></a><b>§2.1.6.1.10. Adaptation to RANDOM. </b>To choose a random \(x\) such that \(\phi(x)\), we essentially run the same code
|
|
as for NUMBER searches, but twice over: first to count how many such \(x\) there
|
|
are, then to run through again to find the \(n\)th of these, where \(n\) is a
|
|
uniformly random number such that \(1\leq n\leq x\).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">This avoids needing to store the full list of matches anywhere, which would
|
|
be impossible since (a) it's potentially a lot of storage and (b) it can
|
|
only safely live on the current stack frame, and I6 does not allow arrays
|
|
on the current stack frame (because of restrictions in the Z-machine).
|
|
This means that, on average, the compiled code takes 50\% longer to find
|
|
its random \(x\) than it ideally would, but we accept the trade-off.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Initialisation before RANDOM search</span> <span class="cwebmacronumber">2.1.6.1.10</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">selection_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, (</span><span class="identifier">inter_t</span><span class="plain">) -1);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">WHILE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_truth_state</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">1</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="12-cdp.html#SP5">Calculus::Propositions::Deferred::compile_loop_header</a></span><span class="plain">(0, </span><span class="identifier">var_ix_lv</span><span class="plain">[0], </span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_4"></a><b>§2.1.6.1.2.2.4. </b>Again we exit the searcher as soon as a match is found, since that guarantees
|
|
that \(\phi(x)\).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Note that we can only return here on the second pass, since <code class="display"><span class="extract">selection</span></code> is \(-1\)
|
|
throughout the first pass, whereas <code class="display"><span class="extract">counter</span></code> is non-negative.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Act on successful match in RANDOM search</span> <span class="cwebmacronumber">2.1.6.1.2.2.4</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">POSTINCREMENT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">EQ_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">selection_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<<span class="cwebmacro">Jump to next outer loop for this reason</span> <span class="cwebmacronumber">2.1.6.1.2.2.2.1</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_11"></a><b>§2.1.6.1.11. </b>We return <code class="display"><span class="extract">nothing</span></code> — the non-object — if <code class="display"><span class="extract">counter</span></code> is zero, since that
|
|
means the set of possible \(x\) is empty. But we also return if <code class="display"><span class="extract">selection</span></code>
|
|
has been made already, because that means that the second pass has been
|
|
completed without a return — something which in theory cannot happen, but
|
|
just might do if testing part of the proposition had some side-effect changing
|
|
the state of the objects and thus the size of the set of possibilities.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Winding-up after RANDOM search</span> <span class="cwebmacronumber">2.1.6.1.11</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">OR_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">EQ_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">selection_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_nothing</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">selection_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RANDOM_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">counter_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_12"></a><b>§2.1.6.1.12. Adaptation to TOTAL. </b>Here the task is to sum the values of property \(P\) attached to each object
|
|
in the domain \(\lbrace x\mid \phi(x)\rbrace\).
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Initialisation before TOTAL search</span> <span class="cwebmacronumber">2.1.6.1.12</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="12-cdp.html#SP5">Calculus::Propositions::Deferred::compile_loop_header</a></span><span class="plain">(0, </span><span class="identifier">var_ix_lv</span><span class="plain">[0], </span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_5"></a><b>§2.1.6.1.2.2.5. </b>The only wrinkle here is the way the compiled code knows which property it
|
|
should be totalling. If we know that ourselves, we can compile in a direct
|
|
reference. But if we are compiling a multipurpose deferred proposition, then
|
|
it might be used to total any property over the domain, and we won't know
|
|
which until runtime — when its identity will be found in the I6 variable
|
|
<code class="display"><span class="extract">property_to_be_totalled</span></code>.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Act on successful match in TOTAL search</span> <span class="cwebmacronumber">2.1.6.1.2.2.5</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">PLUS_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">PROPERTYVALUE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">multipurpose_routine</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">PROPERTY_TO_BE_TOTALLED_HL</span><span class="plain">));</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="identifier">prn</span><span class="plain"> = </span><span class="identifier">RETRIEVE_POINTER_property</span><span class="plain">(</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">defn_ref</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="15-pr.html#SP27">Properties::iname</a></span><span class="plain">(</span><span class="identifier">prn</span><span class="plain">));</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<<span class="cwebmacro">Jump to next outer loop for this reason</span> <span class="cwebmacronumber">2.1.6.1.2.2.2.1</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_13"></a><b>§2.1.6.1.13. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Winding-up after TOTAL search</span> <span class="cwebmacronumber">2.1.6.1.13</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">total_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_14"></a><b>§2.1.6.1.14. Adaptation to EXTREMAL. </b>This is rather similar. We find the member of \(\lbrace x\mid \phi(x)\rbrace\)
|
|
which either minimises, or maximises, the value of some property \(P\). We use
|
|
two local variables: <code class="display"><span class="extract">best</span></code>, the extreme \(P\) value found so far; and <code class="display"><span class="extract">best_with</span></code>,
|
|
the member of the domain set which achieves that.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">If two or more \(x\) achieve the optimal \(P\)-value, it is deliberately left
|
|
undefined which one is returned. The user may be typing "the heaviest thing
|
|
on the table", but what he gets is "a heaviest thing on the table".
|
|
</p>
|
|
|
|
<p class="inwebparagraph">We open the search with <code class="display"><span class="extract">best_with</span></code> equal to <code class="display"><span class="extract">nothing</span></code>, the non-object, which
|
|
is what we will return if the domain set turns out to be empty; and with
|
|
<code class="display"><span class="extract">best</span></code> set to the furthest-from-optimal value possible. For a search maximising
|
|
\(P\), <code class="display"><span class="extract">best</span></code> starts at the lowest number representable in the virtual machine;
|
|
for a minimisation, it starts at the highest. That way, if any member of the
|
|
domain is found, its \(P\)-value must be at least as good as the starting
|
|
value of <code class="display"><span class="extract">best</span></code>.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Again the only nuisance is that sometimes we know \(P\), and whether we are
|
|
maximising or minimising, at compile time; but for a multipurpose routine
|
|
we don't, and have to look that up at run-time.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Initialisation before EXTREMAL search</span> <span class="cwebmacronumber">2.1.6.1.14</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">multipurpose_routine</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IFELSE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">PROPERTY_LOOP_SIGN_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">MIN_NEGATIVE_NUMBER_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">MAX_POSITIVE_NUMBER_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="reserved">measurement_definition</span><span class="plain"> *</span><span class="identifier">mdef</span><span class="plain"> =</span>
|
|
<span class="identifier">RETRIEVE_POINTER_measurement_definition</span><span class="plain">(</span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">defn_ref</span><span class="plain">);</span>
|
|
<span class="functiontext"><a href="15-ma.html#SP6">Properties::Measurement::read_property_details</a></span><span class="plain">(</span><span class="identifier">mdef</span><span class="plain">, &</span><span class="identifier">def_prn</span><span class="plain">, &</span><span class="identifier">def_prn_sign</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">def_prn_sign</span><span class="plain"> == </span><span class="constant">1</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">MIN_NEGATIVE_NUMBER_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">MAX_POSITIVE_NUMBER_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="12-cdp.html#SP5">Calculus::Propositions::Deferred::compile_loop_header</a></span><span class="plain">(0, </span><span class="identifier">var_ix_lv</span><span class="plain">[0], </span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_6"></a><b>§2.1.6.1.2.2.6. </b>It might look as if we could speed up the multipurpose case by
|
|
multiplying by <code class="display"><span class="extract">property_loop_sign</span></code>, thus combining the max and min
|
|
versions into one, and saving an <code class="display"><span class="extract">if</span></code>. But (a) the multiplication is as
|
|
expensive as the <code class="display"><span class="extract">if</span></code> (remember that on a VM there's no real branch
|
|
penalty), and (b) we need to watch out because \(-1\) times \(-32768\), on a
|
|
16-bit machine, is \(-1\), not \(32768\): so it is not always true that
|
|
multiplying by \(-1\) is order-reversing.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Act on successful match in EXTREMAL search</span> <span class="cwebmacronumber">2.1.6.1.2.2.6</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">multipurpose_routine</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IFELSE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">PROPERTY_LOOP_SIGN_HL</span><span class="plain">));</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<<span class="cwebmacro">Emit code for a property lookup</span> <span class="cwebmacronumber">2.1.6.1.2.2.6.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<<span class="cwebmacro">Emit code for a property lookup</span> <span class="cwebmacronumber">2.1.6.1.2.2.6.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_with_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">LE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<<span class="cwebmacro">Emit code for a property lookup</span> <span class="cwebmacronumber">2.1.6.1.2.2.6.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<<span class="cwebmacro">Emit code for a property lookup</span> <span class="cwebmacronumber">2.1.6.1.2.2.6.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_with_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">def_prn_sign</span><span class="plain"> == </span><span class="constant">1</span><span class="plain">) </span><span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GE_BIP</span><span class="plain">);</span>
|
|
<span class="reserved">else</span><span class="plain"> </span><span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">LE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<<span class="cwebmacro">Emit code for a property lookup</span> <span class="cwebmacronumber">2.1.6.1.2.2.6.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_s</span><span class="plain">);</span>
|
|
<<span class="cwebmacro">Emit code for a property lookup</span> <span class="cwebmacronumber">2.1.6.1.2.2.6.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">STORE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_with_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_6_1"></a><b>§2.1.6.1.2.2.6.1. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Emit code for a property lookup</span> <span class="cwebmacronumber">2.1.6.1.2.2.6.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">PROPERTYVALUE_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">multipurpose_routine</span><span class="plain">) {</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::find</a></span><span class="plain">(</span><span class="constant">PROPERTY_TO_BE_TOTALLED_HL</span><span class="plain">));</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="identifier">Produce::val_iname</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="functiontext"><a href="15-pr.html#SP27">Properties::iname</a></span><span class="plain">(</span><span class="identifier">def_prn</span><span class="plain">));</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2_6">§2.1.6.1.2.2.6</a> (6 times).</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_15"></a><b>§2.1.6.1.15. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Winding-up after EXTREMAL search</span> <span class="cwebmacronumber">2.1.6.1.15</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">best_with_s</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_16"></a><b>§2.1.6.1.16. Adaptation to LOOP. </b>Here the proposition is used to iterate through the members of the domain
|
|
set \(\lbrace x\mid \phi(x)\rbrace\). Two local variables exist: <code class="display"><span class="extract">x</span></code> and <code class="display"><span class="extract">x_ix</span></code>.
|
|
One of the following is true:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(1) The domain set contains only objects, so that <code class="display"><span class="extract">x</span></code> is non-zero if it
|
|
represents a member of that set. In this case <code class="display"><span class="extract">x_ix</span></code> may or may not be used,
|
|
and we will not rely on it.
|
|
</li><li>(2) The domain set contains only values, and then <code class="display"><span class="extract">x</span></code> might easily be zero,
|
|
but <code class="display"><span class="extract">x_ix</span></code> is always the index within the domain set: 1 if <code class="display"><span class="extract">x</span></code> is the first
|
|
value, 2 for the second and so on.
|
|
</li></ul>
|
|
<p class="inwebparagraph">The proposition is called with a pair of values <code class="display"><span class="extract">x</span></code>, <code class="display"><span class="extract">x_ix</span></code> and returns
|
|
the next value <code class="display"><span class="extract">x</span></code> in the domain set, or 0 if the domain is exhausted. (In
|
|
case (2) it's not safe to regard 0 as an end-of-set sentinel value because
|
|
0 can be a valid member of the set; so in looping through (2) we should
|
|
first find the size of the set using NUMBER OF, then keep calling for
|
|
members until the index reaches the size.) There is no need to return the
|
|
next <code class="display"><span class="extract">x_ix</span></code> value since it is always the present value plus 1.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">If the proposition is called with <code class="display"><span class="extract">x</span></code> set to <code class="display"><span class="extract">nothing</span></code>, in case (1), or
|
|
with <code class="display"><span class="extract">x_ix</span></code> equal to 0, in case (2), it returns the first value in the
|
|
domain.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_17"></a><b>§2.1.6.1.17. </b>Snarkily, this is how we do it:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">if we're called with a valid member of the domain, go to Z</span>
|
|
<span class="plain">loop x over members of the domain {</span>
|
|
<span class="plain">return x</span>
|
|
<span class="plain">label Z is here</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">Which is not really a loop at all, but is a cheap way to extract either the
|
|
initial value or the successor value from a loop header. (The trick actually
|
|
caused some consternation for I6 hackers when early drafts of I7 came out,
|
|
because they had been experimenting with a patch to I6 which protected
|
|
<code class="display"><span class="extract">objectloop</span></code> from object-tree rearrangements but which assumed that nobody
|
|
ever used <code class="display"><span class="extract">jump</span></code> to enter a loop body bypassing its header. But the DM4,
|
|
which defines I6, doesn't forbid this. The designer of I6 has learned his
|
|
lesson, though: I7 has no goto or jump instruction, and I7 loops can be
|
|
proved to be entered and exited cleanly.)
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Initialisation before LOOP search</span> <span class="cwebmacronumber">2.1.6.1.17</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">GT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_ix_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::val</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_number</span><span class="plain">, </span><span class="identifier">LITERAL_IVAL</span><span class="plain">, </span><span class="constant">0</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">POSTDECREMENT_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::ref_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_ix_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<<span class="cwebmacro">Jump to next outer loop for this reason</span> <span class="cwebmacronumber">2.1.6.1.2.2.2.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">IF_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::code</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<<span class="cwebmacro">Jump to next outer loop for this reason</span> <span class="cwebmacronumber">2.1.6.1.2.2.2.1</span>><span class="plain">;</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="12-cdp.html#SP5">Calculus::Propositions::Deferred::compile_loop_header</a></span><span class="plain">(0, </span><span class="identifier">var_ix_lv</span><span class="plain">[0], </span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">FALSE</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">);</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_2_2_7"></a><b>§2.1.6.1.2.2.7. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Act on successful match in LOOP search</span> <span class="cwebmacronumber">2.1.6.1.2.2.7</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_symbol</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">K_value</span><span class="plain">, </span><span class="identifier">var_s</span><span class="plain">[0]);</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1_2_2">§2.1.6.1.2.2</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP2_1_6_1_18"></a><b>§2.1.6.1.18. </b><code class="display">
|
|
<<span class="cwebmacrodefn">Winding-up after LOOP search</span> <span class="cwebmacronumber">2.1.6.1.18</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="identifier">Produce::inv_primitive</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">(), </span><span class="identifier">RETURN_BIP</span><span class="plain">);</span>
|
|
<span class="identifier">Produce::down</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::val_nothing</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
<span class="identifier">Produce::up</span><span class="plain">(</span><span class="functiontext"><a href="27-em.html#SP2">Emit::tree</a></span><span class="plain">());</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP2_1_6_1">§2.1.6.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP3"></a><b>§3. Compiling loop headers. </b>The final task of this entire chapter is to compile an I6 loop header which
|
|
causes a given variable \(v\) to range through a domain set \(D\) — which we
|
|
have to deduce by looking at the proposition \(\psi\) in front of us.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">We want this loop to run as quickly as possible: efficiency here makes
|
|
a very big difference to the running time of compiled I7 code. Most
|
|
optimisations aren't worth the risk in added complexity — but these are.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Loops through kinds of value are not in general optimisable. The problem cases
|
|
involve loops through objects. Consider:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>if everyone in the Dining Room can see an animal, ...</p>
|
|
|
|
</blockquote>
|
|
|
|
<p class="inwebparagraph">Code like this will run very slowly:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">loop over objects (x)</span>
|
|
<span class="plain">loop over objects (y)</span>
|
|
<span class="plain">if x is a person</span>
|
|
<span class="plain">if x is in the Dining Room</span>
|
|
<span class="plain">if y is an animal</span>
|
|
<span class="plain">if x can see y</span>
|
|
<span class="plain">success!</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">This is folly in so many ways. Most objects aren't people or animals, so
|
|
almost all combinations of \(x\) and \(y\) are wasted. We test the eligibility
|
|
of \(x\) for every possible \(y\). And there are quick ways to find what is in
|
|
the Dining Room, so we're missing a trick there, too. What we want is:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">loop over objects in the Dining Room (x)</span>
|
|
<span class="plain">if x is a person</span>
|
|
<span class="plain">loop over animals (y)</span>
|
|
<span class="plain">if x can see y</span>
|
|
<span class="plain">success!</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="inwebparagraph"><a id="SP4"></a><b>§4. </b>Part of the work is done already: we generate propositions with
|
|
quantifiers as far forwards as they can be, so we won't loop over \(y\) before
|
|
checking the validity of \(x\). The rest of the work comes from two basic
|
|
optimisations:
|
|
</p>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<ul class="items"><li>(1) if a loop over \(v\) is such that \(K(v)\) holds in every case, where \(K\)
|
|
is a kind, then loop \(v\) over \(K\) rather than all objects, and
|
|
</li><li>(2) if a loop over \(v\) is such that \(R(v, t)\) holds in every case, then loop over
|
|
all \(v\) such that \(R(v, t)\) in cases where \(R\) has a run-time representation
|
|
making this quick and easy.
|
|
</li></ul>
|
|
<p class="inwebparagraph">In each case we can then delete \(K(v)\) or \(R(v, t)\) from the proposition
|
|
as redundant, since the loop header has taken care of it.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">Case (1) is called "kind optimisation"; case (2), "parent
|
|
optimisation", because the prototype case is \(R\) being containment — we
|
|
exploit that the object-tree parent of \(v\) is known, and that I6 has a fast
|
|
form of <code class="display"><span class="extract">objectloop</span></code> to visit the children of a given node in the object
|
|
tree. Case (2) has to be avoided if we are compiling code to force a
|
|
proposition, rather than test it, because then \(R(v, t)\) is not an
|
|
accomplished fact but is something we have yet to make come true. This is
|
|
why the loop-compiler takes a flag <code class="display"><span class="extract">avoid_parent_optimisation</span></code>. Case (1)
|
|
doesn't suffer from this since kinds cannot be changed at run-time.
|
|
</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP5"></a><b>§5. </b>So here is the code. We write an I6 schema for the loop into <code class="display"><span class="extract">loop_schema</span></code>,
|
|
then expand it into the output.
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="reserved">i6_schema</span><span class="plain"> </span><span class="identifier">loop_schema</span><span class="plain">;</span>
|
|
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="functiontext">Calculus::Propositions::Deferred::compile_loop_header<button class="popup" onclick="togglePopup('usagePopup842')">...<span class="popuptext" id="usagePopup842">Usage of <b>Calculus::Propositions::Deferred::compile_loop_header</b>:<br><a href="12-cdp.html#SP2_1_6_1_2_3_5">§2.1.6.1.2.3.5</a>, <a href="12-cdp.html#SP2_1_6_1_5">§2.1.6.1.5</a>, <a href="12-cdp.html#SP2_1_6_1_8">§2.1.6.1.8</a>, <a href="12-cdp.html#SP2_1_6_1_10">§2.1.6.1.10</a>, <a href="12-cdp.html#SP2_1_6_1_12">§2.1.6.1.12</a>, <a href="12-cdp.html#SP2_1_6_1_14">§2.1.6.1.14</a>, <a href="12-cdp.html#SP2_1_6_1_17">§2.1.6.1.17</a></span></button></span><span class="plain">(</span><span class="reserved">int</span><span class="plain"> </span><span class="identifier">var</span><span class="plain">, </span><span class="reserved">local_variable</span><span class="plain"> *</span><span class="identifier">index_var</span><span class="plain">,</span>
|
|
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">proposition</span><span class="plain">,</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">avoid_parent_optimisation</span><span class="plain">, </span><span class="reserved">int</span><span class="plain"> </span><span class="identifier">grouped</span><span class="plain">, </span><span class="reserved">pcalc_prop_deferral</span><span class="plain"> *</span><span class="identifier">pdef</span><span class="plain">) {</span>
|
|
|
|
<span class="identifier">kind</span><span class="plain"> *</span><span class="identifier">K</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="reserved">pcalc_prop</span><span class="plain"> *</span><span class="identifier">kind_position</span><span class="plain"> = </span><span class="identifier">NULL</span><span class="plain">;</span>
|
|
<span class="reserved">pcalc_term</span><span class="plain"> </span><span class="identifier">var_term</span><span class="plain"> = </span><span class="functiontext"><a href="11-tr.html#SP4">Calculus::Terms::new_variable</a></span><span class="plain">(</span><span class="identifier">var</span><span class="plain">);</span>
|
|
<span class="reserved">pcalc_term</span><span class="plain"> </span><span class="identifier">second_term</span><span class="plain"> = </span><span class="functiontext"><a href="11-tr.html#SP4">Calculus::Terms::new_constant</a></span><span class="plain">(</span>
|
|
<span class="functiontext"><a href="14-lv.html#SP2">Lvalues::new_LOCAL_VARIABLE</a></span><span class="plain">(</span><span class="identifier">EMPTY_WORDING</span><span class="plain">, </span><span class="identifier">index_var</span><span class="plain">));</span>
|
|
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">parent_optimised</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
|
|
|
|
<span class="comment"> the default, if we are unable to provide either kind or parent optimisation</span>
|
|
<span class="functiontext"><a href="12-is.html#SP4_1">Calculus::Schemas::modify</a></span><span class="plain">(&</span><span class="identifier">loop_schema</span><span class="plain">, </span><span class="string">"objectloop (*1 ofclass Object)"</span><span class="plain">);</span>
|
|
|
|
<<span class="cwebmacro">Scan the proposition to find the domain of the loop, and look for opportunities</span> <span class="cwebmacronumber">5.1</span>><span class="plain">;</span>
|
|
|
|
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">K</span><span class="plain">) && (</span><span class="identifier">parent_optimised</span><span class="plain"> == </span><span class="identifier">FALSE</span><span class="plain">)) { </span><span class="comment"> parent optimisation is stronger, so we prefer that</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="functiontext"><a href="12-dtd.html#SP24">Calculus::Deferrals::write_loop_schema</a></span><span class="plain">(&</span><span class="identifier">loop_schema</span><span class="plain">, </span><span class="identifier">K</span><span class="plain">) == </span><span class="identifier">FALSE</span><span class="plain">) {</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pdef</span><span class="plain">-></span><span class="identifier">rtp_iname</span><span class="plain"> == </span><span class="identifier">NULL</span><span class="plain">) {</span>
|
|
<span class="identifier">pdef</span><span class="plain">-></span><span class="element">rtp_iname</span><span class="plain"> = </span><span class="functiontext"><a href="27-hr.html#SP4">Hierarchy::make_iname_in</a></span><span class="plain">(</span><span class="constant">RTP_HL</span><span class="plain">, </span><span class="identifier">pdef</span><span class="plain">-></span><span class="element">ppd_package</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
<span class="functiontext"><a href="12-is.html#SP4_1">Calculus::Schemas::modify</a></span><span class="plain">(&</span><span class="identifier">loop_schema</span><span class="plain">, </span><span class="string">"if (RunTimeProblem(RTP_CANTITERATE, %n))"</span><span class="plain">,</span>
|
|
<span class="identifier">pdef</span><span class="plain">-></span><span class="element">rtp_iname</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="11-pr.html#SP18">Calculus::Propositions::delete_atom</a></span><span class="plain">(</span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">kind_position</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
|
|
<span class="functiontext"><a href="12-is.html#SP6">Calculus::Schemas::emit_expand_from_terms</a></span><span class="plain">(&</span><span class="identifier">loop_schema</span><span class="plain">, &</span><span class="identifier">var_term</span><span class="plain">, &</span><span class="identifier">second_term</span><span class="plain">, </span><span class="identifier">TRUE</span><span class="plain">);</span>
|
|
|
|
<span class="reserved">return</span><span class="plain"> </span><span class="identifier">proposition</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="inwebparagraph"><a id="SP5_1"></a><b>§5.1. </b>The following looks more complicated than it really is. Sometimes it's
|
|
called to compile a loop arising from a quantifier with a domain, in
|
|
which case <code class="display"><span class="extract">grouped</span></code> is set and <code class="display"><span class="extract">proposition</span></code> points to:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">QUANTIFIER --> DOMAIN_OPEN --> psi --> DOMAIN_CLOSE --> ...</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">so that \(\psi\), the part in the domain group, defines the range of the
|
|
variable. But sometimes the call is to compile a loop not arising from a
|
|
quantifier, so there is no domain group to scan; instead the whole
|
|
proposition makes up \(\psi\), and now <code class="display"><span class="extract">grouped</span></code> is clear.
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Scan the proposition to find the domain of the loop, and look for opportunities</span> <span class="cwebmacronumber">5.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">bl</span><span class="plain"> = </span><span class="constant">0</span><span class="plain">, </span><span class="identifier">enabled</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
|
|
<span class="identifier">TRAVERSE_VARIABLE</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">);</span>
|
|
<span class="identifier">TRAVERSE_PROPOSITION</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">, </span><span class="identifier">proposition</span><span class="plain">) {</span>
|
|
<span class="reserved">switch</span><span class="plain"> (</span><span class="functiontext"><a href="11-ap.html#SP5">Calculus::Atoms::element_get_group</a></span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">element</span><span class="plain">)) {</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">OPEN_OPERATORS_GROUP:</span><span class="plain"> </span><span class="identifier">bl</span><span class="plain">++; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">case</span><span class="plain"> </span><span class="identifier">CLOSE_OPERATORS_GROUP:</span><span class="plain"> </span><span class="identifier">bl</span><span class="plain">--; </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">grouped</span><span class="plain">) {</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">element</span><span class="plain"> == </span><span class="constant">DOMAIN_OPEN_ATOM</span><span class="plain">) </span><span class="identifier">enabled</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">element</span><span class="plain"> == </span><span class="constant">DOMAIN_CLOSE_ATOM</span><span class="plain">) </span><span class="identifier">enabled</span><span class="plain"> = </span><span class="identifier">FALSE</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">bl</span><span class="plain"> < </span><span class="constant">0</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">enabled</span><span class="plain"> == </span><span class="identifier">FALSE</span><span class="plain">) </span><span class="reserved">continue</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">bl</span><span class="plain"> != </span><span class="constant">1</span><span class="plain">) </span><span class="reserved">continue</span><span class="plain">;</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> {</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">bl</span><span class="plain"> < </span><span class="constant">0</span><span class="plain">) </span><span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">bl</span><span class="plain"> > </span><span class="constant">0</span><span class="plain">) </span><span class="reserved">continue</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<<span class="cwebmacro">Scan $\psi$, the part of the proposition establishing the domain</span> <span class="cwebmacronumber">5.1.1</span>><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP5">§5</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP5_1_1"></a><b>§5.1.1. </b>In either case, we scan \(\psi\) looking for \(K(v)\) atoms, which would tell
|
|
us the domain set for the variable \(v\), or for \(R(v, t)\) atoms for
|
|
parent-optimisable relations \(R\).
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Scan $\psi$, the part of the proposition establishing the domain</span> <span class="cwebmacronumber">5.1.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">element</span><span class="plain"> == </span><span class="constant">KIND_ATOM</span><span class="plain">) && (</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain"> == </span><span class="identifier">var</span><span class="plain">)) {</span>
|
|
<span class="identifier">K</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-></span><span class="element">assert_kind</span><span class="plain">;</span>
|
|
<span class="identifier">kind_position</span><span class="plain"> = </span><span class="identifier">pl_prev</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
|
|
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">avoid_parent_optimisation</span><span class="plain"> == </span><span class="identifier">FALSE</span><span class="plain">) &&</span>
|
|
<span class="plain">(</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">element</span><span class="plain"> == </span><span class="constant">PREDICATE_ATOM</span><span class="plain">) && (</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">arity</span><span class="plain"> == </span><span class="constant">2</span><span class="plain">))</span>
|
|
<<span class="cwebmacro">Consider parent optimisation on this binary predicate</span> <span class="cwebmacronumber">5.1.1.1</span>><span class="plain">;</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP5_1">§5.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP5_1_1_1"></a><b>§5.1.1.1. </b>We give the relation \(R\) an opportunity to write a loop which runs \(v\)
|
|
through all possible \(x\) such that \(R(x, t)\), by writing a schema for the
|
|
loop in which <code class="display"><span class="extract">*1</span></code> denotes the variable \(v\) and <code class="display"><span class="extract">*2</span></code> the term \(t\).
|
|
</p>
|
|
|
|
<p class="inwebparagraph">For example, the worn-by relation writes the schema:
|
|
</p>
|
|
|
|
<pre class="display">
|
|
<span class="plain">objectloop (*1 in *2) if (WearerOf(*1)==parent(*1))</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph">where \(v\) runs quickly through the object-tree children of \(t\), but items
|
|
carried rather than worn are skipped.
|
|
</p>
|
|
|
|
<p class="inwebparagraph">We have to check three possible cases: \(R(v, t)\) direct, and then
|
|
\({\it is}(f_R(v), t)\) or \({\it is}(t, f_R(v))\), which can arise from
|
|
simplifications. We set <code class="display"><span class="extract">optimise_on</span></code> to \(R\) and <code class="display"><span class="extract">parent</span></code> to \(t\).
|
|
</p>
|
|
|
|
|
|
<p class="macrodefinition"><code class="display">
|
|
<<span class="cwebmacrodefn">Consider parent optimisation on this binary predicate</span> <span class="cwebmacronumber">5.1.1.1</span>> =
|
|
</code></p>
|
|
|
|
|
|
<pre class="displaydefn">
|
|
<span class="reserved">binary_predicate</span><span class="plain"> *</span><span class="identifier">bp</span><span class="plain"> = </span><span class="identifier">RETRIEVE_POINTER_binary_predicate</span><span class="plain">(</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">predicate</span><span class="plain">);</span>
|
|
<span class="reserved">if</span><span class="plain"> (</span><span class="identifier">bp</span><span class="plain"> == </span><span class="identifier">R_equality</span><span class="plain">) {</span>
|
|
<span class="reserved">int</span><span class="plain"> </span><span class="identifier">chk</span><span class="plain">;</span>
|
|
<span class="reserved">for</span><span class="plain"> (</span><span class="identifier">chk</span><span class="plain">=0; </span><span class="identifier">chk</span><span class="plain"><=1; </span><span class="identifier">chk</span><span class="plain">++) {</span>
|
|
<span class="reserved">pcalc_func</span><span class="plain"> *</span><span class="identifier">pf</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[</span><span class="identifier">chk</span><span class="plain">].</span><span class="element">function</span><span class="plain">;</span>
|
|
<span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">pf</span><span class="plain">) && (</span><span class="identifier">pf</span><span class="plain">-></span><span class="element">fn_of</span><span class="plain">.</span><span class="element">variable</span><span class="plain"> == </span><span class="identifier">var</span><span class="plain">) &&</span>
|
|
<span class="plain">(</span><span class="functiontext"><a href="6-bp.html#SP44">BinaryPredicates::write_optimised_loop_schema</a></span><span class="plain">(&</span><span class="identifier">loop_schema</span><span class="plain">, </span><span class="identifier">pf</span><span class="plain">-></span><span class="element">bp</span><span class="plain">))) {</span>
|
|
<span class="identifier">second_term</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[1-</span><span class="identifier">chk</span><span class="plain">];</span>
|
|
<span class="identifier">parent_optimised</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="11-pr.html#SP18">Calculus::Propositions::delete_atom</a></span><span class="plain">(</span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">);</span>
|
|
<span class="reserved">break</span><span class="plain">;</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">}</span>
|
|
<span class="plain">} </span><span class="reserved">else</span><span class="plain"> </span><span class="reserved">if</span><span class="plain"> ((</span><span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[0].</span><span class="element">variable</span><span class="plain"> == </span><span class="identifier">var</span><span class="plain">) &&</span>
|
|
<span class="plain">(</span><span class="functiontext"><a href="6-bp.html#SP44">BinaryPredicates::write_optimised_loop_schema</a></span><span class="plain">(&</span><span class="identifier">loop_schema</span><span class="plain">, </span><span class="identifier">bp</span><span class="plain">))) {</span>
|
|
<span class="identifier">second_term</span><span class="plain"> = </span><span class="identifier">pl</span><span class="plain">-></span><span class="element">terms</span><span class="plain">[1];</span>
|
|
<span class="identifier">parent_optimised</span><span class="plain"> = </span><span class="identifier">TRUE</span><span class="plain">;</span>
|
|
<span class="identifier">proposition</span><span class="plain"> = </span><span class="functiontext"><a href="11-pr.html#SP18">Calculus::Propositions::delete_atom</a></span><span class="plain">(</span><span class="identifier">proposition</span><span class="plain">, </span><span class="identifier">pl_prev</span><span class="plain">);</span>
|
|
<span class="plain">}</span>
|
|
</pre>
|
|
|
|
<p class="inwebparagraph"></p>
|
|
|
|
<p class="endnote">This code is used in <a href="12-cdp.html#SP5_1_1">§5.1.1</a>.</p>
|
|
|
|
<p class="inwebparagraph"><a id="SP6"></a><b>§6. </b>And that concludes the predicate-calculus engine at the heart of Inform.
|
|
</p>
|
|
|
|
<hr class="tocbar">
|
|
<ul class="toc"><li><a href="12-cad.html">Back to 'Cinders and Deferrals'</a></li><li><i>(This section ends Chapter 12: Use of Propositions.)</i></li></ul><hr class="tocbar">
|
|
<!--End of weave-->
|
|
<script>
|
|
function togglePopup(material_id) {
|
|
var popup = document.getElementById(material_id);
|
|
popup.classList.toggle("show");
|
|
}
|
|
</script>
|
|
|
|
<link href="Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script>
|
|
MathJax = {
|
|
tex: {
|
|
inlineMath: '$', '$'], ['\\(', '\\)'
|
|
},
|
|
svg: {
|
|
fontCache: 'global'
|
|
}
|
|
};
|
|
</script>
|
|
<script type="text/javascript" id="MathJax-script" async
|
|
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
|
|
</script>
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|