mirror of
https://github.com/ganelson/inform.git
synced 2024-07-16 22:14:23 +03:00
945 lines
181 KiB
HTML
945 lines
181 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>Propositions</title>
|
|
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<meta name="viewport" content="width=device-width initial-scale=1">
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<meta http-equiv="Content-Language" content="en-gb">
|
|
|
|
<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script>
|
|
MathJax = {
|
|
tex: {
|
|
inlineMath: '$', '$'], ['\\(', '\\)'
|
|
},
|
|
svg: {
|
|
fontCache: 'global'
|
|
}
|
|
};
|
|
</script>
|
|
<script type="text/javascript" id="MathJax-script" async
|
|
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
|
|
</script>
|
|
|
|
<script>
|
|
function togglePopup(material_id) {
|
|
var popup = document.getElementById(material_id);
|
|
popup.classList.toggle("show");
|
|
}
|
|
</script>
|
|
|
|
<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
|
|
</head>
|
|
<body class="commentary-font">
|
|
<nav role="navigation">
|
|
<h1><a href="../index.html">
|
|
<img src="../docs-assets/Inform.png" height=72">
|
|
</a></h1>
|
|
<ul><li><a href="../compiler.html">compiler tools</a></li>
|
|
<li><a href="../other.html">other tools</a></li>
|
|
<li><a href="../extensions.html">extensions and kits</a></li>
|
|
<li><a href="../units.html">unit test tools</a></li>
|
|
</ul><h2>Compiler Webs</h2><ul>
|
|
<li><a href="../inbuild/index.html">inbuild</a></li>
|
|
<li><a href="../inform7/index.html">inform7</a></li>
|
|
<li><a href="../inter/index.html">inter</a></li>
|
|
</ul><h2>Inbuild Modules</h2><ul>
|
|
<li><a href="../supervisor-module/index.html">supervisor</a></li>
|
|
</ul><h2>Inform7 Modules</h2><ul>
|
|
<li><a href="index.html"><span class="selectedlink">core</span></a></li>
|
|
<li><a href="../if-module/index.html">if</a></li>
|
|
<li><a href="../multimedia-module/index.html">multimedia</a></li>
|
|
<li><a href="../index-module/index.html">index</a></li>
|
|
</ul><h2>Inter Modules</h2><ul>
|
|
<li><a href="../bytecode-module/index.html">bytecode</a></li>
|
|
<li><a href="../building-module/index.html">building</a></li>
|
|
<li><a href="../codegen-module/index.html">codegen</a></li>
|
|
</ul><h2>Services</h2><ul>
|
|
<li><a href="../arch-module/index.html">arch</a></li>
|
|
<li><a href="../calculus-module/index.html">calculus</a></li>
|
|
<li><a href="../html-module/index.html">html</a></li>
|
|
<li><a href="../inflections-module/index.html">inflections</a></li>
|
|
<li><a href="../kinds-module/index.html">kinds</a></li>
|
|
<li><a href="../linguistics-module/index.html">linguistics</a></li>
|
|
<li><a href="../problems-module/index.html">problems</a></li>
|
|
<li><a href="../syntax-module/index.html">syntax</a></li>
|
|
<li><a href="../words-module/index.html">words</a></li>
|
|
<li><a href="../../../inweb/docs/foundation-module/index.html">foundation</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
<!--Weave of 'Propositions' generated by Inweb-->
|
|
<div class="breadcrumbs">
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../compiler.html">Inform7 Modules</a></li><li><a href="index.html">core</a></li><li><a href="index.html#11">Chapter 11: Predicate Calculus</a></li><li><b>Propositions</b></li></ul></div>
|
|
<p class="purpose">To build and modify structures representing propositions in predicate calculus.</p>
|
|
|
|
<ul class="toc"><li><a href="11-pr.html#SP6">§6. Implied conjunction</a></li><li><a href="11-pr.html#SP9">§9. Validity</a></li><li><a href="11-pr.html#SP12">§12. Complexity</a></li><li><a href="11-pr.html#SP13">§13. Primitive operations on propositions</a></li><li><a href="11-pr.html#SP16">§16. Inserting and deleting atoms</a></li><li><a href="11-pr.html#SP18">§18. Inspecting contents</a></li><li><a href="11-pr.html#SP19">§19. Matching sequences of atoms</a></li><li><a href="11-pr.html#SP20">§20. Seeking atoms</a></li><li><a href="11-pr.html#SP28">§28. Bracketed groups</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>§1. </b>We now begin on the data structures to hold propositions. Now a properly
|
|
constructed proposition has a natural tree structure — one can regard
|
|
quantification, negation, and conjunction as higher nodes, and predicates
|
|
as leaves. So the idea of storing propositions as trees has a certain elegance.
|
|
At first it seems an advantage that any such tree is necessarily a valid
|
|
proposition. But in fact this is not so helpful, because we want to build
|
|
propositions gradually, and in particular intermediate states need to exist
|
|
which are not yet valid but will be. If we used a tree representation, we
|
|
would also need some cursor-position-like marker for the region of current
|
|
growth, and that could all become complicated. We will also find that the
|
|
main operation we need to perform is a depth-first traverse of the tree,
|
|
which is a little tiresome to do in a conventional loop (it lends itself to
|
|
recursion, but that's inconvenient).
|
|
</p>
|
|
|
|
<p class="commentary">So we will instead store propositions in a linked list, imitating the notation
|
|
used by mathematicians who write them along in a single line. Now there's a
|
|
natural way to store incomplete propositions and a natural build-point (at
|
|
the end), and depth-first traverses are easy — just work along from left
|
|
to right. The disadvantage is that it's also easy to make malformed
|
|
propositions, so we have to build carefully.
|
|
</p>
|
|
|
|
<p class="commentary">For instance, "Test sentence (internal) with no man can see the box."
|
|
produces:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> 1. no man can see the box</span>
|
|
<span class="plain-syntax"> [ DoesNotExist x IN[ man(x) IN] : can-see(x, 'box') ]</span>
|
|
</pre>
|
|
<p class="commentary">The proposition is stored as a linked list of atoms, of elements like so:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> QUANTIFIER --> DOMAIN_OPEN --> PREDICATE --> DOMAIN_CLOSE --> PREDICATE</span>
|
|
</pre>
|
|
<p class="commentary">In short: a proposition is a linked list of <span class="extract"><span class="extract-syntax">pcalc_prop</span></span> atoms, joined by
|
|
their <span class="extract"><span class="extract-syntax">next</span></span> fields. The present section contains routines to help build
|
|
and edit such lists.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>§2. </b>In particular:
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) The empty list, a <span class="extract"><span class="extract-syntax">NULL</span></span> pointer, represents the universally true
|
|
proposition \(\top\). Asserting it does nothing; testing it at run-time always
|
|
evaluates to <span class="extract"><span class="extract-syntax">true</span></span>.
|
|
</li><li>(b) The conjunction \(\phi\land\psi\) is just the concatenation of their
|
|
linked lists.
|
|
</li><li>(c) Negation \(\lnot(\phi)\) is the concatenation <span class="extract"><span class="extract-syntax">NEGATION_OPEN --> P --> NEGATION_CLOSE</span></span>,
|
|
where <span class="extract"><span class="extract-syntax">P</span></span> is the linked list for \(\phi\).
|
|
</li><li>(d) The quantifier \(Q v\in \lbrace v\mid\phi(v)\rbrace\) is
|
|
<span class="extract"><span class="extract-syntax">QUANTIFIER --> DOMAIN_OPEN --> P --> DOMAIN_CLOSE</span></span>.
|
|
</li></ul>
|
|
<p class="commentary">In this section, we'll call a segment of the list representing a pair of
|
|
matched brackets, like <span class="extract"><span class="extract-syntax">DOMAIN_OPEN --> P --> DOMAIN_CLOSE</span></span>, a "group".
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>§3. </b>We sometimes need to indicate a position within a proposition — a
|
|
position not of an atom, but between atoms. Consider the possible places
|
|
where letters could be inserted into the word "rap": before the "r"
|
|
(trap), between "r" and "a" (reap), between "a" and "p" (ramp),
|
|
after the "p" (rapt). Though "rap" is a three-letter word, there are
|
|
four possible insertion points — so they can't exactly correspond to
|
|
letters. The convention used with Inform propositions is that a position
|
|
marker points to the <span class="extract"><span class="extract-syntax">pcalc_prop</span></span> structure for the atom before
|
|
the position meant: and a <span class="extract"><span class="extract-syntax">NULL</span></span> pointer in this context means the
|
|
front position, before the opening atom.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>§4. </b>The code needed to perform a depth-first traverse of a proposition is
|
|
abstracted by the following macros. Note that we often need to remember
|
|
the atom before the current one, so we keep that in a spare variable
|
|
during each traverse. (This saves us having to maintain the proposition
|
|
data structure as a doubly linked list, which would be harder to edit.)
|
|
</p>
|
|
|
|
<p class="commentary">One macro declares the name of a marker variable to be used when traversing;
|
|
the other is the necessary loop head. Note that we do not assume that <span class="extract"><span class="extract-syntax">p</span></span>
|
|
will still be non-<span class="extract"><span class="extract-syntax">NULL</span></span> at the end of a loop iteration, just because it
|
|
was at the beginning: local edits are sometimes performed in the traverse,
|
|
and it can happen that an edit truncates the proposition so savagely that the
|
|
loop finds its ground cut out from under it.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, *</span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="definition-keyword">define</span> <span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">start</span><span class="plain-syntax">)</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">=</span><span class="identifier-syntax">start</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax">=</span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</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">p</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">_repeat</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)?(</span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax">=</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">=(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)?(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">):</span><span class="identifier-syntax">NULL</span><span class="plain-syntax">):0, </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>§5. </b>An edit which happens during a traverse is permitted to make any change
|
|
to the proposition at and beyond the marker position <span class="extract"><span class="extract-syntax">p</span></span>, but not allowed
|
|
to change what came before. Since such an edit might leave <span class="extract"><span class="extract-syntax">p</span></span> pointing
|
|
to an atom which has been cut, or moved later, we must perform the following
|
|
macro after edits to restore <span class="extract"><span class="extract-syntax">p</span></span>. We know that the atom which was before
|
|
<span class="extract"><span class="extract-syntax">p</span></span> at the start of the loop has not been changed — since edits aren't
|
|
allowed there — so <span class="extract"><span class="extract-syntax">p_prev</span></span> must be correct, and we therefore restore
|
|
<span class="extract"><span class="extract-syntax">p</span></span> to the next atom after <span class="extract"><span class="extract-syntax">p_prev</span></span>.
|
|
</p>
|
|
|
|
<p class="commentary">There is a catch, however: if our edit consists only of deleting some
|
|
atoms then using <span class="extract"><span class="extract-syntax">PROPOSITION_EDITED</span></span> correctly resets <span class="extract"><span class="extract-syntax">p</span></span> to the current
|
|
atom at the marker position, and that will be the first atom after the
|
|
ones deleted. If we then just go around the loop, we move on to the next
|
|
atom; as a result, the first atom after the deleted ones is skipped over.
|
|
We can avoid this by using <span class="extract"><span class="extract-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span></span> instead.
|
|
</p>
|
|
|
|
<p class="commentary">Every routine which simplifies a proposition is expected to have an <span class="extract"><span class="extract-syntax">int *</span></span>
|
|
argument called <span class="extract"><span class="extract-syntax">changed</span></span>: on exit, the <span class="extract"><span class="extract-syntax">int</span></span> variable this points to
|
|
should be set if and only if a change has been made to the proposition.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="definition-keyword">define</span> <span class="identifier-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>§6. Implied conjunction. </b>Conjunction (logical "and") occurs so densely in propositions arising from
|
|
natural language that our data structures would grow large and unmanageable
|
|
if we wrote all of them out. So we adopt a convention similar to the one
|
|
in algebra, where the formula
|
|
$$ xy+w(v-1) $$
|
|
is understood to mean multiplication of \(x\) by \(y\), and of \(w\) by \((v-1)\).
|
|
Note that if we were to write it out as a sequence of symbols
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> x y + w ( v - 1 )</span>
|
|
</pre>
|
|
<p class="commentary">then multiplication would only be understood at two positions, not between
|
|
every pair of symbols. In the same way, the following routine looks at a
|
|
pair of adjacent atoms and decides whether or not conjunction should be
|
|
understood between them.
|
|
</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">Calculus::Propositions::implied_conjunction_between</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">Calculus::Propositions::implied_conjunction_between</span></span>:<br/><a href="11-pr.html#SP7">§7</a><br/>Deciding to Defer - <a href="12-dtd.html#SP7">§7</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p2</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">p1</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p2</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="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">Calculus::Atoms::element_get_group</span><span class="plain-syntax">(</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">) == </span><span class="identifier-syntax">OPEN_OPERATORS_GROUP</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Calculus::Atoms::element_get_group</span><span class="plain-syntax">(</span><span class="identifier-syntax">p2</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">) == </span><span class="identifier-syntax">CLOSE_OPERATORS_GROUP</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">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="SP7" class="paragraph-anchor"></a><b>§7. </b>Purely decoratively, we print some punctuation when logging a proposition;
|
|
this is chosen to look like standard mathematical notation.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::debugging_log_text_between</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">Calculus::Propositions::debugging_log_text_between</span></span>:<br/><a href="11-pr.html#SP8">§8</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p2</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">p1</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p2</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="string-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">p1</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">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">p2</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</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">return</span><span class="plain-syntax"> </span><span class="string-syntax">":"</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">p1</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</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">if</span><span class="plain-syntax"> (</span><a href="11-pr.html#SP6" class="function-link"><span class="function-syntax">Calculus::Propositions::implied_conjunction_between</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="identifier-syntax">p2</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">Streams::I6_escapes_enabled</span><span class="plain-syntax">(</span><span class="identifier-syntax">DL</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax">(</span><span class="string-syntax">"&"</span><span class="plain-syntax">); </span><span class="comment-syntax"> since </span><span class="extract"><span class="extract-syntax">^</span></span><span class="comment-syntax"> in I6 strings means newline</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="string-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="string-syntax">""</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. </b>So we may as well complete the debugging log code now. Note that \(\top\) is
|
|
logged as just <span class="extract"><span class="extract-syntax">[ ]</span></span>.
|
|
</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">log_addresses</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::log</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">Calculus::Propositions::log</span></span>:<br/>Core Module - <a href="1-cm.html#SP5">§5</a>, <a href="1-cm.html#SP6_6">§6.6</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><a href="11-pr.html#SP8" class="function-link"><span class="function-syntax">Calculus::Propositions::write</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">DL</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">void</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::write</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">Calculus::Propositions::write</span></span>:<br/>Core Module - <a href="1-cm.html#SP7">§7</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">OUTPUT_STREAM</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="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">"[ "</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">p</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">char</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bridge</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP7" class="function-link"><span class="function-syntax">Calculus::Propositions::debugging_log_text_between</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</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">bridge</span><span class="plain-syntax">[0]) </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">"%s "</span><span class="plain-syntax">, </span><span class="identifier-syntax">bridge</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">log_addresses</span><span class="plain-syntax">) </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">"%08x="</span><span class="plain-syntax">, (</span><span class="reserved-syntax">unsigned</span><span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax">) </span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">Calculus::Atoms::write</span><span class="plain-syntax">(</span><span class="identifier-syntax">OUT</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">" "</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">"]"</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. Validity. </b>Since the proposition data structure lets us build all kinds of nonsense,
|
|
we'll be much safer if we can check our working — if we can verify that a
|
|
proposition is valid. But what does that mean? We might mean:
|
|
</p>
|
|
|
|
<ul class="items"><li>(i) a proposition is good if its sequence of <span class="extract"><span class="extract-syntax">next</span></span> pointers all correctly
|
|
point to <span class="extract"><span class="extract-syntax">pcalc_prop</span></span> structures, and don't loop around into a circle;
|
|
</li><li>(ii) a proposition is good if (i) is true, and it is correctly punctuated;
|
|
</li><li>(iii) a proposition is good if (ii) is true, and it never confuses
|
|
together two different variables by giving both the same letter;
|
|
</li><li>(iv) a proposition is good if (iii) is true, and all of its predicates
|
|
can safely be applied to all of their terms, and we can identify what
|
|
kind of value each variable ranges over.
|
|
</li></ul>
|
|
<p class="commentary">These are steadily stronger conditions. The first is a basic invariant of
|
|
our data structures: nothing failing (i) will ever be allowed to exist,
|
|
provided the routines in this section are free of bugs. Condition (ii) is
|
|
called syntactic validity; (iii) is well-formedness; (iv) is
|
|
type safety. Correct source text eventually makes propositions which
|
|
have all four properties, but intermediate half-built states often satisfy
|
|
only (i).
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>§10. </b>The following examples illustrate the differences. This one is not even
|
|
syntactically valid:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">|DOMAIN_OPEN_ATOM --> NEGATION_CLOSE_ATOM --> NEGATION_CLOSE_ATOM|</span>
|
|
</pre>
|
|
<p class="commentary">This one is syntactically valid, but not well-formed:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">|EVERYWHERE_ATOM(x) --> QUANTIFIER=for-all(x) --> PREDICATE=open(x)|</span>
|
|
</pre>
|
|
<p class="commentary">(If <span class="extract"><span class="extract-syntax">x</span></span> ranges over all objects at the middle of the proposition, it had
|
|
better not already have a value, but if it doesn't, what can that first
|
|
atom mean? It would be like writing the formula \(n + \sum_{n=1}^{10} n^2\),
|
|
where clearly two different things have been called \(n\).)
|
|
</p>
|
|
|
|
<p class="commentary">And this proposition is well-formed but not type-safe:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">|QUANTIFIER=for-all(x) --> KIND=number(x) --> EVERYWHERE(x)|</span>
|
|
</pre>
|
|
<p class="commentary">(Here <span class="extract"><span class="extract-syntax">x</span></span> is supposed to be a number, and therefore has no location, but
|
|
<span class="extract"><span class="extract-syntax">EVERYWHERE</span></span> can validly be applied only to backdrop objects, so what
|
|
could <span class="extract"><span class="extract-syntax">EVERYWHERE(x)</span></span> possibly mean?)
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>§11. </b>Well-formedness and type safety are left to later sections in this chapter,
|
|
but we can at least test syntactic validity here.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">MAX_PROPOSITION_GROUP_NESTING</span><span class="plain-syntax"> </span><span class="constant-syntax">100</span><span class="plain-syntax"> </span><span class="comment-syntax"> vastly more than could realistically be used</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::is_syntactically_valid</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">Calculus::Propositions::is_syntactically_valid</span></span>:<br/>Binding and Substitution - <a href="11-bas.html#SP4">§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="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">groups_stack</span><span class="plain-syntax">[</span><span class="constant-syntax">MAX_PROPOSITION_GROUP_NESTING</span><span class="plain-syntax">], </span><span class="identifier-syntax">group_sp</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">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="comment-syntax"> (1) each individual atom has to be properly built:</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="identifier-syntax">err</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Atoms::validate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">err</span><span class="plain-syntax">) { </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Atom error: %s: $o\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</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="comment-syntax"> (2) every open bracket must be matched by a close bracket of the same kind:</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Calculus::Atoms::element_get_group</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">) == </span><span class="identifier-syntax">OPEN_OPERATORS_GROUP</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">group_sp</span><span class="plain-syntax"> >= </span><span class="constant-syntax">MAX_PROPOSITION_GROUP_NESTING</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Group nesting too deep\n"</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="identifier-syntax">groups_stack</span><span class="plain-syntax">[</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax">++] = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</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">Calculus::Atoms::element_get_group</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">) == </span><span class="identifier-syntax">CLOSE_OPERATORS_GROUP</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">group_sp</span><span class="plain-syntax"> <= </span><span class="constant-syntax">0</span><span class="plain-syntax">) { </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Too many close groups\n"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; }</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Calculus::Atoms::element_get_match</span><span class="plain-syntax">(</span><span class="identifier-syntax">groups_stack</span><span class="plain-syntax">[--</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax">]) != </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Group open/close doesn't match\n"</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="comment-syntax"> (3) every quantifier except "exists" must be followed by domain brackets, which occur nowhere else:</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">Calculus::Atoms::is_quantifier</span><span class="plain-syntax">(</span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">)) && (</span><span class="identifier-syntax">Calculus::Atoms::is_existence_quantifier</span><span class="plain-syntax">(</span><span class="identifier-syntax">p_prev</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">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> != </span><span class="identifier-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) { </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Quant without domain\n"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; }</span>
|
|
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</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">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) { </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Domain without quant\n"</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">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">Calculus::Atoms::is_quantifier</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)) && (</span><span class="identifier-syntax">Calculus::Atoms::is_existence_quantifier</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Ends without domain of final quantifier\n"</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="comment-syntax"> (4) a proposition must end with all its brackets closed:</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax"> != </span><span class="constant-syntax">0</span><span class="plain-syntax">) { </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"%d group(s) open\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">group_sp</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; }</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>§12. Complexity. </b>Simple propositions contain only unary predicates or assertions that the
|
|
free variable has a given kind, or a given value. For example, "a closed
|
|
lockable door" is a simple proposition, but "four women in a lighted room"
|
|
is complex.
|
|
</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">Calculus::Propositions::is_complex</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">Calculus::Propositions::is_complex</span></span>:<br/>Descriptions - <a href="14-ds.html#SP7">§7</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</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="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Calculus::Atoms::is_equality_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">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">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="identifier-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="identifier-syntax">constant</span><span class="plain-syntax">)) ||</span>
|
|
<span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</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="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="identifier-syntax">constant</span><span class="plain-syntax">)))) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>§13. Primitive operations on propositions. </b>First, copying, which means copying not just the current atom, but all
|
|
subsequent ones.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::copy</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">Calculus::Propositions::copy</span></span>:<br/>Refine Parse Tree - <a href="5-rpt.html#SP2">§2</a><br/>Parse Tree Usage - <a href="8-ptu.html#SP2">§2</a><br/>Sentence Conversions - <a href="11-sc.html#SP3">§3</a>, <a href="11-sc.html#SP3_4">§3.4</a><br/>Deciding to Defer - <a href="12-dtd.html#SP6">§6</a><br/>Compile Deferred Propositions - <a href="12-cdp.html#SP2_1">§2.1</a>, <a href="12-cdp.html#SP2_1_6">§2.1.6</a><br/>Descriptions - <a href="14-ds.html#SP6">§6</a>, <a href="14-ds.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">original</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">first</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, *</span><span class="identifier-syntax">last</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">original</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">while</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">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Atoms::new</span><span class="plain-syntax">(0);</span>
|
|
<span class="plain-syntax"> *</span><span class="identifier-syntax">copied_atom</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">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax"><prop-></span><span class="identifier-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++)</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">Calculus::Terms::copy</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">first</span><span class="plain-syntax">) </span><span class="identifier-syntax">last</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">copied_atom</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">first</span><span class="plain-syntax"> = </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">last</span><span class="plain-syntax"> = </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">first</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP14" class="paragraph-anchor"></a><b>§14. </b>Now to concatenate propositions. If \(E\) and \(T\) are both syntactically valid,
|
|
the result will be, too; but the same is not true of well-formedness, so we
|
|
need to be careful in using this.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::concatenate</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">Calculus::Propositions::concatenate</span></span>:<br/><a href="11-pr.html#SP15">§15</a><br/>The Creator - <a href="5-tc.html#SP5_4_1_1">§5.4.1.1</a>, <a href="5-tc.html#SP5_4_2_1">§5.4.2.1</a>, <a href="5-tc.html#SP5_4_2_2">§5.4.2.2</a>, <a href="5-tc.html#SP5_4_2_3">§5.4.2.3</a><br/>Implications - <a href="5-imp.html#SP6_1_3">§6.1.3</a><br/>Tree Conversions - <a href="11-tc.html#SP1">§1</a>, <a href="11-tc.html#SP2">§2</a><br/>Sentence Conversions - <a href="11-sc.html#SP1_13">§1.13</a>, <a href="11-sc.html#SP3_7">§3.7</a>, <a href="11-sc.html#SP3_8">§3.8</a><br/>Deciding to Defer - <a href="12-dtd.html#SP9">§9</a>, <a href="12-dtd.html#SP12">§12</a><br/>Descriptions - <a href="14-ds.html#SP8">§8</a>, <a href="14-ds.html#SP9">§9</a>, <a href="14-ds.html#SP10">§10</a><br/>Condition Properties - <a href="15-cp.html#SP3">§3</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tail</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">end</span><span class="plain-syntax"> = </span><span class="identifier-syntax">existing_body</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">end</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="identifier-syntax">tail</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">sc</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">while</span><span class="plain-syntax"> (</span><span class="identifier-syntax">end</span><span class="plain-syntax"> && (</span><span class="identifier-syntax">end</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">sc</span><span class="plain-syntax">++ == </span><span class="constant-syntax">100000</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"malformed proposition"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">end</span><span class="plain-syntax"> = </span><span class="identifier-syntax">end</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">end</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">tail</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">existing_body</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP15" class="paragraph-anchor"></a><b>§15. </b>And here is a version which protects us:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::conjoin</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::conjoin</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP7">§7</a>, <a href="11-tc.html#SP7_1">§7.1</a>, <a href="11-tc.html#SP7_2">§7.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">existing_body</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tail</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">p</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">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">existing_body</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">p</span><span class="plain-syntax"> == </span><span class="identifier-syntax">tail</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="11-pr.html#SP15_1" class="named-paragraph-link"><span class="named-paragraph">Report failure to log</span><span class="named-paragraph-number">15.1</span></a></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">"conjoin proposition to a subset of itself"</span><span class="plain-syntax">);</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">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">tail</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">p</span><span class="plain-syntax"> == </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="11-pr.html#SP15_1" class="named-paragraph-link"><span class="named-paragraph">Report failure to log</span><span class="named-paragraph-number">15.1</span></a></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">"conjoin proposition to a superset of itself"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> }</span>
|
|
|
|
<span class="plain-syntax"> </span><a href="11-bas.html#SP10" class="function-link"><span class="function-syntax">Calculus::Variables::renumber_bound</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">tail</span><span class="plain-syntax">, </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, -1);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP14" class="function-link"><span class="function-syntax">Calculus::Propositions::concatenate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, </span><span class="identifier-syntax">tail</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">existing_body</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP15_1" class="paragraph-anchor"></a><b>§15.1. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Report failure to log</span><span class="named-paragraph-number">15.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">"Seriously misguided attempt to conjoin propositions:\n"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">log_addresses</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Existing body: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Tail: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">tail</span><span class="plain-syntax">);</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="11-pr.html#SP15">§15</a> (twice).</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP16" class="paragraph-anchor"></a><b>§16. Inserting and deleting atoms. </b>Here we insert an atom at a given position, or at the front if the position
|
|
is <span class="extract"><span class="extract-syntax">NULL</span></span>.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::insert_atom</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::insert_atom</span></span>:<br/>Binding and Substitution - <a href="11-bas.html#SP11">§11</a><br/>Simplifications - <a href="11-sm.html#SP2_2">§2.2</a>, <a href="11-sm.html#SP3">§3</a>, <a href="11-sm.html#SP5">§5</a>, <a href="11-sm.html#SP6">§6</a>, <a href="11-sm.html#SP7">§7</a>, <a href="11-sm.html#SP9_3_2">§9.3.2</a>, <a href="11-sm.html#SP14">§14</a>, <a href="11-sm.html#SP18">§18</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="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"inserting atom nowhere"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">position</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">position</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP17" class="paragraph-anchor"></a><b>§17. </b>And similarly, with the deleted atom the one after the position given:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::delete_atom</span><button class="popup" onclick="togglePopup('usagePopup11')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup11">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::delete_atom</span></span>:<br/><a href="11-pr.html#SP31">§31</a>, <a href="11-pr.html#SP32">§32</a>, <a href="11-pr.html#SP33">§33</a><br/>Simplifications - <a href="11-sm.html#SP9_3_1">§9.3.1</a>, <a href="11-sm.html#SP9_3_2">§9.3.2</a>, <a href="11-sm.html#SP9_4">§9.4</a>, <a href="11-sm.html#SP13">§13</a>, <a href="11-sm.html#SP14">§14</a>, <a href="11-sm.html#SP16_1">§16.1</a>, <a href="11-sm.html#SP18">§18</a><br/>Compile Deferred Propositions - <a href="12-cdp.html#SP5">§5</a>, <a href="12-cdp.html#SP5_1_1_1">§5.1.1.1</a><br/>Descriptions - <a href="14-ds.html#SP10">§10</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"deleting atom nowhere"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"deleting atom off end"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">position</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">position</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP18" class="paragraph-anchor"></a><b>§18. Inspecting contents. </b>First, we count the number of atoms in a given proposition. This is used by
|
|
other parts of Inform as a crude measure of how complicated it is; though in
|
|
fact it is not all that crude so long as it is applied to a proposition
|
|
which has been simplified.
|
|
</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">Calculus::Propositions::length</span><button class="popup" onclick="togglePopup('usagePopup12')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup12">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::length</span></span>:<br/>Conditions - <a href="14-cn.html#SP14">§14</a><br/>Descriptions - <a href="14-ds.html#SP7">§7</a>, <a href="14-ds.html#SP12_1">§12.1</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">n</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">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) </span><span class="identifier-syntax">n</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">n</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP19" class="paragraph-anchor"></a><b>§19. Matching sequences of atoms. </b>The following sneakily variable-argument-length function can be used to
|
|
detect subsequences within a proposition: say, the sequence
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> QUANTIFIER --> PREDICATE --> anything --> CALLED</span>
|
|
</pre>
|
|
<p class="commentary">starting at the current position, which could be tested with:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> Calculus::Propositions::match(p, 4, QUANTIFIER_ATOM, NULL, PREDICATE_ATOM, NULL,</span>
|
|
<span class="plain-syntax"> ANY_ATOM_HERE, NULL, CALLED_ATOM, &cp);</span>
|
|
</pre>
|
|
<p class="commentary">As can be seen, each atom is tested with an element number and an optional
|
|
pointer; when a successful match is made, the optional pointer is set to
|
|
the atom making the match. (So if the routine returns <span class="extract"><span class="extract-syntax">TRUE</span></span> then we can
|
|
be certain that <span class="extract"><span class="extract-syntax">cp</span></span> points to the <span class="extract"><span class="extract-syntax">CALLED_ATOM</span></span> at the end of the run of
|
|
four.) There are two special pseudo-element-numbers:
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">ANY_ATOM_HERE</span><span class="plain-syntax"> </span><span class="constant-syntax">0</span><span class="plain-syntax"> </span><span class="comment-syntax"> match any atom, but don't match beyond the end of the proposition</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">END_PROP_HERE</span><span class="plain-syntax"> -1 </span><span class="comment-syntax"> a sentinel meaning "the proposition must end at this point"</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::match</span><button class="popup" onclick="togglePopup('usagePopup13')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup13">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::match</span></span>:<br/><a href="11-pr.html#SP32">§32</a><br/>Sentence Conversions - <a href="11-sc.html#SP3_4">§3.4</a><br/>Simplifications - <a href="11-sm.html#SP4">§4</a>, <a href="11-sm.html#SP5">§5</a>, <a href="11-sm.html#SP6">§6</a>, <a href="11-sm.html#SP9_2">§9.2</a>, <a href="11-sm.html#SP14">§14</a>, <a href="11-sm.html#SP18">§18</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">c</span><span class="plain-syntax">, ...) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">, </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">va_list</span><span class="plain-syntax"> </span><span class="identifier-syntax">ap</span><span class="plain-syntax">; </span><span class="comment-syntax"> the variable argument list signified by the dots</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">va_start</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax">); </span><span class="comment-syntax"> macro to begin variable argument processing</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax"> < </span><span class="identifier-syntax">c</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">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> = </span><span class="identifier-syntax">va_arg</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">atom_p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">va_arg</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_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">atom_p</span><span class="plain-syntax"> != </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) *</span><span class="identifier-syntax">atom_p</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">a</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">ANY_ATOM_HERE:</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</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">END_PROP_HERE:</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> != </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</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">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</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="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> != </span><span class="identifier-syntax">a</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</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">break</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">prop</span><span class="plain-syntax">) </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">va_end</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">); </span><span class="comment-syntax"> macro to end variable argument processing</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">outcome</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP20" class="paragraph-anchor"></a><b>§20. Seeking atoms. </b>Here we run through the proposition looking for either a given element, or
|
|
a given arity, or both:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span><button class="popup" onclick="togglePopup('usagePopup14')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup14">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></span>:<br/><a href="11-pr.html#SP21">§21</a>, <a href="11-pr.html#SP22">§22</a>, <a href="11-pr.html#SP24">§24</a>, <a href="11-pr.html#SP27">§27</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">atom_req</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">arity_req</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">p</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">p</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">atom_req</span><span class="plain-syntax"> < </span><span class="constant-syntax">0</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">atom_req</span><span class="plain-syntax">)) &&</span>
|
|
<span class="plain-syntax"> ((</span><span class="identifier-syntax">arity_req</span><span class="plain-syntax"> < </span><span class="constant-syntax">0</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">arity</span><span class="plain-syntax"> == </span><span class="identifier-syntax">arity_req</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">p</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="SP21" class="paragraph-anchor"></a><b>§21. </b>Seeking different kinds of atom is now easy:
|
|
</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">Calculus::Propositions::contains_binary_predicate</span><button class="popup" onclick="togglePopup('usagePopup15')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup15">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::contains_binary_predicate</span></span>:<br/>Property Knowledge - <a href="5-pk.html#SP3_2">§3.2</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">PREDICATE_ATOM</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">TRUE</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::contains_quantifier</span><button class="popup" onclick="togglePopup('usagePopup16')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup16">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::contains_quantifier</span></span>:<br/>Define by Table Requests - <a href="4-dbtr.html#SP4_1_1_2">§4.1.1.2</a><br/>Deciding to Defer - <a href="12-dtd.html#SP6">§6</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><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, -1)) </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="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::composited_kind</span><button class="popup" onclick="togglePopup('usagePopup17')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup17">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::composited_kind</span></span>:<br/>Sentence Conversions - <a href="11-sc.html#SP1_13_1">§1.13.1</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">KIND_ATOM</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">k_atom</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">-></span><span class="identifier-syntax">composited</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)) </span><span class="identifier-syntax">k_atom</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">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::contains_nonexistence_quantifier</span><button class="popup" onclick="togglePopup('usagePopup18')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup18">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::contains_nonexistence_quantifier</span></span>:<br/>Assert Propositions - <a href="12-ap.html#SP8">§8</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">while</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">1</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">quantifier</span><span class="plain-syntax"> *</span><span class="identifier-syntax">quant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">quant</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">quant</span><span class="plain-syntax"> != </span><span class="identifier-syntax">exists_quantifier</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::contains_callings</span><button class="popup" onclick="togglePopup('usagePopup19')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup19">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::contains_callings</span></span>:<br/>Deciding to Defer - <a href="12-dtd.html#SP5">§5</a>, <a href="12-dtd.html#SP8_1">§8.1</a>, <a href="12-dtd.html#SP15">§15</a>, <a href="12-dtd.html#SP23">§23</a><br/>Descriptions - <a href="14-ds.html#SP10">§10</a><br/>Chronology - <a href="24-ch.html#SP6_4_1">§6.4.1</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">CALLED_ATOM</span><span class="plain-syntax">, -1)) </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="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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP22" class="paragraph-anchor"></a><b>§22. </b>Here we try to find out the kind of value of variable 0 without the full
|
|
expense of typechecking the proposition:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::describes_kind</span><button class="popup" onclick="togglePopup('usagePopup20')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup20">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::describes_kind</span></span>:<br/>Deciding to Defer - <a href="12-dtd.html#SP17">§17</a><br/>Descriptions - <a href="14-ds.html#SP4">§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="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</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">while</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">ISAKIND_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">1</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">Calculus::Terms::variable_underlying</span><span class="plain-syntax">(&(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0])) == </span><span class="constant-syntax">0</span><span class="plain-syntax">) &&</span>
|
|
<span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::eq</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">assert_kind</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_value</span><span class="plain-syntax">))) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</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="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</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">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">while</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">KIND_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">1</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">Calculus::Terms::variable_underlying</span><span class="plain-syntax">(&(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0])) == </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">p</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="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</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">val</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP23" class="function-link"><span class="function-syntax">Calculus::Propositions::describes_value</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="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">val</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="14-sp.html#SP1" class="function-link"><span class="function-syntax">Specifications::to_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">val</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="SP23" class="paragraph-anchor"></a><b>§23. </b>And, similarly, the actual value it must have:
|
|
</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">Calculus::Propositions::describes_value</span><button class="popup" onclick="togglePopup('usagePopup21')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup21">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::describes_value</span></span>:<br/><a href="11-pr.html#SP22">§22</a><br/>Specifications - <a href="14-sp.html#SP3">§3</a><br/>Descriptions - <a href="14-ds.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="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</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">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">p</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="identifier-syntax">bl</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">NEGATION_CLOSE_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</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">DOMAIN_OPEN_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</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">DOMAIN_CLOSE_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</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">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bl</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">Calculus::Atoms::is_equality_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="identifier-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="identifier-syntax">constant</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</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">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</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="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="identifier-syntax">constant</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="identifier-syntax">constant</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">break</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="SP24" class="paragraph-anchor"></a><b>§24. </b>Finding an adjective is easy: it's a predicate of arity 1.
|
|
</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">Calculus::Propositions::contains_adjective</span><button class="popup" onclick="togglePopup('usagePopup22')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup22">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::contains_adjective</span></span>:<br/>Property Knowledge - <a href="5-pk.html#SP3_2">§3.2</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::count_unary_predicates</span><button class="popup" onclick="togglePopup('usagePopup23')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup23">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::count_unary_predicates</span></span>:<br/>Descriptions - <a href="14-ds.html#SP8">§8</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">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">ac</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">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</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">while</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">1</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">Calculus::Terms::variable_underlying</span><span class="plain-syntax">(&(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0])) == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">ac</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">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">ac</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP25" class="paragraph-anchor"></a><b>§25. </b>The following searches not for an atom, but for the lexically earliest
|
|
term in the proposition:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::get_first_cited_term</span><button class="popup" onclick="togglePopup('usagePopup24')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup24">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::get_first_cited_term</span></span>:<br/>Sentence Conversions - <a href="11-sc.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="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">p</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">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">arity</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">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0];</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"Calculus::Propositions::get_first_cited_term on termless proposition"</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">Calculus::Terms::new_variable</span><span class="plain-syntax">(0); </span><span class="comment-syntax"> never executed, but needed to prevent </span><span class="extract"><span class="extract-syntax">gcc</span></span><span class="comment-syntax"> warnings</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP26" class="paragraph-anchor"></a><b>§26. </b>Here we attempt, if possible, to read a proposition as being either
|
|
{\it adjective}(\(v\)) or \(\exists v: {\it adjective}(v)\), where the adjective
|
|
can be also be read as a noun, and if so we return a constant term \(t\) for
|
|
that noun; or if the proposition isn't in that form, we return \(t=x\), that
|
|
is, variable 0.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Propositions::convert_adj_to_noun</span><button class="popup" onclick="togglePopup('usagePopup25')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup25">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::convert_adj_to_noun</span></span>:<br/>Sentence Conversions - <a href="11-sc.html#SP3_6">§3.6</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">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pct</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Terms::new_variable</span><span class="plain-syntax">(0);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">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="identifier-syntax">pct</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">Calculus::Atoms::is_existence_quantifier</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)) </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">next</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="identifier-syntax">pct</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="element-syntax">next</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="identifier-syntax">pct</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">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">prop</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="plain-syntax"> </span><span class="identifier-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tr</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">predicate</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">Calculus::Terms::adj_to_noun_conversion</span><span class="plain-syntax">(</span><span class="identifier-syntax">tr</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">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">KIND_ATOM</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">prop</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="reserved-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pname</span><span class="plain-syntax"> = </span><a href="15-cp.html#SP5" class="function-link"><span class="function-syntax">Properties::Conditions::get_coinciding_property</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pname</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">Calculus::Terms::new_constant</span><span class="plain-syntax">(</span><a href="14-rv.html#SP1" class="function-link"><span class="function-syntax">Rvalues::from_property</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pname</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">pct</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP27" class="paragraph-anchor"></a><b>§27. </b>We often form propositions which are really lists of adjectives, and the
|
|
following are useful for looping through them:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::first_unary_predicate</span><button class="popup" onclick="togglePopup('usagePopup26')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup26">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::first_unary_predicate</span></span>:<br/>Descriptions - <a href="14-ds.html#SP8">§8</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="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">ppp</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">PREDICATE_ATOM</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">ppp</span><span class="plain-syntax">) *</span><span class="identifier-syntax">ppp</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="identifier-syntax">NULL</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">Calculus::Atoms::au_from_unary_PREDICATE</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">unary_predicate</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::next_unary_predicate</span><button class="popup" onclick="togglePopup('usagePopup27')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup27">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::next_unary_predicate</span></span>:<br/>Descriptions - <a href="14-ds.html#SP8">§8</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">ppp</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">ppp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"bad ppp"</span><span class="plain-syntax">);</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><a href="11-pr.html#SP20" class="function-link"><span class="function-syntax">Calculus::Propositions::prop_seek_atom</span></a><span class="plain-syntax">((*</span><span class="identifier-syntax">ppp</span><span class="plain-syntax">)-></span><span class="element-syntax">next</span><span class="plain-syntax">, </span><span class="identifier-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> *</span><span class="identifier-syntax">ppp</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="identifier-syntax">NULL</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">Calculus::Atoms::au_from_unary_PREDICATE</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP28" class="paragraph-anchor"></a><b>§28. Bracketed groups. </b>The following routine tests whether the entire proposition is a single
|
|
bracketed group. For instance:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> NEGATION_OPEN --> PREDICATE --> KIND --> NEGATION_CLOSE</span>
|
|
</pre>
|
|
<p class="commentary">would qualify. Note that detection succeeds only if the parentheses match,
|
|
and that they may be nested.
|
|
</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">Calculus::Propositions::is_a_group</span><button class="popup" onclick="togglePopup('usagePopup28')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup28">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::is_a_group</span></span>:<br/><a href="11-pr.html#SP29">§29</a>, <a href="11-pr.html#SP30">§30</a><br/>Deciding to Defer - <a href="12-dtd.html#SP6_1_1">§6.1.1</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">governing</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">match</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Atoms::element_get_match</span><span class="plain-syntax">(</span><span class="identifier-syntax">governing</span><span class="plain-syntax">), </span><span class="identifier-syntax">level</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">match</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"Calculus::Propositions::is_a_group called on unmatchable"</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">p</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> != </span><span class="identifier-syntax">governing</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="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">Calculus::Atoms::element_get_group</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">) == </span><span class="identifier-syntax">OPEN_OPERATORS_GROUP</span><span class="plain-syntax">) </span><span class="identifier-syntax">level</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">Calculus::Atoms::element_get_group</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">) == </span><span class="identifier-syntax">CLOSE_OPERATORS_GROUP</span><span class="plain-syntax">) </span><span class="identifier-syntax">level</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">p_prev</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">match</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">level</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">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP29" class="paragraph-anchor"></a><b>§29. </b>The following removes matched parentheses, leaving just the interior:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::remove_topmost_group</span><button class="popup" onclick="togglePopup('usagePopup29')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup29">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::remove_topmost_group</span></span>:<br/><a href="11-pr.html#SP30">§30</a><br/>Deciding to Defer - <a href="12-dtd.html#SP6_1_1">§6.1.1</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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><a href="11-pr.html#SP28" class="function-link"><span class="function-syntax">Calculus::Propositions::is_a_group</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</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">"tried to remove topmost group which wasn't there"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"ungrouping proposition: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">next</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">p</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">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) { </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</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">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"to ungrouped result: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP30" class="paragraph-anchor"></a><b>§30. </b>The main application of which is to remove negation:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::unnegate</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="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="11-pr.html#SP28" class="function-link"><span class="function-syntax">Calculus::Propositions::is_a_group</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="11-pr.html#SP29" class="function-link"><span class="function-syntax">Calculus::Propositions::remove_topmost_group</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="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="SP31" class="paragraph-anchor"></a><b>§31. </b>More ambitiously, this removes matched parentheses found at any given
|
|
point in a proposition (which can continue after the close bracket).
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::ungroup_after</span><button class="popup" onclick="togglePopup('usagePopup30')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup30">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::ungroup_after</span></span>:<br/><a href="11-pr.html#SP32">§32</a><br/>Simplifications - <a href="11-sm.html#SP5">§5</a>, <a href="11-sm.html#SP14">§14</a><br/>Descriptions - <a href="14-ds.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="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">last</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">p</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">from</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">opener</span><span class="plain-syntax">, </span><span class="identifier-syntax">closer</span><span class="plain-syntax">, </span><span class="identifier-syntax">level</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"removing frontmost group from proposition: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">from</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">from</span><span class="plain-syntax"> = </span><span class="identifier-syntax">position</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">opener</span><span class="plain-syntax"> = </span><span class="identifier-syntax">from</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">closer</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Atoms::element_get_match</span><span class="plain-syntax">(</span><span class="identifier-syntax">opener</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">closer</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to remove frontmost group which doesn't open"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">from</span><span class="plain-syntax"> = </span><span class="identifier-syntax">from</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP17" class="function-link"><span class="function-syntax">Calculus::Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove opening atom</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">from</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">closer</span><span class="plain-syntax">) { </span><span class="comment-syntax"> the special case of an empty group</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP17" class="function-link"><span class="function-syntax">Calculus::Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove opening atom</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">goto</span><span class="plain-syntax"> </span><span class="identifier-syntax">Ungrouped</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">level</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">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">from</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">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">opener</span><span class="plain-syntax">) </span><span class="identifier-syntax">level</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">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">closer</span><span class="plain-syntax">) </span><span class="identifier-syntax">level</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">level</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">last</span><span class="plain-syntax">) *</span><span class="identifier-syntax">last</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP17" class="function-link"><span class="function-syntax">Calculus::Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove closing atom</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">goto</span><span class="plain-syntax"> </span><span class="identifier-syntax">Ungrouped</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">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to remove frontmost group which doesn't close"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">Ungrouped:</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"to ungrouped result: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP32" class="paragraph-anchor"></a><b>§32. </b>Occasionally we want to strip away a "for all", and since that is always
|
|
followed by a domain specification, we must also ungroup this:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::trim_universal_quantifier</span><button class="popup" onclick="togglePopup('usagePopup31')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup31">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::trim_universal_quantifier</span></span>:<br/>Descriptions - <a href="14-ds.html#SP6">§6</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">Calculus::Atoms::is_for_all_x</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)) &&</span>
|
|
<span class="plain-syntax"> (</span><a href="11-pr.html#SP19" class="function-link"><span class="function-syntax">Calculus::Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">2</span><span class="plain-syntax">, </span><span class="identifier-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">))) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP31" class="function-link"><span class="function-syntax">Calculus::Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-pr.html#SP17" class="function-link"><span class="function-syntax">Calculus::Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"Calculus::Propositions::trim_universal_quantifier: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP33" class="paragraph-anchor"></a><b>§33. </b>Less ambitiously:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::remove_final_close_domain</span><button class="popup" onclick="togglePopup('usagePopup32')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup32">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::remove_final_close_domain</span></span>:<br/>Sentence Conversions - <a href="11-sc.html#SP1_13">§1.13</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">move_domain</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> *</span><span class="identifier-syntax">move_domain</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_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</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">p</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">p</span><span class="plain-syntax">-></span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> *</span><span class="identifier-syntax">move_domain</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="11-pr.html#SP17" class="function-link"><span class="function-syntax">Calculus::Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">p_prev</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">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP34" class="paragraph-anchor"></a><b>§34. </b>The following routine takes a SP and returns the best proposition it can,
|
|
with a single unbound variable, to represent SP.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Propositions::from_spec</span><button class="popup" onclick="togglePopup('usagePopup33')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup33">Usage of <span class="code-font"><span class="function-syntax">Calculus::Propositions::from_spec</span></span>:<br/>Sentence Conversions - <a href="11-sc.html#SP1_3">§1.3</a>, <a href="11-sc.html#SP3_4">§3.4</a><br/>Deciding to Defer - <a href="12-dtd.html#SP9">§9</a>, <a href="12-dtd.html#SP12">§12</a>, <a href="12-dtd.html#SP14">§14</a>, <a href="12-dtd.html#SP16">§16</a>, <a href="12-dtd.html#SP17">§17</a>, <a href="12-dtd.html#SP19">§19</a>, <a href="12-dtd.html#SP20">§20</a>, <a href="12-dtd.html#SP21">§21</a>, <a href="12-dtd.html#SP22">§22</a>, <a href="12-dtd.html#SP23">§23</a><br/>Descriptions - <a href="14-ds.html#SP9">§9</a></span></button><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="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">spec</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="identifier-syntax">NULL</span><span class="plain-syntax">; </span><span class="comment-syntax"> the null description is universally true</span>
|
|
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="14-sp.html#SP3" class="function-link"><span class="function-syntax">Specifications::is_description</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="14-ds.html#SP1" class="function-link"><span class="function-syntax">Descriptions::to_proposition</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="identifier-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="14-sp.html#SP3" class="function-link"><span class="function-syntax">Specifications::to_proposition</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">prop</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="comment-syntax"> a propositional form is already made</span>
|
|
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="11-pr.html#SP34_1" class="named-paragraph-link"><span class="named-paragraph">If this is an instance of a kind, but can be used adjectivally, convert it as such</span><span class="named-paragraph-number">34.1</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="11-pr.html#SP34_2" class="named-paragraph-link"><span class="named-paragraph">If it's an either-or property name, it must be being used adjectivally</span><span class="named-paragraph-number">34.2</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="11-pr.html#SP34_3" class="named-paragraph-link"><span class="named-paragraph">It must be an ordinary noun</span><span class="named-paragraph-number">34.3</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP34_1" class="paragraph-anchor"></a><b>§34.1. </b>For example, if we have written:
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>Colour is a kind of value. The colours are pink, green and black. A thing has a colour.</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">then "pink" is both a noun and an adjective. If SP is its representation as a
|
|
noun, we return the proposition testing it adjectivally: {\it pink}(\(x\)).
|
|
</p>
|
|
|
|
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">If this is an instance of a kind, but can be used adjectivally, convert it as such</span><span class="named-paragraph-number">34.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">instance</span><span class="plain-syntax"> *</span><span class="identifier-syntax">I</span><span class="plain-syntax"> = </span><a href="14-rv.html#SP3" class="function-link"><span class="function-syntax">Rvalues::to_instance</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">I</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pname</span><span class="plain-syntax"> = </span><a href="15-cp.html#SP5" class="function-link"><span class="function-syntax">Properties::Conditions::get_coinciding_property</span></a><span class="plain-syntax">(</span><a href="6-ins.html#SP17" class="function-link"><span class="function-syntax">Instances::to_kind</span></a><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">pname</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Atoms::unary_PREDICATE_from_aph</span><span class="plain-syntax">(</span><a href="6-ins.html#SP34" class="function-link"><span class="function-syntax">Instances::get_adjective</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">I</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="11-pr.html#SP34_1_1" class="named-paragraph-link"><span class="named-paragraph">Typecheck the propositional form, and return</span><span class="named-paragraph-number">34.1.1</span></a></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="11-pr.html#SP34">§34</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP34_2" class="paragraph-anchor"></a><b>§34.2. </b>For example, if the SP is "scenery", we return the proposition {\it scenery}(\(x\)).
|
|
</p>
|
|
|
|
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">If it's an either-or property name, it must be being used adjectivally</span><span class="named-paragraph-number">34.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><a href="14-rv.html#SP19" class="function-link"><span class="function-syntax">Rvalues::is_CONSTANT_construction</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">CON_property</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prn</span><span class="plain-syntax"> = </span><a href="14-rv.html#SP2" class="function-link"><span class="function-syntax">Rvalues::to_property</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="15-pr.html#SP15" class="function-link"><span class="function-syntax">Properties::is_either_or</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prn</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Atoms::unary_PREDICATE_from_aph</span><span class="plain-syntax">(</span>
|
|
<span class="plain-syntax"> </span><a href="15-ep.html#SP8" class="function-link"><span class="function-syntax">Properties::EitherOr::get_aph</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prn</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="11-pr.html#SP34_1_1" class="named-paragraph-link"><span class="named-paragraph">Typecheck the propositional form, and return</span><span class="named-paragraph-number">34.1.1</span></a></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="11-pr.html#SP34">§34</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP34_3" class="paragraph-anchor"></a><b>§34.3. </b>For example, if the SP is the number 17, we return the proposition {\it is}(\(x\), 17).
|
|
</p>
|
|
|
|
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">It must be an ordinary noun</span><span class="named-paragraph-number">34.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">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Calculus::Atoms::prop_x_is_constant</span><span class="plain-syntax">(</span><span class="identifier-syntax">Node::duplicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">));</span>
|
|
<span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="11-pr.html#SP34_1_1" class="named-paragraph-link"><span class="named-paragraph">Typecheck the propositional form, and return</span><span class="named-paragraph-number">34.1.1</span></a></span><span class="plain-syntax">;</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="11-pr.html#SP34">§34</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP34_1_1" class="paragraph-anchor"></a><b>§34.1.1. </b>In all cases, we finish by doing the following. In the one-atom noun cases
|
|
it's a formality, but we want to enforce the rule that all propositions
|
|
created in Inform go through type-checking, so:
|
|
</p>
|
|
|
|
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Typecheck the propositional form, and return</span><span class="named-paragraph-number">34.1.1</span></span><span class="comment-syntax"> =</span>
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> </span><a href="11-tcp.html#SP5" class="function-link"><span class="function-syntax">Calculus::Propositions::Checker::type_check</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><a href="11-tcp.html#SP3" class="function-link"><span class="function-syntax">Calculus::Propositions::Checker::tc_no_problem_reporting</span></a><span class="plain-syntax">());</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="11-pr.html#SP34_1">§34.1</a>, <a href="11-pr.html#SP34_2">§34.2</a>, <a href="11-pr.html#SP34_3">§34.3</a>.</li></ul>
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprev"><a href="10-cap.html">❮</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bv.html">3</a></li><li class="progresschapter"><a href="4-dlr.html">4</a></li><li class="progresschapter"><a href="5-rpt.html">5</a></li><li class="progresschapter"><a href="6-lp.html">6</a></li><li class="progresschapter"><a href="7-am.html">7</a></li><li class="progresschapter"><a href="8-ptu.html">8</a></li><li class="progresschapter"><a href="9-ef.html">9</a></li><li class="progresschapter"><a href="10-its.html">10</a></li><li class="progresscurrentchapter">11</li><li class="progresscurrent">pr</li><li class="progresssection"><a href="11-bas.html">bas</a></li><li class="progresssection"><a href="11-tc.html">tc</a></li><li class="progresssection"><a href="11-sc.html">sc</a></li><li class="progresssection"><a href="11-sm.html">sm</a></li><li class="progresssection"><a href="11-tcp.html">tcp</a></li><li class="progresschapter"><a href="12-ter.html">12</a></li><li class="progresschapter"><a href="13-kak.html">13</a></li><li class="progresschapter"><a href="14-sp.html">14</a></li><li class="progresschapter"><a href="15-pr.html">15</a></li><li class="progresschapter"><a href="16-is.html">16</a></li><li class="progresschapter"><a href="17-tl.html">17</a></li><li class="progresschapter"><a href="18-lc.html">18</a></li><li class="progresschapter"><a href="19-tc.html">19</a></li><li class="progresschapter"><a href="20-eq.html">20</a></li><li class="progresschapter"><a href="21-rl.html">21</a></li><li class="progresschapter"><a href="22-itp.html">22</a></li><li class="progresschapter"><a href="23-ad.html">23</a></li><li class="progresschapter"><a href="24-lv.html">24</a></li><li class="progresschapter"><a href="25-in.html">25</a></li><li class="progresschapter"><a href="26-fc.html">26</a></li><li class="progresschapter"><a href="27-hr.html">27</a></li><li class="progressnext"><a href="11-bas.html">❯</a></li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|