mirror of
https://github.com/ganelson/inform.git
synced 2024-07-17 06:24:24 +03:00
642 lines
128 KiB
HTML
642 lines
128 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>Atomic Propositions</title>
|
|
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<meta name="viewport" content="width=device-width initial-scale=1">
|
|
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
|
|
<meta http-equiv="Content-Language" content="en-gb">
|
|
|
|
<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<script>
|
|
MathJax = {
|
|
tex: {
|
|
inlineMath: '$', '$'], ['\\(', '\\)'
|
|
},
|
|
svg: {
|
|
fontCache: 'global'
|
|
}
|
|
};
|
|
</script>
|
|
<script type="text/javascript" id="MathJax-script" async
|
|
src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
|
|
</script>
|
|
|
|
<script>
|
|
function togglePopup(material_id) {
|
|
var popup = document.getElementById(material_id);
|
|
popup.classList.toggle("show");
|
|
}
|
|
</script>
|
|
|
|
<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
|
|
</head>
|
|
<body class="commentary-font">
|
|
<nav role="navigation">
|
|
<h1><a href="../index.html">
|
|
<img src="../docs-assets/Inform.png" height=72">
|
|
</a></h1>
|
|
<ul><li><a href="../compiler.html">compiler tools</a></li>
|
|
<li><a href="../other.html">other tools</a></li>
|
|
<li><a href="../extensions.html">extensions and kits</a></li>
|
|
<li><a href="../units.html">unit test tools</a></li>
|
|
</ul><h2>Compiler Webs</h2><ul>
|
|
<li><a href="../inbuild/index.html">inbuild</a></li>
|
|
<li><a href="../inform7/index.html">inform7</a></li>
|
|
<li><a href="../inter/index.html">inter</a></li>
|
|
</ul><h2>Inbuild Modules</h2><ul>
|
|
<li><a href="../supervisor-module/index.html">supervisor</a></li>
|
|
</ul><h2>Inform7 Modules</h2><ul>
|
|
<li><a href="index.html"><span class="selectedlink">core</span></a></li>
|
|
<li><a href="../kinds-module/index.html">kinds</a></li>
|
|
<li><a href="../if-module/index.html">if</a></li>
|
|
<li><a href="../multimedia-module/index.html">multimedia</a></li>
|
|
<li><a href="../index-module/index.html">index</a></li>
|
|
</ul><h2>Inter Modules</h2><ul>
|
|
<li><a href="../bytecode-module/index.html">bytecode</a></li>
|
|
<li><a href="../building-module/index.html">building</a></li>
|
|
<li><a href="../codegen-module/index.html">codegen</a></li>
|
|
</ul><h2>Services</h2><ul>
|
|
<li><a href="../arch-module/index.html">arch</a></li>
|
|
<li><a href="../syntax-module/index.html">syntax</a></li>
|
|
<li><a href="../words-module/index.html">words</a></li>
|
|
<li><a href="../html-module/index.html">html</a></li>
|
|
<li><a href="../inflections-module/index.html">inflections</a></li>
|
|
<li><a href="../linguistics-module/index.html">linguistics</a></li>
|
|
<li><a href="../problems-module/index.html">problems</a></li>
|
|
<li><a href="../../../inweb/docs/foundation-module/index.html">foundation</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
<!--Weave of 'Atomic Propositions' generated by Inweb-->
|
|
<div class="breadcrumbs">
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../compiler.html">Inform7 Modules</a></li><li><a href="index.html">core</a></li><li><a href="index.html#11">Chapter 11: Predicate Calculus</a></li><li><b>Atomic Propositions</b></li></ul></div>
|
|
<p class="purpose">To build and modify atoms, the syntactic pieces from which propositions are built up.</p>
|
|
|
|
<ul class="toc"><li><a href="11-ap.html#SP1">§1. Definitions</a></li><li><a href="11-ap.html#SP5">§5. The elements</a></li><li><a href="11-ap.html#SP7">§7. Creating atoms</a></li><li><a href="11-ap.html#SP8">§8. The STRUCTURAL group</a></li><li><a href="11-ap.html#SP11">§11. The PREDICATES group</a></li><li><a href="11-ap.html#SP24">§24. Validating atoms</a></li><li><a href="11-ap.html#SP25">§25. Debugging log</a></li></ul><hr class="tocbar">
|
|
|
|
<p class="commentary firstcommentary"><a id="SP1"></a><b>§1. Definitions. </b></p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP2"></a><b>§2. </b>As the description in the Introduction showed, propositions are complicated
|
|
data structures. Roughly speaking, they are made up of small independent pieces
|
|
which can be combined in a variety of ways into larger assemblies. In this
|
|
section, we look at the smallest pieces: some of these could be propositions in
|
|
their own right, others are only structural items needed to form up the
|
|
larger collections. But each individual piece, or "atom", is stored in
|
|
a <span class="extract"><span class="extract-syntax">pcalc_prop</span></span> structure.
|
|
</p>
|
|
|
|
<p class="commentary">The question of how these are joined together is left until the next section.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">MAX_ATOM_ARITY</span><span class="plain-syntax"> </span><span class="constant-syntax">2</span><span class="plain-syntax"> </span><span class="comment-syntax"> for the moment, at any rate</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">typedef</span><span class="plain-syntax"> </span><span class="reserved-syntax">struct</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">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">element</span><span class="plain-syntax">; </span><span class="comment-syntax"> one of the constants below: always 1 or greater</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">arity</span><span class="plain-syntax">; </span><span class="comment-syntax"> 1 for quantifiers and unary predicates; 2 for BPs; 0 otherwise</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="identifier-syntax">general_pointer</span><span class="plain-syntax"> </span><span class="identifier-syntax">predicate</span><span class="plain-syntax">; </span><span class="comment-syntax"> indicates which predicate structure is meant</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">terms</span><span class="plain-syntax">[</span><span class="constant-syntax">MAX_ATOM_ARITY</span><span class="plain-syntax">]; </span><span class="comment-syntax"> terms to which the predicate applies</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">assert_kind</span><span class="plain-syntax">; </span><span class="comment-syntax"> </span><span class="extract"><span class="extract-syntax">KIND_ATOM</span></span><span class="comment-syntax">: the kind of value of a variable</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">composited</span><span class="plain-syntax">; </span><span class="comment-syntax"> </span><span class="extract"><span class="extract-syntax">KIND_ATOM</span></span><span class="comment-syntax">: arises from a composite determiner/noun like "somewhere"</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">unarticled</span><span class="plain-syntax">; </span><span class="comment-syntax"> </span><span class="extract"><span class="extract-syntax">KIND_ATOM</span></span><span class="comment-syntax">: arises from an unarticled usage like "vehicle", not "a vehicle"</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">calling_name</span><span class="plain-syntax">; </span><span class="comment-syntax"> </span><span class="extract"><span class="extract-syntax">CALLED_ATOM</span></span><span class="comment-syntax">: text of the name this is called</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">struct</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="comment-syntax"> </span><span class="extract"><span class="extract-syntax">QUANTIFIER_ATOM</span></span><span class="comment-syntax">: which one</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">quantification_parameter</span><span class="plain-syntax">; </span><span class="comment-syntax"> </span><span class="extract"><span class="extract-syntax">QUANTIFIER_ATOM</span></span><span class="comment-syntax">: e.g., the 3 in "all three"</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">next</span><span class="plain-syntax">; </span><span class="comment-syntax"> next atom in the list for this proposition</span>
|
|
<span class="plain-syntax">} </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax">;</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>The structure pcalc_prop is accessed in 3/ptmn, 3/cs, 4/dlr, 4/pr, 4/tr, 4/nuor, 4/uor, 4/tr2, 4/dbtr, 4/rpr, 4/nar, 4/nlpr, 4/nrr, 4/npr, 4/nvr, 4/nar2, 5/rpt, 5/tc, 5/ass, 5/npa, 5/rk, 5/ass2, 5/imp, 6/lp, 6/ins, 7/rlt, 8/rs, 10/teav, 10/cap, 11/pr, 11/bas, 11/tc, 11/sc, 11/sm, 11/tcp, 12/ap, 12/ca, 12/dtd, 12/cad, 12/cdp, 14/rv, 14/lv, 14/cn, 14/ds, 14/ds2, 15/ps, 15/cp, 16/is, 16/in, 19/tb, 19/rsft, 20/eq, 21/rl, 21/rl2, 21/fao, 21/sv, 21/ac, 22/ph, 22/tp, 22/tp2, 23/ad, 24/lv, 24/sf, 25/in, 25/pi, 25/cii, 25/cp, 26/pc, 26/itc, 27/cm and here.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP3"></a><b>§3. </b>The Universe is filled with atoms, but they come in different kinds, called
|
|
elements. For us, an "element" is the identifying number, stored in the
|
|
<span class="extract"><span class="extract-syntax">element</span></span> field, which tells Inform what kind of atom something is. The
|
|
following is our Periodic Table of all possible elements:
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">define</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="comment-syntax"> any generalised quantifier</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">10</span><span class="plain-syntax"> </span><span class="comment-syntax"> a property-based unary predicate, or any predicate of higher arity</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">KIND_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">11</span><span class="plain-syntax"> </span><span class="comment-syntax"> a unary predicate </span>\(K(x)\)<span class="comment-syntax"> associated with a kind </span>\(K\)
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">ISAKIND_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">12</span><span class="plain-syntax"> </span><span class="comment-syntax"> a unary predicate asserting that </span>\(x\)<span class="comment-syntax"> is the world-object for a kind</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">ISAVAR_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">13</span><span class="plain-syntax"> </span><span class="comment-syntax"> a unary predicate asserting that </span>\(x\)<span class="comment-syntax"> is the SP for a global variable</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">ISACONST_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">14</span><span class="plain-syntax"> </span><span class="comment-syntax"> a unary predicate asserting that </span>\(x\)<span class="comment-syntax"> is the SP for a named constant</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">EVERYWHERE_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">15</span><span class="plain-syntax"> </span><span class="comment-syntax"> a unary predicate asserting omnipresence</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">NOWHERE_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">16</span><span class="plain-syntax"> </span><span class="comment-syntax"> a unary predicate asserting nonpresence</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">HERE_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">17</span><span class="plain-syntax"> </span><span class="comment-syntax"> a unary predicate asserting presence "here"</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">CALLED_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">18</span><span class="plain-syntax"> </span><span class="comment-syntax"> to keep track of "(called the intruder)"-style names</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">20</span><span class="plain-syntax"> </span><span class="comment-syntax"> logical negation </span>\(\lnot\)<span class="comment-syntax"> applied to contents of group</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">30</span><span class="plain-syntax"> </span><span class="comment-syntax"> end of logical negation </span>\(\lnot\)
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">21</span><span class="plain-syntax"> </span><span class="comment-syntax"> logical negation </span>\(\lnot\)<span class="comment-syntax"> applied to contents of group</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax"> </span><span class="constant-syntax">31</span><span class="plain-syntax"> </span><span class="comment-syntax"> end of logical negation </span>\(\lnot\)
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP4"></a><b>§4. </b>And as with columns in the Periodic Table, these elements come in what are
|
|
called "groups", because it often happens that atoms of different elements
|
|
behave similarly when the elements have something in common.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">STRUCTURAL_GROUP</span><span class="plain-syntax"> </span><span class="constant-syntax">10</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">PREDICATES_GROUP</span><span class="plain-syntax"> </span><span class="constant-syntax">20</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">OPEN_OPERATORS_GROUP</span><span class="plain-syntax"> </span><span class="constant-syntax">30</span>
|
|
<span class="definition-keyword">define</span> <span class="constant-syntax">CLOSE_OPERATORS_GROUP</span><span class="plain-syntax"> </span><span class="constant-syntax">40</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP5"></a><b>§5. The elements. </b>Given an element, the following returns the group to which it belongs.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::element_get_group</span><button class="popup" onclick="togglePopup('usagePopup1')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup1">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::element_get_group</span></span>:<br/><a href="11-ap.html#SP24">§24</a><br/>Propositions - <a href="11-pr.html#SP7">§7</a>, <a href="11-pr.html#SP12">§12</a>, <a href="11-pr.html#SP29">§29</a><br/>Binding and Substitution - <a href="11-bas.html#SP4">§4</a><br/>Simplifications - <a href="11-sm.html#SP10_1">§10.1</a>, <a href="11-sm.html#SP10_2">§10.2</a>, <a href="11-sm.html#SP10_3">§10.3</a>, <a href="11-sm.html#SP10_3_1">§10.3.1</a>, <a href="11-sm.html#SP10_4">§10.4</a>, <a href="11-sm.html#SP14">§14</a>, <a href="11-sm.html#SP14_1">§14.1</a><br/>Compile Deferred Propositions - <a href="12-cdp.html#SP5_1">§5.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">element</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="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">element</span><span class="plain-syntax"> < </span><span class="constant-syntax">STRUCTURAL_GROUP</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">STRUCTURAL_GROUP</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">element</span><span class="plain-syntax"> < </span><span class="constant-syntax">PREDICATES_GROUP</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">PREDICATES_GROUP</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">element</span><span class="plain-syntax"> < </span><span class="constant-syntax">OPEN_OPERATORS_GROUP</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">OPEN_OPERATORS_GROUP</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">element</span><span class="plain-syntax"> < </span><span class="constant-syntax">CLOSE_OPERATORS_GROUP</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">CLOSE_OPERATORS_GROUP</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP6"></a><b>§6. </b>Some atoms occur in pairs, which have to match like opening and closing
|
|
parentheses. The following returns 0 for an element code which does not behave
|
|
like this, or else returns the opposite number to any element code which does.
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::element_get_match</span><button class="popup" onclick="togglePopup('usagePopup2')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup2">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::element_get_match</span></span>:<br/>Propositions - <a href="11-pr.html#SP12">§12</a>, <a href="11-pr.html#SP29">§29</a>, <a href="11-pr.html#SP32">§32</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEGATION_OPEN_ATOM:</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><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">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEGATION_CLOSE_ATOM:</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">NEGATION_OPEN_ATOM</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="reserved-syntax">return</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">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">DOMAIN_CLOSE_ATOM:</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">default:</span><span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP7"></a><b>§7. Creating atoms. </b>Every atom is created by the following routine:
|
|
</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">Calculus::Atoms::new</span><button class="popup" onclick="togglePopup('usagePopup3')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup3">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::new</span></span>:<br/><a href="11-ap.html#SP8">§8</a>, <a href="11-ap.html#SP11">§11</a>, <a href="11-ap.html#SP12">§12</a>, <a href="11-ap.html#SP13">§13</a>, <a href="11-ap.html#SP14">§14</a>, <a href="11-ap.html#SP15">§15</a>, <a href="11-ap.html#SP16">§16</a>, <a href="11-ap.html#SP17">§17</a>, <a href="11-ap.html#SP18">§18</a>, <a href="11-ap.html#SP20">§20</a>, <a href="11-ap.html#SP21">§21</a><br/>Implications - <a href="5-imp.html#SP7_1_3">§7.1.3</a><br/>Propositions - <a href="11-pr.html#SP14">§14</a><br/>Tree Conversions - <a href="11-tc.html#SP7_2">§7.2</a><br/>Sentence Conversions - <a href="11-sc.html#SP1_13">§1.13</a>, <a href="11-sc.html#SP3_8">§3.8</a><br/>Simplifications - <a href="11-sm.html#SP3_2">§3.2</a>, <a href="11-sm.html#SP6">§6</a>, <a href="11-sm.html#SP7">§7</a>, <a href="11-sm.html#SP19">§19</a><br/>Deciding to Defer - <a href="12-dtd.html#SP13">§13</a><br/>Descriptions - <a href="14-ds.html#SP9">§9</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">element</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">CREATE</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">element</span><span class="plain-syntax"> = </span><span class="identifier-syntax">element</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">assert_kind</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><span class="identifier-syntax">composited</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">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">unarticled</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">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL_GENERAL_POINTER</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">quant</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">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP8"></a><b>§8. The STRUCTURAL group. </b>Some convenient routines to handle atoms of specific elements now follow:
|
|
first, <span class="extract"><span class="extract-syntax">QUANTIFIER</span></span> atoms. These have arity 1, and the single term must always
|
|
be a variable, the one which is being bound. The parameter is a number
|
|
needed for some <span class="extract"><span class="extract-syntax">quantifier</span></span> types to identify the range: for instance,
|
|
it would be 7 in the case of \(V_{=7}\).
|
|
</p>
|
|
|
|
<p class="commentary">Tying specific variables to quantifiers seems to be out of fashion in
|
|
modern computer science. Contemporary theorem-proving assistants mostly
|
|
use de Bruijn's numbering scheme, in which numbers 1, 2, 3, ..., refer
|
|
to variables being quantified in an indirect way. The advantage is that
|
|
propositions are easier to construct, since the same numbers can be used
|
|
in different subexpressions of the same proposition, and there's no
|
|
worrying about clashes. But it all just moves the difficulty elsewhere,
|
|
by making it less obvious how to pair up the numbers with variables at
|
|
compilation time, and less obvious even how many variables are needed.
|
|
So we stick to the old-fashioned way of imitating \(\forall x: P(x)\)
|
|
rather than \(\forall 1. P\).
|
|
</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">Calculus::Atoms::QUANTIFIER_new</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::QUANTIFIER_new</span></span>:<br/>Binding and Substitution - <a href="11-bas.html#SP12">§12</a><br/>Tree Conversions - <a href="11-tc.html#SP1">§1</a><br/>Simplifications - <a href="11-sm.html#SP3_2">§3.2</a>, <a href="11-sm.html#SP4">§4</a><br/>Descriptions - <a href="14-ds.html#SP9">§9</a></span></button><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">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">QUANTIFIER_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><a href="11-tr.html#SP4" class="function-link"><span class="function-syntax">Calculus::Terms::new_variable</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">v</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">quant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">quant</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">quantification_parameter</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><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP9"></a><b>§9. </b>Quantifier atoms can be detected as follows:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_quantifier</span><button class="popup" onclick="togglePopup('usagePopup5')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup5">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_quantifier</span></span>:<br/>Propositions - <a href="11-pr.html#SP12">§12</a><br/>Simplifications - <a href="11-sm.html#SP14_1">§14.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">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="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">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">quantifier</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Atoms::get_quantifier</span><button class="popup" onclick="togglePopup('usagePopup6')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup6">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::get_quantifier</span></span>:<br/>Descriptions - <a href="14-ds.html#SP9">§9</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) && (</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">QUANTIFIER_ATOM</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">quant</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">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::get_quantification_parameter</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::get_quantification_parameter</span></span>:<br/>Compile Deferred Propositions - <a href="12-cdp.html#SP2_1_6_1_2_3">§2.1.6.1.2.3</a><br/>Descriptions - <a href="14-ds.html#SP9">§9</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) && (</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">QUANTIFIER_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="element-syntax">quantification_parameter</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</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">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_existence_quantifier</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_existence_quantifier</span></span>:<br/>Propositions - <a href="11-pr.html#SP12">§12</a>, <a href="11-pr.html#SP27">§27</a><br/>Simplifications - <a href="11-sm.html#SP5">§5</a>, <a href="11-sm.html#SP7">§7</a>, <a href="11-sm.html#SP10_2">§10.2</a>, <a href="11-sm.html#SP14_1">§14.1</a><br/>Deciding to Defer - <a href="12-dtd.html#SP11_1">§11.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">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="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="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">exists_quantifier</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_nonexistence_quantifier</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_nonexistence_quantifier</span></span>:<br/>Simplifications - <a href="11-sm.html#SP10_2">§10.2</a>, <a href="11-sm.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="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="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="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">not_exists_quantifier</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_forall_quantifier</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_forall_quantifier</span></span>:<br/>Simplifications - <a href="11-sm.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="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="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="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">for_all_quantifier</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_notall_quantifier</span><button class="popup" onclick="togglePopup('usagePopup11')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup11">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_notall_quantifier</span></span>:<br/>Simplifications - <a href="11-sm.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="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="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="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">quant</span><span class="plain-syntax"> == </span><span class="identifier-syntax">not_for_all_quantifier</span><span class="plain-syntax">))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_for_all_x</span><button class="popup" onclick="togglePopup('usagePopup12')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup12">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_for_all_x</span></span>:<br/>Propositions - <a href="11-pr.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="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="11-ap.html#SP9" class="function-link"><span class="function-syntax">Calculus::Atoms::is_forall_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="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="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="SP10"></a><b>§10. </b>See "Determiners and Quantifiers" for what a now-assertable quantifier is:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_now_assertable_quantifier</span><button class="popup" onclick="togglePopup('usagePopup13')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup13">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_now_assertable_quantifier</span></span>:<br/>Deciding to Defer - <a href="12-dtd.html#SP11_1">§11.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">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">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">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">Quantifiers::is_now_assertable</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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP11"></a><b>§11. The PREDICATES group. </b>Next, unary predicates, beginning with the <span class="extract"><span class="extract-syntax">EVERYWHERE</span></span> special case.
|
|
</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">Calculus::Atoms::EVERYWHERE_new</span><button class="popup" onclick="togglePopup('usagePopup14')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup14">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::EVERYWHERE_new</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP5">§5</a><br/>Simplifications - <a href="11-sm.html#SP19">§19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">EVERYWHERE_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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="SP12"></a><b>§12. </b>And <span class="extract"><span class="extract-syntax">NOWHERE</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">Calculus::Atoms::NOWHERE_new</span><button class="popup" onclick="togglePopup('usagePopup15')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup15">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::NOWHERE_new</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP5">§5</a><br/>Simplifications - <a href="11-sm.html#SP19">§19</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NOWHERE_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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="SP13"></a><b>§13. </b>And <span class="extract"><span class="extract-syntax">HERE</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">Calculus::Atoms::HERE_new</span><button class="popup" onclick="togglePopup('usagePopup16')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup16">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::HERE_new</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP5">§5</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">HERE_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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="SP14"></a><b>§14. </b>And <span class="extract"><span class="extract-syntax">ISAKIND</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">Calculus::Atoms::ISAKIND_new</span><button class="popup" onclick="togglePopup('usagePopup17')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup17">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::ISAKIND_new</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP1">§1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">ISAKIND_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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">assert_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">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="SP15"></a><b>§15. </b>And <span class="extract"><span class="extract-syntax">ISAVAR</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">Calculus::Atoms::ISAVAR_new</span><button class="popup" onclick="togglePopup('usagePopup18')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup18">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::ISAVAR_new</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP1">§1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">ISAVAR_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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="SP16"></a><b>§16. </b>And <span class="extract"><span class="extract-syntax">ISACONST</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">Calculus::Atoms::ISACONST_new</span><button class="popup" onclick="togglePopup('usagePopup19')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup19">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::ISACONST_new</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP1">§1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">ISACONST_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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="SP17"></a><b>§17. </b><span class="extract"><span class="extract-syntax">CALLED</span></span> atoms are interesting because they exist only for their side-effects:
|
|
they have no effect at all on the logical status of a proposition (well, except
|
|
that they should not be applied to free variables referred to nowhere else).
|
|
They can therefore be added or removed freely. In the phrase
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>if a woman is in a lighted room (called the den), ...</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">we need to note that the value of the bound variable corresponding to the
|
|
lighted room will need to be kept and to have a name ("the den"): this
|
|
will probably mean the inclusion of a <span class="extract"><span class="extract-syntax">CALLED=den(y)</span></span> atom.
|
|
</p>
|
|
|
|
<p class="commentary">The calling data for a <span class="extract"><span class="extract-syntax">CALLED</span></span> atom is the textual name by which the variable
|
|
will be called.
|
|
</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">Calculus::Atoms::CALLED_new</span><button class="popup" onclick="togglePopup('usagePopup20')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup20">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::CALLED_new</span></span>:<br/>Tree Conversions - <a href="11-tc.html#SP1">§1</a><br/>Descriptions - <a href="14-ds.html#SP10">§10</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">W</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">CALLED_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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">calling_name</span><span class="plain-syntax"> = </span><span class="identifier-syntax">W</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">assert_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::CALLED_get_name</span><button class="popup" onclick="togglePopup('usagePopup21')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup21">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::CALLED_get_name</span></span>:<br/><a href="11-ap.html#SP25">§25</a><br/>Assert Propositions - <a href="12-ap.html#SP9_5_1">§9.5.1</a><br/>Compile Atoms - <a href="12-ca.html#SP6_1">§6.1</a><br/>Deciding to Defer - <a href="12-dtd.html#SP9_2">§9.2</a><br/>Descriptions - <a href="14-ds.html#SP10">§10</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">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">calling_name</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP18"></a><b>§18. </b>Now for a <span class="extract"><span class="extract-syntax">KIND</span></span> atom. At first sight, it looks odd that a unary
|
|
predicate for a kind is represented differently from other predicates.
|
|
Isn't it a unary predicate just like any other? Well: it is, but then
|
|
again, we want to compile propositions to reasonably efficient I6 code
|
|
which determines whether or not they are true. We particularly want to
|
|
look out for patterns like
|
|
$$ \forall x : ... \land {\it container}(x) \land ... $$
|
|
since they allow us to consider \(x\) ranging over a smaller, and therefore
|
|
more efficiently searchable, domain: most objects aren't containers. So
|
|
<span class="extract"><span class="extract-syntax">KIND_ATOM</span></span> atoms are useful in ways which other unary predicate atoms
|
|
are not.
|
|
</p>
|
|
|
|
<p class="commentary">Once again, this atom has arity 1, but the term no longer has to be a
|
|
variable; when Inform reads a sentence like
|
|
</p>
|
|
|
|
<blockquote>
|
|
<p>Viper Pit is a room.</p>
|
|
</blockquote>
|
|
|
|
<p class="commentary">the resulting proposition will include a <span class="extract"><span class="extract-syntax">KIND</span></span> atom whose term is the
|
|
constant value for the Viper Pit.
|
|
</p>
|
|
|
|
<p class="commentary">Any kind of value can be assigned, but the commonest case involves a kind
|
|
of object, so a special routine exists just to create <span class="extract"><span class="extract-syntax">KIND</span></span> atoms in
|
|
that case.
|
|
</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">Calculus::Atoms::KIND_new</span><button class="popup" onclick="togglePopup('usagePopup22')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup22">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::KIND_new</span></span>:<br/>Assertions - <a href="5-ass.html#SP6_3_39_5">§6.3.39.5</a><br/>Implications - <a href="5-imp.html#SP7_1_3">§7.1.3</a><br/>Tree Conversions - <a href="11-tc.html#SP1">§1</a>, <a href="11-tc.html#SP2">§2</a>, <a href="11-tc.html#SP7">§7</a><br/>Sentence Conversions - <a href="11-sc.html#SP3_3">§3.3</a><br/>Simplifications - <a href="11-sm.html#SP3_2">§3.2</a>, <a href="11-sm.html#SP4">§4</a>, <a href="11-sm.html#SP8">§8</a>, <a href="11-sm.html#SP10_3_2">§10.3.2</a><br/>Deciding to Defer - <a href="12-dtd.html#SP10">§10</a>, <a href="12-dtd.html#SP13">§13</a><br/>Descriptions - <a href="14-ds.html#SP3">§3</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">KIND_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">assert_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Atoms::KIND_new_composited</span><button class="popup" onclick="togglePopup('usagePopup23')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup23">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::KIND_new_composited</span></span>:<br/>Descriptions - <a href="14-ds.html#SP3">§3</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">KIND_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">assert_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt</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">composited</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">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="function-syntax">Calculus::Atoms::get_asserted_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">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">assert_kind</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">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_composited</span><button class="popup" onclick="togglePopup('usagePopup24')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup24">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_composited</span></span>:<br/>Simplifications - <a href="11-sm.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="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="element-syntax">composited</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::set_composited</span><button class="popup" onclick="togglePopup('usagePopup25')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup25">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::set_composited</span></span>:<br/>Sentence Conversions - <a href="11-sc.html#SP1_13_1">§1.13.1</a></span></button><span class="plain-syntax">(</span><span class="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">state</span><span 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="element-syntax">composited</span><span class="plain-syntax"> = </span><span class="identifier-syntax">state</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP19"></a><b>§19. </b>Likewise:
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_unarticled</span><button class="popup" onclick="togglePopup('usagePopup26')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup26">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_unarticled</span></span>:<br/>Simplifications - <a href="11-sm.html#SP10_3_2">§10.3.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="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="element-syntax">unarticled</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
|
|
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::set_unarticled</span><button class="popup" onclick="togglePopup('usagePopup27')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup27">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::set_unarticled</span></span>:<br/>Sentence Conversions - <a href="11-sc.html#SP3_4">§3.4</a><br/>Simplifications - <a href="11-sm.html#SP10_3_2">§10.3.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="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">state</span><span 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="element-syntax">unarticled</span><span class="plain-syntax"> = </span><span class="identifier-syntax">state</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP20"></a><b>§20. </b>That just leaves the general sort of unary predicate. In principle we ought
|
|
to be able to create \(U(t)\) for any term \(t\), but in practice we only ever
|
|
need \(t=x\), that is, variable 0.
|
|
</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">Calculus::Atoms::unary_PREDICATE_from_aph</span><button class="popup" onclick="togglePopup('usagePopup28')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup28">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::unary_PREDICATE_from_aph</span></span>:<br/>Implications - <a href="5-imp.html#SP7_1_3">§7.1.3</a><br/>Propositions - <a href="11-pr.html#SP35_1">§35.1</a>, <a href="11-pr.html#SP35_2">§35.2</a><br/>Tree Conversions - <a href="11-tc.html#SP7_2">§7.2</a><br/>Sentence Conversions - <a href="11-sc.html#SP3_3">§3.3</a><br/>Descriptions - <a href="14-ds.html#SP8">§8</a><br/>Either-Or Properties - <a href="15-ep.html#SP9">§9</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">adjective</span><span class="plain-syntax"> *</span><span class="identifier-syntax">aph</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">negated</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="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">PREDICATE_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">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">terms</span><span class="plain-syntax">[0] = </span><a href="11-tr.html#SP4" class="function-link"><span class="function-syntax">Calculus::Terms::new_variable</span></a><span class="plain-syntax">(0);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_unary_predicate</span><span class="plain-syntax">(</span>
|
|
<span class="plain-syntax"> </span><a href="7-up.html#SP2" class="function-link"><span class="function-syntax">UnaryPredicates::new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">aph</span><span class="plain-syntax">, (</span><span class="identifier-syntax">negated</span><span class="plain-syntax">)?</span><span class="identifier-syntax">FALSE: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">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">Calculus::Atoms::au_from_unary_PREDICATE</span><button class="popup" onclick="togglePopup('usagePopup29')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup29">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::au_from_unary_PREDICATE</span></span>:<br/>Propositions - <a href="11-pr.html#SP28">§28</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">return</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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP21"></a><b>§21. </b>And binary predicates are pretty well the same:
|
|
</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">Calculus::Atoms::binary_PREDICATE_new</span><button class="popup" onclick="togglePopup('usagePopup30')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup30">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::binary_PREDICATE_new</span></span>:<br/><a href="11-ap.html#SP22">§22</a><br/>Tree Conversions - <a href="11-tc.html#SP3">§3</a>, <a href="11-tc.html#SP4">§4</a><br/>Sentence Conversions - <a href="11-sc.html#SP1_13">§1.13</a>, <a href="11-sc.html#SP3_7">§3.7</a><br/>Simplifications - <a href="11-sm.html#SP4">§4</a>, <a href="11-sm.html#SP15">§15</a><br/>Measurement Adjectives - <a href="15-ma.html#SP13">§13</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt1</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pt2</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="11-ap.html#SP7" class="function-link"><span class="function-syntax">Calculus::Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">PREDICATE_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">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="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="identifier-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">bp</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">terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">pt1</span><span class="plain-syntax">; </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1] = </span><span class="identifier-syntax">pt2</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="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Atoms::is_binary_predicate</span><button class="popup" onclick="togglePopup('usagePopup31')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup31">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_binary_predicate</span></span>:<br/>Simplifications - <a href="11-sm.html#SP3">§3</a>, <a href="11-sm.html#SP8">§8</a>, <a href="11-sm.html#SP11">§11</a>, <a href="11-sm.html#SP12">§12</a>, <a href="11-sm.html#SP13">§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="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">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="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</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="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_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">int</span><span class="plain-syntax"> </span><span class="function-syntax">Calculus::Atoms::is_equality_predicate</span><button class="popup" onclick="togglePopup('usagePopup32')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup32">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_equality_predicate</span></span>:<br/><a href="11-ap.html#SP23">§23</a><br/>Propositions - <a href="11-pr.html#SP13">§13</a>, <a href="11-pr.html#SP24">§24</a><br/>Simplifications - <a href="11-sm.html#SP3">§3</a>, <a href="11-sm.html#SP7">§7</a>, <a href="11-sm.html#SP14">§14</a>, <a href="11-sm.html#SP17">§17</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">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP21" class="function-link"><span class="function-syntax">Calculus::Atoms::is_binary_predicate</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">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">R_equality</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="SP22"></a><b>§22. </b>Given \(C\), return the proposition {\it is}(\(x\), \(C\)):
|
|
</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">Calculus::Atoms::prop_x_is_constant</span><button class="popup" onclick="togglePopup('usagePopup33')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup33">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::prop_x_is_constant</span></span>:<br/>Propositions - <a href="11-pr.html#SP35_3">§35.3</a><br/>Descriptions - <a href="14-ds.html#SP5">§5</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="11-ap.html#SP21" class="function-link"><span class="function-syntax">Calculus::Atoms::binary_PREDICATE_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">R_equality</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><a href="11-tr.html#SP4" class="function-link"><span class="function-syntax">Calculus::Terms::new_variable</span></a><span class="plain-syntax">(0), </span><a href="11-tr.html#SP4" class="function-link"><span class="function-syntax">Calculus::Terms::new_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">));</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP23"></a><b>§23. </b>And conversely:
|
|
</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">Calculus::Atoms::is_x_equals</span><button class="popup" onclick="togglePopup('usagePopup34')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup34">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::is_x_equals</span></span>:<br/>Sentence Conversions - <a href="11-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="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="11-ap.html#SP21" class="function-link"><span class="function-syntax">Calculus::Atoms::is_equality_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">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="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="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> &(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[1]);</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP24"></a><b>§24. Validating atoms. </b></p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="function-syntax">Calculus::Atoms::validate</span><button class="popup" onclick="togglePopup('usagePopup35')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup35">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::validate</span></span>:<br/>Propositions - <a href="11-pr.html#SP12">§12</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">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">group</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">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="identifier-syntax">group</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP5" class="function-link"><span class="function-syntax">Calculus::Atoms::element_get_group</span></a><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="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">group</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="string-syntax">"atom of undiscovered 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">prop</span><span class="plain-syntax">-></span><span class="element-syntax">arity</span><span class="plain-syntax"> > </span><span class="constant-syntax">MAX_ATOM_ARITY</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">"atom with overly large arity"</span><span 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">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">"atom with negative arity"</span><span 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">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">group</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATES_GROUP</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">"predicate without terms"</span><span 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">QUANTIFIER_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">"quantifier without variable"</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="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">return</span><span class="plain-syntax"> </span><span class="string-syntax">"unary atom with other than one term"</span><span 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</span><span class="plain-syntax"> == </span><span class="constant-syntax">OPEN_OPERATORS_GROUP</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">group</span><span class="plain-syntax"> == </span><span class="constant-syntax">CLOSE_OPERATORS_GROUP</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">"parentheses with terms"</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="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == -1))</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">"missing variable in quantification"</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="SP25"></a><b>§25. Debugging log. </b>Logging atomic propositions divides into cases:
|
|
</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">Calculus::Atoms::log</span><button class="popup" onclick="togglePopup('usagePopup36')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup36">Usage of <span class="code-font"><span class="function-syntax">Calculus::Atoms::log</span></span>:<br/>Core Module - <a href="1-cm.html#SP5">§5</a>, <a href="1-cm.html#SP6_6">§6.6</a><br/>Propositions - <a href="11-pr.html#SP9">§9</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) { </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"<null-atom>"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</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">prop</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">PREDICATE_ATOM:</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">switch</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="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span><span class="plain-syntax">: </span><span class="named-paragraph-container code-font"><a href="11-ap.html#SP25_1" class="named-paragraph-link"><span class="named-paragraph">Log some suitable textual name for this unary predicate</span><span class="named-paragraph-number">25.1</span></a></span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="constant-syntax">2</span><span class="plain-syntax">: </span><span class="named-paragraph-container code-font"><a href="11-ap.html#SP25_2" class="named-paragraph-link"><span class="named-paragraph">Log some suitable textual name for this binary predicate</span><span class="named-paragraph-number">25.2</span></a></span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">default:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"?exotic-predicate-arity=%d?"</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="reserved-syntax">break</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">QUANTIFIER_ATOM:</span><span class="plain-syntax"> {</span>
|
|
<span class="plain-syntax"> </span><span class="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="identifier-syntax">Quantifiers::log</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">quantification_parameter</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">" "</span><span class="plain-syntax">); </span><span class="named-paragraph-container code-font"><a href="11-ap.html#SP25_3" class="named-paragraph-link"><span class="named-paragraph">Log a comma-separated list of terms for this atomic proposition</span><span class="named-paragraph-number">25.3</span></a></span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> }</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">CALLED_ATOM:</span><span class="plain-syntax"> {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">W</span><span class="plain-syntax"> = </span><a href="11-ap.html#SP17" class="function-link"><span class="function-syntax">Calculus::Atoms::CALLED_get_name</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">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"called='%W'"</span><span class="plain-syntax">, </span><span class="identifier-syntax">W</span><span 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">assert_kind</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"($u)"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">assert_kind</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">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">KIND_ATOM:</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="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"kind="</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">"$u"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">assert_kind</span><span 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="identifier-syntax">FALSE</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">composited</span><span class="plain-syntax">)) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"_c"</span><span 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="identifier-syntax">FALSE</span><span class="plain-syntax">) && (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="element-syntax">unarticled</span><span class="plain-syntax">)) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"_u"</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="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">ISAKIND_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"is-a-kind"</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">ISAVAR_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"is-a-var"</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">ISACONST_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"is-a-const"</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">EVERYWHERE_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"everywhere"</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">NOWHERE_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"nowhere"</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">HERE_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"here"</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_OPEN_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"NOT["</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">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"NOT]"</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">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"IN["</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">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"IN]"</span><span class="plain-syntax">); </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">default:</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"?bad-atom?"</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="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="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"("</span><span class="plain-syntax">); </span><span class="named-paragraph-container code-font"><a href="11-ap.html#SP25_3" class="named-paragraph-link"><span class="named-paragraph">Log a comma-separated list of terms for this atomic proposition</span><span class="named-paragraph-number">25.3</span></a></span><span class="plain-syntax">; </span><span class="identifier-syntax">LOG</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>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP25_1"></a><b>§25.1. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Log some suitable textual name for this unary predicate</span><span class="named-paragraph-number">25.1</span></span><span class="comment-syntax"> =</span>
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tr</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-></span><span class="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><a href="7-up.html#SP4" class="function-link"><span class="function-syntax">UnaryPredicates::get_parity</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">tr</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"not-"</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">Adjectives::log</span><span class="plain-syntax">(</span><a href="7-up.html#SP4" class="function-link"><span class="function-syntax">UnaryPredicates::get_adj</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">tr</span><span class="plain-syntax">));</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="11-ap.html#SP25">§25</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP25_2"></a><b>§25.2. </b>And more easily:
|
|
</p>
|
|
|
|
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Log some suitable textual name for this binary predicate</span><span class="named-paragraph-number">25.2</span></span><span class="comment-syntax"> =</span>
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">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">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"?bad-bp?"</span><span class="plain-syntax">); </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"%S"</span><span class="plain-syntax">, </span><a href="7-bp.html#SP36" class="function-link"><span class="function-syntax">BinaryPredicates::get_log_name</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">));</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="11-ap.html#SP25">§25</a>.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP25_3"></a><b>§25.3. </b>Just a diagnostic way of printing the terms in an atomic proposition, by
|
|
their index numbers. (They are numbered from 0 to \(A-1\), where \(A\) is the
|
|
arity.)
|
|
</p>
|
|
|
|
<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Log a comma-separated list of terms for this atomic proposition</span><span class="named-paragraph-number">25.3</span></span><span class="comment-syntax"> =</span>
|
|
</p>
|
|
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">t</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">t</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">t</span><span class="function-syntax"><prop-></span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">t</span><span class="plain-syntax">++) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">t</span><span class="plain-syntax">>0) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">", "</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><a href="11-tr.html#SP11" class="function-link"><span class="function-syntax">Calculus::Terms::log</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">t</span><span class="plain-syntax">]));</span>
|
|
<span class="plain-syntax"> }</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>This code is used in <a href="11-ap.html#SP25">§25</a> (twice).</li></ul>
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprev"><a href="11-tr.html">❮</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bv.html">3</a></li><li class="progresschapter"><a href="4-dlr.html">4</a></li><li class="progresschapter"><a href="5-rpt.html">5</a></li><li class="progresschapter"><a href="6-lp.html">6</a></li><li class="progresschapter"><a href="7-up.html">7</a></li><li class="progresschapter"><a href="8-ptu.html">8</a></li><li class="progresschapter"><a href="9-ef.html">9</a></li><li class="progresschapter"><a href="10-its.html">10</a></li><li class="progresscurrentchapter">11</li><li class="progresssection"><a href="11-itpc.html">itpc</a></li><li class="progresssection"><a href="11-tr.html">tr</a></li><li class="progresscurrent">ap</li><li class="progresssection"><a href="11-pr.html">pr</a></li><li class="progresssection"><a href="11-bas.html">bas</a></li><li class="progresssection"><a href="11-tc.html">tc</a></li><li class="progresssection"><a href="11-sc.html">sc</a></li><li class="progresssection"><a href="11-sm.html">sm</a></li><li class="progresssection"><a href="11-tcp.html">tcp</a></li><li class="progresschapter"><a href="12-ter.html">12</a></li><li class="progresschapter"><a href="13-kak.html">13</a></li><li class="progresschapter"><a href="14-sp.html">14</a></li><li class="progresschapter"><a href="15-pr.html">15</a></li><li class="progresschapter"><a href="16-is.html">16</a></li><li class="progresschapter"><a href="17-tl.html">17</a></li><li class="progresschapter"><a href="18-lc.html">18</a></li><li class="progresschapter"><a href="19-tc.html">19</a></li><li class="progresschapter"><a href="20-eq.html">20</a></li><li class="progresschapter"><a href="21-rl.html">21</a></li><li class="progresschapter"><a href="22-itp.html">22</a></li><li class="progresschapter"><a href="23-ad.html">23</a></li><li class="progresschapter"><a href="24-lv.html">24</a></li><li class="progresschapter"><a href="25-in.html">25</a></li><li class="progresschapter"><a href="26-fc.html">26</a></li><li class="progresschapter"><a href="27-hr.html">27</a></li><li class="progressnext"><a href="11-pr.html">❯</a></li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|