ifhub/inform7
1
0
Fork 0
mirror of https://github.com/ganelson/inform.git synced 2024-07-08 10:04:21 +03:00
Code Issues Projects Releases Wiki Activity
inform7/docs/core-module/12-ap.html
Graham Nelson 22d2c3d8bd Moved sentence conversion into calculus module
2020-08-25 21:47:14 +01:00

780 lines
125 KiB
HTML
Raw Blame History

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
<head>
<title>Assert Propositions</title>
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
<meta name="viewport" content="width=device-width initial-scale=1">
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta http-equiv="Content-Language" content="en-gb">
<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
<script>
MathJax = {
tex: {
inlineMath: '$', '$'], ['\\(', '\\)'
},
svg: {
fontCache: 'global'
}
};
</script>
<script type="text/javascript" id="MathJax-script" async
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
</script>
<script>
function togglePopup(material_id) {
var popup = document.getElementById(material_id);
popup.classList.toggle("show");
}
</script>
<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
</head>
<body class="commentary-font">
<nav role="navigation">
<h1><a href="../index.html">
<img src="../docs-assets/Inform.png" height=72">
</a></h1>
<ul><li><a href="../compiler.html">compiler tools</a></li>
<li><a href="../other.html">other tools</a></li>
<li><a href="../extensions.html">extensions and kits</a></li>
<li><a href="../units.html">unit test tools</a></li>
</ul><h2>Compiler Webs</h2><ul>
<li><a href="../inbuild/index.html">inbuild</a></li>
<li><a href="../inform7/index.html">inform7</a></li>
<li><a href="../inter/index.html">inter</a></li>
</ul><h2>Inbuild Modules</h2><ul>
<li><a href="../supervisor-module/index.html">supervisor</a></li>
</ul><h2>Inform7 Modules</h2><ul>
<li><a href="index.html"><span class="selectedlink">core</span></a></li>
<li><a href="../if-module/index.html">if</a></li>
<li><a href="../multimedia-module/index.html">multimedia</a></li>
<li><a href="../index-module/index.html">index</a></li>
</ul><h2>Inter Modules</h2><ul>
<li><a href="../bytecode-module/index.html">bytecode</a></li>
<li><a href="../building-module/index.html">building</a></li>
<li><a href="../codegen-module/index.html">codegen</a></li>
</ul><h2>Services</h2><ul>
<li><a href="../arch-module/index.html">arch</a></li>
<li><a href="../calculus-module/index.html">calculus</a></li>
<li><a href="../html-module/index.html">html</a></li>
<li><a href="../inflections-module/index.html">inflections</a></li>
<li><a href="../kinds-module/index.html">kinds</a></li>
<li><a href="../linguistics-module/index.html">linguistics</a></li>
<li><a href="../problems-module/index.html">problems</a></li>
<li><a href="../syntax-module/index.html">syntax</a></li>
<li><a href="../words-module/index.html">words</a></li>
<li><a href="../../../inweb/docs/foundation-module/index.html">foundation</a></li>
</ul>
</nav>
<main role="main">
<!--Weave of 'Assert Propositions' generated by Inweb-->
<div class="breadcrumbs">
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../compiler.html">Inform7 Modules</a></li><li><a href="index.html">core</a></li><li><a href="index.html#12">Chapter 12: Use of Propositions</a></li><li><b>Assert Propositions</b></li></ul></div>
<p class="purpose">To declare that a given proposition is a true statement about the state of the world when play begins.</p>
<ul class="toc"><li><a href="12-ap.html#SP4">&#167;4. Entrance</a></li><li><a href="12-ap.html#SP8">&#167;8. Main procedure</a></li><li><a href="12-ap.html#SP8_5">&#167;8.5. Creations</a></li><li><a href="12-ap.html#SP8_6">&#167;8.6. Asserting predicates</a></li><li><a href="12-ap.html#SP10">&#167;10. Evaluating terms</a></li><li><a href="12-ap.html#SP12">&#167;12. Testing at compile-time</a></li></ul><hr class="tocbar">
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>&#167;1. </b>Inside Inform, the term "the model" means the collection of the following:
</p>
<ul class="items"><li>(1) The inference subjects capable of holding properties, divided into:
<ul class="items"><li>(1a) World objects, such as "Brazilian frog" or "Jungle Clearing"; each
of which belongs to a kind;
</li><li>(1b) Kinds of object, such as "animal" or "room"; each of which
is a kind in turn of another kind, even if only "kind", which is its own kind;
</li><li>(1c) Named constant values, such as "red" or "Entire Game"; each of which
belongs to a kind of value;
</li><li>(1d) Kinds of value whose values are all named, such as "colour" or "scene".
</li></ul>
<li>(2) The associated values, divided into:
<ul class="items"><li>(2a) Properties, such as "open" or "carrying capacity", each of which is
held by some subset of the objects &mdash; for instance, containers and people are
permitted to have the "carrying capacity" property;
</li><li>(2b) Global variables, such as "time of day".
</li></ul>
<li>(3) Relations between the objects (or in some cases between objects and values
outside the model), such as "containment".
</li></ul>
<p class="commentary">Much else lies outside the model: values like <span class="extract"><span class="extract-syntax">152</span></span> or <span class="extract"><span class="extract-syntax">"alfalfa"</span></span>, rules,
rulebooks, phrases, relations which can only be tested (such as "less than"
or "visibility") and so on. Some of this is excluded because it is beyond
the source text's power to decide facts about it (for instance, that 5 is
less than 6); other matter is left out because it only relates to what
happens to the world after its initial creation (for instances, actions
and activities). The model is that which the source text can decide about
the initial state of things.
</p>
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>&#167;2. </b>The initial state of the world is built from the model. Properly speaking
a few other things contribute, too &mdash; such as the entries initially found in
table cells &mdash; but these don't need careful handling, since they are explicitly
declared as literals in the source text: there is no need to analyse their
meaning.
</p>
<p class="commentary">To build or change the model, we assert that propositions about it are true,
using <span class="extract"><span class="extract-syntax">Propositions::Assert::assert_true</span></span> or
<span class="extract"><span class="extract-syntax">Propositions::Assert::assert_true_about</span></span>. This is the only way to
create kinds, instances, global variables, and constant values, and also the
only way to attach properties to objects, to set property values or
the kind of a given object or the value of a global variable, or to declare
that relationships hold.
</p>
<p class="commentary">However, creating new property names and new relations does not count as a
change in the model world. (After all, we could create a new property
called "scent" and a new relation called "admiring", but then choose
not to attach scent to anything or to relate any objects by admiring. The
model world would then not have changed at all.) So creating new properties
and new relations is not done by asserting propositions.
</p>
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>&#167;3. </b><span class="extract"><span class="extract-syntax">Propositions::Assert::assert_true</span></span> asserts propositions in which all variables are
bound (or which have no variables); <span class="extract"><span class="extract-syntax">Propositions::Assert::assert_true_about</span></span> asserts
propositions in which \(x\) is free but all other variables are bound, and
substitutes either an object \(O\) or a value \(V\) into \(x\) before asserting.
These two procedures are the entire API, so to speak, for growing or changing
the model. They are used by the detailed-look part of the A-parser,
which takes assertion sentences in the source text and
converts them into a series of propositions which it would like to make true.
</p>
<p class="commentary">Either way those requests come in, they all end up in the central
<span class="extract"><span class="extract-syntax">Propositions::Assert::prop_true_in_model</span></span> procedure, one of the most important choke points within
Inform. <span class="extract"><span class="extract-syntax">Propositions::Assert::prop_true_in_model</span></span> and its delegates &mdash; routines to assert the
truth of various adjectives or relations &mdash; are allowed to call routines such
as <span class="extract"><span class="extract-syntax">Instances::set_kind</span></span> and <span class="extract"><span class="extract-syntax">Instances::new</span></span> which are forbidden for use in the
rest of Inform. These are guarded with the following macro, to ensure that
we don't accidentally break this rule:
</p>
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">PROTECTED_MODEL_PROCEDURE</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">ptim_recursion_depth</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"protected model-affecting procedure used outside proposition assert"</span><span class="plain-syntax">);</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">ptim_recursion_depth</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">; </span><span class="comment-syntax"> depth of recursion of </span><span class="extract"><span class="extract-syntax">Propositions::Assert::prop_true_in_model</span></span>
</pre>
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>&#167;4. Entrance. </b>This first entrance is a mere alias for the second.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::Assert::assert_true</span><button class="popup" onclick="togglePopup('usagePopup1')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup1">Usage of <span class="code-font"><span class="function-syntax">Propositions::Assert::assert_true</span></span>:<br/>New Property Requests - <a href="4-npr.html#SP5_11">&#167;5.11</a><br/>The Creator - <a href="5-tc.html#SP5_4_1_1">&#167;5.4.1.1</a>, <a href="5-tc.html#SP5_4_2_1">&#167;5.4.2.1</a>, <a href="5-tc.html#SP5_4_2_2">&#167;5.4.2.2</a>, <a href="5-tc.html#SP5_4_2_3">&#167;5.4.2.3</a>, <a href="5-tc.html#SP8_4_1">&#167;8.4.1</a>, <a href="5-tc.html#SP12">&#167;12</a><br/>Property Knowledge - <a href="5-pk.html#SP2">&#167;2</a><br/>Relation Knowledge - <a href="5-rk.html#SP3">&#167;3</a><br/>Condition Properties - <a href="15-cp.html#SP3">&#167;3</a></span></button><span class="plain-syntax">(</span><span class="identifier-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">certitude</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><a href="12-ap.html#SP7" class="function-link"><span class="function-syntax">Propositions::Assert::prop_true_in_world_model_inner</span></a><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">certitude</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::Assert::assert_true_about</span><button class="popup" onclick="togglePopup('usagePopup2')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup2">Usage of <span class="code-font"><span class="function-syntax">Propositions::Assert::assert_true_about</span></span>:<br/>Define by Table Requests - <a href="4-dbtr.html#SP4_2">&#167;4.2</a><br/>New Property Requests - <a href="4-npr.html#SP5_9">&#167;5.9</a>, <a href="4-npr.html#SP5_10">&#167;5.10</a><br/>Assertions - <a href="5-ass.html#SP6_3_39_5">&#167;6.3.39.5</a><br/>New Property Assertions - <a href="5-npa.html#SP1_1">&#167;1.1</a><br/>Property Knowledge - <a href="5-pk.html#SP3">&#167;3</a><br/>Relation Knowledge - <a href="5-rk.html#SP1_2">&#167;1.2</a><br/>Implications - <a href="5-imp.html#SP6_1_3">&#167;6.1.3</a><br/>Tree Conversions - <a href="5-tc2.html#SP2">&#167;2</a><br/>Relations - <a href="7-rlt.html#SP4">&#167;4</a><br/>Either-Or Properties - <a href="15-ep.html#SP9">&#167;9</a><br/>Valued Properties - <a href="15-vp.html#SP10">&#167;10</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">infs</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">certitude</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><a href="12-ap.html#SP7" class="function-link"><span class="function-syntax">Propositions::Assert::prop_true_in_world_model_inner</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">infs</span><span class="plain-syntax">, </span><span class="identifier-syntax">certitude</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>&#167;5. </b>If we are working along a proposition and reach, say, \(door(x)\), we
can only assert that if we know what the value of \(x\) is. We therefore keep
an array (or a pair of arrays) holding our current beliefs about the values
of the variables &mdash; this is called the "identification slate".
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> **</span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">; </span><span class="comment-syntax"> must point to a 26-element array</span>
<span class="identifier-syntax">parse_node</span><span class="plain-syntax"> **</span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">; </span><span class="comment-syntax"> must point to a 26-element array</span>
</pre>
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>&#167;6. </b>Purely to avoid multiply producing a problem message.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">last_couldnt_assert_at</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::Assert::issue_couldnt_problem</span><span class="plain-syntax">(</span><span class="identifier-syntax">adjective</span><span class="plain-syntax"> *</span><span class="identifier-syntax">aph</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">parity</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">last_couldnt_assert_at</span><span class="plain-syntax"> != </span><span class="identifier-syntax">current_sentence</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">W</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Adjectives::get_nominative_singular</span><span class="plain-syntax">(</span><span class="identifier-syntax">aph</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">Problems::quote_source</span><span class="plain-syntax">(1, </span><span class="identifier-syntax">current_sentence</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">Problems::quote_wording</span><span class="plain-syntax">(2, </span><span class="identifier-syntax">W</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">StandardProblems::handmade_problem</span><span class="plain-syntax">(</span><a href="1-wtc.html#SP6" class="function-link"><span class="function-syntax">Task::syntax_tree</span></a><span class="plain-syntax">(), </span><span class="identifier-syntax">_p_</span><span class="plain-syntax">(</span><span class="identifier-syntax">PM_CantAssertAdjective</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">parity</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="identifier-syntax">Problems::issue_problem_segment</span><span class="plain-syntax">(</span>
<span class="plain-syntax"> </span><span class="string-syntax">"In the sentence %1, you ask me to arrange for something not to be "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"'%2' at the start of play. This is only possible when an adjective "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"talks about an either/or property, like 'open'/'closed' - if there "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"are three or more possibilities then it's ambiguous. Even if there "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"are only two possibilities, I can't always fix them just on your "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"request - 'visible'/'invisible', for instance, is something I can "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"test during play at any time, but not something I can arrange at "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"the start."</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">Problems::issue_problem_segment</span><span class="plain-syntax">(</span>
<span class="plain-syntax"> </span><span class="string-syntax">"In the sentence %1, you ask me to arrange for something to be '%2' "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"at the start of play. There are some adjectives ('open' or 'dark', "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"for instance) which I can fix, but others are just too vague. For "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"example, saying 'Peter is visible.' isn't allowed, because it "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"doesn't tell me where Peter is. Like 'visible', being '%2' is "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"something I can test during play at any time, but not something "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"I can arrange at the start."</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">Problems::issue_problem_end</span><span class="plain-syntax">();</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">last_couldnt_assert_at</span><span class="plain-syntax"> = </span><span class="identifier-syntax">current_sentence</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>&#167;7. </b>The second entrance, then, keeps track of the recursion depth but also
ensures that the identification slate is always correct, stacking them
so that an inner <span class="extract"><span class="extract-syntax">Propositions::Assert::prop_true_in_model</span></span> has an independent slate from an outer
one.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::Assert::prop_true_in_world_model_inner</span><button class="popup" onclick="togglePopup('usagePopup3')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup3">Usage of <span class="code-font"><span class="function-syntax">Propositions::Assert::prop_true_in_world_model_inner</span></span>:<br/><a href="12-ap.html#SP4">&#167;4</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">subject</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">certainty</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> **</span><span class="identifier-syntax">saved_interpretation_as_infs</span><span class="plain-syntax"> = </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> **</span><span class="identifier-syntax">saved_interpretation_as_spec</span><span class="plain-syntax"> = </span><span class="identifier-syntax">current_interpretation_as_spec</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">saved_prevailing_mood</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prevailing_mood</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">certainty</span><span class="plain-syntax"> != </span><span class="identifier-syntax">UNKNOWN_CE</span><span class="plain-syntax">) </span><span class="identifier-syntax">prevailing_mood</span><span class="plain-syntax"> = </span><span class="identifier-syntax">certainty</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">ciawo</span><span class="plain-syntax">[26]; </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">ciats</span><span class="plain-syntax">[26];</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP7_1" class="named-paragraph-link"><span class="named-paragraph">Establish a new identification slate for the variables in the proposition</span><span class="named-paragraph-number">7.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">ptim_recursion_depth</span><span class="plain-syntax">++;</span>
<span class="plain-syntax"> </span><a href="12-ap.html#SP8" class="function-link"><span class="function-syntax">Propositions::Assert::prop_true_in_model</span></a><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">ptim_recursion_depth</span><span class="plain-syntax">--;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">prevailing_mood</span><span class="plain-syntax"> = </span><span class="identifier-syntax">saved_prevailing_mood</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax"> = </span><span class="identifier-syntax">saved_interpretation_as_infs</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax"> = </span><span class="identifier-syntax">saved_interpretation_as_spec</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP7_1" class="paragraph-anchor"></a><b>&#167;7.1. </b>The slate is initially blank unless substitutions for variable \(x\) have
been supplied; \(x\) of course is variable number 0.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Establish a new identification slate for the variables in the proposition</span><span class="named-paragraph-number">7.1</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<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">k</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">k</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">k</span><span class="plain-syntax">++) { </span><span class="identifier-syntax">ciawo</span><span class="plain-syntax">[</span><span class="identifier-syntax">k</span><span class="plain-syntax">] = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">; </span><span class="identifier-syntax">ciats</span><span class="plain-syntax">[</span><span class="identifier-syntax">k</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">ciawo</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">subject</span><span class="plain-syntax">; </span><span class="identifier-syntax">ciats</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax"> = </span><span class="identifier-syntax">ciawo</span><span class="plain-syntax">; </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax"> = </span><span class="identifier-syntax">ciats</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP7">&#167;7</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>&#167;8. Main procedure. </b>As can be seen, <span class="extract"><span class="extract-syntax">Propositions::Assert::prop_true_in_model</span></span> is a simple procedure. After a little
fuss to check that everything is set up right, we simply run through the
proposition one atom at a time.
</p>
<p class="commentary">This is a modest scheme. We are unable to assert any proposition other
than \(\exists\), so that we never see their attendant domain brackets.
We are therefore left with a proposition in the form $P_1\land P_2\land ...
\land P_n\( where each \)P_i\( is either a predicate-like atom, an \)\exists v$
term for some variable \(v\), or else \(\lnot(...)\) of a similar conjunction.
</p>
<p class="commentary">This is an ambiguous task if we have to assert \(\lnot(P\land Q)\), which is
in effect a form of disjunction: \(P\land Q\) fails if either is false, so
which do we falsify? We choose both.
</p>
<p class="commentary">That means we can simply assert each atom in turn, with a parity depending on
its nesting in negation brackets, which is nice and easy to write:
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::Assert::prop_true_in_model</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">Propositions::Assert::prop_true_in_model</span></span>:<br/><a href="12-ap.html#SP3">&#167;3</a>, <a href="12-ap.html#SP7">&#167;7</a></span></button><span class="plain-syntax">(</span><span class="identifier-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"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_1" class="named-paragraph-link"><span class="named-paragraph">Record the proposition in the debugging log</span><span class="named-paragraph-number">8.1</span></a></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">Propositions::contains_nonexistence_quantifier</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_2" class="named-paragraph-link"><span class="named-paragraph">Issue a problem message explaining that the proposition isn't exact enough</span><span class="named-paragraph-number">8.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_3" class="named-paragraph-link"><span class="named-paragraph">Typecheck the proposition, in case this has not already been done</span><span class="named-paragraph-number">8.3</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_4" class="named-paragraph-link"><span class="named-paragraph">Check the identification slate against variable usage in the proposition</span><span class="named-paragraph-number">8.4</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</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">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">now_negated</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">TRAVERSE_PROPOSITION</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">switch</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEGATION_OPEN_ATOM:</span><span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEGATION_CLOSE_ATOM:</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">now_negated</span><span class="plain-syntax"> = (</span><span class="identifier-syntax">now_negated</span><span class="plain-syntax">)?</span><span class="identifier-syntax">FALSE:TRUE</span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">QUANTIFIER_ATOM:</span><span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_5" class="named-paragraph-link"><span class="named-paragraph">Assert the truth or falsity of a QUANTIFIER atom</span><span class="named-paragraph-number">8.5</span></a></span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">PREDICATE_ATOM:</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">arity</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span><span class="plain-syntax">: </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_6" class="named-paragraph-link"><span class="named-paragraph">Assert the truth or falsity of a unary predicate</span><span class="named-paragraph-number">8.6</span></a></span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="constant-syntax">2</span><span class="plain-syntax">: </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_7" class="named-paragraph-link"><span class="named-paragraph">Assert the truth or falsity of a binary predicate</span><span class="named-paragraph-number">8.7</span></a></span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</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>
<span class="plain-syntax"> }</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP8_1" class="paragraph-anchor"></a><b>&#167;8.1. </b>The certainty, the initial interpretation slate, and the proposition are
combined into a single line in the log:
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Record the proposition in the debugging log</span><span class="named-paragraph-number">8.1</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">"::"</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">switch</span><span class="plain-syntax">(</span><span class="identifier-syntax">prevailing_mood</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">IMPOSSIBLE_CE:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" (impossible)"</span><span class="plain-syntax">); </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">UNLIKELY_CE:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" (unlikely)"</span><span class="plain-syntax">); </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">UNKNOWN_CE:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" (no certainty)"</span><span class="plain-syntax">); </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">LIKELY_CE:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" (likely)"</span><span class="plain-syntax">); </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">INITIALLY_CE:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" (initially)"</span><span class="plain-syntax">); </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">CERTAIN_CE:</span><span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">default:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">" (unknown certainty)"</span><span class="plain-syntax">); </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</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;26; </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">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</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">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" %c = $j"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</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">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" %c = $P"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> }</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">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">" $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_2" class="paragraph-anchor"></a><b>&#167;8.2. </b>It's surprisingly hard to get this problem message, because the assertion-maker
rejects most of the obvious ways to try it with more direct problems. It took
me about twenty sentences to get there ("The car is a vehicle in most rooms
which are dark" will do it).
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Issue a problem message explaining that the proposition isn't exact enough</span><span class="named-paragraph-number">8.2</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">StandardProblems::sentence_problem</span><span class="plain-syntax">(</span><a href="1-wtc.html#SP6" class="function-link"><span class="function-syntax">Task::syntax_tree</span></a><span class="plain-syntax">(), </span><span class="identifier-syntax">_p_</span><span class="plain-syntax">(</span><span class="identifier-syntax">PM_CantAssertQuantifier</span><span class="plain-syntax">),</span>
<span class="plain-syntax"> </span><span class="string-syntax">"the relationship you describe is not exact enough"</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="string-syntax">"so that I cannot be sure of the initial situation. A specific "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"relationship would be something like 'the box is a container in "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"the Attic', rather than 'the box is a container in a room which "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"is dark' (fine, but which dark room? You must say)."</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_3" class="paragraph-anchor"></a><b>&#167;8.3. </b>Almost all propositions derive from sentences in the source text, but a
crucial exception is the first one to be asserted: \(\exists x: isakind(x)\),
which creates the kind "kind". Type-checking problems never arise with this
in any case, so it doesn't matter that we wouldn't know what text to use in them.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Typecheck the proposition, in case this has not already been done</span><span class="named-paragraph-number">8.3</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">W</span><span class="plain-syntax"> = </span><span class="identifier-syntax">EMPTY_WORDING</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">current_sentence</span><span class="plain-syntax">) </span><span class="identifier-syntax">W</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Node::get_text</span><span class="plain-syntax">(</span><span class="identifier-syntax">current_sentence</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">Propositions::Checker::type_check</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">Propositions::Checker::tc_problem_reporting</span><span class="plain-syntax">(</span><span class="identifier-syntax">W</span><span class="plain-syntax">, </span><span class="string-syntax">"be asserting something"</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> != </span><span class="identifier-syntax">ALWAYS_MATCH</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_4" class="paragraph-anchor"></a><b>&#167;8.4. </b>This does nothing functional, except that it allows an interpretation as an
instance to trump one as a specification; useful since the A-parser
often specifies \(O\) and \(V\) as the object and value referred to by a given
node in the parse tree, and since an object is also a value, this often means
that both are given. If we have \(O\), then, we cancel \(V\).
</p>
<p class="commentary">As we shall see, it's permitted to interpret a bound variable after its
quantifier, but not before, and in particular not at the start of the
proposition. So we require that the slate identify exactly the free
variables, and no others.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Check the identification slate against variable usage in the proposition</span><span class="named-paragraph-number">8.4</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[26];</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">valid</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Binding::determine_status</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_states</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">valid</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to assert malformed proposition"</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;26; </span><span class="identifier-syntax">i</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">set</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">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]) </span><span class="identifier-syntax">set</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">current_interpretation_as_infs</span><span class="plain-syntax">[</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">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]) </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</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">set</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">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] == </span><span class="identifier-syntax">UNUSED_VST</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">set</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to set an unused variable"</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">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] == </span><span class="identifier-syntax">BOUND_VST</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">set</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to set a bound variable"</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">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] == </span><span class="identifier-syntax">FREE_VST</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">set</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">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"failed to set a free variable"</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_5" class="paragraph-anchor"></a><b>&#167;8.5. Creations. </b>To assert the truth of \(\exists x\), we must create an object to become \(x\);
that will provide a value in subsequent uses of \(x\) in the same proposition,
so the new value has to be added to the identification slate.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Assert the truth or falsity of a QUANTIFIER atom</span><span class="named-paragraph-number">8.5</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</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">[0].</span><span class="identifier-syntax">variable</span><span class="plain-syntax">; </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> == -1) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"bad QUANTIFIER 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">now_negated</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to negate existence"</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">NW</span><span class="plain-syntax"> = </span><span class="identifier-syntax">EMPTY_WORDING</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">is_a_var</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">is_a_const</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">, </span><span class="identifier-syntax">is_a_kind</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="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_5_1" class="named-paragraph-link"><span class="named-paragraph">Scan subsequent atoms to find the name, nature and kind of what is to be created</span><span class="named-paragraph-number">8.5.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_5_2" class="named-paragraph-link"><span class="named-paragraph">Create the object and add to the identification slate</span><span class="named-paragraph-number">8.5.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_5_3" class="named-paragraph-link"><span class="named-paragraph">Record the new creation in the debugging log</span><span class="named-paragraph-number">8.5.3</span></a></span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_5_1" class="paragraph-anchor"></a><b>&#167;8.5.1. </b>Note that all four of these atoms are optional; the proposition might consist
of just \(\exists x\) alone, which creates a nameless object, since as usual we
interpret no indication of a kind as meaning "object".
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Scan subsequent atoms to find the name, nature and kind of what is to be created</span><span class="named-paragraph-number">8.5.1</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">lookahead</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">lookahead</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">lookahead</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">lookahead</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="identifier-syntax">variable</span><span class="plain-syntax"> == </span><span class="identifier-syntax">v</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax"> (</span><span class="identifier-syntax">lookahead</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">PREDICATE_ATOM</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-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">lookahead</span><span class="plain-syntax">-&gt;</span><span class="identifier-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="identifier-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">calling_up_family</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">NW</span><span class="plain-syntax"> = </span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">calling_name</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">up</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">assert_kind</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">up</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">is_a_kind_up_family</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">is_a_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">assert_kind</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">up</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">is_a_var_up_family</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">is_a_var</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">up</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">is_a_const_up_family</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">is_a_const</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>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8_5">&#167;8.5</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_5_2" class="paragraph-anchor"></a><b>&#167;8.5.2. </b>There are really three cases: new kind, new global variable, new instance.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Create the object and add to the identification slate</span><span class="named-paragraph-number">8.5.2</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">is_a_kind</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Kinds::new_base</span><span class="plain-syntax">(</span><span class="identifier-syntax">NW</span><span class="plain-syntax">, </span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><a href="13-kak.html#SP1" class="function-link"><span class="function-syntax">Kinds::Knowledge::as_subject</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><a href="14-sp.html#SP1" class="function-link"><span class="function-syntax">Specifications::from_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">is_a_var</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">is_a_const</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">K</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K_object</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">nonlocal_variable</span><span class="plain-syntax"> *</span><span class="identifier-syntax">q</span><span class="plain-syntax"> = </span><a href="6-nv.html#SP5" class="function-link"><span class="function-syntax">NonlocalVariables::new_global</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">NW</span><span class="plain-syntax">, </span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</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">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><a href="14-lv.html#SP2" class="function-link"><span class="function-syntax">Lvalues::new_actual_NONLOCAL_VARIABLE</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q</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">is_a_const</span><span class="plain-syntax">) </span><a href="6-nv.html#SP21" class="function-link"><span class="function-syntax">NonlocalVariables::make_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">q</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">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">instance</span><span class="plain-syntax"> *</span><span class="identifier-syntax">nc</span><span class="plain-syntax"> = </span><a href="6-ins.html#SP5" class="function-link"><span class="function-syntax">Instances::new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">NW</span><span class="plain-syntax">, </span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><a href="6-ins.html#SP12" class="function-link"><span class="function-syntax">Instances::as_subject</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">nc</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">K</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">Kinds::Behaviour::is_object</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">)))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><a href="14-rv.html#SP4" class="function-link"><span class="function-syntax">Rvalues::from_instance</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">nc</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">else</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><a href="14-rv.html#SP4" class="function-link"><span class="function-syntax">Rvalues::from_instance</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">nc</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8_5">&#167;8.5</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_5_3" class="paragraph-anchor"></a><b>&#167;8.5.3. </b>It's useful to log the new creation, especially for objects which have
duplicate names to others already made:
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Record the new creation in the debugging log</span><span class="named-paragraph-number">8.5.3</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</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">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">":: %c &lt;-- $P\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">], </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</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">ASSERTIONS</span><span class="plain-syntax">, </span><span class="string-syntax">":: %c &lt;-- $j\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">], </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">]);</span>
<span class="plain-syntax"> }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8_5">&#167;8.5</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_6" class="paragraph-anchor"></a><b>&#167;8.6. Asserting predicates. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Assert the truth or falsity of a unary predicate</span><span class="named-paragraph-number">8.6</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-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">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">UnaryPredicateFamilies::assert</span><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">now_negated</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_7" class="paragraph-anchor"></a><b>&#167;8.7. </b>Binary predicates, unlike unary ones, can only be asserted positively. This
is because \(\lnot P(x)\) tells you something fairly definite, whereas \(\lnot Q(x, y)\)
gives no information about what \(z\) might exist, if any, such that \(Q(x, z)\).
For instance, knowing that X is not part of Y gives us no help in determining
where X is.
</p>
<p class="commentary">Another difference is that \(R(x, y)\) can give you definite information about
the kinds of \(x\) and \(y\), where they are objects, because binary predicates
have single definitions. (Knowing \(locked(x)\), by contrast, doesn't
tell you whether \(x\) is a door or a container &mdash; adjectives can have multiple
domains in which they have differing definitions.) In the case of a
proposition produced by sentence conversion, that information is redundant
since appropriate kind atoms were added to the proposition anyway. But we
also assert propositions generated from tree conversion, which don't have
these kind atoms.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Assert the truth or falsity of a binary predicate</span><span class="named-paragraph-number">8.7</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">now_negated</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">StandardProblems::sentence_problem</span><span class="plain-syntax">(</span><a href="1-wtc.html#SP6" class="function-link"><span class="function-syntax">Task::syntax_tree</span></a><span class="plain-syntax">(), </span><span class="identifier-syntax">_p_</span><span class="plain-syntax">(</span><span class="identifier-syntax">PM_CantAssertNegatedRelations</span><span class="plain-syntax">),</span>
<span class="plain-syntax"> </span><span class="string-syntax">"that seems to make a negative statement about a relationship"</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="string-syntax">"which is too vague. You must make positive assertions."</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt0</span><span class="plain-syntax">, </span><span class="identifier-syntax">pt1</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_7_2" class="named-paragraph-link"><span class="named-paragraph">Determine the BP and terms to be asserted</span><span class="named-paragraph-number">8.7.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec0</span><span class="plain-syntax"> = </span><a href="12-ap.html#SP10" class="function-link"><span class="function-syntax">Propositions::Assert::spec_of_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt0</span><span class="plain-syntax">), *</span><span class="identifier-syntax">spec1</span><span class="plain-syntax"> = </span><a href="12-ap.html#SP10" class="function-link"><span class="function-syntax">Propositions::Assert::spec_of_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt1</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">subj0</span><span class="plain-syntax"> = </span><a href="12-ap.html#SP11" class="function-link"><span class="function-syntax">Propositions::Assert::subject_of_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt0</span><span class="plain-syntax">), *</span><span class="identifier-syntax">subj1</span><span class="plain-syntax"> = </span><a href="12-ap.html#SP11" class="function-link"><span class="function-syntax">Propositions::Assert::subject_of_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt1</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">subj0</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">spec0</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) </span><span class="identifier-syntax">spec0</span><span class="plain-syntax"> = </span><a href="16-is.html#SP17" class="function-link"><span class="function-syntax">InferenceSubjects::as_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">subj0</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">subj1</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">spec1</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) </span><span class="identifier-syntax">spec1</span><span class="plain-syntax"> = </span><a href="16-is.html#SP17" class="function-link"><span class="function-syntax">InferenceSubjects::as_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">subj1</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>
<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"> != </span><span class="identifier-syntax">R_regional_containment</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K0</span><span class="plain-syntax"> = </span><span class="identifier-syntax">BinaryPredicates::term_kind</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="constant-syntax">0</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">K1</span><span class="plain-syntax"> = </span><span class="identifier-syntax">BinaryPredicates::term_kind</span><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="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::is_subkind_of_object</span><span class="plain-syntax">(</span><span class="identifier-syntax">K0</span><span class="plain-syntax">)) </span><a href="12-ap.html#SP9" class="function-link"><span class="function-syntax">Propositions::Assert::cautiously_set_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">subj0</span><span class="plain-syntax">, </span><span class="identifier-syntax">K0</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_subkind_of_object</span><span class="plain-syntax">(</span><span class="identifier-syntax">K1</span><span class="plain-syntax">)) </span><a href="12-ap.html#SP9" class="function-link"><span class="function-syntax">Propositions::Assert::cautiously_set_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">subj1</span><span class="plain-syntax">, </span><span class="identifier-syntax">K1</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>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">BinaryPredicateFamilies::assert</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">subj0</span><span class="plain-syntax">, </span><span class="identifier-syntax">spec0</span><span class="plain-syntax">, </span><span class="identifier-syntax">subj1</span><span class="plain-syntax">, </span><span class="identifier-syntax">spec1</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)</span>
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP8_7_1" class="named-paragraph-link"><span class="named-paragraph">Issue a problem message for failure to assert</span><span class="named-paragraph-number">8.7.1</span></a></span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8">&#167;8</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_7_1" class="paragraph-anchor"></a><b>&#167;8.7.1. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Issue a problem message for failure to assert</span><span class="named-paragraph-number">8.7.1</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"$2 on ($j, $P; $j, $P)\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">subj0</span><span class="plain-syntax">, </span><span class="identifier-syntax">spec0</span><span class="plain-syntax">, </span><span class="identifier-syntax">subj1</span><span class="plain-syntax">, </span><span class="identifier-syntax">spec1</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="14-rv.html#SP7" class="function-link"><span class="function-syntax">Rvalues::is_nothing_object_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec0</span><span class="plain-syntax">)) ||</span>
<span class="plain-syntax"> (</span><a href="14-rv.html#SP7" class="function-link"><span class="function-syntax">Rvalues::is_nothing_object_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec1</span><span class="plain-syntax">)))</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">StandardProblems::sentence_problem</span><span class="plain-syntax">(</span><a href="1-wtc.html#SP6" class="function-link"><span class="function-syntax">Task::syntax_tree</span></a><span class="plain-syntax">(), </span><span class="identifier-syntax">_p_</span><span class="plain-syntax">(</span><span class="identifier-syntax">PM_RelationFailedOnNothing</span><span class="plain-syntax">),</span>
<span class="plain-syntax"> </span><span class="string-syntax">"that is an assertion which involves 'nothing'"</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="string-syntax">"which looks as if it might be trying to give me negative rather "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"than positive information. There's no need to tell me something "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"like 'Nothing is in the box.': just don't put anything in the box, "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"and then nothing will be in it."</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">else</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">StandardProblems::sentence_problem</span><span class="plain-syntax">(</span><a href="1-wtc.html#SP6" class="function-link"><span class="function-syntax">Task::syntax_tree</span></a><span class="plain-syntax">(), </span><span class="identifier-syntax">_p_</span><span class="plain-syntax">(</span><span class="identifier-syntax">BelievedImpossible</span><span class="plain-syntax">),</span>
<span class="plain-syntax"> </span><span class="string-syntax">"that is an assertion I can't puzzle out"</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="string-syntax">"which seems to involve placing two things in some sort of "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"relationship, but if so then I can't make it work. Perhaps the "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"sentence is too complicatedly phrased, and could be broken up "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"into two or more sentences?"</span><span class="plain-syntax">);</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8_7">&#167;8.7</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP8_7_2" class="paragraph-anchor"></a><b>&#167;8.7.2. </b>The "is" predicate is not usually assertable, but \(is(x, f_R(y))\)
can be asserted since it is equivalent to \(R(x, y)\) &mdash; this is where we
unravel that. We reject compound uses of functions in this way, but in
practice they hardly ever arise, and could only do so with quite complex
sentences where it seems reasonable to tell the user to write something
simpler and clearer.
</p>
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Determine the BP and terms to be asserted</span><span class="named-paragraph-number">8.7.2</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pt0</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">[0]; </span><span class="identifier-syntax">pt1</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="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">R_equality</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_func</span><span class="plain-syntax"> *</span><span class="identifier-syntax">the_fn</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pt0</span><span class="plain-syntax">.</span><span class="identifier-syntax">function</span><span class="plain-syntax">; </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">side</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">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">the_fn</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) { </span><span class="identifier-syntax">the_fn</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pt1</span><span class="plain-syntax">.</span><span class="identifier-syntax">function</span><span class="plain-syntax">; </span><span class="identifier-syntax">side</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</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">the_fn</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">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">side</span><span class="plain-syntax">].</span><span class="identifier-syntax">function</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">the_fn</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">fn_of</span><span class="plain-syntax">.</span><span class="identifier-syntax">function</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">StandardProblems::sentence_problem</span><span class="plain-syntax">(</span><a href="1-wtc.html#SP6" class="function-link"><span class="function-syntax">Task::syntax_tree</span></a><span class="plain-syntax">(), </span><span class="identifier-syntax">_p_</span><span class="plain-syntax">(</span><span class="identifier-syntax">BelievedImpossible</span><span class="plain-syntax">),</span>
<span class="plain-syntax"> </span><span class="string-syntax">"that is too complicated an assertion"</span><span class="plain-syntax">,</span>
<span class="plain-syntax"> </span><span class="string-syntax">"and cannot be declared as part of the initial situation. (It "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"does make sense, and could be tested with 'if' - it's just "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"too difficult to get right as an instruction about the starting "</span>
<span class="plain-syntax"> </span><span class="string-syntax">"situation."</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">the_fn</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">bp</span><span class="plain-syntax">; </span><span class="identifier-syntax">pt0</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">side</span><span class="plain-syntax">]; </span><span class="identifier-syntax">pt1</span><span class="plain-syntax"> = </span><span class="identifier-syntax">the_fn</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">fn_of</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> }</span>
<span class="plain-syntax"> }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP8_7">&#167;8.7</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>&#167;9. </b>As we've already seen, we have to be cautious about the mechanism to draw
inferences about kinds based on the relationships which objects have. Some
cases are easy: if A is worn by B, then B is a person. But "in" can be
very problematic. When one region is in another, we want to suppress any
inferences which might wrongly be drawn about "in": this is a different
kind of containment from the three-dimensional spatial one suggested by
containers and rooms. It also complicates things that a backdrop can be
"in" a region. So we play very safe and make no guesses about regions or
the first term of <span class="extract"><span class="extract-syntax">R_regional_containment</span></span>.
</p>
<p class="commentary">We also never deduce "thing" as the kind by this mechanism. This is
because instances of "object" with no apparent declared kind are made into
things by default when we complete the model world anyway; so there is no
need to risk setting the kind here at this stage.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::Assert::cautiously_set_kind</span><button class="popup" onclick="togglePopup('usagePopup5')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup5">Usage of <span class="code-font"><span class="function-syntax">Propositions::Assert::cautiously_set_kind</span></span>:<br/><a href="12-ap.html#SP8_7">&#167;8.7</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">inst</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">k</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">inst</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">k</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</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>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><span class="identifier-syntax">k</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_thing</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">instance</span><span class="plain-syntax"> *</span><span class="identifier-syntax">instance_wo</span><span class="plain-syntax"> = </span><a href="16-is.html#SP18" class="function-link"><span class="function-syntax">InferenceSubjects::as_object_instance</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">inst</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">instance_wo</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><a href="6-ins.html#SP18" class="function-link"><span class="function-syntax">Instances::set_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">instance_wo</span><span class="plain-syntax">, </span><span class="identifier-syntax">k</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>&#167;10. Evaluating terms. </b>In asserting a proposition, we are in effect acting as an interpreter rather
than a compiler. Given any term, we need to produce either an object \(O\) or a
more general value \(V\). Recall that a term can be
</p>
<ul class="items"><li>(a) a constant \(C\),
</li><li>(b) a variable \(v\), or
</li><li>(c) a function \(f_R(t)\) for another term \(t\).
</li></ul>
<p class="commentary">We are unable, at compile-time, to evaluate \(f_R(t)\) for any relation \(R\),
and won't even try. We can evaluate a variable using the interpretation
slate &mdash; that was its whole purpose. So the only case left is a constant:
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::Assert::spec_of_term</span><button class="popup" onclick="togglePopup('usagePopup6')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup6">Usage of <span class="code-font"><span class="function-syntax">Propositions::Assert::spec_of_term</span></span>:<br/><a href="12-ap.html#SP8_7">&#167;8.7</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</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">pt</span><span class="plain-syntax">.</span><span class="identifier-syntax">function</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</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">pt</span><span class="plain-syntax">.</span><span class="identifier-syntax">variable</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_spec</span><span class="plain-syntax">[</span><span class="identifier-syntax">pt</span><span class="plain-syntax">.</span><span class="identifier-syntax">variable</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">pt</span><span class="plain-syntax">.</span><span class="identifier-syntax">constant</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>&#167;11. </b>The analogous routine to extract an instance, which normally takes
precedence, is more convoluted. First, we could be looking at the name of a
kind &mdash; in "A door is usually closed", "door" will appear here as a
description node, and we need to extract the instance of the kind as our
return value. Second, we want to divert all assertions about "the player" so
that they refer to the player object, not to the global variable "the player".
</p>
<p class="commentary">Users tend to expect that they can talk about properties of things as
values, when setting up the world, and since a property value might be
an object, we are going to be careful to reject a <span class="extract"><span class="extract-syntax">PROPERTY_VALUE_NT</span></span>
type with a problem message. In practice the A-parser gets there first,
but just in case.
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::Assert::subject_of_term</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::Assert::subject_of_term</span></span>:<br/><a href="12-ap.html#SP8_7">&#167;8.7</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</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">pt</span><span class="plain-syntax">.</span><span class="identifier-syntax">function</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</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">pt</span><span class="plain-syntax">.</span><span class="identifier-syntax">variable</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">current_interpretation_as_infs</span><span class="plain-syntax">[</span><span class="identifier-syntax">pt</span><span class="plain-syntax">.</span><span class="identifier-syntax">variable</span><span class="plain-syntax">];</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pt</span><span class="plain-syntax">.</span><span class="identifier-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">Node::is</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="constant-syntax">CONSTANT_NT</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="16-is.html#SP16" class="function-link"><span class="function-syntax">InferenceSubjects::from_specification</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">);</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="14-sp.html#SP3" class="function-link"><span class="function-syntax">Specifications::is_description</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="14-ds.html#SP5" class="function-link"><span class="function-syntax">Descriptions::to_instance</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="6-ins.html#SP12" class="function-link"><span class="function-syntax">Instances::as_subject</span></a><span class="plain-syntax">(</span><a href="14-ds.html#SP5" class="function-link"><span class="function-syntax">Descriptions::to_instance</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">));</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="14-sp.html#SP1" class="function-link"><span class="function-syntax">Specifications::to_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">))</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="13-kak.html#SP1" class="function-link"><span class="function-syntax">Kinds::Knowledge::as_subject</span></a><span class="plain-syntax">(</span><a href="14-sp.html#SP1" class="function-link"><span class="function-syntax">Specifications::to_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</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">Node::is</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="constant-syntax">NONLOCAL_VARIABLE_NT</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">diversion</span><span class="plain-syntax"> =</span>
<span class="plain-syntax"> </span><a href="6-nv.html#SP23" class="function-link"><span class="function-syntax">NonlocalVariables::get_alias</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Node::get_constant_nonlocal_variable</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</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">diversion</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">diversion</span><span class="plain-syntax">;</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">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>&#167;12. Testing at compile-time. </b>We can, to a more limited extent, also test whether a given proposition is true
of a given inference subject at the current stage of the world model. (This is
necessary for the implications code to work.)
</p>
<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::Assert::testable_at_compile_time</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::Assert::testable_at_compile_time</span></span>:<br/><a href="12-ap.html#SP13">&#167;13</a><br/>Implications - <a href="5-imp.html#SP3_2_2">&#167;3.2.2</a></span></button><span class="plain-syntax">(</span><span class="identifier-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="identifier-syntax">TRAVERSE_VARIABLE</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">TRAVERSE_PROPOSITION</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">switch</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">PREDICATE_ATOM:</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">arity</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span><span class="plain-syntax">: </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP12_1" class="named-paragraph-link"><span class="named-paragraph">See if this unary predicate can be tested</span><span class="named-paragraph-number">12.1</span></a></span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="constant-syntax">2</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="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">default:</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="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>
</pre>
<p class="commentary firstcommentary"><a id="SP12_1" class="paragraph-anchor"></a><b>&#167;12.1. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">See if this unary predicate can be tested</span><span class="named-paragraph-number">12.1</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-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">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-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">UnaryPredicateFamilies::testable</span><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</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>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP12">&#167;12</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>&#167;13. </b>And the actual test:
</p>
<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::Assert::test_at_compile_time</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::Assert::test_at_compile_time</span></span>:<br/>Implications - <a href="5-imp.html#SP6_1">&#167;6.1</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">about</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="12-ap.html#SP12" class="function-link"><span class="function-syntax">Propositions::Assert::testable_at_compile_time</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NOT_APPLICABLE</span><span class="plain-syntax">;</span>
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</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">TRAVERSE_PROPOSITION</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">switch</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">PREDICATE_ATOM:</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-syntax">arity</span><span class="plain-syntax">) {</span>
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span><span class="plain-syntax">: </span><span class="named-paragraph-container code-font"><a href="12-ap.html#SP13_1" class="named-paragraph-link"><span class="named-paragraph">Test if this unary predicate is true</span><span class="named-paragraph-number">13.1</span></a></span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</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>
<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>
</pre>
<p class="commentary firstcommentary"><a id="SP13_1" class="paragraph-anchor"></a><b>&#167;13.1. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Test if this unary predicate is true</span><span class="named-paragraph-number">13.1</span></span><span class="comment-syntax"> =</span>
</p>
<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax"> </span><span class="identifier-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">pl</span><span class="plain-syntax">-&gt;</span><span class="identifier-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">UnaryPredicateFamilies::test</span><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">about</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</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>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="12-ap.html#SP13">&#167;13</a>.</li></ul>
<nav role="progress"><div class="progresscontainer">
<ul class="progressbar"><li class="progressprev"><a href="12-qr.html">&#10094;</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bv.html">3</a></li><li class="progresschapter"><a href="4-dlr.html">4</a></li><li class="progresschapter"><a href="5-rpt.html">5</a></li><li class="progresschapter"><a href="6-lp.html">6</a></li><li class="progresschapter"><a href="7-am.html">7</a></li><li class="progresschapter"><a href="8-ptu.html">8</a></li><li class="progresschapter"><a href="9-ef.html">9</a></li><li class="progresschapter"><a href="10-its.html">10</a></li><li class="progresschapter"></li><li class="progresscurrentchapter">12</li><li class="progresssection"><a href="12-terr.html">terr</a></li><li class="progresssection"><a href="12-qr.html">qr</a></li><li class="progresscurrent">ap</li><li class="progresssection"><a href="12-ca.html">ca</a></li><li class="progresssection"><a href="12-dtd.html">dtd</a></li><li class="progresssection"><a href="12-cad.html">cad</a></li><li class="progresssection"><a href="12-cdp.html">cdp</a></li><li class="progresschapter"><a href="13-kak.html">13</a></li><li class="progresschapter"><a href="14-sp.html">14</a></li><li class="progresschapter"><a href="15-pr.html">15</a></li><li class="progresschapter"><a href="16-is.html">16</a></li><li class="progresschapter"><a href="17-tl.html">17</a></li><li class="progresschapter"><a href="18-lc.html">18</a></li><li class="progresschapter"><a href="19-tc.html">19</a></li><li class="progresschapter"><a href="20-eq.html">20</a></li><li class="progresschapter"><a href="21-rl.html">21</a></li><li class="progresschapter"><a href="22-itp.html">22</a></li><li class="progresschapter"><a href="23-ad.html">23</a></li><li class="progresschapter"><a href="24-lv.html">24</a></li><li class="progresschapter"><a href="25-in.html">25</a></li><li class="progresschapter"><a href="26-fc.html">26</a></li><li class="progresschapter"><a href="27-hr.html">27</a></li><li class="progressnext"><a href="12-ca.html">&#10095;</a></li></ul></div>
</nav><!--End of weave-->
</main>
</body>
</html>
Reference in a new issue View git blame Copy permalink