mirror of
https://github.com/ganelson/inform.git
synced 2024-07-05 16:44:21 +03:00
218 lines
30 KiB
HTML
218 lines
30 KiB
HTML
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html>
|
|
<head>
|
|
<title>Unary Predicate Families</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>
|
|
function togglePopup(material_id) {
|
|
var popup = document.getElementById(material_id);
|
|
popup.classList.toggle("show");
|
|
}
|
|
</script>
|
|
|
|
<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
|
|
|
|
</head>
|
|
<body class="commentary-font">
|
|
<nav role="navigation">
|
|
<h1><a href="../index.html">
|
|
<img src="../docs-assets/Inform.png" height=72">
|
|
</a></h1>
|
|
<ul><li><a href="../index.html">home</a></li>
|
|
</ul><h2>Compiler</h2><ul>
|
|
<li><a href="../structure.html">structure</a></li>
|
|
<li><a href="../inbuildn.html">inbuild</a></li>
|
|
<li><a href="../inform7n.html">inform7</a></li>
|
|
<li><a href="../intern.html">inter</a></li>
|
|
<li><a href="../services.html">services</a></li>
|
|
</ul><h2>Other Tools</h2><ul>
|
|
<li><a href="../inblorbn.html">inblorb</a></li>
|
|
<li><a href="../indocn.html">indoc</a></li>
|
|
<li><a href="../inform6.html">inform6</a></li>
|
|
<li><a href="../inpolicyn.html">inpolicy</a></li>
|
|
<li><a href="../inrtpsn.html">inrtps</a></li>
|
|
</ul><h2>Resources</h2><ul>
|
|
<li><a href="../extensions.html">extensions</a></li>
|
|
<li><a href="../kits.html">kits</a></li>
|
|
</ul><h2>Repository</h2><ul>
|
|
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=18> github</a></li>
|
|
</ul><h2>Related Projects</h2><ul>
|
|
<li><a href="../../../inweb/docs/index.html">inweb</a></li>
|
|
<li><a href="../../../intest/docs/index.html">intest</a></li>
|
|
|
|
</ul>
|
|
</nav>
|
|
<main role="main">
|
|
<!--Weave of 'Unary Predicate Families' generated by Inweb-->
|
|
<div class="breadcrumbs">
|
|
<ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#2">Chapter 2: Unary Predicates</a></li><li><b>Unary Predicate Families</b></li></ul></div>
|
|
<p class="purpose">To create sets of unary predicates for different purposes.</p>
|
|
|
|
<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>§1. </b>Want to create a new unary predicate? First you'll need a family for it to
|
|
belong to. A <a href="2-upf.html#SP1" class="internal">up_family</a> object is simply a receiver for the method calls
|
|
providing the predicate's implementation. In effect, a family is a collection
|
|
of UPs which share an implementation.
|
|
</p>
|
|
|
|
<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">up_family</span><span class="plain-syntax"> {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="identifier-syntax">method_set</span><span class="plain-syntax"> *</span><span class="identifier-syntax">methods</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">CLASS_DEFINITION</span>
|
|
<span class="plain-syntax">} </span><span class="reserved-syntax">up_family</span><span class="plain-syntax">;</span>
|
|
|
|
<span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="function-syntax">UnaryPredicateFamilies::new</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">UnaryPredicateFamilies::new</span></span>:<br/>Kind Predicates - <a href="2-kp.html#SP2">§2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">void</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax"> = </span><span class="identifier-syntax">CREATE</span><span class="plain-syntax">(</span><span class="reserved-syntax">up_family</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">f</span><span class="plain-syntax">-></span><span class="element-syntax">methods</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Methods::new_set</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">f</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>The structure up_family is accessed in 3/bpf and here.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>§2. </b><span class="extract"><span class="extract-syntax">STOCK_UPF_MTID</span></span> is for stocking up on unaries, and happens very early
|
|
in Inform's run.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">STOCK_UPF_MTID</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">VOID_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">STOCK_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">n</span><span class="plain-syntax">)</span>
|
|
|
|
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">UnaryPredicateFamilies::stock</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">UnaryPredicateFamilies::stock</span></span>:<br/>Binary Predicate Families - <a href="3-bpf.html#SP2">§2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">n</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">LOOP_OVER</span><span class="plain-syntax">(</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax">)</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">VOID_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="constant-syntax">STOCK_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">n</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>§3. </b>This method performs a type-check to see whether the value supplied as the
|
|
term of the predicate is acceptable. For example, <span class="extract"><span class="extract-syntax">even(t)</span></span> should reject
|
|
<span class="extract"><span class="extract-syntax">t</span></span> if it is a text, because <span class="extract"><span class="extract-syntax">even</span></span> is meaningful only for numbers.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">TYPECHECK_UPF_MTID</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">variable_type_assignment</span><span class="plain-syntax"> {</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">assigned_kinds</span><span class="plain-syntax">[26]; </span><span class="comment-syntax"> one for each of the 26 variables</span>
|
|
<span class="plain-syntax">} </span><span class="reserved-syntax">variable_type_assignment</span><span class="plain-syntax">;</span>
|
|
|
|
<span class="identifier-syntax">INT_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">TYPECHECK_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="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">variable_type_assignment</span><span class="plain-syntax"> *</span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">)</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">UnaryPredicateFamilies::typecheck</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">UnaryPredicateFamilies::typecheck</span></span>:<br/>Type Check Propositions - <a href="4-tcp.html#SP4_5">§4.5</a>, <a href="4-tcp.html#SP8">§8</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="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">variable_type_assignment</span><span class="plain-syntax"> *</span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</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">rv</span><span class="plain-syntax"> = </span><span class="constant-syntax">DECLINE_TO_MATCH</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">INT_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">rv</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax">, </span><span class="constant-syntax">TYPECHECK_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</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">rv</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<ul class="endnotetexts"><li>The structure variable_type_assignment is accessed in 4/tcp.</li></ul>
|
|
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>§4. </b>A unary predicate is "testable" if its truth can be determined at compile
|
|
time. (We assume everything can be tested at run time.) For example,
|
|
<span class="extract"><span class="extract-syntax">kind=number(t)</span></span> can generally be tested at compile time, but <span class="extract"><span class="extract-syntax">even(t)</span></span> cannot.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">TESTABLE_UPF_MTID</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">INT_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">TESTABLE_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">)</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">UnaryPredicateFamilies::testable</span><span class="plain-syntax">(</span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">rv</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">INT_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">rv</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax">, </span><span class="constant-syntax">TESTABLE_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</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">rv</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>§5. </b>And for a testable UP, the following should perform that test. It will never
|
|
be called for non-testable ones.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">TEST_UPF_MTID</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">INT_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">TEST_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="constant-syntax">TERM_DOMAIN_CALCULUS_TYPE</span><span class="plain-syntax"> *</span><span class="identifier-syntax">about</span><span class="plain-syntax">)</span>
|
|
|
|
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">UnaryPredicateFamilies::test</span><span class="plain-syntax">(</span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="constant-syntax">TERM_DOMAIN_CALCULUS_TYPE</span><span class="plain-syntax"> *</span><span class="identifier-syntax">about</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">rv</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">INT_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">rv</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax">, </span><span class="constant-syntax">TEST_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">about</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">rv</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>§6. </b>Assertion is used in Inform when constructing the model world. The <a href="index.html" class="internal">calculus</a>
|
|
module doesn't really get involved in this, and provides this method only for
|
|
Inform's benefit.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">ASSERT_UPF_MTID</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">VOID_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">ASSERT_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">now_negated</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)</span>
|
|
|
|
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">UnaryPredicateFamilies::assert</span><span class="plain-syntax">(</span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">now_negated</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pl</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">VOID_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax">, </span><span class="constant-syntax">ASSERT_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">now_negated</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>§7. </b>Schemas are used in compilation: see <a href="3-cs.html" class="internal">Compilation Schemas</a> for more.
|
|
Again, the <a href="index.html" class="internal">calculus</a> module doesn't really get involved in this.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">SCHEMA_UPF_MTID</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">VOID_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">SCHEMA_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">task</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">annotated_i6_schema</span><span class="plain-syntax"> *</span><span class="identifier-syntax">asch</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="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">UnaryPredicateFamilies::get_schema</span><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">task</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">annotated_i6_schema</span><span class="plain-syntax"> *</span><span class="identifier-syntax">asch</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="identifier-syntax">VOID_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax">, </span><span class="constant-syntax">SCHEMA_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">task</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">asch</span><span class="plain-syntax">, </span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>§8. </b>If the usage of this UP implies the kind of its term, here's where we say so.
|
|
The obvious example is <span class="extract"><span class="extract-syntax">kind=K(t)</span></span>, which necessarily means <span class="extract"><span class="extract-syntax">t</span></span> has kind <span class="extract"><span class="extract-syntax">K</span></span>.
|
|
But one could also imagine UPs which are appropriate only for, say, real numbers.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">INFER_KIND_UPF_MTID</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">VOID_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">INFER_KIND_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> **</span><span class="identifier-syntax">K</span><span class="plain-syntax">)</span>
|
|
|
|
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">UnaryPredicateFamilies::infer_kind</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">UnaryPredicateFamilies::infer_kind</span></span>:<br/>Binding and Substitution - <a href="4-bas.html#SP16">§16</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">VOID_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax">, </span><span class="constant-syntax">INFER_KIND_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</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">K</span><span class="plain-syntax">;</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>§9. </b>Logging should be brief: something like <span class="extract"><span class="extract-syntax">kind=number</span></span> is plenty.
|
|
</p>
|
|
|
|
<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">LOG_UPF_MTID</span>
|
|
</pre>
|
|
<pre class="displayed-code all-displayed-code code-font">
|
|
<span class="identifier-syntax">VOID_METHOD_TYPE</span><span class="plain-syntax">(</span><span class="constant-syntax">LOG_UPF_MTID</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">, </span><span class="identifier-syntax">text_stream</span><span class="plain-syntax"> *</span><span class="identifier-syntax">OUT</span><span class="plain-syntax">,</span>
|
|
<span class="plain-syntax"> </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">)</span>
|
|
|
|
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">UnaryPredicateFamilies::log</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">UnaryPredicateFamilies::log</span></span>:<br/>Unary Predicates - <a href="2-up.html#SP2">§2</a><br/>Atomic Propositions - <a href="4-ap.html#SP14_2">§14.2</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">OUTPUT_STREAM</span><span class="plain-syntax">, </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax">) {</span>
|
|
<span class="plain-syntax"> </span><span class="identifier-syntax">VOID_METHOD_CALL</span><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">-></span><span class="element-syntax">family</span><span class="plain-syntax">, </span><span class="constant-syntax">LOG_UPF_MTID</span><span class="plain-syntax">, </span><span class="identifier-syntax">OUT</span><span class="plain-syntax">, </span><span class="identifier-syntax">up</span><span class="plain-syntax">);</span>
|
|
<span class="plain-syntax">}</span>
|
|
</pre>
|
|
<nav role="progress"><div class="progresscontainer">
|
|
<ul class="progressbar"><li class="progressprev"><a href="2-up.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="progresscurrentchapter">2</li><li class="progresssection"><a href="2-up.html">up</a></li><li class="progresscurrent">upf</li><li class="progresssection"><a href="2-kp.html">kp</a></li><li class="progresschapter"><a href="3-bpf.html">3</a></li><li class="progresschapter"><a href="4-trm.html">4</a></li><li class="progresschapter"><a href="5-sc.html">5</a></li><li class="progressnext"><a href="2-kp.html">❯</a></li></ul></div>
|
|
</nav><!--End of weave-->
|
|
|
|
</main>
|
|
</body>
|
|
</html>
|
|
|