ifhub/inform7
1
0
Fork 0
mirror of https://github.com/ganelson/inform.git synced 2024-06-30 22:14:58 +03:00
Code Issues Projects Releases Wiki Activity

Completed simplifications

Browse source
This commit is contained in:
Graham Nelson 2021-02-04 09:24:35 +00:00
parent 4994386ea4
commit 65f41dbca4
9 changed files with 157 additions and 159 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
README.md
View file

@ -1,6 +1,6 @@
# Inform 7
v10.1.0-alpha.1+6R14 'Krypton' (3 February 2021)
v10.1.0-alpha.1+6R15 'Krypton' (4 February 2021)
## About Inform 7

4
build.txt
View file

@ -1,3 +1,3 @@
Prerelease: alpha.1
Build Date: 3 February 2021
Build Number: 6R14
Build Date: 4 February 2021
Build Number: 6R15

2
docs/calculus-module/2-kp.html
View file

@ -108,7 +108,7 @@ and these all belong to the family:
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">KindPredicates::get_kind</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">KindPredicates::get_kind</span></span>:<br/>Propositions - <a href="4-prp.html#SP25">&#167;25</a>, <a href="4-prp.html#SP29">&#167;29</a><br/>Binding and Substitution - <a href="4-bas.html#SP14">&#167;14</a><br/>Type Check Propositions - <a href="4-tcp.html#SP4_2">&#167;4.2</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_13_1">&#167;2.13.1</a><br/>Simplifications - <a href="5-smp.html#SP9_3">&#167;9.3</a>, <a href="5-smp.html#SP9_3_1">&#167;9.3.1</a>, <a href="5-smp.html#SP9_4">&#167;9.4</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">KindPredicates::get_kind</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">KindPredicates::get_kind</span></span>:<br/>Propositions - <a href="4-prp.html#SP25">&#167;25</a>, <a href="4-prp.html#SP29">&#167;29</a><br/>Binding and Substitution - <a href="4-bas.html#SP14">&#167;14</a><br/>Type Check Propositions - <a href="4-tcp.html#SP4_2">&#167;4.2</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_13_1">&#167;2.13.1</a><br/>Simplifications - <a href="5-smp.html#SP9_3">&#167;9.3</a>, <a href="5-smp.html#SP9_3_1">&#167;9.3.1</a>, <a href="5-smp.html#SP9_4">&#167;9.4</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">assert_kind</span><span class="plain-syntax">;</span>

8
docs/calculus-module/4-ap.html
View file

@ -156,7 +156,7 @@ in 2020 simplified the picture considerably.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Atoms::new</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Atoms::new</span></span>:<br/><a href="4-ap.html#SP6">&#167;6</a>, <a href="4-ap.html#SP9">&#167;9</a>, <a href="4-ap.html#SP10">&#167;10</a><br/>Propositions - <a href="4-prp.html#SP13">&#167;13</a>, <a href="4-prp.html#SP16">&#167;16</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_13">&#167;2.13</a>, <a href="5-sc.html#SP3_8">&#167;3.8</a><br/>Simplifications - <a href="5-smp.html#SP2_2">&#167;2.2</a>, <a href="5-smp.html#SP5">&#167;5</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Atoms::new</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Atoms::new</span></span>:<br/><a href="4-ap.html#SP6">&#167;6</a>, <a href="4-ap.html#SP9">&#167;9</a>, <a href="4-ap.html#SP10">&#167;10</a><br/>Propositions - <a href="4-prp.html#SP13">&#167;13</a>, <a href="4-prp.html#SP16">&#167;16</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_13">&#167;2.13</a>, <a href="5-sc.html#SP3_8">&#167;3.8</a><br/>Simplifications - <a href="5-smp.html#SP2_2">&#167;2.2</a>, <a href="5-smp.html#SP5">&#167;5</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">CREATE</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax"> = </span><span class="identifier-syntax">element</span><span class="plain-syntax">;</span>
@ -221,21 +221,21 @@ compilation time, and less obvious even how many variables are needed.
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Atoms::is_nonexistence_quantifier</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></span>:<br/>Simplifications - <a href="5-smp.html#SP9_2">&#167;9.2</a>, <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Atoms::is_nonexistence_quantifier</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></span>:<br/>Simplifications - <a href="5-smp.html#SP9_2">&#167;9.2</a>, <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">not_exists_quantifier</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Atoms::is_forall_quantifier</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Atoms::is_forall_quantifier</span></span>:<br/>Simplifications - <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Atoms::is_forall_quantifier</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Atoms::is_forall_quantifier</span></span>:<br/>Simplifications - <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">for_all_quantifier</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Atoms::is_notall_quantifier</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">Atoms::is_notall_quantifier</span></span>:<br/>Simplifications - <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Atoms::is_notall_quantifier</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">Atoms::is_notall_quantifier</span></span>:<br/>Simplifications - <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">not_for_all_quantifier</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>

6
docs/calculus-module/4-prp.html
View file

@ -559,7 +559,7 @@ is <span class="extract"><span class="extract-syntax">NULL</span></span>.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::insert_atom</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">Propositions::insert_atom</span></span>:<br/>Binding and Substitution - <a href="4-bas.html#SP10">&#167;10</a><br/>Simplifications - <a href="5-smp.html#SP2_2">&#167;2.2</a>, <a href="5-smp.html#SP3">&#167;3</a>, <a href="5-smp.html#SP5">&#167;5</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP7">&#167;7</a>, <a href="5-smp.html#SP9_3_2">&#167;9.3.2</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">,</span>
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::insert_atom</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">Propositions::insert_atom</span></span>:<br/>Binding and Substitution - <a href="4-bas.html#SP10">&#167;10</a><br/>Simplifications - <a href="5-smp.html#SP2_2">&#167;2.2</a>, <a href="5-smp.html#SP3">&#167;3</a>, <a href="5-smp.html#SP5">&#167;5</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP7">&#167;7</a>, <a href="5-smp.html#SP9_3_2">&#167;9.3.2</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
@ -576,7 +576,7 @@ is <span class="extract"><span class="extract-syntax">NULL</span></span>.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::delete_atom</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Propositions::delete_atom</span></span>:<br/><a href="4-prp.html#SP34">&#167;34</a>, <a href="4-prp.html#SP35">&#167;35</a>, <a href="4-prp.html#SP36">&#167;36</a><br/>Simplifications - <a href="5-smp.html#SP9_3_1">&#167;9.3.1</a>, <a href="5-smp.html#SP9_3_2">&#167;9.3.2</a>, <a href="5-smp.html#SP9_4">&#167;9.4</a>, <a href="5-smp.html#SP13">&#167;13</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP16_1">&#167;16.1</a>, <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">) {</span>
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::delete_atom</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Propositions::delete_atom</span></span>:<br/><a href="4-prp.html#SP34">&#167;34</a>, <a href="4-prp.html#SP35">&#167;35</a>, <a href="4-prp.html#SP36">&#167;36</a><br/>Simplifications - <a href="5-smp.html#SP9_3_1">&#167;9.3.1</a>, <a href="5-smp.html#SP9_3_2">&#167;9.3.2</a>, <a href="5-smp.html#SP9_4">&#167;9.4</a>, <a href="5-smp.html#SP13">&#167;13</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP16_1">&#167;16.1</a>, <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"deleting atom nowhere"</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
@ -653,7 +653,7 @@ two special pseudo-element-numbers:
<span class="definition-keyword">define</span> <span class="constant-syntax">END_PROP_HERE</span><span class="plain-syntax"> -1 </span><span class="comment-syntax"> a sentinel meaning "the proposition must end at this point"</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::match</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Propositions::match</span></span>:<br/><a href="4-prp.html#SP35">&#167;35</a><br/>Sentence Conversions - <a href="5-sc.html#SP3_4">&#167;3.4</a><br/>Simplifications - <a href="5-smp.html#SP4">&#167;4</a>, <a href="5-smp.html#SP5">&#167;5</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP9_2">&#167;9.2</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP18">&#167;18</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">c</span><span class="plain-syntax">, ...) {</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::match</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Propositions::match</span></span>:<br/><a href="4-prp.html#SP35">&#167;35</a><br/>Sentence Conversions - <a href="5-sc.html#SP3_4">&#167;3.4</a><br/>Simplifications - <a href="5-smp.html#SP4">&#167;4</a>, <a href="5-smp.html#SP5">&#167;5</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP9_2">&#167;9.2</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP18">&#167;18</a>, <a href="5-smp.html#SP19">&#167;19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">c</span><span class="plain-syntax">, ...) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">va_list</span><span class="plain-syntax"> </span><span class="identifier-syntax">ap</span><span class="plain-syntax">; </span><span class="comment-syntax"> the variable argument list signified by the dots</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">va_start</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax">); </span><span class="comment-syntax"> macro to begin variable argument processing</span>

2
docs/calculus-module/5-sc.html
View file

@ -599,7 +599,7 @@ Still, rule (iii) can only be ensured by writing the routines carefully.
<span class="plain-syntax"> </span><span class="identifier-syntax">APPLY_SIMP</span><span class="plain-syntax">(</span><span class="identifier-syntax">sentence_prop</span><span class="plain-syntax">, </span><a href="5-smp.html#SP10" class="function-link"><span class="function-syntax">Simplifications::turn_right_way_round</span></a><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">APPLY_SIMP</span><span class="plain-syntax">(</span><span class="identifier-syntax">sentence_prop</span><span class="plain-syntax">, </span><a href="5-smp.html#SP11" class="function-link"><span class="function-syntax">Simplifications::region_containment</span></a><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">APPLY_SIMP</span><span class="plain-syntax">(</span><span class="identifier-syntax">sentence_prop</span><span class="plain-syntax">, </span><a href="5-smp.html#SP18" class="function-link"><span class="function-syntax">Simplifications::everywhere_and_nowhere</span></a><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">APPLY_SIMP</span><span class="plain-syntax">(</span><span class="identifier-syntax">sentence_prop</span><span class="plain-syntax">, </span><a href="5-smp.html#SP19" class="function-link"><span class="function-syntax">Simplifications::everywhere_and_nowhere</span></a><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">APPLY_SIMP</span><span class="plain-syntax">(</span><span class="identifier-syntax">sentence_prop</span><span class="plain-syntax">, </span><a href="5-smp.html#SP12" class="function-link"><span class="function-syntax">Simplifications::reduce_predicates</span></a><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">APPLY_SIMP</span><span class="plain-syntax">(</span><span class="identifier-syntax">sentence_prop</span><span class="plain-syntax">, </span><a href="5-smp.html#SP13" class="function-link"><span class="function-syntax">Simplifications::eliminate_redundant_variables</span></a><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">APPLY_SIMP</span><span class="plain-syntax">(</span><span class="identifier-syntax">sentence_prop</span><span class="plain-syntax">, </span><a href="5-smp.html#SP14" class="function-link"><span class="function-syntax">Simplifications::not_related_to_something</span></a><span class="plain-syntax">);</span>

136
docs/calculus-module/5-smp.html
View file

@ -91,7 +91,7 @@ function togglePopup(material_id) {
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../compiler.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#5">Chapter 5: Sentences</a></li><li><b>Simplifications</b></li></ul></div>
<p class="purpose">A set of operations which rewrite propositions to make them easier or quicker to test at run-time without changing their meaning.</p>
<ul class="toc"><li><a href="5-smp.html#SP1">&#167;1. Golden rules</a></li><li><a href="5-smp.html#SP2">&#167;2. Simplify the nothing constant (fudge)</a></li><li><a href="5-smp.html#SP3">&#167;3. Use listed-in predicates (deduction)</a></li><li><a href="5-smp.html#SP4">&#167;4. Simplify negated determiners (deduction)</a></li><li><a href="5-smp.html#SP6">&#167;6. Simplify negated satisfiability (deduction)</a></li><li><a href="5-smp.html#SP7">&#167;7. Make kind requirements explicit (deduction)</a></li><li><a href="5-smp.html#SP8">&#167;8. Remove redundant kind predicates (deduction)</a></li><li><a href="5-smp.html#SP10">&#167;10. Turn binary predicates the right way round (deduction)</a></li><li><a href="5-smp.html#SP11">&#167;11. Simplify region containment (fudge)</a></li><li><a href="5-smp.html#SP12">&#167;12. Reduce binary predicates (deduction)</a></li><li><a href="5-smp.html#SP13">&#167;13. Eliminating determined variables (deduction)</a></li><li><a href="5-smp.html#SP14">&#167;14. Simplify non-relation (deduction)</a></li><li><a href="5-smp.html#SP15">&#167;15. Convert gerunds to nouns (deduction)</a></li><li><a href="5-smp.html#SP16">&#167;16. Eliminate to have meaning property ownership (fudge)</a></li><li><a href="5-smp.html#SP18">&#167;18. Turn all rooms to everywhere (fudge)</a></li></ul><hr class="tocbar">
<ul class="toc"><li><a href="5-smp.html#SP1">&#167;1. Golden rules</a></li><li><a href="5-smp.html#SP2">&#167;2. Simplify the nothing constant (fudge)</a></li><li><a href="5-smp.html#SP3">&#167;3. Use listed-in predicates (deduction)</a></li><li><a href="5-smp.html#SP4">&#167;4. Simplify negated determiners (deduction)</a></li><li><a href="5-smp.html#SP6">&#167;6. Simplify negated satisfiability (deduction)</a></li><li><a href="5-smp.html#SP7">&#167;7. Make kind requirements explicit (deduction)</a></li><li><a href="5-smp.html#SP8">&#167;8. Remove redundant kind predicates (deduction)</a></li><li><a href="5-smp.html#SP10">&#167;10. Turn binary predicates the right way round (deduction)</a></li><li><a href="5-smp.html#SP11">&#167;11. Simplify region containment (fudge)</a></li><li><a href="5-smp.html#SP12">&#167;12. Reduce binary predicates (deduction)</a></li><li><a href="5-smp.html#SP13">&#167;13. Eliminating determined variables (deduction)</a></li><li><a href="5-smp.html#SP14">&#167;14. Simplify non-relation (deduction)</a></li><li><a href="5-smp.html#SP15">&#167;15. Convert gerunds to nouns (deduction)</a></li><li><a href="5-smp.html#SP16">&#167;16. Eliminate to have meaning property ownership (fudge)</a></li><li><a href="5-smp.html#SP18">&#167;18. Turn all rooms to everywhere (fudge)</a></li><li><a href="5-smp.html#SP19">&#167;19. Everywhere and nowhere (fudge)</a></li></ul><hr class="tocbar">
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>&#167;1. Golden rules. </b>The following functions all take a propeosition \(\Sigma\) in the parameter
<span class="extract"><span class="extract-syntax">prop</span></span>, and return \(\Sigma'\); they set the flag pointed to by <span class="extract"><span class="extract-syntax">changed</span></span> if
@ -848,11 +848,9 @@ only one thing at a time, but might be in many regions at once.
point where we choose to divert some uses to <span class="extract"><span class="extract-syntax">R_regional_containment</span></span>.
If \(R\) is a constant region name, and \(C_D\), \(C_R\) are the predicates for
direct and region containment, then
\(\) \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots C_R(t, R)\cdots \(\)
\(\) \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots C_R(R, t)\cdots \(\)
(Note that a region cannot directly contain any object, except a backdrop.)
$$ \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(t, R)\cdots $$
$$ \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(R, t)\cdots $$
Note that a region cannot directly contain any object, except a backdrop.
</p>
<pre class="displayed-code all-displayed-code code-font">
@ -874,7 +872,8 @@ direct and region containment, then
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">KB</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Specifications::to_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::is_object_of_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">KB</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_backdrop</span><span class="plain-syntax">)) </span><span class="identifier-syntax">backdropping</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::is_object_of_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">KB</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_backdrop</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">backdropping</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">regionality</span><span class="plain-syntax">) &amp;&amp; (!</span><span class="identifier-syntax">backdropping</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">R_regional_containment</span><span class="plain-syntax">);</span>
@ -891,23 +890,22 @@ direct and region containment, then
gain considerably by being able to eliminate a variable altogether. For
instance, suppose we have "Mme Cholet is in a burrow". This will
initially come out as
\(\) \exists x: {\it burrow}(x)\land {\it in}(<span class="extract"><span class="extract-syntax">Cholet</span></span>, x) \(\)
$$ \exists x: {\it burrow}(x)\land {\it in}(C, x) $$
To test that proposition requires trying all possible burrows \(x\).
But exploiting the fact that Mme Cholet can only be in one place at a
time, we can reduce the binary predicate to equality, thus:
\(\) \exists x: {\it burrow}(x)\land {\it is}(<span class="extract"><span class="extract-syntax">ContainerOf(Cholet)</span></span>, x) \(\)
A later simplification can then observe that this tells us what \(x\) must be,
$$ \exists x: {\it burrow}(x)\land {\it is}(f(C), x) $$
where \(f\) is the function determining the location of something. A later
simplification can then observe that this tells us what \(x\) must be,
and eliminate both quantifier and variable.
</p>
<p class="commentary">Formally, suppose \(B\) is a predicate with a function \(f_B\) such that \(B(x, y)\)
is true if and only \(y = f_B(x)\). Then:
\(\) \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots \(\)
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots $$
Similarly, if there is a function \(g_B\) such that \(B(x, y)\) if and only if
\(x = g_B(y)\) then
\(\) \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots \(\)
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots $$
Not all BPs have these: the reason for our fudge on regional containment (above)
is that direct containment does, but region containment doesn't, and this is
why it was necessary to separate the two out.
@ -970,13 +968,13 @@ where this is safe.
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">permitted</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"Substituting %c &lt;-- $0\n"</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">], &amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> first delete the </span>\({\it is}(v, t)\)<span class="comment-syntax"> predicate</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> first delete the is(v, t) predicate</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> then unbind the variable, by deleting its </span>\(\exists v\)<span class="comment-syntax"> quantifier</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> then unbind the variable, by deleting its exists v quantifier</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position_of_binding</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"After deletion: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">binding_status</span><span class="plain-syntax">[</span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">] = </span><span class="constant-syntax">NOT_BOUND_AT_ALL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> then substitute for all other occurrences of </span>\(v\)
<span class="plain-syntax"> </span><span class="comment-syntax"> then substitute for all other occurrences of v</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-bas.html#SP13" class="function-link"><span class="function-syntax">Binding::substitute_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_to_sub</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">j</span><span class="plain-syntax">],</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">changed</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
@ -1028,7 +1026,7 @@ substituting \(v = f_A(f_B(\cdots s))\).
<p class="commentary">But only if the term \(s\) underneath those functions does not make the equation
\({\it is}(v, f_A(f_B(\cdots s)))\) implicit. Suppose \(s\) depends
on a variable \(w\) which is bound and occurs {\it after} the binding of \(v\).
on a variable \(w\) which is bound and occurs after the binding of \(v\).
The value of such a variable \(w\) can depend on the value of \(v\). Saying that
\(v=s\) may therefore not determine a unique value of \(v\) at all: it may be
a subtle condition passed by a whole class of possible values, or none.
@ -1039,10 +1037,10 @@ More problematic is \({\it is}(v, f_C(v))\), "\(v\) is the container of \(v\)",
which is never true. Still worse is
$$ \exists v: V_{=2} w: {\it is}(v, w) $$
which literally says there is a value of \(v\) equal to two different things &mdash;
certainly false. But if we were allowed to eliminate \(v\), we would get just
certainly false. But if we eliminated \(v\), we would get just
$$ V_{=2} w $$
which asserts "there are exactly two objects" &mdash; which is certainly not a
valid deduction, and might even be true.
valid deduction.
</p>
<p class="commentary">Here <span class="extract"><span class="extract-syntax">var_to_sub</span></span> is \(v\) and <span class="extract"><span class="extract-syntax">var_in_other_term</span></span> is \(w\), or else they are \(-1\)
@ -1066,14 +1064,15 @@ if no variables are present in their respective terms.
<ul class="endnotetexts"><li>This code is used in <a href="5-smp.html#SP13">&#167;13</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP14" class="paragraph-anchor"></a><b>&#167;14. Simplify non-relation (deduction). </b>As a result of the previous simplifications, it fairly often happens that we
find a term like
\(\) \lnot({\it thing}(t<span class="extract"><span class="extract-syntax">.component_parent</span></span>)) \(\)
in the proposition. This comes out of text such as "... not part of something",
$$ \lnot({\it thing}(f_P(t))) $$
where \(f_P\) is the function determining what, if anything, the object \(t\) is
a component part of. This comes out of text such as "... not part of something",
asserting first that there is no \(y\) such that \(t\) is a part of \(y\), and then
simplifying to remove the \(y\) variable. A term like the one above is then
left behind. But the negation is cumbersome, and makes the proposition harder
to assert or test. Exploiting the fact that <span class="extract"><span class="extract-syntax">component_parent</span></span> is a property
which is either the part-parent or else <span class="extract"><span class="extract-syntax">nothing</span></span>, we can simplify to:
\(\) {\it is}(t<span class="extract"><span class="extract-syntax">.component_parent</span></span>, <span class="extract"><span class="extract-syntax">nothing</span></span>) \(\)
to assert or test. Exploiting the fact that \(f_P(t)\) is a property
which is either the part-parent or else \(N =\) <span class="extract"><span class="extract-syntax">nothing</span></span>, we can simplify to:
$$ {\it is}(f_P(t), N) $$
And similar tricks can be pulled for other various-to-one-object predicates.
</p>
@ -1081,8 +1080,7 @@ And similar tricks can be pulled for other various-to-one-object predicates.
such that \(B(x, y)\) iff \(f_B(x) = y\), or else such that \(B(x, y)\) iff \(f_B(y) = x\);
and such that the values of \(f_B\) are objects. Let \(K\) be a kind of object.
Then:
\(\) \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(f_B(t), <span class="extract"><span class="extract-syntax">nothing</span></span>) \cdots \(\)
$$ \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t), N) \cdots $$
</p>
<p class="commentary">A similar trick for kinds of value is not possible, because &mdash; unlike objects &mdash;
@ -1107,7 +1105,8 @@ they have no "not a valid case" value analogous to the non-object <span class="e
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">KIND_term</span><span class="plain-syntax"> = </span><span class="identifier-syntax">kind_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0];</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">KIND_term</span><span class="plain-syntax">.</span><span class="element-syntax">function</span><span class="plain-syntax">) </span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">KIND_term</span><span class="plain-syntax">.</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">bp</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">bp</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::term_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">)))) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP34" class="function-link"><span class="function-syntax">Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove negation grouping</span>
<span class="plain-syntax"> </span><span class="comment-syntax"> remove negation grouping</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP34" class="function-link"><span class="function-syntax">Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">kind=K</span></span>
<span class="plain-syntax"> </span><span class="comment-syntax"> now insert equality predicate:</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
@ -1125,17 +1124,10 @@ they have no "not a valid case" value analogous to the non-object <span class="e
<p class="commentary firstcommentary"><a id="SP15" class="paragraph-anchor"></a><b>&#167;15. Convert gerunds to nouns (deduction). </b>Suppose we write:
</p>
<blockquote>
<p>The funky thing to do is a stored action that varies.</p>
</blockquote>
<p class="commentary">and subsequently:
</p>
<blockquote>
<p>the funky thing to do is waiting</p>
</blockquote>
<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">The</span><span class="plain-syntax"> </span><span class="identifier-syntax">funky</span><span class="plain-syntax"> </span><span class="identifier-syntax">thing</span><span class="plain-syntax"> </span><span class="identifier-syntax">to</span><span class="plain-syntax"> </span><span class="identifier-syntax">do</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> </span><span class="identifier-syntax">stored</span><span class="plain-syntax"> </span><span class="identifier-syntax">action</span><span class="plain-syntax"> </span><span class="identifier-syntax">that</span><span class="plain-syntax"> </span><span class="identifier-syntax">varies</span><span class="plain-syntax">.</span>
<span class="identifier-syntax">The</span><span class="plain-syntax"> </span><span class="identifier-syntax">funky</span><span class="plain-syntax"> </span><span class="identifier-syntax">thing</span><span class="plain-syntax"> </span><span class="identifier-syntax">to</span><span class="plain-syntax"> </span><span class="identifier-syntax">do</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">waiting</span><span class="plain-syntax">.</span>
</pre>
<p class="commentary">Here "waiting" is a gerund, and although it describes an action it is a
noun (thus a value) rather than a condition. We coerce its constant value
accordingly.
@ -1151,7 +1143,8 @@ accordingly.
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Conditions::is_TEST_ACTION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="identifier-syntax">constant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Conditions::action_tested</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="identifier-syntax">constant</span><span class="plain-syntax"> =</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">Conditions::action_tested</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
@ -1165,23 +1158,19 @@ can also arise from text such as
</blockquote>
<p class="commentary">where it's the numerical "weight" property which is owned by the balloon.
(The language of abstract "property" always echoes that of real physical
things &mdash; consider how the iTunes Music Store invites you to "buy" what
is at best a lease of temporary, partial and revocable rights to make use
of something with no physical essence. This isn't a con trick, or not
altogether so. We like the word "buy"; we immediately understand it.)
At this stage of simplification, the above has produced
\(\) {\hbox{\it at-most}}(<span class="extract"><span class="extract-syntax">weight</span></span>, 1)\land {\it is}(<span class="extract"><span class="extract-syntax">balloon</span></span>, f_H(<span class="extract"><span class="extract-syntax">weight</span></span>)) \(\)
where \(H\) is the predicate <span class="extract"><span class="extract-syntax">a_has_b_predicate</span></span>. As it stands, this
proposition will fail type-checking, because it contains an implicit
free variable &mdash; the object which owns the weight. We make this explicit
by removing ${\it is}(<span class="extract"><span class="extract-syntax">balloon</span></span>, f_H(<span class="extract"><span class="extract-syntax">weight</span></span>))$ and replacing all other
references to <span class="extract"><span class="extract-syntax">weight</span></span> with "the weight of <span class="extract"><span class="extract-syntax">balloon</span></span>".
$$ {\it atmost}(w, 1)\land {\it is}(B, f_H(w)) $$
where \(H\) is the predicate <span class="extract"><span class="extract-syntax">a_has_b_predicate</span></span>. As it stands, this proposition
will fail type-checking, because it contains an implicit free variable &mdash; the
object which owns the weight. We make this explicit by removing
\({\it is}(B, f_H(w))\) and replacing all other references to \(w\) with "the
weight of \(B\)".
</p>
<p class="commentary">This is a fudge because it assumes &mdash; possibly wrongly &mdash; that all
references to the weight are to the weight of the same thing. In
sufficiently contrived sentences, this wouldn't be true.
<p class="commentary">This is a fudge because it assumes &mdash; possibly wrongly &mdash; that all references
to the weight are to the weight of the same thing. In sufficiently contrived
sentences, this wouldn't be true. No bugs have ever been reported which suggest
that real users run into this.
</p>
<pre class="displayed-code all-displayed-code code-font">
@ -1221,7 +1210,8 @@ term \(C\).
<span class="plain-syntax"> </span><span class="identifier-syntax">Lvalues::new_PROPERTY_VALUE</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1-</span><span class="identifier-syntax">i</span><span class="plain-syntax">].</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">Node::set_text</span><span class="plain-syntax">(</span><span class="identifier-syntax">po_spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">prn</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">name</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">no_substitutions_made</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP17" class="function-link"><span class="function-syntax">Simplifications::prop_substitute_prop_cons</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prn</span><span class="plain-syntax">, </span><span class="identifier-syntax">po_spec</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">no_substitutions_made</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="5-smp.html#SP17" class="function-link"><span class="function-syntax">Simplifications::prop_substitute_prop_cons</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prn</span><span class="plain-syntax">, </span><span class="identifier-syntax">po_spec</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> &amp;</span><span class="identifier-syntax">no_substitutions_made</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">no_substitutions_made</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
@ -1274,17 +1264,11 @@ usually mean "in all rooms", so that the sentence
<p class="commentary">means the sky is in every room, not that the sky is equal to every room.
Since the literal reading would make no useful sense, Inform fudges the
proposition to change it to the idiomatic one.
\(\) \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
\Sigma' = \cdots {\it everywhere}(t) \(\)
\(\) \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
\Sigma' = \cdots {\it everywhere}(t) \(\)
\(\) \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
\Sigma' = \cdots \lnot({\it everywhere}(t)) \(\)
\(\) \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
\Sigma' = \cdots \lnot({\it everywhere}(t)) \(\)
</p>
<p class="commentary">Note that we match this only at the end of a proposition, where \(v\) can
$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
Note that we match this only at the end of a proposition, where \(v\) can
have no other consequence.
</p>
@ -1316,11 +1300,13 @@ have no other consequence.
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_CLOSE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">WherePredicates::everywhere_up</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
@ -1357,6 +1343,14 @@ have no other consequence.
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP19" class="paragraph-anchor"></a><b>&#167;19. Everywhere and nowhere (fudge). </b>Similarly, if the proposition expresses the idea of "nowhere" or "everywhere"
by spelling this out in quantifiers about being no place or every place, then
replace those with uses of the special unary predicates for "nowhere" and
"everywhere".
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Simplifications::everywhere_and_nowhere</span><button class="popup" onclick="togglePopup('usagePopup18')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup18">Usage of <span class="code-font"><span class="function-syntax">Simplifications::everywhere_and_nowhere</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_14">&#167;2.14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">IF_MODULE</span>
@ -1387,7 +1381,8 @@ have no other consequence.
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">DOMAIN_CLOSE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove </span><span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_nonexistence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax"> = </span><span class="identifier-syntax">WherePredicates::nowhere_up</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
@ -1395,7 +1390,8 @@ have no other consequence.
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax"> = </span><span class="identifier-syntax">WherePredicates::everywhere_up</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_notall_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q_atom</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">, </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP18" class="function-link"><span class="function-syntax">Propositions::insert_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl_prev</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>

29
inform7/Figures/timings-diagnostics.txt
View file

@ -1,35 +1,36 @@
100.0% in inform7 run
66.9% in compilation to Inter
25.4% in //Phrases::Manager::compile_first_block//
8.9% in //Phrases::Manager::compile_as_needed//
6.9% in //Strings::compile_responses//
6.3% in //World::Compile::compile//
25.7% in //Phrases::Manager::compile_first_block//
8.8% in //Phrases::Manager::compile_as_needed//
7.0% in //Strings::compile_responses//
6.1% in //World::Compile::compile//
3.8% in //MajorNodes::pre_pass//
3.2% in //MajorNodes::pass_1//
2.1% in //Phrases::Manager::RulePrintingRule_routine//
3.3% in //MajorNodes::pass_1//
2.0% in //Phrases::Manager::RulePrintingRule_routine//
2.0% in //Phrases::Manager::rulebooks_array//
1.0% in //RTVerbs::ConjugateVerb//
0.9% in //Phrases::Manager::traverse//
1.1% in //RTVerbs::ConjugateVerb//
0.8% in //Phrases::Manager::traverse//
0.5% in //Phrases::Manager::compile_rulebooks//
0.5% in //Phrases::Manager::parse_rule_parameters//
0.5% in //World::complete//
0.3% in //MajorNodes::pass_2//
0.3% in //Phrases::Manager::compile_rulebooks//
0.3% in //RTRelations::compile_defined_relations//
0.1% in //Kinds::RunTime::compile_data_type_support_routines//
0.1% in //PL::Parsing::Verbs::compile_all//
0.1% in //Task::make_built_in_kind_constructors//
3.3% not specifically accounted for
30.9% in running Inter pipeline
30.7% in running Inter pipeline
10.6% in step preparation
9.8% in inter step 2/12: link
9.8% in step preparation
7.4% in inter step 12/12: generate inform6 -> auto.inf
7.1% in inter step 12/12: generate inform6 -> auto.inf
0.3% in inter step 9/12: make-identifiers-unique
0.1% in inter step 10/12: reconcile-verbs
0.1% in inter step 11/12: eliminate-redundant-labels
0.1% in inter step 4/12: parse-linked-matter
0.1% in inter step 5/12: resolve-conditional-compilation
0.1% in inter step 6/12: assimilate
0.1% in inter step 7/12: resolve-external-symbols
0.1% in inter step 8/12: inspect-plugs
2.4% not specifically accounted for
1.5% not specifically accounted for
2.0% in supervisor
0.2% not specifically accounted for
0.4% not specifically accounted for

127
services/calculus-module/Chapter 5/Simplifications.w
View file

@ -684,11 +684,9 @@ So far we assume every "in" means the |R_containment|. This is the
point where we choose to divert some uses to |R_regional_containment|.
If $R$ is a constant region name, and $C_D$, $C_R$ are the predicates for
direct and region containment, then
$$ \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots C_R(t, R)\cdots $$
$$ \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad
\Sigma' = \cdots C_R(R, t)\cdots $$
(Note that a region cannot directly contain any object, except a backdrop.)
$$ \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(t, R)\cdots $$
$$ \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(R, t)\cdots $$
Note that a region cannot directly contain any object, except a backdrop.
=
pcalc_prop *Simplifications::region_containment(pcalc_prop *prop, int *changed) {
@ -709,7 +707,8 @@ pcalc_prop *Simplifications::region_containment(pcalc_prop *prop, int *changed)
}
if (pl->terms[1-j].constant) {
kind *KB = Specifications::to_kind(pl->terms[1-j].constant);
if (Kinds::Behaviour::is_object_of_kind(KB, K_backdrop)) backdropping = TRUE;
if (Kinds::Behaviour::is_object_of_kind(KB, K_backdrop))
backdropping = TRUE;
}
if ((regionality) && (!backdropping)) {
pl->predicate = STORE_POINTER_binary_predicate(R_regional_containment);
@ -727,22 +726,21 @@ If we are able to reduce a binary to a unary predicate, we will probably
gain considerably by being able to eliminate a variable altogether. For
instance, suppose we have "Mme Cholet is in a burrow". This will
initially come out as
$$ \exists x: {\it burrow}(x)\land {\it in}(|Cholet|, x) $$
$$ \exists x: {\it burrow}(x)\land {\it in}(C, x) $$
To test that proposition requires trying all possible burrows $x$.
But exploiting the fact that Mme Cholet can only be in one place at a
time, we can reduce the binary predicate to equality, thus:
$$ \exists x: {\it burrow}(x)\land {\it is}(|ContainerOf(Cholet)|, x) $$
A later simplification can then observe that this tells us what $x$ must be,
$$ \exists x: {\it burrow}(x)\land {\it is}(f(C), x) $$
where $f$ is the function determining the location of something. A later
simplification can then observe that this tells us what $x$ must be,
and eliminate both quantifier and variable.
Formally, suppose $B$ is a predicate with a function $f_B$ such that $B(x, y)$
is true if and only $y = f_B(x)$. Then:
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots $$
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots $$
Similarly, if there is a function $g_B$ such that $B(x, y)$ if and only if
$x = g_B(y)$ then
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots $$
$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots $$
Not all BPs have these: the reason for our fudge on regional containment (above)
is that direct containment does, but region containment doesn't, and this is
why it was necessary to separate the two out.
@ -804,13 +802,13 @@ pcalc_prop *Simplifications::eliminate_redundant_variables(pcalc_prop *prop, int
if (permitted) {
LOGIF(PREDICATE_CALCULUS_WORKINGS, "Substituting %c <-- $0\n",
pcalc_vars[var_to_sub], &(pl->terms[1-j]));
/* first delete the ${\it is}(v, t)$ predicate */
/* first delete the is(v, t) predicate */
prop = Propositions::delete_atom(prop, pl_prev);
/* then unbind the variable, by deleting its $\exists v$ quantifier */
/* then unbind the variable, by deleting its exists v quantifier */
prop = Propositions::delete_atom(prop, position_of_binding[var_to_sub]);
LOGIF(PREDICATE_CALCULUS_WORKINGS, "After deletion: $D\n", prop);
binding_status[var_to_sub] = NOT_BOUND_AT_ALL;
/* then substitute for all other occurrences of $v$ */
/* then substitute for all other occurrences of v */
prop = Binding::substitute_term(prop, var_to_sub, pl->terms[1-j],
FALSE, NULL, changed);
*changed = TRUE;
@ -856,7 +854,7 @@ substituting $v = f_A(f_B(\cdots s))$.
But only if the term $s$ underneath those functions does not make the equation
${\it is}(v, f_A(f_B(\cdots s)))$ implicit. Suppose $s$ depends
on a variable $w$ which is bound and occurs {\it after} the binding of $v$.
on a variable $w$ which is bound and occurs after the binding of $v$.
The value of such a variable $w$ can depend on the value of $v$. Saying that
$v=s$ may therefore not determine a unique value of $v$ at all: it may be
a subtle condition passed by a whole class of possible values, or none.
@ -866,10 +864,10 @@ More problematic is ${\it is}(v, f_C(v))$, "$v$ is the container of $v$",
which is never true. Still worse is
$$ \exists v: V_{=2} w: {\it is}(v, w) $$
which literally says there is a value of $v$ equal to two different things --
certainly false. But if we were allowed to eliminate $v$, we would get just
certainly false. But if we eliminated $v$, we would get just
$$ V_{=2} w $$
which asserts "there are exactly two objects" -- which is certainly not a
valid deduction, and might even be true.
valid deduction.
Here |var_to_sub| is $v$ and |var_in_other_term| is $w$, or else they are $-1$
if no variables are present in their respective terms.
@ -888,22 +886,22 @@ if no variables are present in their respective terms.
@h Simplify non-relation (deduction).
As a result of the previous simplifications, it fairly often happens that we
find a term like
$$ \lnot({\it thing}(t|.component_parent|)) $$
in the proposition. This comes out of text such as "... not part of something",
$$ \lnot({\it thing}(f_P(t))) $$
where $f_P$ is the function determining what, if anything, the object $t$ is
a component part of. This comes out of text such as "... not part of something",
asserting first that there is no $y$ such that $t$ is a part of $y$, and then
simplifying to remove the $y$ variable. A term like the one above is then
left behind. But the negation is cumbersome, and makes the proposition harder
to assert or test. Exploiting the fact that |component_parent| is a property
which is either the part-parent or else |nothing|, we can simplify to:
$$ {\it is}(t|.component_parent|, |nothing|) $$
to assert or test. Exploiting the fact that $f_P(t)$ is a property
which is either the part-parent or else $N =$ |nothing|, we can simplify to:
$$ {\it is}(f_P(t), N) $$
And similar tricks can be pulled for other various-to-one-object predicates.
Formally, let $B$ be a binary predicate supporting either a function $f_B$
such that $B(x, y)$ iff $f_B(x) = y$, or else such that $B(x, y)$ iff $f_B(y) = x$;
and such that the values of $f_B$ are objects. Let $K$ be a kind of object.
Then:
$$ \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad
\Sigma' = \cdots {\it is}(f_B(t), |nothing|) \cdots $$
$$ \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t), N) \cdots $$
A similar trick for kinds of value is not possible, because -- unlike objects --
they have no "not a valid case" value analogous to the non-object |nothing|.
@ -926,7 +924,8 @@ pcalc_prop *Simplifications::not_related_to_something(pcalc_prop *prop, int *cha
pcalc_term KIND_term = kind_atom->terms[0];
if (KIND_term.function) bp = KIND_term.function->bp;
if ((bp) && (Kinds::eq(K, BinaryPredicates::term_kind(bp, 1)))) {
prop = Propositions::ungroup_after(prop, pl_prev, NULL); /* remove negation grouping */
/* remove negation grouping */
prop = Propositions::ungroup_after(prop, pl_prev, NULL);
prop = Propositions::delete_atom(prop, pl_prev); /* remove |kind=K| */
/* now insert equality predicate: */
prop = Propositions::insert_atom(prop, pl_prev,
@ -943,13 +942,10 @@ pcalc_prop *Simplifications::not_related_to_something(pcalc_prop *prop, int *cha
@h Convert gerunds to nouns (deduction).
Suppose we write:
>> The funky thing to do is a stored action that varies.
and subsequently:
>> the funky thing to do is waiting
= (text as Inform 7)
The funky thing to do is a stored action that varies.
The funky thing to do is waiting.
=
Here "waiting" is a gerund, and although it describes an action it is a
noun (thus a value) rather than a condition. We coerce its constant value
accordingly.
@ -964,7 +960,8 @@ pcalc_prop *Simplifications::convert_gerunds(pcalc_prop *prop, int *changed) {
if ((pl->element == PREDICATE_ATOM) && (pl->arity == 2))
for (int i=0; i<2; i++)
if (Conditions::is_TEST_ACTION(pl->terms[i].constant))
pl->terms[i].constant = Conditions::action_tested(pl->terms[i].constant);
pl->terms[i].constant =
Conditions::action_tested(pl->terms[i].constant);
return prop;
}
#endif
@ -976,22 +973,18 @@ can also arise from text such as
>> the balloon has weight at most 1
where it's the numerical "weight" property which is owned by the balloon.
(The language of abstract "property" always echoes that of real physical
things -- consider how the iTunes Music Store invites you to "buy" what
is at best a lease of temporary, partial and revocable rights to make use
of something with no physical essence. This isn't a con trick, or not
altogether so. We like the word "buy"; we immediately understand it.)
At this stage of simplification, the above has produced
$$ {\hbox{\it at-most}}(|weight|, 1)\land {\it is}(|balloon|, f_H(|weight|)) $$
where $H$ is the predicate |a_has_b_predicate|. As it stands, this
proposition will fail type-checking, because it contains an implicit
free variable -- the object which owns the weight. We make this explicit
by removing ${\it is}(|balloon|, f_H(|weight|))$ and replacing all other
references to |weight| with "the weight of |balloon|".
$$ {\it atmost}(w, 1)\land {\it is}(B, f_H(w)) $$
where $H$ is the predicate |a_has_b_predicate|. As it stands, this proposition
will fail type-checking, because it contains an implicit free variable -- the
object which owns the weight. We make this explicit by removing
${\it is}(B, f_H(w))$ and replacing all other references to $w$ with "the
weight of $B$".
This is a fudge because it assumes -- possibly wrongly -- that all
references to the weight are to the weight of the same thing. In
sufficiently contrived sentences, this wouldn't be true.
This is a fudge because it assumes -- possibly wrongly -- that all references
to the weight are to the weight of the same thing. In sufficiently contrived
sentences, this wouldn't be true. No bugs have ever been reported which suggest
that real users run into this.
=
#ifdef CORE_MODULE
@ -1026,7 +1019,8 @@ term $C$.
Lvalues::new_PROPERTY_VALUE(spec, pl->terms[1-i].constant);
Node::set_text(po_spec, prn->name);
int no_substitutions_made;
prop = Simplifications::prop_substitute_prop_cons(prop, prn, po_spec, &no_substitutions_made, pl);
prop = Simplifications::prop_substitute_prop_cons(prop, prn, po_spec,
&no_substitutions_made, pl);
if (no_substitutions_made > 0) {
prop = Propositions::delete_atom(prop, pl_prev);
PROPOSITION_EDITED_REPEATING_CURRENT(pl, prop);
@ -1075,15 +1069,10 @@ usually mean "in all rooms", so that the sentence
means the sky is in every room, not that the sky is equal to every room.
Since the literal reading would make no useful sense, Inform fudges the
proposition to change it to the idiomatic one.
$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
\Sigma' = \cdots {\it everywhere}(t) $$
$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
\Sigma' = \cdots {\it everywhere}(t) $$
$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
\Sigma' = \cdots \lnot({\it everywhere}(t)) $$
$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
\Sigma' = \cdots \lnot({\it everywhere}(t)) $$
$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
Note that we match this only at the end of a proposition, where $v$ can
have no other consequence.
@ -1115,11 +1104,13 @@ pcalc_prop *Simplifications::is_all_rooms(pcalc_prop *prop, int *changed) {
prop = Propositions::delete_atom(prop, pl_prev); /* remove |DOMAIN_CLOSE_ATOM| */
prop = Propositions::delete_atom(prop, pl_prev); /* remove |PREDICATE_ATOM| */
if (Atoms::is_notall_quantifier(q_atom))
prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_CLOSE_ATOM));
prop = Propositions::insert_atom(prop, pl_prev,
Atoms::new(NEGATION_CLOSE_ATOM));
prop = Propositions::insert_atom(prop, pl_prev,
WherePredicates::everywhere_up(bp_atom->terms[j]));
if (Atoms::is_notall_quantifier(q_atom))
prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_OPEN_ATOM));
prop = Propositions::insert_atom(prop, pl_prev,
Atoms::new(NEGATION_OPEN_ATOM));
PROPOSITION_EDITED(pl, prop);
break;
}
@ -1156,6 +1147,14 @@ pcalc_prop *Simplifications::is_all_rooms(pcalc_prop *prop, int *changed) {
return prop;
#endif
}
@h Everywhere and nowhere (fudge).
Similarly, if the proposition expresses the idea of "nowhere" or "everywhere"
by spelling this out in quantifiers about being no place or every place, then
replace those with uses of the special unary predicates for "nowhere" and
"everywhere".
=
pcalc_prop *Simplifications::everywhere_and_nowhere(pcalc_prop *prop, int *changed) {
*changed = FALSE;
#ifdef IF_MODULE
@ -1186,7 +1185,8 @@ pcalc_prop *Simplifications::everywhere_and_nowhere(pcalc_prop *prop, int *chang
prop = Propositions::delete_atom(prop, pl_prev); /* remove |DOMAIN_CLOSE_ATOM| */
prop = Propositions::delete_atom(prop, pl_prev); /* remove |PREDICATE_ATOM| */
if (Atoms::is_notall_quantifier(q_atom))
prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_CLOSE_ATOM));
prop = Propositions::insert_atom(prop, pl_prev,
Atoms::new(NEGATION_CLOSE_ATOM));
pcalc_prop *new_atom;
if (Atoms::is_nonexistence_quantifier(q_atom))
new_atom = WherePredicates::nowhere_up(bp_atom->terms[j]);
@ -1194,7 +1194,8 @@ pcalc_prop *Simplifications::everywhere_and_nowhere(pcalc_prop *prop, int *chang
new_atom = WherePredicates::everywhere_up(bp_atom->terms[j]);
prop = Propositions::insert_atom(prop, pl_prev, new_atom);
if (Atoms::is_notall_quantifier(q_atom))
prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_OPEN_ATOM));
prop = Propositions::insert_atom(prop, pl_prev,
Atoms::new(NEGATION_OPEN_ATOM));
PROPOSITION_EDITED(pl, prop);
break;
}