COMPILE_WRITER(pcalc_prop *, Propositions::log) -COMPILE_WRITER(pcalc_prop *, Atoms::log) +COMPILE_WRITER(pcalc_prop *, Atoms::log) COMPILE_WRITER(pcalc_term *, Terms::log) COMPILE_WRITER(binary_predicate *, BinaryPredicates::log) COMPILE_WRITER(unary_predicate *, UnaryPredicates::log) void CalculusModule::start(void) { REGISTER_WRITER('D', Propositions::log); - REGISTER_WRITER('o', Atoms::log); + REGISTER_WRITER('o', Atoms::log); REGISTER_WRITER('0', Terms::log); REGISTER_WRITER('2', BinaryPredicates::log); REGISTER_WRITER('r', UnaryPredicates::log); diff --git a/docs/calculus-module/2-bp.html b/docs/calculus-module/2-bp.html index 7d4be83dd..c618ff271 100644 --- a/docs/calculus-module/2-bp.html +++ b/docs/calculus-module/2-bp.html @@ -825,7 +825,7 @@ so the fact that it runs relatively slowly does not matter.--text_stream *BinaryPredicates::get_log_name(binary_predicate *bp) { +text_stream *BinaryPredicates::get_log_name(binary_predicate *bp) { return bp->debugging_log_name; }diff --git a/docs/calculus-module/2-tcp.html b/docs/calculus-module/2-tcp.html index 9f4d2cfb1..b00ebd877 100644 --- a/docs/calculus-module/2-tcp.html +++ b/docs/calculus-module/2-tcp.html @@ -75,7 +75,12 @@ exist.up_family *calling_up_family = NULL; -up_family *creation_up_family = NULL; +up_family *is_a_var_up_family = NULL; +up_family *is_a_const_up_family = NULL; +up_family *is_a_kind_up_family = NULL; + +unary_predicate *is_a_var_up = NULL; +unary_predicate *is_a_const_up = NULL;§2. Family. This is a minimal representation only: Inform adds other methods to the equality family to handle its typechecking and so on. @@ -84,8 +89,19 @@ family to handle its typechecking and so on.
void Calculus::Creation::start(void) { calling_up_family = UnaryPredicateFamilies::new(); - creation_up_family = UnaryPredicateFamilies::new(); - METHOD_ADD(creation_up_family, STOCK_UPF_MTID, Calculus::Creation::stock_creation); + is_a_var_up_family = UnaryPredicateFamilies::new(); + METHOD_ADD(is_a_var_up_family, STOCK_UPF_MTID, Calculus::Creation::stock_is_a_var); + METHOD_ADD(is_a_var_up_family, LOG_UPF_MTID, Calculus::Creation::log_is_a_var); + is_a_const_up_family = UnaryPredicateFamilies::new(); + METHOD_ADD(is_a_const_up_family, STOCK_UPF_MTID, Calculus::Creation::stock_is_a_const); + METHOD_ADD(is_a_const_up_family, LOG_UPF_MTID, Calculus::Creation::log_is_a_const); + is_a_kind_up_family = UnaryPredicateFamilies::new(); + METHOD_ADD(is_a_kind_up_family, LOG_UPF_MTID, Calculus::Creation::log_is_a_kind); + #ifdef CORE_MODULE + METHOD_ADD(is_a_var_up_family, TYPECHECK_UPF_MTID, Calculus::Creation::typecheck_is_a_var); + METHOD_ADD(is_a_const_up_family, TYPECHECK_UPF_MTID, Calculus::Creation::typecheck_is_a_const); + METHOD_ADD(is_a_kind_up_family, TYPECHECK_UPF_MTID, Calculus::Creation::typecheck_is_a_kind); + #endif }§3. Initial stock. This relation is hard-wired in, and it is made in a slightly special way @@ -93,11 +109,62 @@ since (alone among binary predicates) it has no distinct reversal.
-void Calculus::Creation::stock_creation(up_family *self, int n) { +void Calculus::Creation::stock_is_a_var(up_family *self, int n) { if (n == 1) { - ; make isakind, etc., here + is_a_var_up = UnaryPredicates::blank(is_a_var_up_family); } } + +void Calculus::Creation::stock_is_a_const(up_family *self, int n) { + if (n == 1) { + is_a_const_up = UnaryPredicates::blank(is_a_const_up_family); + } +} + +pcalc_prop *Calculus::Creation::is_a_var_up(pcalc_term t) { + return Atoms::unary_PREDICATE_new(is_a_var_up, t); +} + +pcalc_prop *Calculus::Creation::is_a_const_up(pcalc_term t) { + return Atoms::unary_PREDICATE_new(is_a_const_up, t); +} + +pcalc_prop *Calculus::Creation::is_a_kind_up(pcalc_term t, kind *K) { + unary_predicate *up = UnaryPredicates::blank(is_a_kind_up_family); + up->assert_kind = K; + return Atoms::unary_PREDICATE_new(up, t); +} + +#ifdef CORE_MODULE +int Calculus::Creation::typecheck_is_a_var(up_family *self, unary_predicate *up, + pcalc_prop *prop, variable_type_assignment *vta, tc_problem_kit *tck) { + return ALWAYS_MATCH; +} +int Calculus::Creation::typecheck_is_a_const(up_family *self, unary_predicate *up, + pcalc_prop *prop, variable_type_assignment *vta, tc_problem_kit *tck) { + return ALWAYS_MATCH; +} +int Calculus::Creation::typecheck_is_a_kind(up_family *self, unary_predicate *up, + pcalc_prop *prop, variable_type_assignment *vta, tc_problem_kit *tck) { + kind *actually_find = Propositions::Checker::kind_of_term(&(prop->terms[0]), vta, tck); + if (Kinds::compatible(actually_find, K_object) == NEVER_MATCH) + internal_error("is_a_kind predicate misapplied"); + return ALWAYS_MATCH; +} +#endif + +void Calculus::Creation::log_is_a_var(up_family *self, OUTPUT_STREAM, unary_predicate *up) { + WRITE("is-a-var"); +} + +void Calculus::Creation::log_is_a_const(up_family *self, OUTPUT_STREAM, unary_predicate *up) { + WRITE("is-a-const"); +} + +void Calculus::Creation::log_is_a_kind(up_family *self, OUTPUT_STREAM, unary_predicate *up) { + WRITE("is-a-kind"); + if (up->assert_kind) WRITE("=%u", up->assert_kind); +}
§2. Each atom is an instance of an "element", and its element field is one of the *_ATOM numbers below. Those elements in turn occur in "groups".
@@ -120,9 +120,6 @@ of the *_ATOM n define PREDICATES_GROUP 20 define PREDICATE_ATOM 10 a regular predicate, rather than these special cases — define KIND_ATOM 11 a unary predicate asserting that \(x\) has kind \(K\) -define ISAKIND_ATOM 12 a unary predicate asserting that \(x\) is itself a kind -define ISAVAR_ATOM 13 a unary predicate asserting that \(x\) is a global variable -define ISACONST_ATOM 14 a unary predicate asserting that \(x\) is a named constant define EVERYWHERE_ATOM 15 a unary predicate asserting omnipresence define NOWHERE_ATOM 16 a unary predicate asserting nonpresence define HERE_ATOM 17 a unary predicate asserting presence "here" @@ -135,7 +132,7 @@ of the *_ATOM n define DOMAIN_CLOSE_ATOM 31 end of quantifier domain-int Atoms::group(int element) { +int Atoms::group(int element) { if (element <= 0) return 0; if (element < QUANTIFIERS_GROUP) return QUANTIFIERS_GROUP; if (element < PREDICATES_GROUP) return PREDICATES_GROUP; @@ -164,7 +161,7 @@ like this, or else returns the opposite number to any element code which does.--pcalc_prop *Atoms::new(int element) { +pcalc_prop *Atoms::new(int element) { pcalc_prop *prop = CREATE(pcalc_prop); prop->next = NULL; prop->element = element; @@ -291,30 +288,7 @@ special cases. return prop; }-§10. And the ISAKIND, ISAVAR and ISACONST creation predicates: -
- --pcalc_prop *Atoms::ISAKIND_new(pcalc_term pt, kind *K) { - pcalc_prop *prop = Atoms::new(ISAKIND_ATOM); - prop->terms[prop->arity++] = pt; - prop->assert_kind = K; - return prop; -} - -pcalc_prop *Atoms::ISAVAR_new(pcalc_term pt) { - pcalc_prop *prop = Atoms::new(ISAVAR_ATOM); - prop->terms[prop->arity++] = pt; - return prop; -} - -pcalc_prop *Atoms::ISACONST_new(pcalc_term pt) { - pcalc_prop *prop = Atoms::new(ISACONST_ATOM); - prop->terms[prop->arity++] = pt; - return prop; -} --§11. CALLED atoms are interesting because they exist only for their side-effects: +
§10. CALLED 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 @@ -334,7 +308,7 @@ will be called.
-int Atoms::is_CALLED(pcalc_prop *prop) { +int Atoms::is_CALLED(pcalc_prop *prop) { if (prop->element == CALLED_ATOM) return TRUE; return FALSE; } @@ -347,11 +321,11 @@ will be called. return prop; } -wording Atoms::CALLED_get_name(pcalc_prop *prop) { +wording Atoms::CALLED_get_name(pcalc_prop *prop) { return prop->calling_name; }-§12. Now for a KIND atom. At first sight, it looks odd that a unary +
§11. Now for a KIND 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 has the special property that its truth does not change over time. If a value v @@ -376,7 +350,7 @@ ways. return NULL; }
§13. Composited KIND atoms are special in that they represent composites +
§12. Composited KIND atoms are special in that they represent composites of quantifiers with common nouns — for example, "everyone" is a composite meaning "every person".
@@ -400,7 +374,7 @@ meaning "every person". if (prop) prop->composited = state; } -§14. Unarticled kinds are those which were introduced without an article, in +
§13. Unarticled kinds are those which were introduced without an article, in the linguistic sense.
@@ -414,34 +388,37 @@ the linguistic sense. if (prop) prop->unarticled = state; } -§15. That just leaves the general sort of unary predicate. In principle we ought +
§14. 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.
-pcalc_prop *Atoms::from_adjective(adjective *aph, int negated, pcalc_term t) { +pcalc_prop *Atoms::unary_PREDICATE_new(unary_predicate *up, pcalc_term t) { pcalc_prop *prop = Atoms::new(PREDICATE_ATOM); prop->arity = 1; prop->terms[0] = t; - prop->predicate = STORE_POINTER_unary_predicate( - UnaryPredicates::new(aph, (negated)?FALSE:TRUE)); + prop->predicate = STORE_POINTER_unary_predicate(up); return prop; } -pcalc_prop *Atoms::from_adjective_on_x(adjective *aph, int negated) { - return Atoms::from_adjective(aph, negated, Terms::new_variable(0)); +pcalc_prop *Atoms::from_adjective(adjective *aph, int negated, pcalc_term t) { + return Atoms::unary_PREDICATE_new(UnaryPredicates::new(aph, (negated)?FALSE:TRUE), t); } -unary_predicate *Atoms::to_adjectival_usage(pcalc_prop *prop) { +pcalc_prop *Atoms::from_adjective_on_x(adjective *aph, int negated) { + return Atoms::from_adjective(aph, negated, Terms::new_variable(0)); +} + +unary_predicate *Atoms::to_adjectival_usage(pcalc_prop *prop) { return RETRIEVE_POINTER_unary_predicate(prop->predicate); }-
§16. And binary predicates are pretty well the same: +
§15. And binary predicates are pretty well the same:
-pcalc_prop *Atoms::binary_PREDICATE_new(binary_predicate *bp, +pcalc_prop *Atoms::binary_PREDICATE_new(binary_predicate *bp, pcalc_term pt1, pcalc_term pt2) { pcalc_prop *prop = Atoms::new(PREDICATE_ATOM); prop->arity = 2; @@ -457,35 +434,35 @@ need \(t=x\), that is, variable 0. return RETRIEVE_POINTER_binary_predicate(prop->predicate); } -int Atoms::is_equality_predicate(pcalc_prop *prop) { - binary_predicate *bp = Atoms::is_binary_predicate(prop); +int Atoms::is_equality_predicate(pcalc_prop *prop) { + binary_predicate *bp = Atoms::is_binary_predicate(prop); if (bp == R_equality) return TRUE; return FALSE; }-
§17. Given \(C\), return the proposition (x == C): +
§16. Given \(C\), return the proposition (x == C):
pcalc_prop *Atoms::prop_x_is_constant(parse_node *C) { - return Atoms::binary_PREDICATE_new(R_equality, + return Atoms::binary_PREDICATE_new(R_equality, Terms::new_variable(0), Terms::new_constant(C)); }-
pcalc_term *Atoms::is_x_equals(pcalc_prop *prop) { - if (Atoms::is_equality_predicate(prop) == FALSE) return NULL; + if (Atoms::is_equality_predicate(prop) == FALSE) return NULL; if (prop->terms[0].variable != 0) return NULL; return &(prop->terms[1]); }- +
-char *Atoms::validate(pcalc_prop *prop) { +char *Atoms::validate(pcalc_prop *prop) { int group; if (prop == NULL) return NULL; group = Atoms::group(prop->element); @@ -506,18 +483,18 @@ need \(t=x\), that is, variable 0. return NULL; }-
§20. Writing to text. Logging atomic propositions divides into cases: +
§19. Writing to text. Logging atomic propositions divides into cases:
-void Atoms::log(pcalc_prop *prop) { - Atoms::write(DL, prop); +void Atoms::log(pcalc_prop *prop) { + Atoms::write(DL, prop); } -void Atoms::write(text_stream *OUT, pcalc_prop *prop) { +void Atoms::write(text_stream *OUT, pcalc_prop *prop) { if (prop == NULL) { WRITE("<null-atom>"); return; } - Use a special notation for equality20.1; - if (Atoms::is_CALLED(prop)) { - wording W = Atoms::CALLED_get_name(prop); + Use a special notation for equality19.1; + if (Atoms::is_CALLED(prop)) { + wording W = Atoms::CALLED_get_name(prop); WRITE("called='%W'", W); if (prop->assert_kind) { WRITE("("); @@ -528,15 +505,15 @@ need \(t=x\), that is, variable 0. switch(prop->element) { case PREDICATE_ATOM: switch(prop->arity) { - case 1: Log some suitable textual name for this unary predicate20.2; break; - case 2: Log some suitable textual name for this binary predicate20.3; break; + case 1: Log some suitable textual name for this unary predicate19.2; break; + case 2: Log some suitable textual name for this binary predicate19.3; break; default: WRITE("?exotic-predicate-arity=%d?", prop->arity); break; } break; case QUANTIFIER_ATOM: { quantifier *quant = prop->quant; Quantifiers::log(OUT, quant, prop->quantification_parameter); - WRITE(" "); Log a comma-separated list of terms for this atomic proposition20.4; + WRITE(" "); Log a comma-separated list of terms for this atomic proposition19.4; return; } case KIND_ATOM: @@ -545,9 +522,6 @@ need \(t=x\), that is, variable 0. if ((Streams::I6_escapes_enabled(DL) == FALSE) && (prop->composited)) WRITE("_c"); if ((Streams::I6_escapes_enabled(DL) == FALSE) && (prop->unarticled)) WRITE("_u"); break; - case ISAKIND_ATOM: WRITE("is-a-kind"); break; - case ISAVAR_ATOM: WRITE("is-a-var"); break; - case ISACONST_ATOM: WRITE("is-a-const"); break; case EVERYWHERE_ATOM: WRITE("everywhere"); break; case NOWHERE_ATOM: WRITE("nowhere"); break; case HERE_ATOM: WRITE("here"); break; @@ -559,12 +533,12 @@ need \(t=x\), that is, variable 0. } if (prop->arity > 0) { WRITE("("); - Log a comma-separated list of terms for this atomic proposition20.4; + Log a comma-separated list of terms for this atomic proposition19.4; WRITE(")"); } }-
§20.1. Use a special notation for equality20.1 = +
§19.1. Use a special notation for equality19.1 =
@@ -578,24 +552,24 @@ need \(t=x\), that is, variable 0. return; }-
§20.2. Log some suitable textual name for this unary predicate20.2 = +
§19.2. Log some suitable textual name for this unary predicate19.2 =
unary_predicate *tr = RETRIEVE_POINTER_unary_predicate(prop->predicate); UnaryPredicateFamilies::log(OUT, tr);-
§20.3. Log some suitable textual name for this binary predicate20.3 = +
§19.3. Log some suitable textual name for this binary predicate19.3 =
binary_predicate *bp = RETRIEVE_POINTER_binary_predicate(prop->predicate); if (bp == NULL) WRITE("?bad-bp?"); else WRITE("%S", BinaryPredicates::get_log_name(bp));-
§20.4. Log a comma-separated list of terms for this atomic proposition20.4 = +
§19.4. Log a comma-separated list of terms for this atomic proposition19.4 =
@@ -604,7 +578,7 @@ need \(t=x\), that is, variable 0. Terms::write(OUT, &(prop->terms[t])); }-
§10. The following tests only (ii), validity. calculus-test is unable to make -atoms which fail to pass Atoms::validate, nor can it make some of the +atoms which fail to pass Atoms::validate, nor can it make some of the misconstructions tested for below, but numerous other defects can be tested:
@@ -334,7 +334,7 @@ misconstructions tested for below, but numerous other defects can be tested: int groups_stack[MAX_PROPOSITION_GROUP_NESTING], group_sp = 0; TRAVERSE_PROPOSITION(p, prop) { (1) each individual atom has to be properly built: - char *v_err = Atoms::validate(p); + char *v_err = Atoms::validate(p); if (v_err) { WRITE_TO(err, "atom error: %s", err); return FALSE; } (2) every open bracket must be matched by a close bracket of the same kind: if (Atoms::group(p->element) == OPEN_OPERATORS_GROUP) { @@ -401,7 +401,7 @@ value to x. Exa if (p->element == DOMAIN_OPEN_ATOM) return TRUE; if (p->element == DOMAIN_CLOSE_ATOM) return TRUE; if ((p->element == PREDICATE_ATOM) && (p->arity == 2)) { - if (Atoms::is_equality_predicate(p) == FALSE) return TRUE; + if (Atoms::is_equality_predicate(p) == FALSE) return TRUE; if (!(((p->terms[0].variable == 0) && (p->terms[1].constant)) || ((p->terms[1].variable == 0) && (p->terms[0].constant)))) return TRUE; } @@ -681,7 +681,7 @@ a given arity, or both: return NULL; } -pcalc_prop *Propositions::prop_seek_up_family(pcalc_prop *prop, up_family *f) { +pcalc_prop *Propositions::prop_seek_up_family(pcalc_prop *prop, up_family *f) { TRAVERSE_VARIABLE(p); TRAVERSE_PROPOSITION(p, prop) if ((p->element == PREDICATE_ATOM) && (p->arity == 1)) { @@ -720,7 +720,7 @@ a given arity, or both: int Propositions::contains_callings(pcalc_prop *prop) { for (pcalc_prop *p = prop; p; p = p->next) - if (Atoms::is_CALLED(p)) + if (Atoms::is_CALLED(p)) return TRUE; return FALSE; } @@ -732,9 +732,12 @@ expense of typechecking the proposition:kind *Propositions::describes_kind(pcalc_prop *prop) { pcalc_prop *p = prop; - while ((p = Propositions::prop_seek_atom(p, ISAKIND_ATOM, 1)) != NULL) { + while ((p = Propositions::prop_seek_up_family(p, is_a_kind_up_family)) != NULL) { if ((Terms::variable_underlying(&(p->terms[0])) == 0) && - (Kinds::eq(p->assert_kind, K_value))) return p->assert_kind; + (Kinds::eq(p->assert_kind, K_value))) { + unary_predicate *up = RETRIEVE_POINTER_unary_predicate(p->predicate); + return up->assert_kind; + } p = p->next; } p = prop; @@ -761,7 +764,7 @@ expense of typechecking the proposition: case DOMAIN_CLOSE_ATOM: bl--; break; default: if (bl == 0) { - if (Atoms::is_equality_predicate(p)) { + if (Atoms::is_equality_predicate(p)) { if ((p->terms[0].variable == 0) && (p->terms[1].constant)) return p->terms[1].constant; if ((p->terms[1].variable == 0) && (p->terms[0].constant)) @@ -850,7 +853,7 @@ following are useful for looping through them: prop = Propositions::prop_seek_up_family(prop, adjectival_up_family); if (ppp) *ppp = prop; if (prop == NULL) return NULL; - return Atoms::to_adjectival_usage(prop); + return Atoms::to_adjectival_usage(prop); } unary_predicate *Propositions::next_unary_predicate(pcalc_prop **ppp) { @@ -858,7 +861,7 @@ following are useful for looping through them: pcalc_prop *prop = Propositions::prop_seek_up_family((*ppp)->next, adjectival_up_family); *ppp = prop; if (prop == NULL) return NULL; - return Atoms::to_adjectival_usage(prop); + return Atoms::to_adjectival_usage(prop); }
§31. Bracketed groups. The following routine tests whether the entire proposition is a single diff --git a/docs/calculus-module/3-trm.html b/docs/calculus-module/3-trm.html index 1463e7e0a..8c077f436 100644 --- a/docs/calculus-module/3-trm.html +++ b/docs/calculus-module/3-trm.html @@ -165,14 +165,14 @@ field is
-pcalc_term Terms::new_variable(int v) { +pcalc_term Terms::new_variable(int v) { pcalc_term pt; Make new blank term structure pt4.1; if ((v < 0) || (v >= 26)) internal_error("bad variable term created"); pt.variable = v; return pt; } -pcalc_term Terms::new_constant(parse_node *c) { +pcalc_term Terms::new_constant(parse_node *c) { pcalc_term pt; Make new blank term structure pt4.1; pt.constant = c; return pt; @@ -357,7 +357,7 @@ concisely and without fuss. void Terms::log(pcalc_term *pt) { Terms::write(DL, pt); } -void Terms::write(text_stream *OUT, pcalc_term *pt) { +void Terms::write(text_stream *OUT, pcalc_term *pt) { if (pt == NULL) { WRITE("<null-term>"); } else if (pt->constant) { diff --git a/docs/calculus-module/P-wtmd.html b/docs/calculus-module/P-wtmd.html index a8c41b7ff..3dfa21199 100644 --- a/docs/calculus-module/P-wtmd.html +++ b/docs/calculus-module/P-wtmd.html @@ -294,14 +294,13 @@ calls.2. Unary predicate atoms are made using:
-
Binary predicate atoms are made using Atoms::binary_PREDICATE_new. +
Binary predicate atoms are made using Atoms::binary_PREDICATE_new.
3. Propositions are then built up from atoms or other propositions8 by calling: diff --git a/docs/calculus-test/1-dcl.html b/docs/calculus-test/1-dcl.html index 9efc3c481..1b9860094 100644 --- a/docs/calculus-test/1-dcl.html +++ b/docs/calculus-test/1-dcl.html @@ -222,9 +222,9 @@ sentence. In effect, this is a read-evaluate-print loop. everywhere ( <term> ) | ==> { -, Atoms::EVERYWHERE_new(*((pcalc_term *) RP[1])) } nowhere ( <term> ) | ==> { -, Atoms::NOWHERE_new(*((pcalc_term *) RP[1])) } here ( <term> ) | ==> { -, Atoms::HERE_new(*((pcalc_term *) RP[1])) } - is-a-kind ( <term> ) | ==> { -, Atoms::ISAKIND_new(*((pcalc_term *) RP[1]), NULL) } - is-a-var ( <term> ) | ==> { -, Atoms::ISAVAR_new(*((pcalc_term *) RP[1])) } - is-a-const ( <term> ) | ==> { -, Atoms::ISACONST_new(*((pcalc_term *) RP[1])) } + is-a-kind ( <term> ) | ==> { -, Calculus::Creation::is_a_kind_up(*((pcalc_term *) RP[1]), NULL) } + is-a-var ( <term> ) | ==> { -, Calculus::Creation::is_a_var_up(*((pcalc_term *) RP[1])) } + is-a-const ( <term> ) | ==> { -, Calculus::Creation::is_a_const_up(*((pcalc_term *) RP[1])) } not< | ==> { -, Atoms::new(NEGATION_OPEN_ATOM) } not> | ==> { -, Atoms::new(NEGATION_CLOSE_ATOM) } in< | ==> { -, Atoms::new(DOMAIN_OPEN_ATOM) } diff --git a/docs/core-module/11-tc.html b/docs/core-module/11-tc.html index 07879a700..1f42db2e9 100644 --- a/docs/core-module/11-tc.html +++ b/docs/core-module/11-tc.html @@ -81,15 +81,15 @@ their existence.
pcalc_prop *Propositions::Abstract::to_make_a_kind(kind *K) { - return Atoms::ISAKIND_new(Terms::new_variable(0), K); + return Calculus::Creation::is_a_kind_up(Terms::new_variable(0), K); } pcalc_prop *Propositions::Abstract::to_make_a_var(void) { - return Atoms::ISAVAR_new(Terms::new_variable(0)); + return Calculus::Creation::is_a_var_up(Terms::new_variable(0)); } pcalc_prop *Propositions::Abstract::to_make_a_const(void) { - return Atoms::ISACONST_new(Terms::new_variable(0)); + return Calculus::Creation::is_a_const_up(Terms::new_variable(0)); } pcalc_prop *Propositions::Abstract::to_create_something(kind *K, wording W) { diff --git a/docs/core-module/11-tcp.html b/docs/core-module/11-tcp.html index 090899b75..4f5666485 100644 --- a/docs/core-module/11-tcp.html +++ b/docs/core-module/11-tcp.html @@ -160,16 +160,14 @@ sense of the proposition by changing it, it will do so. if ((pl->element == PREDICATE_ATOM) && (pl->arity == 1)) A unary predicate is required to have an interpretation matching the kind of its term4.6; if (pl->element == EVERYWHERE_ATOM) - An EVERYWHERE atom needs its term to be an object4.9; + An EVERYWHERE atom needs its term to be an object4.8; if (pl->element == NOWHERE_ATOM) - A NOWHERE atom needs its term to be an object4.10; - if (pl->element == ISAKIND_ATOM) - An ISAKIND atom needs its term to be an object4.8; + A NOWHERE atom needs its term to be an object4.9; if (pl->element == HERE_ATOM) - A HERE atom needs its term to be an object4.11; + A HERE atom needs its term to be an object4.10; } - if (tck->log_to_I6_text) Show the variable assignment in the debugging log4.12; + if (tck->log_to_I6_text) Show the variable assignment in the debugging log4.11; return ALWAYS_MATCH; }@@ -423,16 +421,7 @@ would work instead. If it would, we make the change within the proposition. return NEVER_MATCH;
§4.8. An ISAKIND atom needs its term to be an object4.8 = -
- -- kind *actually_find = Propositions::Checker::kind_of_term(&(pl->terms[0]), &vta, tck); - if (Kinds::compatible(actually_find, K_object) == NEVER_MATCH) - internal_error("ISAKIND atom misapplied"); --
§4.9. An EVERYWHERE atom needs its term to be an object4.9 = +
§4.8. An EVERYWHERE atom needs its term to be an object4.8 =
@@ -451,7 +440,7 @@ would work instead. If it would, we make the change within the proposition.
}
§4.10. A NOWHERE atom needs its term to be an object4.10 = +
§4.9. A NOWHERE atom needs its term to be an object4.9 =
@@ -469,11 +458,11 @@ would work instead. If it would, we make the change within the proposition.
}
§4.11. It seems to be true that the A-parser never generates propositions which +
§4.10. It seems to be true that the A-parser never generates propositions which apply HERE incorrectly, but just in case:
-A HERE atom needs its term to be an object4.11 = +
A HERE atom needs its term to be an object4.10 =
@@ -490,12 +479,12 @@ apply HERE inco }
§4.12. Not so much for the debugging log as for the internal test, in fact, which +
§4.11. Not so much for the debugging log as for the internal test, in fact, which prints the log to an I6 string. This is the type-checking report in the case of success.
-Show the variable assignment in the debugging log4.12 = +
Show the variable assignment in the debugging log4.11 =
@@ -517,7 +506,7 @@ which is why the routine is here and not in the Terms section.-kind *Propositions::Checker::kind_of_term(pcalc_term *pt, variable_type_assignment *vta, +kind *Propositions::Checker::kind_of_term(pcalc_term *pt, variable_type_assignment *vta, tc_problem_kit *tck) { kind *K = Propositions::Checker::kind_of_term_inner(pt, vta, tck); pt->term_checked_as_kind = K; diff --git a/docs/core-module/12-ap.html b/docs/core-module/12-ap.html index 0c39822f2..31c38ff80 100644 --- a/docs/core-module/12-ap.html +++ b/docs/core-module/12-ap.html @@ -451,11 +451,18 @@ interpret no indication of a kind as meaning "object". if ((lookahead->arity == 1) && (lookahead->terms[0].variable == v)) { if (Atoms::is_CALLED(lookahead)) { NW = Atoms::CALLED_get_name(lookahead); - } else switch(lookahead->element) { - case KIND_ATOM: K = lookahead->assert_kind; break; - case ISAKIND_ATOM: is_a_kind = TRUE; K = lookahead->assert_kind; break; - case ISAVAR_ATOM: is_a_var = TRUE; break; - case ISACONST_ATOM: is_a_const = TRUE; break; + } else if (lookahead->element == KIND_ATOM) K = lookahead->assert_kind; + else if ((lookahead->element == PREDICATE_ATOM) && (lookahead->arity == 1)) { + unary_predicate *up = RETRIEVE_POINTER_unary_predicate(lookahead->predicate); + if (up->family == is_a_kind_up_family) { + is_a_kind = TRUE; K = up->assert_kind; + } + if (up->family == is_a_var_up_family) { + is_a_var = TRUE; + } + if (up->family == is_a_const_up_family) { + is_a_const = TRUE; + } } }diff --git a/docs/core-module/2-si.html b/docs/core-module/2-si.html index 652657b97..2acea3ad0 100644 --- a/docs/core-module/2-si.html +++ b/docs/core-module/2-si.html @@ -208,7 +208,7 @@ table we are in, yet still only cite a small part of it —-void StandardProblems::tcp_problem(SIGIL_ARGUMENTS, tc_problem_kit *tck, char *prototype) { +void StandardProblems::tcp_problem(SIGIL_ARGUMENTS, tc_problem_kit *tck, char *prototype) { if (tck->issue_error) { ACT_ON_SIGIL Problems::quote_source(1, current_sentence); diff --git a/docs/core-module/2-sq.html b/docs/core-module/2-sq.html index 921c109e7..952ccce7d 100644 --- a/docs/core-module/2-sq.html +++ b/docs/core-module/2-sq.html @@ -176,7 +176,7 @@ this as some kind of marginal will-never-happen case.-void Problems::quote_kind(int t, kind *K) { +void Problems::quote_kind(int t, kind *K) { if ((K == NULL) || (Kinds::eq(K, K_nil))) Problems::quote_text(t, "nothing"); else if ((K == NULL) || (Kinds::eq(K, K_void))) Problems::quote_text(t, "nothing"); else Problems::problem_quote(t, (void *) K, Problems::expand_kind); diff --git a/docs/core-module/5-tc.html b/docs/core-module/5-tc.html index 268e39002..12a18f0e2 100644 --- a/docs/core-module/5-tc.html +++ b/docs/core-module/5-tc.html @@ -942,6 +942,7 @@ to abbreviated forms of object names are normally allowed. else prop = Propositions::concatenate(prop, Propositions::Abstract::to_make_a_var()); Propositions::Assert::assert_true(prop, prevailing_mood); + if (NonlocalVariables::get_latest() == NULL) internal_error("failed to create"); val = Lvalues::new_actual_NONLOCAL_VARIABLE(NonlocalVariables::get_latest());