RequirementMachine: Fix up some comments

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -21,7 +21,7 @@
 //
 // Redundant rules that are not part of the minimal set are redundant are
 // detected by analyzing the set of rewrite loops computed by the completion
-// procedure.
+// procedure. See RewriteLoop.cpp for a discussion of rewrite loops.
 //
 // If a rewrite rule appears exactly once in a loop and without context, the
 // loop witnesses a redundancy; the rewrite rule is equivalent to traveling

lib/AST/RequirementMachine/KnuthBendix.cpp

@@ -23,6 +23,10 @@
 // pair to the other. This can introduce more overlaps with existing rules, and
 // the process iterates until fixed point.
 //
+// When completion records a new rewrite rule, it also constructs a rewrite loop
+// describing how this rule is derived from existing rules. See RewriteLoop.cpp
+// for a discussion of rewrite loops.
+//
 // This implementation also extends Knuth-Bendix to introduce new _generators_,
 // in addition to new relations as in the standard algorithm. See the comment at
 // the top of RewriteSystem::processMergedAssociatedTypes() for a description.

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -237,6 +237,9 @@ PropertyMap::~PropertyMap() {
 
 /// Look for a property bag corresponding to a suffix of the given range.
 ///
+/// The symbol range must correspond to a term that has already been
+/// simplified.
+///
 /// Returns nullptr if no information is known about this key.
 PropertyBag *
 PropertyMap::lookUpProperties(std::reverse_iterator<const Symbol *> begin,
@@ -249,6 +252,8 @@ PropertyMap::lookUpProperties(std::reverse_iterator<const Symbol *> begin,
 
 /// Look for a property bag corresponding to a suffix of the given key.
 ///
+/// The term must have already been simplified.
+///
 /// Returns nullptr if no information is known about this key.
 PropertyBag *
 PropertyMap::lookUpProperties(const MutableTerm &key) const {

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -9,6 +9,52 @@
 // See https://swift.org/CONTRIBUTORS.txt for the list of Swift project authors
 //
 //===----------------------------------------------------------------------===//
+//
+// This file defines data types used for representing redundancies among
+// rewrite rules. The information encoded in these types is ultimately used
+// for generic signature minimization.
+//
+// A RewriteStep is a single primitive transformation; the canonical example is
+// the application of a rewrite rule, possibly to a subterm.
+//
+// A RewritePath is a composition of RewriteSteps describing the transformation
+// of a term into another term. One place where a RewritePath originates is
+// RewriteSystem::simplify(); that method takes an optional RewritePath argument
+// to which the series of RewriteSteps performed during simplification are
+// appended. If the term was already canonical, the resulting path is empty,
+// otherwise it will consist of at least one RewriteStep.
+//
+// Simplification always applies rules by replacing a subterm equal to the LHS
+// with the RHS where LHS > RHS, so the RewriteSteps constructed there always
+// make the term shorter. However, more generally, RewriteSteps  can also
+// express the inverse rewrite, where RHS is replaced with LHS, making the term
+// longer.
+//
+// Inverted RewriteSteps are constructed in the Knuth-Bendix completion
+// algorithm. A simple example is where two rules (U.V => X) and (V.W => Y)
+// overlap on the term U.V.W. Then the induced rule (X.W => U.Y) (assuming that
+// X.W > U.Y) can be described by a RewritePath which begins at X.W, applies
+// the inverted rule (X => U.V) to the subterm X to obtain U.V.W, then applies
+// the rule (V.W => Y) to the subterm V.W to obtain U.Y.
+//
+// A RewriteLoop is a path that begins and ends at the same term. A RewriteLoop
+// describes a _redundancy_. For example, when completion adds a new rule to
+// resolve an overlap, it constructs a RewritePath describing this new rule in
+// terms of existing rules; by adding an additional rewrite step corresponding
+// to the new rule, we get a loop that begins and ends at the same point, or in
+// other words, a RewriteLoop.
+//
+// In the above example, we have a RewritePath from X.W to U.Y via the two
+// existing rewrite rules with the overlap term U.V.W in the middle. If we then
+// add a third rewrite step for the new rule inverted, (U.Y => X.W), we get a
+// loop that begins and ends at X.W. This loop encodes that the new rule
+// (X.W => U.Y) is redundant because it can be expresed in terms of other rules.
+//
+// The homotopy reduction algorithm in HomotopyReduction.cpp uses rewrite loops
+// to find a minimal set of rewrite rules, which are then used to construct a
+// minimal generic signature.
+//
+//===----------------------------------------------------------------------===//
 
 #include "swift/AST/Type.h"
 #include "llvm/Support/raw_ostream.h"

lib/AST/RequirementMachine/RewriteLoop.h

@@ -73,12 +73,24 @@ struct RewriteStep {
     Shift,
 
     /// If not inverted: the top of the primary stack must be a term ending
-    /// with a superclass or concrete type symbol. Each concrete substitution
-    /// in the term is pushed onto the primary stack.
+    /// with a superclass or concrete type symbol:
     ///
-    /// If inverted: pop concrete substitutions from the primary stack, which
-    /// must follow a term ending with a superclass or concrete type symbol.
-    /// The new substitutions replace the substitutions in that symbol.
+    ///    T.[concrete: C<...> with <X1, X2...>]
+    ///
+    /// Each concrete substitution Xn is pushed onto the primary stack,
+    /// producing:
+    ///
+    ///    T.[concrete: C<...> with <X1, X2...>] X1 X2...
+    ///
+    /// If inverted: pop concrete substitutions Xn' from the primary stack,
+    /// which must follow a term ending with a superclass or concrete type
+    /// symbol:
+    ///
+    ///    T.[concrete: C<...> with <X1, X2...>] X1' X2'...
+    ///
+    /// The new substitutions replace the substitutions in that symbol:
+    ///
+    ///    T.[concrete: C<...> with <X1', X2'...>]
     ///
     /// The Arg field encodes the number of substitutions.
     Decompose,
@@ -301,7 +313,8 @@ struct AppliedRewriteStep {
 
 /// A rewrite path is a list of instructions for a two-stack interpreter.
 ///
-/// - Shift moves a term from A to B (if not inverted) or B to A (if inverted).
+/// - Shift moves a term from the primary stack to the secondary stack
+///   (if not inverted) or secondary to primary (if inverted).
 ///
 /// - Decompose splits off the substitutions from a superclass or concrete type
 ///   symbol at the top of the primary stack (if not inverted) or assembles a

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -263,6 +263,7 @@ bool RewriteSystem::simplifySubstitutions(Symbol &symbol,
                                           RewritePath *path) const {
   assert(symbol.hasSubstitutions());
 
+  // Fast path if the type is fully concrete.
   auto substitutions = symbol.getSubstitutions();
   if (substitutions.empty())
     return false;
@@ -272,10 +273,12 @@ bool RewriteSystem::simplifySubstitutions(Symbol &symbol,
   unsigned oldSize = (path ? path->size() : 0);
 
   if (path) {
-    // The term is on the A stack. Push all substitutions onto the A stack.
-    path->add(RewriteStep::forDecompose(substitutions.size(), /*inverse=*/false));
+    // The term is at the top of the primary stack. Push all substitutions onto
+    // the primary stack.
+    path->add(RewriteStep::forDecompose(substitutions.size(),
+                                        /*inverse=*/false));
 
-    // Move all substitutions but the first one to the B stack.
+    // Move all substitutions but the first one to the secondary stack.
     for (unsigned i = 1; i < substitutions.size(); ++i)
       path->add(RewriteStep::forShift(/*inverse=*/false));
   }
@@ -287,23 +290,25 @@ bool RewriteSystem::simplifySubstitutions(Symbol &symbol,
   bool first = true;
   bool anyChanged = false;
   for (auto substitution : substitutions) {
-    // Move the next substitution from the B stack to the A stack.
+    // Move the next substitution from the secondary stack to the primary stack.
     if (!first && path)
       path->add(RewriteStep::forShift(/*inverse=*/true));
     first = false;
 
-    // The current substitution is at the top of the A stack; simplify it.
+    // The current substitution is at the top of the primary stack; simplify it.
     MutableTerm mutTerm(substitution);
     anyChanged |= simplify(mutTerm, path);
 
     // Record the new substitution.
     newSubstitutions.push_back(Term::get(mutTerm, Context));
   }
 
-  // All simplified substitutions are now on the A stack. Collect them to
+  // All simplified substitutions are now on the primary stack. Collect them to
   // produce the new term.
-  if (path)
-    path->add(RewriteStep::forDecompose(substitutions.size(), /*inverse=*/true));
+  if (path) {
+    path->add(RewriteStep::forDecompose(substitutions.size(),
+                                        /*inverse=*/true));
+  }
 
   // If nothing changed, we don't have to rebuild the symbol.
   if (!anyChanged) {
@@ -566,7 +571,7 @@ void RewriteSystem::simplifyRightHandSides() {
   }
 }
 
-/// Simplify substitutions in superclass, concrete type and concrete
+/// Simplify substitution terms in superclass, concrete type and concrete
 /// conformance symbols.
 void RewriteSystem::simplifyLeftHandSideSubstitutions() {
   for (unsigned ruleID = 0, e = Rules.size(); ruleID < e; ++ruleID) {