From 65f41dbca47e370dc559213249a4afedc2652a49 Mon Sep 17 00:00:00 2001 From: Graham Nelson Date: Thu, 4 Feb 2021 09:24:35 +0000 Subject: [PATCH] Completed simplifications --- README.md | 2 +- build.txt | 4 +- docs/calculus-module/2-kp.html | 2 +- docs/calculus-module/4-ap.html | 8 +- docs/calculus-module/4-prp.html | 6 +- docs/calculus-module/5-sc.html | 2 +- docs/calculus-module/5-smp.html | 136 +++++++++--------- inform7/Figures/timings-diagnostics.txt | 29 ++-- .../Chapter 5/Simplifications.w | 127 ++++++++-------- 9 files changed, 157 insertions(+), 159 deletions(-) diff --git a/README.md b/README.md index 19e8aa60b..c6a7d4088 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Inform 7 -v10.1.0-alpha.1+6R14 'Krypton' (3 February 2021) +v10.1.0-alpha.1+6R15 'Krypton' (4 February 2021) ## About Inform 7 diff --git a/build.txt b/build.txt index e292dfe26..c08008298 100644 --- a/build.txt +++ b/build.txt @@ -1,3 +1,3 @@ Prerelease: alpha.1 -Build Date: 3 February 2021 -Build Number: 6R14 +Build Date: 4 February 2021 +Build Number: 6R15 diff --git a/docs/calculus-module/2-kp.html b/docs/calculus-module/2-kp.html index 6f5cb382a..6e5bc6aa5 100644 --- a/docs/calculus-module/2-kp.html +++ b/docs/calculus-module/2-kp.html @@ -108,7 +108,7 @@ and these all belong to the family: return FALSE; } -kind *KindPredicates::get_kind(pcalc_prop *prop) { +kind *KindPredicates::get_kind(pcalc_prop *prop) { if ((prop) && (prop->element == PREDICATE_ATOM) && (prop->arity == 1)) { unary_predicate *up = RETRIEVE_POINTER_unary_predicate(prop->predicate); if (up->family == kind_up_family) return up->assert_kind; diff --git a/docs/calculus-module/4-ap.html b/docs/calculus-module/4-ap.html index 567e434fa..15c1792b9 100644 --- a/docs/calculus-module/4-ap.html +++ b/docs/calculus-module/4-ap.html @@ -156,7 +156,7 @@ in 2020 simplified the picture considerably. 

-pcalc_prop *Atoms::new(int element) {
+pcalc_prop *Atoms::new(int element) {
     pcalc_prop *prop = CREATE(pcalc_prop);
     prop->next = NULL;
     prop->element = element;
@@ -221,21 +221,21 @@ compilation time, and less obvious even how many variables are needed.
     return FALSE;
 }
 
-int Atoms::is_nonexistence_quantifier(pcalc_prop *prop) {
+int Atoms::is_nonexistence_quantifier(pcalc_prop *prop) {
     if ((prop) && (prop->element == QUANTIFIER_ATOM) &&
         (prop->quant == not_exists_quantifier))
         return TRUE;
     return FALSE;
 }
 
-int Atoms::is_forall_quantifier(pcalc_prop *prop) {
+int Atoms::is_forall_quantifier(pcalc_prop *prop) {
     if ((prop) && (prop->element == QUANTIFIER_ATOM) &&
         (prop->quant == for_all_quantifier))
         return TRUE;
     return FALSE;
 }
 
-int Atoms::is_notall_quantifier(pcalc_prop *prop) {
+int Atoms::is_notall_quantifier(pcalc_prop *prop) {
     if ((prop) && (prop->element == QUANTIFIER_ATOM) &&
         (prop->quant == not_for_all_quantifier))
         return TRUE;
diff --git a/docs/calculus-module/4-prp.html b/docs/calculus-module/4-prp.html
index 6fde6344a..872f4e110 100644
--- a/docs/calculus-module/4-prp.html
+++ b/docs/calculus-module/4-prp.html
@@ -559,7 +559,7 @@ is NULL.
 

 
 
-pcalc_prop *Propositions::insert_atom(pcalc_prop *prop, pcalc_prop *position,
+pcalc_prop *Propositions::insert_atom(pcalc_prop *prop, pcalc_prop *position,
     pcalc_prop *new_atom) {
     if (position == NULL) {
         new_atom->next = prop;
@@ -576,7 +576,7 @@ is NULL.
 

 
 
-pcalc_prop *Propositions::delete_atom(pcalc_prop *prop, pcalc_prop *position) {
+pcalc_prop *Propositions::delete_atom(pcalc_prop *prop, pcalc_prop *position) {
     if (position == NULL) {
         if (prop == NULL) internal_error("deleting atom nowhere");
         return prop->next;
@@ -653,7 +653,7 @@ two special pseudo-element-numbers:
 define END_PROP_HERE -1  a sentinel meaning "the proposition must end at this point"
 

 
-int Propositions::match(pcalc_prop *prop, int c, ...) {
+int Propositions::match(pcalc_prop *prop, int c, ...) {
     int outcome = TRUE;
     va_list ap;  the variable argument list signified by the dots
     va_start(ap, c);  macro to begin variable argument processing
diff --git a/docs/calculus-module/5-sc.html b/docs/calculus-module/5-sc.html
index 0fbca2bea..13d7b770c 100644
--- a/docs/calculus-module/5-sc.html
+++ b/docs/calculus-module/5-sc.html
@@ -599,7 +599,7 @@ Still, rule (iii) can only be ensured by writing the routines carefully.
 
     APPLY_SIMP(sentence_prop, Simplifications::turn_right_way_round);
     APPLY_SIMP(sentence_prop, Simplifications::region_containment);
-    APPLY_SIMP(sentence_prop, Simplifications::everywhere_and_nowhere);
+    APPLY_SIMP(sentence_prop, Simplifications::everywhere_and_nowhere);
     APPLY_SIMP(sentence_prop, Simplifications::reduce_predicates);
     APPLY_SIMP(sentence_prop, Simplifications::eliminate_redundant_variables);
     APPLY_SIMP(sentence_prop, Simplifications::not_related_to_something);
diff --git a/docs/calculus-module/5-smp.html b/docs/calculus-module/5-smp.html
index 419fcb663..8276ff205 100644
--- a/docs/calculus-module/5-smp.html
+++ b/docs/calculus-module/5-smp.html
@@ -91,7 +91,7 @@ function togglePopup(material_id) {
     
 
A set of operations which rewrite propositions to make them easier or quicker to test at run-time without changing their meaning.

 
-

+

 
 
§1. Golden rules. The following functions all take a propeosition \(\Sigma\) in the parameter
 prop, and return \(\Sigma'\); they set the flag pointed to by changed if
@@ -848,11 +848,9 @@ only one thing at a time, but might be in many regions at once.
 point where we choose to divert some uses to R_regional_containment.
 If \(R\) is a constant region name, and \(C_D\), \(C_R\) are the predicates for
 direct and region containment, then
-\(\) \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad
-\Sigma' = \cdots C_R(t, R)\cdots \(\)
-\(\) \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad
-\Sigma' = \cdots C_R(R, t)\cdots \(\)
-(Note that a region cannot directly contain any object, except a backdrop.)
+$$ \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(t, R)\cdots $$
+$$ \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(R, t)\cdots $$
+Note that a region cannot directly contain any object, except a backdrop.
 

 
 
@@ -874,7 +872,8 @@ direct and region containment, then
                 }
                 if (pl->terms[1-j].constant) {
                     kind *KB = Specifications::to_kind(pl->terms[1-j].constant);
-                    if (Kinds::Behaviour::is_object_of_kind(KB, K_backdrop)) backdropping = TRUE;
+                    if (Kinds::Behaviour::is_object_of_kind(KB, K_backdrop))
+                        backdropping = TRUE;
                 }
                 if ((regionality) && (!backdropping)) {
                     pl->predicate = STORE_POINTER_binary_predicate(R_regional_containment);
@@ -891,23 +890,22 @@ direct and region containment, then
 gain considerably by being able to eliminate a variable altogether. For
 instance, suppose we have "Mme Cholet is in a burrow". This will
 initially come out as
-\(\) \exists x: {\it burrow}(x)\land {\it in}(Cholet, x) \(\)
+$$ \exists x: {\it burrow}(x)\land {\it in}(C, x) $$
 To test that proposition requires trying all possible burrows \(x\).
 But exploiting the fact that Mme Cholet can only be in one place at a
 time, we can reduce the binary predicate to equality, thus:
-\(\) \exists x: {\it burrow}(x)\land {\it is}(ContainerOf(Cholet), x) \(\)
-A later simplification can then observe that this tells us what \(x\) must be,
+$$ \exists x: {\it burrow}(x)\land {\it is}(f(C), x) $$
+where \(f\) is the function determining the location of something. A later
+simplification can then observe that this tells us what \(x\) must be,
 and eliminate both quantifier and variable.
 

 
 
Formally, suppose \(B\) is a predicate with a function \(f_B\) such that \(B(x, y)\)
 is true if and only \(y = f_B(x)\). Then:
-\(\) \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
-\Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots \(\)
+$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots $$
 Similarly, if there is a function \(g_B\) such that \(B(x, y)\) if and only if
 \(x = g_B(y)\) then
-\(\) \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
-\Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots \(\)
+$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots $$
 Not all BPs have these: the reason for our fudge on regional containment (above)
 is that direct containment does, but region containment doesn't, and this is
 why it was necessary to separate the two out.
@@ -970,13 +968,13 @@ where this is safe.
                     if (permitted) {
                         LOGIF(PREDICATE_CALCULUS_WORKINGS, "Substituting %c <-- $0\n",
                             pcalc_vars[var_to_sub], &(pl->terms[1-j]));
-                         first delete the \({\it is}(v, t)\) predicate
+                         first delete the is(v, t) predicate
                         prop = Propositions::delete_atom(prop, pl_prev);
-                         then unbind the variable, by deleting its \(\exists v\) quantifier
+                         then unbind the variable, by deleting its exists v quantifier
                         prop = Propositions::delete_atom(prop, position_of_binding[var_to_sub]);
                         LOGIF(PREDICATE_CALCULUS_WORKINGS, "After deletion: $D\n", prop);
                         binding_status[var_to_sub] = NOT_BOUND_AT_ALL;
-                         then substitute for all other occurrences of \(v\)
+                         then substitute for all other occurrences of v
                         prop = Binding::substitute_term(prop, var_to_sub, pl->terms[1-j],
                             FALSE, NULL, changed);
                         *changed = TRUE;
@@ -1028,7 +1026,7 @@ substituting \(v = f_A(f_B(\cdots s))\).
 
 
But only if the term \(s\) underneath those functions does not make the equation
 \({\it is}(v, f_A(f_B(\cdots s)))\) implicit. Suppose \(s\) depends
-on a variable \(w\) which is bound and occurs {\it after} the binding of \(v\).
+on a variable \(w\) which is bound and occurs after the binding of \(v\).
 The value of such a variable \(w\) can depend on the value of \(v\). Saying that
 \(v=s\) may therefore not determine a unique value of \(v\) at all: it may be
 a subtle condition passed by a whole class of possible values, or none.
@@ -1039,10 +1037,10 @@ More problematic is \({\it is}(v, f_C(v))\), "\(v\) is the container of \(v\)",
 which is never true. Still worse is
 $$ \exists v: V_{=2} w: {\it is}(v, w) $$
 which literally says there is a value of \(v\) equal to two different things —
-certainly false. But if we were allowed to eliminate \(v\), we would get just
+certainly false. But if we eliminated \(v\), we would get just
 $$ V_{=2} w $$
 which asserts "there are exactly two objects" — which is certainly not a
-valid deduction, and might even be true.
+valid deduction.
 

 
 
Here var_to_sub is \(v\) and var_in_other_term is \(w\), or else they are \(-1\)
@@ -1066,14 +1064,15 @@ if no variables are present in their respective terms.
 
  • This code is used in §13.

 
§14. Simplify non-relation (deduction). As a result of the previous simplifications, it fairly often happens that we
 find a term like
-\(\) \lnot({\it thing}(t.component_parent)) \(\)
-in the proposition. This comes out of text such as "... not part of something",
+$$ \lnot({\it thing}(f_P(t))) $$
+where \(f_P\) is the function determining what, if anything, the object \(t\) is
+a component part of. This comes out of text such as "... not part of something",
 asserting first that there is no \(y\) such that \(t\) is a part of \(y\), and then
 simplifying to remove the \(y\) variable. A term like the one above is then
 left behind. But the negation is cumbersome, and makes the proposition harder
-to assert or test. Exploiting the fact that component_parent is a property
-which is either the part-parent or else nothing, we can simplify to:
-\(\) {\it is}(t.component_parent, nothing) \(\)
+to assert or test. Exploiting the fact that \(f_P(t)\) is a property
+which is either the part-parent or else \(N =\) nothing, we can simplify to:
+$$ {\it is}(f_P(t), N) $$
 And similar tricks can be pulled for other various-to-one-object predicates.
 

 
@@ -1081,8 +1080,7 @@ And similar tricks can be pulled for other various-to-one-object predicates.
 such that \(B(x, y)\) iff \(f_B(x) = y\), or else such that \(B(x, y)\) iff \(f_B(y) = x\);
 and such that the values of \(f_B\) are objects. Let \(K\) be a kind of object.
 Then:
-\(\) \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad
-\Sigma' = \cdots {\it is}(f_B(t), nothing) \cdots \(\)
+$$ \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t), N) \cdots $$
 

 
 
A similar trick for kinds of value is not possible, because — unlike objects —
@@ -1107,7 +1105,8 @@ they have no "not a valid case" value analogous to the non-object                 pcalc_term KIND_term = kind_atom->terms[0];
                 if (KIND_term.function) bp = KIND_term.function->bp;
                 if ((bp) && (Kinds::eq(K, BinaryPredicates::term_kind(bp, 1)))) {
-                    prop = Propositions::ungroup_after(prop, pl_prev, NULL);  remove negation grouping
+                     remove negation grouping
+                    prop = Propositions::ungroup_after(prop, pl_prev, NULL);
                     prop = Propositions::delete_atom(prop, pl_prev);  remove kind=K
                      now insert equality predicate:
                     prop = Propositions::insert_atom(prop, pl_prev,
@@ -1125,17 +1124,10 @@ they have no "not a valid case" value analogous to the non-object §15. Convert gerunds to nouns (deduction). Suppose we write:
 

 
-

-    
The funky thing to do is a stored action that varies.

-

-
-
and subsequently:
-

-
-

-    
the funky thing to do is waiting

-

-
+
+The funky thing to do is a stored action that varies.
+The funky thing to do is waiting.
+

 
Here "waiting" is a gerund, and although it describes an action it is a
 noun (thus a value) rather than a condition. We coerce its constant value
 accordingly.
@@ -1151,7 +1143,8 @@ accordingly.
         if ((pl->element == PREDICATE_ATOM) && (pl->arity == 2))
             for (int i=0; i<2; i++)
                 if (Conditions::is_TEST_ACTION(pl->terms[i].constant))
-                    pl->terms[i].constant = Conditions::action_tested(pl->terms[i].constant);
+                    pl->terms[i].constant =
+                        Conditions::action_tested(pl->terms[i].constant);
     return prop;
 }
 #endif
@@ -1165,23 +1158,19 @@ can also arise from text such as
 
 
 
where it's the numerical "weight" property which is owned by the balloon.
-(The language of abstract "property" always echoes that of real physical
-things — consider how the iTunes Music Store invites you to "buy" what
-is at best a lease of temporary, partial and revocable rights to make use
-of something with no physical essence. This isn't a con trick, or not
-altogether so. We like the word "buy"; we immediately understand it.)
 At this stage of simplification, the above has produced
-\(\) {\hbox{\it at-most}}(weight, 1)\land {\it is}(balloon, f_H(weight)) \(\)
-where \(H\) is the predicate a_has_b_predicate. As it stands, this
-proposition will fail type-checking, because it contains an implicit
-free variable — the object which owns the weight. We make this explicit
-by removing ${\it is}(balloon, f_H(weight))$ and replacing all other
-references to weight with "the weight of balloon".
+$$ {\it atmost}(w, 1)\land {\it is}(B, f_H(w)) $$
+where \(H\) is the predicate a_has_b_predicate. As it stands, this proposition
+will fail type-checking, because it contains an implicit free variable — the
+object which owns the weight. We make this explicit by removing
+\({\it is}(B, f_H(w))\) and replacing all other references to \(w\) with "the
+weight of \(B\)".
 

 
-
This is a fudge because it assumes — possibly wrongly — that all
-references to the weight are to the weight of the same thing. In
-sufficiently contrived sentences, this wouldn't be true.
+
This is a fudge because it assumes — possibly wrongly — that all references
+to the weight are to the weight of the same thing. In sufficiently contrived
+sentences, this wouldn't be true. No bugs have ever been reported which suggest
+that real users run into this.
 

 
 
@@ -1221,7 +1210,8 @@ term \(C\).
         Lvalues::new_PROPERTY_VALUE(spec, pl->terms[1-i].constant);
     Node::set_text(po_spec, prn->name);
     int no_substitutions_made;
-    prop = Simplifications::prop_substitute_prop_cons(prop, prn, po_spec, &no_substitutions_made, pl);
+    prop = Simplifications::prop_substitute_prop_cons(prop, prn, po_spec,
+        &no_substitutions_made, pl);
     if (no_substitutions_made > 0) {
         prop = Propositions::delete_atom(prop, pl_prev);
         PROPOSITION_EDITED_REPEATING_CURRENT(pl, prop);
@@ -1274,17 +1264,11 @@ usually mean "in all rooms", so that the sentence
 
means the sky is in every room, not that the sky is equal to every room.
 Since the literal reading would make no useful sense, Inform fudges the
 proposition to change it to the idiomatic one.
-\(\) \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
-\Sigma' = \cdots {\it everywhere}(t) \(\)
-\(\) \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
-\Sigma' = \cdots {\it everywhere}(t) \(\)
-\(\) \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
-\Sigma' = \cdots \lnot({\it everywhere}(t)) \(\)
-\(\) \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
-\Sigma' = \cdots \lnot({\it everywhere}(t)) \(\)
-

-
-
Note that we match this only at the end of a proposition, where \(v\) can
+$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
+$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
+$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
+$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
+Note that we match this only at the end of a proposition, where \(v\) can
 have no other consequence.
 

 
@@ -1316,11 +1300,13 @@ have no other consequence.
                     prop = Propositions::delete_atom(prop, pl_prev);  remove DOMAIN_CLOSE_ATOM
                     prop = Propositions::delete_atom(prop, pl_prev);  remove PREDICATE_ATOM
                     if (Atoms::is_notall_quantifier(q_atom))
-                        prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_CLOSE_ATOM));
+                        prop = Propositions::insert_atom(prop, pl_prev,
+                            Atoms::new(NEGATION_CLOSE_ATOM));
                     prop = Propositions::insert_atom(prop, pl_prev,
                         WherePredicates::everywhere_up(bp_atom->terms[j]));
                     if (Atoms::is_notall_quantifier(q_atom))
-                        prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_OPEN_ATOM));
+                        prop = Propositions::insert_atom(prop, pl_prev,
+                            Atoms::new(NEGATION_OPEN_ATOM));
                     PROPOSITION_EDITED(pl, prop);
                     break;
                 }
@@ -1357,6 +1343,14 @@ have no other consequence.
     return prop;
     #endif
 }
+

+
§19. Everywhere and nowhere (fudge). Similarly, if the proposition expresses the idea of "nowhere" or "everywhere"
+by spelling this out in quantifiers about being no place or every place, then
+replace those with uses of the special unary predicates for "nowhere" and
+"everywhere".
+

+
+
 pcalc_prop *Simplifications::everywhere_and_nowhere(pcalc_prop *prop, int *changed) {
     *changed = FALSE;
     #ifdef IF_MODULE
@@ -1387,7 +1381,8 @@ have no other consequence.
                         prop = Propositions::delete_atom(prop, pl_prev);  remove DOMAIN_CLOSE_ATOM
                         prop = Propositions::delete_atom(prop, pl_prev);  remove PREDICATE_ATOM
                         if (Atoms::is_notall_quantifier(q_atom))
-                            prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_CLOSE_ATOM));
+                            prop = Propositions::insert_atom(prop, pl_prev,
+                                Atoms::new(NEGATION_CLOSE_ATOM));
                         pcalc_prop *new_atom;
                         if (Atoms::is_nonexistence_quantifier(q_atom))
                             new_atom = WherePredicates::nowhere_up(bp_atom->terms[j]);
@@ -1395,7 +1390,8 @@ have no other consequence.
                             new_atom = WherePredicates::everywhere_up(bp_atom->terms[j]);
                         prop = Propositions::insert_atom(prop, pl_prev, new_atom);
                         if (Atoms::is_notall_quantifier(q_atom))
-                            prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_OPEN_ATOM));
+                            prop = Propositions::insert_atom(prop, pl_prev,
+                                Atoms::new(NEGATION_OPEN_ATOM));
                         PROPOSITION_EDITED(pl, prop);
                         break;
                     }
diff --git a/inform7/Figures/timings-diagnostics.txt b/inform7/Figures/timings-diagnostics.txt
index 2dcb86bbd..ce357a8df 100644
--- a/inform7/Figures/timings-diagnostics.txt
+++ b/inform7/Figures/timings-diagnostics.txt
@@ -1,35 +1,36 @@
 100.0% in inform7 run
      66.9% in compilation to Inter
-         25.4% in //Phrases::Manager::compile_first_block//
-          8.9% in //Phrases::Manager::compile_as_needed//
-          6.9% in //Strings::compile_responses//
-          6.3% in //World::Compile::compile//
+         25.7% in //Phrases::Manager::compile_first_block//
+          8.8% in //Phrases::Manager::compile_as_needed//
+          7.0% in //Strings::compile_responses//
+          6.1% in //World::Compile::compile//
           3.8% in //MajorNodes::pre_pass//
-          3.2% in //MajorNodes::pass_1//
-          2.1% in //Phrases::Manager::RulePrintingRule_routine//
+          3.3% in //MajorNodes::pass_1//
+          2.0% in //Phrases::Manager::RulePrintingRule_routine//
           2.0% in //Phrases::Manager::rulebooks_array//
-          1.0% in //RTVerbs::ConjugateVerb//
-          0.9% in //Phrases::Manager::traverse//
+          1.1% in //RTVerbs::ConjugateVerb//
+          0.8% in //Phrases::Manager::traverse//
+          0.5% in //Phrases::Manager::compile_rulebooks//
           0.5% in //Phrases::Manager::parse_rule_parameters//
           0.5% in //World::complete//
           0.3% in //MajorNodes::pass_2//
-          0.3% in //Phrases::Manager::compile_rulebooks//
           0.3% in //RTRelations::compile_defined_relations//
           0.1% in //Kinds::RunTime::compile_data_type_support_routines//
           0.1% in //PL::Parsing::Verbs::compile_all//
           0.1% in //Task::make_built_in_kind_constructors//
           3.3% not specifically accounted for
-     30.9% in running Inter pipeline
+     30.7% in running Inter pipeline
+         10.6% in step preparation
           9.8% in inter step 2/12: link
-          9.8% in step preparation
-          7.4% in inter step 12/12: generate inform6 -> auto.inf
+          7.1% in inter step 12/12: generate inform6 -> auto.inf
           0.3% in inter step 9/12: make-identifiers-unique
           0.1% in inter step 10/12: reconcile-verbs
           0.1% in inter step 11/12: eliminate-redundant-labels
+          0.1% in inter step 4/12: parse-linked-matter
           0.1% in inter step 5/12: resolve-conditional-compilation
           0.1% in inter step 6/12: assimilate
           0.1% in inter step 7/12: resolve-external-symbols
           0.1% in inter step 8/12: inspect-plugs
-          2.4% not specifically accounted for
+          1.5% not specifically accounted for
       2.0% in supervisor
-      0.2% not specifically accounted for
+      0.4% not specifically accounted for
diff --git a/services/calculus-module/Chapter 5/Simplifications.w b/services/calculus-module/Chapter 5/Simplifications.w
index 32575429d..4ed1d9613 100644
--- a/services/calculus-module/Chapter 5/Simplifications.w	
+++ b/services/calculus-module/Chapter 5/Simplifications.w	
@@ -684,11 +684,9 @@ So far we assume every "in" means the |R_containment|. This is the
 point where we choose to divert some uses to |R_regional_containment|.
 If $R$ is a constant region name, and $C_D$, $C_R$ are the predicates for
 direct and region containment, then
-$$ \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad
-\Sigma' = \cdots C_R(t, R)\cdots $$
-$$ \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad
-\Sigma' = \cdots C_R(R, t)\cdots $$
-(Note that a region cannot directly contain any object, except a backdrop.)
+$$ \Sigma = \cdots C_D(t, R)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(t, R)\cdots $$
+$$ \Sigma = \cdots C_D(R, t)\cdots \quad \longrightarrow \quad \Sigma' = \cdots C_R(R, t)\cdots $$
+Note that a region cannot directly contain any object, except a backdrop.
 
 =
 pcalc_prop *Simplifications::region_containment(pcalc_prop *prop, int *changed) {
@@ -709,7 +707,8 @@ pcalc_prop *Simplifications::region_containment(pcalc_prop *prop, int *changed)
 				}
 				if (pl->terms[1-j].constant) {
 					kind *KB = Specifications::to_kind(pl->terms[1-j].constant);
-					if (Kinds::Behaviour::is_object_of_kind(KB, K_backdrop)) backdropping = TRUE;
+					if (Kinds::Behaviour::is_object_of_kind(KB, K_backdrop))
+						backdropping = TRUE;
 				}
 				if ((regionality) && (!backdropping)) {
 					pl->predicate = STORE_POINTER_binary_predicate(R_regional_containment);
@@ -727,22 +726,21 @@ If we are able to reduce a binary to a unary predicate, we will probably
 gain considerably by being able to eliminate a variable altogether. For
 instance, suppose we have "Mme Cholet is in a burrow". This will
 initially come out as
-$$ \exists x: {\it burrow}(x)\land {\it in}(|Cholet|, x) $$
+$$ \exists x: {\it burrow}(x)\land {\it in}(C, x) $$
 To test that proposition requires trying all possible burrows $x$.
 But exploiting the fact that Mme Cholet can only be in one place at a
 time, we can reduce the binary predicate to equality, thus:
-$$ \exists x: {\it burrow}(x)\land {\it is}(|ContainerOf(Cholet)|, x) $$
-A later simplification can then observe that this tells us what $x$ must be,
+$$ \exists x: {\it burrow}(x)\land {\it is}(f(C), x) $$
+where $f$ is the function determining the location of something. A later
+simplification can then observe that this tells us what $x$ must be,
 and eliminate both quantifier and variable.
 
 Formally, suppose $B$ is a predicate with a function $f_B$ such that $B(x, y)$
 is true if and only $y = f_B(x)$. Then:
-$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
-\Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots $$
+$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t_1), t_2) \cdots $$
 Similarly, if there is a function $g_B$ such that $B(x, y)$ if and only if
 $x = g_B(y)$ then
-$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad
-\Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots $$
+$$ \Sigma = \cdots B(t_1, t_2) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(t_1, g_B(t_2)) \cdots $$
 Not all BPs have these: the reason for our fudge on regional containment (above)
 is that direct containment does, but region containment doesn't, and this is
 why it was necessary to separate the two out.
@@ -804,13 +802,13 @@ pcalc_prop *Simplifications::eliminate_redundant_variables(pcalc_prop *prop, int
 					if (permitted) {
 						LOGIF(PREDICATE_CALCULUS_WORKINGS, "Substituting %c <-- $0\n",
 							pcalc_vars[var_to_sub], &(pl->terms[1-j]));
-						/* first delete the ${\it is}(v, t)$ predicate */
+						/* first delete the is(v, t) predicate */
 						prop = Propositions::delete_atom(prop, pl_prev);
-						/* then unbind the variable, by deleting its $\exists v$ quantifier */
+						/* then unbind the variable, by deleting its exists v quantifier */
 						prop = Propositions::delete_atom(prop, position_of_binding[var_to_sub]);
 						LOGIF(PREDICATE_CALCULUS_WORKINGS, "After deletion: $D\n", prop);
 						binding_status[var_to_sub] = NOT_BOUND_AT_ALL;
-						/* then substitute for all other occurrences of $v$ */
+						/* then substitute for all other occurrences of v */
 						prop = Binding::substitute_term(prop, var_to_sub, pl->terms[1-j],
 							FALSE, NULL, changed);
 						*changed = TRUE;
@@ -856,7 +854,7 @@ substituting $v = f_A(f_B(\cdots s))$.
 
 But only if the term $s$ underneath those functions does not make the equation
 ${\it is}(v, f_A(f_B(\cdots s)))$ implicit. Suppose $s$ depends
-on a variable $w$ which is bound and occurs {\it after} the binding of $v$.
+on a variable $w$ which is bound and occurs after the binding of $v$.
 The value of such a variable $w$ can depend on the value of $v$. Saying that
 $v=s$ may therefore not determine a unique value of $v$ at all: it may be
 a subtle condition passed by a whole class of possible values, or none.
@@ -866,10 +864,10 @@ More problematic is ${\it is}(v, f_C(v))$, "$v$ is the container of $v$",
 which is never true. Still worse is
 $$ \exists v: V_{=2} w: {\it is}(v, w) $$
 which literally says there is a value of $v$ equal to two different things --
-certainly false. But if we were allowed to eliminate $v$, we would get just
+certainly false. But if we eliminated $v$, we would get just
 $$ V_{=2} w $$
 which asserts "there are exactly two objects" -- which is certainly not a
-valid deduction, and might even be true.
+valid deduction.
 
 Here |var_to_sub| is $v$ and |var_in_other_term| is $w$, or else they are $-1$
 if no variables are present in their respective terms.
@@ -888,22 +886,22 @@ if no variables are present in their respective terms.
 @h Simplify non-relation (deduction).
 As a result of the previous simplifications, it fairly often happens that we
 find a term like
-$$ \lnot({\it thing}(t|.component_parent|)) $$
-in the proposition. This comes out of text such as "... not part of something",
+$$ \lnot({\it thing}(f_P(t))) $$
+where $f_P$ is the function determining what, if anything, the object $t$ is
+a component part of. This comes out of text such as "... not part of something",
 asserting first that there is no $y$ such that $t$ is a part of $y$, and then
 simplifying to remove the $y$ variable. A term like the one above is then
 left behind. But the negation is cumbersome, and makes the proposition harder
-to assert or test. Exploiting the fact that |component_parent| is a property
-which is either the part-parent or else |nothing|, we can simplify to:
-$$ {\it is}(t|.component_parent|, |nothing|) $$
+to assert or test. Exploiting the fact that $f_P(t)$ is a property
+which is either the part-parent or else $N =$ |nothing|, we can simplify to:
+$$ {\it is}(f_P(t), N) $$
 And similar tricks can be pulled for other various-to-one-object predicates.
 
 Formally, let $B$ be a binary predicate supporting either a function $f_B$
 such that $B(x, y)$ iff $f_B(x) = y$, or else such that $B(x, y)$ iff $f_B(y) = x$;
 and such that the values of $f_B$ are objects. Let $K$ be a kind of object.
 Then:
-$$ \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad
-\Sigma' = \cdots {\it is}(f_B(t), |nothing|) \cdots $$
+$$ \Sigma = \cdots \lnot( K(f_B(t))) \cdots \quad \longrightarrow \quad \Sigma' = \cdots {\it is}(f_B(t), N) \cdots $$
 
 A similar trick for kinds of value is not possible, because -- unlike objects --
 they have no "not a valid case" value analogous to the non-object |nothing|.
@@ -926,7 +924,8 @@ pcalc_prop *Simplifications::not_related_to_something(pcalc_prop *prop, int *cha
 				pcalc_term KIND_term = kind_atom->terms[0];
 				if (KIND_term.function) bp = KIND_term.function->bp;
 				if ((bp) && (Kinds::eq(K, BinaryPredicates::term_kind(bp, 1)))) {
-					prop = Propositions::ungroup_after(prop, pl_prev, NULL); /* remove negation grouping */
+					/* remove negation grouping */
+					prop = Propositions::ungroup_after(prop, pl_prev, NULL); 
 					prop = Propositions::delete_atom(prop, pl_prev); /* remove |kind=K| */
 					/* now insert equality predicate: */
 					prop = Propositions::insert_atom(prop, pl_prev,
@@ -943,13 +942,10 @@ pcalc_prop *Simplifications::not_related_to_something(pcalc_prop *prop, int *cha
 
 @h Convert gerunds to nouns (deduction).
 Suppose we write:
-
->> The funky thing to do is a stored action that varies.
-
-and subsequently:
-
->> the funky thing to do is waiting
-
+= (text as Inform 7)
+The funky thing to do is a stored action that varies.
+The funky thing to do is waiting.
+=
 Here "waiting" is a gerund, and although it describes an action it is a
 noun (thus a value) rather than a condition. We coerce its constant value
 accordingly.
@@ -964,7 +960,8 @@ pcalc_prop *Simplifications::convert_gerunds(pcalc_prop *prop, int *changed) {
 		if ((pl->element == PREDICATE_ATOM) && (pl->arity == 2))
 			for (int i=0; i<2; i++)
 				if (Conditions::is_TEST_ACTION(pl->terms[i].constant))
-					pl->terms[i].constant = Conditions::action_tested(pl->terms[i].constant);
+					pl->terms[i].constant =
+						Conditions::action_tested(pl->terms[i].constant);
 	return prop;
 }
 #endif
@@ -976,22 +973,18 @@ can also arise from text such as
 >> the balloon has weight at most 1
 
 where it's the numerical "weight" property which is owned by the balloon.
-(The language of abstract "property" always echoes that of real physical
-things -- consider how the iTunes Music Store invites you to "buy" what
-is at best a lease of temporary, partial and revocable rights to make use
-of something with no physical essence. This isn't a con trick, or not
-altogether so. We like the word "buy"; we immediately understand it.)
 At this stage of simplification, the above has produced
-$$ {\hbox{\it at-most}}(|weight|, 1)\land {\it is}(|balloon|, f_H(|weight|)) $$
-where $H$ is the predicate |a_has_b_predicate|. As it stands, this
-proposition will fail type-checking, because it contains an implicit
-free variable -- the object which owns the weight. We make this explicit
-by removing ${\it is}(|balloon|, f_H(|weight|))$ and replacing all other
-references to |weight| with "the weight of |balloon|".
+$$ {\it atmost}(w, 1)\land {\it is}(B, f_H(w)) $$
+where $H$ is the predicate |a_has_b_predicate|. As it stands, this proposition
+will fail type-checking, because it contains an implicit free variable -- the
+object which owns the weight. We make this explicit by removing
+${\it is}(B, f_H(w))$ and replacing all other references to $w$ with "the
+weight of $B$".
 
-This is a fudge because it assumes -- possibly wrongly -- that all
-references to the weight are to the weight of the same thing. In
-sufficiently contrived sentences, this wouldn't be true.
+This is a fudge because it assumes -- possibly wrongly -- that all references
+to the weight are to the weight of the same thing. In sufficiently contrived
+sentences, this wouldn't be true. No bugs have ever been reported which suggest
+that real users run into this.
 
 =
 #ifdef CORE_MODULE
@@ -1026,7 +1019,8 @@ term $C$.
 		Lvalues::new_PROPERTY_VALUE(spec, pl->terms[1-i].constant);
 	Node::set_text(po_spec, prn->name);
 	int no_substitutions_made;
-	prop = Simplifications::prop_substitute_prop_cons(prop, prn, po_spec, &no_substitutions_made, pl);
+	prop = Simplifications::prop_substitute_prop_cons(prop, prn, po_spec,
+		&no_substitutions_made, pl);
 	if (no_substitutions_made > 0) {
 		prop = Propositions::delete_atom(prop, pl_prev);
 		PROPOSITION_EDITED_REPEATING_CURRENT(pl, prop);
@@ -1075,15 +1069,10 @@ usually mean "in all rooms", so that the sentence
 means the sky is in every room, not that the sky is equal to every room.
 Since the literal reading would make no useful sense, Inform fudges the
 proposition to change it to the idiomatic one.
-$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
-\Sigma' = \cdots {\it everywhere}(t) $$
-$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
-\Sigma' = \cdots {\it everywhere}(t) $$
-$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(v, t) \quad \longrightarrow \quad
-\Sigma' = \cdots \lnot({\it everywhere}(t)) $$
-$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)}\rbrace : {\it is}(t, v) \quad \longrightarrow \quad
-\Sigma' = \cdots \lnot({\it everywhere}(t)) $$
-
+$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
+$$ \Sigma = \cdots \forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots {\it everywhere}(t) $$
+$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(v, t) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
+$$ \Sigma = \cdots \not\forall v\in\lbrace v\mid{\it room}(v)\rbrace : {\it is}(t, v) \quad \longrightarrow \quad \Sigma' = \cdots \lnot({\it everywhere}(t)) $$
 Note that we match this only at the end of a proposition, where $v$ can
 have no other consequence.
 
@@ -1115,11 +1104,13 @@ pcalc_prop *Simplifications::is_all_rooms(pcalc_prop *prop, int *changed) {
 					prop = Propositions::delete_atom(prop, pl_prev); /* remove |DOMAIN_CLOSE_ATOM| */
 					prop = Propositions::delete_atom(prop, pl_prev); /* remove |PREDICATE_ATOM| */
 					if (Atoms::is_notall_quantifier(q_atom))
-						prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_CLOSE_ATOM));
+						prop = Propositions::insert_atom(prop, pl_prev,
+							Atoms::new(NEGATION_CLOSE_ATOM));
 					prop = Propositions::insert_atom(prop, pl_prev,
 						WherePredicates::everywhere_up(bp_atom->terms[j]));
 					if (Atoms::is_notall_quantifier(q_atom))
-						prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_OPEN_ATOM));
+						prop = Propositions::insert_atom(prop, pl_prev,
+							Atoms::new(NEGATION_OPEN_ATOM));
 					PROPOSITION_EDITED(pl, prop);
 					break;
 				}
@@ -1156,6 +1147,14 @@ pcalc_prop *Simplifications::is_all_rooms(pcalc_prop *prop, int *changed) {
 	return prop;
 	#endif
 }
+
+@h Everywhere and nowhere (fudge).
+Similarly, if the proposition expresses the idea of "nowhere" or "everywhere"
+by spelling this out in quantifiers about being no place or every place, then
+replace those with uses of the special unary predicates for "nowhere" and
+"everywhere".
+
+=
 pcalc_prop *Simplifications::everywhere_and_nowhere(pcalc_prop *prop, int *changed) {
 	*changed = FALSE;
 	#ifdef IF_MODULE
@@ -1186,7 +1185,8 @@ pcalc_prop *Simplifications::everywhere_and_nowhere(pcalc_prop *prop, int *chang
 						prop = Propositions::delete_atom(prop, pl_prev); /* remove |DOMAIN_CLOSE_ATOM| */
 						prop = Propositions::delete_atom(prop, pl_prev); /* remove |PREDICATE_ATOM| */
 						if (Atoms::is_notall_quantifier(q_atom))
-							prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_CLOSE_ATOM));
+							prop = Propositions::insert_atom(prop, pl_prev,
+								Atoms::new(NEGATION_CLOSE_ATOM));
 						pcalc_prop *new_atom;
 						if (Atoms::is_nonexistence_quantifier(q_atom))
 							new_atom = WherePredicates::nowhere_up(bp_atom->terms[j]);
@@ -1194,7 +1194,8 @@ pcalc_prop *Simplifications::everywhere_and_nowhere(pcalc_prop *prop, int *chang
 							new_atom = WherePredicates::everywhere_up(bp_atom->terms[j]);
 						prop = Propositions::insert_atom(prop, pl_prev, new_atom);
 						if (Atoms::is_notall_quantifier(q_atom))
-							prop = Propositions::insert_atom(prop, pl_prev, Atoms::new(NEGATION_OPEN_ATOM));
+							prop = Propositions::insert_atom(prop, pl_prev,
+								Atoms::new(NEGATION_OPEN_ATOM));
 						PROPOSITION_EDITED(pl, prop);
 						break;
 					}