mirror of
https://github.com/ganelson/inform.git
synced 2024-07-08 01:54:21 +03:00
723 lines
116 KiB
HTML
723 lines
116 KiB
HTML
<!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="../index.html">home</a></li>
|
|
</ul><h2>Compiler</h2><ul>
|
|
<li><a href="../structure.html">structure</a></li>
|
|
<li><a href="../inbuildn.html">inbuild</a></li>
|
|
<li><a href="../inform7n.html">inform7</a></li>
|
|
<li><a href="../intern.html">inter</a></li>
|
|
<li><a href="../services.html">services</a></li>
|
|
<li><a href="../secrets.html">secrets</a></li>
|
|
</ul><h2>Other Tools</h2><ul>
|
|
<li><a href="../inblorbn.html">inblorb</a></li>
|
|
<li><a href="../indocn.html">indoc</a></li>
|
|
<li><a href="../inform6.html">inform6</a></li>
|
|
<li><a href="../inpolicyn.html">inpolicy</a></li>
|
|
<li><a href="../inrtpsn.html">inrtps</a></li>
|
|
</ul><h2>Resources</h2><ul>
|
|
<li><a href="../extensions.html">extensions</a></li>
|
|
<li><a href="../kits.html">kits</a></li>
|
|
</ul><h2>Repository</h2><ul>
|
|
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=18> github</a></li>
|
|
</ul><h2>Related Projects</h2><ul>
|
|
<li><a href="../../../inweb/index.html">inweb</a></li>
|
|
<li><a href="../../../intest/index.html">intest</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="../inform7n.html">Inform7</a></li><li><a href="index.html">knowledge</a></li><li><a href="index.html#1">Chapter 1: Configuration and Control</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="1-ap.html#SP1">§1. Defensive moat</a></li><li><a href="1-ap.html#SP2">§2. Entrance</a></li><li><a href="1-ap.html#SP6_5">§6.5. Creations</a></li><li><a href="1-ap.html#SP6_6">§6.6. Asserting predicates</a></li><li><a href="1-ap.html#SP8">§8. Evaluating terms</a></li><li><a href="1-ap.html#SP10">§10. Testing at compile-time</a></li><li><a href="1-ap.html#SP12">§12. A catch-all problem</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>§1. Defensive moat. </b>To enforce the doctrine that calls to <a href="1-ap.html#SP2" class="internal">Assert::true</a> or <a href="1-ap.html#SP2" class="internal">Assert::true_about</a>
|
|
are the only way to change the model, we define a macro <span class="extract"><span class="extract-syntax">PROTECTED_MODEL_PROCEDURE</span></span>
|
|
which can be used to guard a function so that it can only be called as a
|
|
consequence of these. For example, <a href="2-ins.html#SP4" class="internal">Instances::new</a> is defended this way.
|
|
</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">assert_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">assert_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">Assert::inner_slated</span></span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>§2. Entrance. </b><a href="1-ap.html#SP2" class="internal">Assert::true</a> takes a proposition with no free variables and converts it
|
|
into inferences at a given certainty level; <a href="1-ap.html#SP2" class="internal">Assert::true_about</a> the same,
|
|
but where the proposition \(\phi(x)\) has one free variable, and an inference
|
|
subject is supplied to stand as \(x\), the thing the proposition is discussing.
|
|
</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">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">Assert::true</span></span>:<br/>Conditions of Subjects - <a href="4-cos.html#SP3_4">§3.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">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="1-ap.html#SP5" class="function-link"><span class="function-syntax">Assert::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">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">Assert::true_about</span></span>:<br/>Either-Or Properties - <a href="3-ep.html#SP8">§8</a><br/>Valued Properties - <a href="3-vp.html#SP9">§9</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="1-ap.html#SP5" class="function-link"><span class="function-syntax">Assert::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="SP3" class="paragraph-anchor"></a><b>§3. </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 record this with
|
|
two 26-element arrays, for the up to 26 predicate calculus variables; there
|
|
are two arrays because the value can be given either as a specification or
|
|
as an inference subject.
|
|
</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="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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>§4. </b>When a proposition is being asserted, there is a prevailing mood of certainty
|
|
or uncertainty about the information implied by it, and this is stored in the
|
|
following global variable:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">prevailing_mood</span><span class="plain-syntax"> = </span><span class="identifier-syntax">UNKNOWN_CE</span><span class="plain-syntax">;</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>§5. </b>The true 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">Assert::inner_slated</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">Assert::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">Assert::inner</span></span>:<br/><a href="1-ap.html#SP2">§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="reserved-syntax">inference_subject</span><span class="plain-syntax"> *</span><span class="identifier-syntax">subject</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="1-ap.html#SP5_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">5.1</span></a></span><span class="plain-syntax">;</span>
|
|
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">assert_recursion_depth</span><span class="plain-syntax">++;</span>
|
|
|
|
<span class="plain-syntax"> </span><a href="1-ap.html#SP6" class="function-link"><span class="function-syntax">Assert::inner_slated</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">assert_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="SP5_1" class="paragraph-anchor"></a><b>§5.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">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="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"><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="1-ap.html#SP5">§5</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>§6. </b>Enough preparation. The actual process is simple: 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">Assert::inner_slated</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">Assert::inner_slated</span></span>:<br/><a href="1-ap.html#SP1">§1</a>, <a href="1-ap.html#SP5">§5</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="1-ap.html#SP6_1" class="named-paragraph-link"><span class="named-paragraph">Record the proposition in the debugging log</span><span class="named-paragraph-number">6.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="1-ap.html#SP6_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">6.2</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="1-ap.html#SP6_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">6.3</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="1-ap.html#SP6_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">6.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">-></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="1-ap.html#SP6_5" class="named-paragraph-link"><span class="named-paragraph">Assert the truth or falsity of a QUANTIFIER atom</span><span class="named-paragraph-number">6.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">-></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="1-ap.html#SP6_6" class="named-paragraph-link"><span class="named-paragraph">Assert the truth or falsity of a unary predicate</span><span class="named-paragraph-number">6.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="1-ap.html#SP6_7" class="named-paragraph-link"><span class="named-paragraph">Assert the truth or falsity of a binary predicate</span><span class="named-paragraph-number">6.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="SP6_1" class="paragraph-anchor"></a><b>§6.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">6.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"><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="1-ap.html#SP6">§6</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_2" class="paragraph-anchor"></a><b>§6.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">6.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><span class="identifier-syntax">Task::syntax_tree</span><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="1-ap.html#SP6">§6</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_3" class="paragraph-anchor"></a><b>§6.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">6.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">TypecheckPropositions::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">TypecheckPropositions::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="1-ap.html#SP6">§6</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_4" class="paragraph-anchor"></a><b>§6.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">6.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"><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">) && (</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">) && (</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">) && (</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="1-ap.html#SP6">§6</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_5" class="paragraph-anchor"></a><b>§6.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">6.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">-></span><span class="identifier-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="1-ap.html#SP6_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">6.5.1</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="1-ap.html#SP6_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">6.5.2</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="1-ap.html#SP6_5_3" class="named-paragraph-link"><span class="named-paragraph">Record the new creation in the debugging log</span><span class="named-paragraph-number">6.5.3</span></a></span><span class="plain-syntax">;</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="1-ap.html#SP6">§6</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_5_1" class="paragraph-anchor"></a><b>§6.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">6.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">-></span><span class="identifier-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">lookahead</span><span class="plain-syntax">-></span><span class="identifier-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">) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">lookahead</span><span class="plain-syntax">-></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">-></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">-></span><span class="element-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">-></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">-></span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">up</span><span class="plain-syntax">-></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">-></span><span class="element-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">-></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">-></span><span class="element-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">-></span><span class="element-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="1-ap.html#SP6_5">§6.5</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_5_2" class="paragraph-anchor"></a><b>§6.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">6.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="4-ks.html#SP3" class="function-link"><span class="function-syntax">KindSubjects::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="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="identifier-syntax">Specifications::from_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">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="2-nv.html#SP2" 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><span class="identifier-syntax">Lvalues::new_actual_NONLOCAL_VARIABLE</span><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="2-nv.html#SP12" 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="2-ins.html#SP4" 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="2-ins.html#SP6" 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><span class="identifier-syntax">Rvalues::from_instance</span><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><span class="identifier-syntax">Rvalues::from_instance</span><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="1-ap.html#SP6_5">§6.5</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_5_3" class="paragraph-anchor"></a><b>§6.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">6.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 <-- $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 <-- $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="1-ap.html#SP6_5">§6.5</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_6" class="paragraph-anchor"></a><b>§6.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">6.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">-></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="1-ap.html#SP6">§6</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_7" class="paragraph-anchor"></a><b>§6.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 — 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">6.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><span class="identifier-syntax">Task::syntax_tree</span><span class="plain-syntax">(),</span>
|
|
<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="1-ap.html#SP6_7_2" class="named-paragraph-link"><span class="named-paragraph">Determine the BP and terms to be asserted</span><span class="named-paragraph-number">6.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="1-ap.html#SP8" class="function-link"><span class="function-syntax">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="1-ap.html#SP8" class="function-link"><span class="function-syntax">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="1-ap.html#SP9" class="function-link"><span class="function-syntax">Assert::subject_of_term</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt0</span><span class="plain-syntax">),</span>
|
|
<span class="plain-syntax"> *</span><span class="identifier-syntax">subj1</span><span class="plain-syntax"> = </span><a href="1-ap.html#SP9" class="function-link"><span class="function-syntax">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">) && (</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="4-is.html#SP15" 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">) && (</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="4-is.html#SP15" 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>
|
|
<span class="plain-syntax"> </span><a href="1-ap.html#SP7" class="function-link"><span class="function-syntax">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>
|
|
<span class="plain-syntax"> </span><a href="1-ap.html#SP7" class="function-link"><span class="function-syntax">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="1-ap.html#SP6_7_1" class="named-paragraph-link"><span class="named-paragraph">Issue a problem message for failure to assert</span><span class="named-paragraph-number">6.7.1</span></a></span><span class="plain-syntax">;</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="1-ap.html#SP6">§6</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_7_1" class="paragraph-anchor"></a><b>§6.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">6.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><span class="identifier-syntax">Rvalues::is_nothing_object_constant</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec0</span><span class="plain-syntax">)) ||</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">Rvalues::is_nothing_object_constant</span><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><span class="identifier-syntax">Task::syntax_tree</span><span class="plain-syntax">(),</span>
|
|
<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><span class="identifier-syntax">Task::syntax_tree</span><span class="plain-syntax">(),</span>
|
|
<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="1-ap.html#SP6_7">§6.7</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP6_7_2" class="paragraph-anchor"></a><b>§6.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)\) — 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">6.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">-></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">-></span><span class="identifier-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">-></span><span class="identifier-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">-></span><span class="identifier-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">-></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><span class="identifier-syntax">Task::syntax_tree</span><span class="plain-syntax">(),</span>
|
|
<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">-></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">-></span><span class="identifier-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">-></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="1-ap.html#SP6_7">§6.7</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>§7. </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">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">Assert::cautiously_set_kind</span></span>:<br/><a href="1-ap.html#SP6_7">§6.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="4-is2.html#SP1" class="function-link"><span class="function-syntax">InstanceSubjects::to_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="2-ins.html#SP11" 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="SP8" class="paragraph-anchor"></a><b>§8. 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 — 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">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">Assert::spec_of_term</span></span>:<br/><a href="1-ap.html#SP6_7">§6.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"> >= </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="SP9" class="paragraph-anchor"></a><b>§9. </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 — 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">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">Assert::subject_of_term</span></span>:<br/><a href="1-ap.html#SP6_7">§6.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"> >= </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="identifier-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="4-is.html#SP14" 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><span class="identifier-syntax">Specifications::is_description</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">Descriptions::to_instance</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">return</span><span class="plain-syntax"> </span><a href="2-ins.html#SP6" class="function-link"><span class="function-syntax">Instances::as_subject</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Descriptions::to_instance</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">Specifications::to_kind</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">return</span><span class="plain-syntax"> </span><a href="4-ks.html#SP3" class="function-link"><span class="function-syntax">KindSubjects::from_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Specifications::to_kind</span><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="identifier-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="2-nv.html#SP14" 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="SP10" class="paragraph-anchor"></a><b>§10. 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">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">Assert::testable_at_compile_time</span></span>:<br/><a href="1-ap.html#SP11">§11</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">-></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">-></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="1-ap.html#SP10_1" class="named-paragraph-link"><span class="named-paragraph">See if this unary predicate can be tested</span><span class="named-paragraph-number">10.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="SP10_1" class="paragraph-anchor"></a><b>§10.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">10.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">-></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="1-ap.html#SP10">§10</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>§11. </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">Assert::test_at_compile_time</span><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="1-ap.html#SP10" class="function-link"><span class="function-syntax">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">-></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">-></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="1-ap.html#SP11_1" class="named-paragraph-link"><span class="named-paragraph">Test if this unary predicate is true</span><span class="named-paragraph-number">11.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="SP11_1" class="paragraph-anchor"></a><b>§11.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">11.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">-></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="1-ap.html#SP11">§11</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>§12. A catch-all problem. </b>This is provided so that code trying to assert predicates, but failing, can
|
|
make use of a generic problem message when stuck for anything better to say.
|
|
</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">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><span class="identifier-syntax">Task::syntax_tree</span><span class="plain-syntax">(),</span>
|
|
<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>
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprev"><a href="1-km.html">❮</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresscurrentchapter">1</li><li class="progresssection"><a href="1-km.html">km</a></li><li class="progresscurrent">ap</li><li class="progresschapter"><a href="2-ins.html">2</a></li><li class="progresschapter"><a href="3-prp.html">3</a></li><li class="progresschapter"><a href="4-is.html">4</a></li><li class="progresschapter"><a href="5-inf.html">5</a></li><li class="progressnext"><a href="2-ins.html">❯</a></li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|