mirror of
https://github.com/ganelson/inform.git
synced 2024-07-05 08:34:22 +03:00
983 lines
188 KiB
HTML
983 lines
188 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="../index.html">home</a></li>
|
|
</ul><h2>Compiler</h2><ul>
|
|
<li><a href="../structure.html">structure</a></li>
|
|
<li><a href="../inbuildn.html">inbuild</a></li>
|
|
<li><a href="../inform7n.html">inform7</a></li>
|
|
<li><a href="../intern.html">inter</a></li>
|
|
<li><a href="../services.html">services</a></li>
|
|
<li><a href="../secrets.html">secrets</a></li>
|
|
</ul><h2>Other Tools</h2><ul>
|
|
<li><a href="../inblorbn.html">inblorb</a></li>
|
|
<li><a href="../indocn.html">indoc</a></li>
|
|
<li><a href="../inform6.html">inform6</a></li>
|
|
<li><a href="../inpolicyn.html">inpolicy</a></li>
|
|
<li><a href="../inrtpsn.html">inrtps</a></li>
|
|
</ul><h2>Resources</h2><ul>
|
|
<li><a href="../extensions.html">extensions</a></li>
|
|
<li><a href="../kits.html">kits</a></li>
|
|
</ul><h2>Repository</h2><ul>
|
|
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=18> github</a></li>
|
|
</ul><h2>Related Projects</h2><ul>
|
|
<li><a href="../../../inweb/index.html">inweb</a></li>
|
|
<li><a href="../../../intest/index.html">intest</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
<!--Weave of 'Propositions' generated by Inweb-->
|
|
<div class="breadcrumbs">
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#4">Chapter 4: Propositions</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="4-prp.html#SP1">§1. Internal representation</a></li><li><a href="4-prp.html#SP4">§4. Walking through propositions</a></li><li><a href="4-prp.html#SP8">§8. Validity</a></li><li><a href="4-prp.html#SP11">§11. Complexity</a></li><li><a href="4-prp.html#SP12">§12. Primitive operations on propositions</a></li><li><a href="4-prp.html#SP17">§17. Inserting and deleting atoms</a></li><li><a href="4-prp.html#SP20">§20. Miscellaneous further operations</a></li><li><a href="4-prp.html#SP21">§21. Inspecting contents</a></li><li><a href="4-prp.html#SP22">§22. Matching sequences of atoms</a></li><li><a href="4-prp.html#SP31">§31. Bracketed groups</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>§1. Internal representation. </b>There is no perfectly convenient way to represent propositions. The two
|
|
obvious strategies are:
|
|
</p>
|
|
|
|
<ul class="items"><li>(a) Hold them more or less as written, in a flat sequence of atoms.
|
|
</li><li>(b) Hold them in a tree which branches at each logical operation.
|
|
</li></ul>
|
|
<p class="commentary">We follow (a), which is easier to iterate through without tiresome amounts
|
|
of recursion, but comes at the cost of extra complexity when it comes to
|
|
grouping the terms — this is why we need the awkward <span class="extract"><span class="extract-syntax">NOT<</span></span> and <span class="extract"><span class="extract-syntax">NOT></span></span>
|
|
atoms, for example. (b) would almost certainly be better if we needed to
|
|
accommodate disjunction as well as conjunction, but we do not. The main
|
|
demerit of (a) is that it is easy to make malformed propositions, so we have
|
|
to build and edit carefully.
|
|
</p>
|
|
|
|
<p class="commentary">So propositions are represented by the <a href="4-ap.html#SP1" class="internal">pcalc_prop</a> object at the front, an
|
|
atomic proposition, and this leads via its <span class="extract"><span class="extract-syntax">next</span></span> field to a second atomit
|
|
proposition, and so on. 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.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>§2. </b>In particular:
|
|
</p>
|
|
|
|
<ul class="items"><li>(1) 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>(2) The conjunction \(\alpha\land\beta\) is almost the concatenation of their
|
|
linked lists <span class="extract"><span class="extract-syntax">A --> B</span></span>, except that we must be careful if they appear to have
|
|
variables in common.
|
|
</li><li>(3) Negation \(\lnot(\phi)\) is the concatenation <span class="extract"><span class="extract-syntax">NOT< --> P --> NOT></span></span>,
|
|
where <span class="extract"><span class="extract-syntax">P</span></span> is the linked list for \(\phi\).
|
|
</li><li>(4) The quantifier \(Q v\in \lbrace v\mid\phi(v)\rbrace\) is
|
|
<span class="extract"><span class="extract-syntax">QUANTIFIER --> IN< --> P --> IN></span></span>, where <span class="extract"><span class="extract-syntax">P</span></span> is the linked list for \(\phi\).
|
|
</li></ul>
|
|
<p class="commentary">Conjunction occurs so densely in propositions arising from
|
|
natural language that we save a lot of memory and fuss by simply implying it:
|
|
thus "great green dragon" is <span class="extract"><span class="extract-syntax">PREDICATE --> PREDICATE --> PREDICATE</span></span>, rather than
|
|
something like <span class="extract"><span class="extract-syntax">PREDICATE --> AND_SIGN --> PREDICATE --> AND_SIGN --> PREDICATE</span></span>.
|
|
Disjunction hardly ever occurs, so although the above scheme could simulate
|
|
it with \(\alpha\lor\beta = \lnot((\lnot\alpha)\land(\lnot\beta))\), we never do.
|
|
</p>
|
|
|
|
<p class="commentary">The following function determines whether or not <span class="extract"><span class="extract-syntax">P1 --> P2</span></span> should be
|
|
understood as a conjunction.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::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">Propositions::implied_conjunction_between</span></span>:<br/><a href="4-prp.html#SP3">§3</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="reserved-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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-></span><span class="element-syntax">element</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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p2</span><span class="plain-syntax">-></span><span class="element-syntax">element</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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="SP3" class="paragraph-anchor"></a><b>§3. </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">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">Propositions::debugging_log_text_between</span></span>:<br/><a href="4-prp.html#SP7">§7</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="reserved-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="4-prp.html#SP2" class="function-link"><span class="function-syntax">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="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 Inter 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="SP4" class="paragraph-anchor"></a><b>§4. Walking through propositions. </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 we use is that a position marker
|
|
points to the //<span class="extract"><span class="extract-syntax">pcalc_prop// structure for the atom before the position
|
|
</span></span>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="SP5" class="paragraph-anchor"></a><b>§5. </b>The code needed to walk through 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="reserved-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="SP6" class="paragraph-anchor"></a><b>§6. </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="SP7" class="paragraph-anchor"></a><b>§7. </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">void</span><span class="plain-syntax"> </span><span class="function-syntax">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">Propositions::log</span></span>:<br/>Calculus Module - <a href="1-cm.html#SP3">§3</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><a href="4-prp.html#SP7" class="function-link"><span class="function-syntax">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">Propositions::write</span><span class="plain-syntax">(</span><span class="identifier-syntax">OUTPUT_STREAM</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="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="4-prp.html#SP3" class="function-link"><span class="function-syntax">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><a href="4-ap.html#SP14" class="function-link"><span class="function-syntax">Atoms::write</span></a><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="SP8" class="paragraph-anchor"></a><b>§8. 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="SP9" class="paragraph-anchor"></a><b>§9. </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">|IN< --> NOT> --> NOT>|</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(x) --> QUANTIFIER x --> PREDICATE(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(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="SP10" class="paragraph-anchor"></a><b>§10. </b>The following tests only (ii), validity. <a href="../calculus-test/index.html" class="internal">calculus-test</a> is unable to make
|
|
atoms which fail to pass <a href="4-ap.html#SP13" class="internal">Atoms::validate</a>, nor can it make some of the
|
|
misconstructions tested for below, but numerous other defects can be tested:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new binary sees (none, none)</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< kind = number (x) ^ even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< sees (4, 10) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (4 == 10) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (x == 10) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (10 == x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (y == x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< NOT< kind = number (x) ^ even (x) NOT> >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Exists x: even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< NOT> >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - too many close groups</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Exists x >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< ForAll x >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - nonexistential quantifier without domain</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< ForAll x IN< kind = number (x) IN>: even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< NOT< ^ NOT> ^ NOT> ^ NOT< ^ even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - too many close groups</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< NOT< ^ NOT< ^ even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - 2 group(s) open</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ NOT< ^ even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - group nesting too deep</span>
|
|
</pre>
|
|
<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">Propositions::is_syntactically_valid</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Propositions::is_syntactically_valid</span></span>:<br/>Binding and Substitution - <a href="4-bas.html#SP2">§2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">text_stream</span><span class="plain-syntax"> *</span><span class="identifier-syntax">err</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">v_err</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP13" class="function-link"><span class="function-syntax">Atoms::validate</span></a><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">v_err</span><span class="plain-syntax">) { </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"atom error: %s"</span><span class="plain-syntax">, </span><span class="identifier-syntax">err</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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">element</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">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"group nesting too deep"</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="element-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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">element</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">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"too many close groups"</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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::counterpart</span></a><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="element-syntax">element</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"group open/close doesn't match"</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:</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">)) && (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><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="element-syntax">element</span><span class="plain-syntax"> != </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"quantifier without domain"</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">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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"domain without quantifier"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">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><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)) && (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><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">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"nonexistential quantifier without domain"</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">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"%d group(s) open"</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="SP11" class="paragraph-anchor"></a><b>§11. 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. The only simple binary predicate is one which assigns a definite
|
|
value to <span class="extract"><span class="extract-syntax">x</span></span>. Examples:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new binary sees (none, none)</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< even (x) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< kind = number (x) ^ even (x) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< sees (4, 10) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (4 == 10) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (x == 10) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (10 == x) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (y == x) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< not< kind = number (x) ^ even (x) not> >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Exists x: even (x) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Forall x IN< kind = number (x) IN>: even (x) >> is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::is_complex</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><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="element-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="element-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="element-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="element-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="SP12" class="paragraph-anchor"></a><b>§12. Primitive operations on propositions. </b>Now for some basic operations, as shown in the following examples:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< NOT> >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - too many close groups</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< Exists x >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< ForAll x >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - nonexistential quantifier without domain</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< ForAll x IN< kind = number (x) IN>: even (x) >> is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">set A to << Exists x >></span><span class="plain-syntax">':</span><span class="string-syntax"> a set to << Exists x >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">set B to << Exists x: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> b set to << Exists x : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">A concatenate B</span><span class="plain-syntax">':</span><span class="string-syntax"> << Exists x : Exists x : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">A conjoin B</span><span class="plain-syntax">':</span><span class="string-syntax"> << Exists x : Exists y : even(y) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">A concatenate B is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">A conjoin B is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">A concatenate B is well-formed</span><span class="plain-syntax">':</span><span class="string-syntax"> false - x used outside its binding</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">A conjoin B is well-formed</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">set P to << Forall x IN< kind = number (x) IN>: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> p set to << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">copy of P</span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">negation of P</span><span class="plain-syntax">':</span><span class="string-syntax"> << NOT< ForAll x IN< kind=number(x) IN> : even(x) NOT> >></span>
|
|
</pre>
|
|
<p class="commentary">Note that the conjunction of A and B renamed the variable <span class="extract"><span class="extract-syntax">x</span></span> in B to <span class="extract"><span class="extract-syntax">y</span></span>,
|
|
so that it no longer clashed with the meaning of <span class="extract"><span class="extract-syntax">x</span></span> in A. The concatenation
|
|
did not, simply writing one after the other.
|
|
</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>§13. </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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::copy</span><button class="popup" onclick="togglePopup('usagePopup5')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup5">Usage of <span class="code-font"><span class="function-syntax">Propositions::copy</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP3">§3</a>, <a href="5-sc.html#SP3_4">§3.4</a></span></button><span class="plain-syntax">(</span><span class="reserved-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="reserved-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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(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="element-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><a href="4-trm.html#SP5" class="function-link"><span class="function-syntax">Terms::copy</span></a><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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::concatenate</span><button class="popup" onclick="togglePopup('usagePopup6')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup6">Usage of <span class="code-font"><span class="function-syntax">Propositions::concatenate</span></span>:<br/><a href="4-prp.html#SP15">§15</a>, <a href="4-prp.html#SP16">§16</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_13">§2.13</a>, <a href="5-sc.html#SP3_7">§3.7</a>, <a href="5-sc.html#SP3_8">§3.8</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, </span><span class="reserved-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="reserved-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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::conjoin</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, </span><span class="reserved-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="4-prp.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="4-prp.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="4-bas.html#SP8" class="function-link"><span class="function-syntax">Binding::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="4-prp.html#SP14" class="function-link"><span class="function-syntax">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</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="4-prp.html#SP15">§15</a> (twice).</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP16" class="paragraph-anchor"></a><b>§16. </b>Negation and quantification can be done with these shorthand functions:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::negate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
|
|
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">),</span>
|
|
<span class="plain-syntax"> </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">)));</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::quantify</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="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">parameter</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">domain</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">Q</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP6" class="function-link"><span class="function-syntax">Atoms::QUANTIFIER_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">quant</span><span class="plain-syntax">, </span><span class="identifier-syntax">v</span><span class="plain-syntax">, </span><span class="identifier-syntax">parameter</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP16" class="function-link"><span class="function-syntax">Propositions::quantify_using</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Q</span><span class="plain-syntax">, </span><span class="identifier-syntax">domain</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">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::quantify_using</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">Q</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">domain</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">domain</span><span class="plain-syntax">)</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">Q</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">Q</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
|
|
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">),</span>
|
|
<span class="plain-syntax"> </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">domain</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_CLOSE_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="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Q</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="SP17" class="paragraph-anchor"></a><b>§17. Inserting and deleting atoms. </b>These operations do what they say, but the result is often syntactically
|
|
invalid. Handle with care.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">set P to << Forall x IN< kind = number (x) IN>: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> p set to << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">insert << (1 == 2) >> at 0 in P</span><span class="plain-syntax">':</span><span class="string-syntax"> << ('1' == '2') ^ ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">insert << even (x) >> at 2 in P</span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< even(x) ^ kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">delete 0 from P</span><span class="plain-syntax">':</span><span class="string-syntax"> << IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">delete 4 from P</span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< kind=number(x) IN> >></span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP18" class="paragraph-anchor"></a><b>§18. </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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::insert_atom</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">Propositions::insert_atom</span></span>:<br/>Binding and Substitution - <a href="4-bas.html#SP10">§10</a><br/>Simplifications - <a href="5-smp.html#SP2_2">§2.2</a>, <a href="5-smp.html#SP3">§3</a>, <a href="5-smp.html#SP5">§5</a>, <a href="5-smp.html#SP6">§6</a>, <a href="5-smp.html#SP7">§7</a>, <a href="5-smp.html#SP9_3_2">§9.3.2</a>, <a href="5-smp.html#SP14">§14</a>, <a href="5-smp.html#SP18">§18</a>, <a href="5-smp.html#SP19">§19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">-></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="SP19" class="paragraph-anchor"></a><b>§19. </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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::delete_atom</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Propositions::delete_atom</span></span>:<br/><a href="4-prp.html#SP34">§34</a>, <a href="4-prp.html#SP35">§35</a>, <a href="4-prp.html#SP36">§36</a><br/>Simplifications - <a href="5-smp.html#SP9_3_1">§9.3.1</a>, <a href="5-smp.html#SP9_3_2">§9.3.2</a>, <a href="5-smp.html#SP9_4">§9.4</a>, <a href="5-smp.html#SP13">§13</a>, <a href="5-smp.html#SP14">§14</a>, <a href="5-smp.html#SP16_1">§16.1</a>, <a href="5-smp.html#SP18">§18</a>, <a href="5-smp.html#SP19">§19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"deleting atom nowhere"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></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="SP20" class="paragraph-anchor"></a><b>§20. Miscellaneous further operations. </b>The rest of this section is given over to miscellaneous utility functions:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">new binary sees (none, sees-f1)</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">set P to << Forall x IN< kind = number (x) IN>: even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> p set to << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">copy of P</span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">set Q to negation of P</span><span class="plain-syntax">':</span><span class="string-syntax"> q set to << NOT< ForAll x IN< kind=number(x) IN> : even(x) NOT> >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">P is a group</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">Q is a group</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">unnegation of Q</span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< kind=number(x) IN> : even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">remove universal quantifier from P</span><span class="plain-syntax">':</span><span class="string-syntax"> << kind=number(x) ^ even(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">set R to delete 4 from P</span><span class="plain-syntax">':</span><span class="string-syntax"> r set to << ForAll x IN< kind=number(x) IN> >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">remove close domain from R</span><span class="plain-syntax">':</span><span class="string-syntax"> << ForAll x IN< kind=number(x) >></span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">P contains quantifier</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">P contains relation</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (1 == 2) >> contains relation</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax"><< (1 == 2) ^ even (x) >> contains quantifier</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">term first cited in << even (x) >></span><span class="plain-syntax">':</span><span class="string-syntax"> x</span>
|
|
<span class="plain-syntax">'</span><span class="element-syntax">term first cited in << not< sees (56, 2) not> >></span><span class="plain-syntax">':</span><span class="string-syntax"> '56'</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP21" class="paragraph-anchor"></a><b>§21. 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">Propositions::length</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="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="SP22" class="paragraph-anchor"></a><b>§22. 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 --> PREDICATE</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"> Propositions::match(p, 4,</span>
|
|
<span class="plain-syntax"> QUANTIFIER_ATOM, NULL,</span>
|
|
<span class="plain-syntax"> PREDICATE_ATOM, NULL, NULL,</span>
|
|
<span class="plain-syntax"> ANY_ATOM_HERE, NULL,</span>
|
|
<span class="plain-syntax"> PREDICATE_ATOM, &pp, NULL);</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. <span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span> atoms are followed by a third
|
|
parameter, which if not <span class="extract"><span class="extract-syntax">NULL</span></span> requires it to be a unary predicate of that
|
|
family. (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">pp</span></span>
|
|
points to the <span class="extract"><span class="extract-syntax">PREDICATE_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">Propositions::match</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Propositions::match</span></span>:<br/><a href="4-prp.html#SP35">§35</a><br/>Sentence Conversions - <a href="5-sc.html#SP3_4">§3.4</a><br/>Simplifications - <a href="5-smp.html#SP4">§4</a>, <a href="5-smp.html#SP5">§5</a>, <a href="5-smp.html#SP6">§6</a>, <a href="5-smp.html#SP9_2">§9.2</a>, <a href="5-smp.html#SP14">§14</a>, <a href="5-smp.html#SP18">§18</a>, <a href="5-smp.html#SP19">§19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">c</span><span class="plain-syntax">, ...) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">va_list</span><span class="plain-syntax"> </span><span class="identifier-syntax">ap</span><span class="plain-syntax">; </span><span class="comment-syntax"> the variable argument list signified by the dots</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">va_start</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax">); </span><span class="comment-syntax"> macro to begin variable argument processing</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax"> = </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="reserved-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="reserved-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">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">req_up</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">a</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) </span><span class="identifier-syntax">req_up</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">up_family</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="element-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">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">req_up</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">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> =</span>
|
|
<span class="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="element-syntax">predicate</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax"> != </span><span class="identifier-syntax">req_up</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="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="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="SP23" class="paragraph-anchor"></a><b>§23. </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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::prop_seek_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">Propositions::prop_seek_atom</span></span>:<br/><a href="4-prp.html#SP24">§24</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">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="element-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="element-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>
|
|
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::prop_seek_up_family</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">Propositions::prop_seek_up_family</span></span>:<br/><a href="4-prp.html#SP24">§24</a>, <a href="4-prp.html#SP25">§25</a>, <a href="4-prp.html#SP30">§30</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</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">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">f</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="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>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">Propositions::contains_binary_predicate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-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">Propositions::contains_quantifier</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::composited_kind</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">Propositions::composited_kind</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_13_1">§2.13.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-kp.html#SP4" class="function-link"><span class="function-syntax">KindPredicates::is_composited_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">k_atom</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">Propositions::contains_nonexistence_quantifier</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="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="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-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="element-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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP25" class="paragraph-anchor"></a><b>§25. </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">Propositions::describes_kind</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-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="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</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><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><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="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><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">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="4-prp.html#SP26" class="function-link"><span class="function-syntax">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><span class="identifier-syntax">VALUE_TO_KIND_FUNCTION</span><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="SP26" class="paragraph-anchor"></a><b>§26. </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">Propositions::describes_value</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">Propositions::describes_value</span></span>:<br/><a href="4-prp.html#SP25">§25</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">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="element-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><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><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="element-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="element-syntax">constant</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">constant</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-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="element-syntax">constant</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-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="SP27" class="paragraph-anchor"></a><b>§27. </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="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::contains_adjective</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-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="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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">)</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="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">Propositions::count_adjectives</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="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="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-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="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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) &&</span>
|
|
<span class="plain-syntax"> (</span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><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="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">) </span><span class="identifier-syntax">ac</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>
|
|
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP28" class="paragraph-anchor"></a><b>§28. </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="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::get_first_cited_term</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">Propositions::get_first_cited_term</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP3_4">§3.4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="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">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">"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><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><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="SP29" class="paragraph-anchor"></a><b>§29. </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="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
|
|
<span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::convert_adj_to_noun</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">Propositions::convert_adj_to_noun</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP3_6">§3.6</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pct</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><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><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</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">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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">)</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-trm.html#SP9" class="function-link"><span class="function-syntax">Terms::adj_to_noun_conversion</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">up</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><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::is_kind_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pname</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Properties::property_with_same_name_as</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pname</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Rvalues::from_property</span><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>
|
|
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP30" class="paragraph-anchor"></a><b>§30. </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="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
|
|
<span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::first_unary_predicate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-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="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">adjectival_up_family</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><a href="4-ap.html#SP9" class="function-link"><span class="function-syntax">Atoms::to_adjectival_usage</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">unary_predicate</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::next_unary_predicate</span><span class="plain-syntax">(</span><span class="reserved-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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</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">adjectival_up_family</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><a href="4-ap.html#SP9" class="function-link"><span class="function-syntax">Atoms::to_adjectival_usage</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="plain-syntax">#</span><span class="identifier-syntax">endif</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP31" class="paragraph-anchor"></a><b>§31. 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"> NOT< --> PREDICATE --> NOT></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">Propositions::is_a_group</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">Propositions::is_a_group</span></span>:<br/><a href="4-prp.html#SP32">§32</a>, <a href="4-prp.html#SP33">§33</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::counterpart</span></a><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">"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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">element</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><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-></span><span class="element-syntax">element</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="element-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="SP32" class="paragraph-anchor"></a><b>§32. </b>The following removes matched parentheses, leaving just the interior:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::remove_topmost_group</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">Propositions::remove_topmost_group</span></span>:<br/><a href="4-prp.html#SP33">§33</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="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="4-prp.html#SP31" class="function-link"><span class="function-syntax">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="element-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="SP33" class="paragraph-anchor"></a><b>§33. </b>The main application of which is to remove negation:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::unnegate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP31" class="function-link"><span class="function-syntax">Propositions::is_a_group</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP32" class="function-link"><span class="function-syntax">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="SP34" class="paragraph-anchor"></a><b>§34. </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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::ungroup_after</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">Propositions::ungroup_after</span></span>:<br/><a href="4-prp.html#SP35">§35</a><br/>Simplifications - <a href="5-smp.html#SP5">§5</a>, <a href="5-smp.html#SP14">§14</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="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="reserved-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="element-syntax">element</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">closer</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::counterpart</span></a><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="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</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="element-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="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</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="element-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="element-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="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">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="SP35" class="paragraph-anchor"></a><b>§35. </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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::trim_universal_quantifier</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_for_all_x</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)) &&</span>
|
|
<span class="plain-syntax"> (</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">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="plain-syntax"> </span><span class="constant-syntax">QUANTIFIER_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="constant-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="4-prp.html#SP34" class="function-link"><span class="function-syntax">Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">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="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">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">"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="SP36" class="paragraph-anchor"></a><b>§36. </b>Less ambitiously:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::remove_final_close_domain</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">Propositions::remove_final_close_domain</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_13">§2.13</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">move_domain</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">move_domain</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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_CLOSE_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">move_domain</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="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">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>
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprev"><a href="4-ap.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-bpf.html">3</a></li><li class="progresscurrentchapter">4</li><li class="progresssection"><a href="4-trm.html">trm</a></li><li class="progresssection"><a href="4-ap.html">ap</a></li><li class="progresscurrent">prp</li><li class="progresssection"><a href="4-bas.html">bas</a></li><li class="progresssection"><a href="4-tcp.html">tcp</a></li><li class="progresschapter"><a href="5-sc.html">5</a></li><li class="progressnext"><a href="4-bas.html">❯</a></li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|