RequirementMachine: RewriteStep stores both whiskers

slavapestov · slavapestov · commit c6403e65e1d3 · 2021-09-24T08:59:50.000-04:00
diff --git a/lib/AST/RequirementMachine/Debug.h b/lib/AST/RequirementMachine/Debug.h
@@ -35,6 +35,9 @@ enum class DebugFlags : unsigned {
 
   /// Print debug output when concretizing nested types in the property map.
   ConcretizeNestedTypes = (1<<5)
+
+  /// Print debug output from the homotopy reduction algorithm.
+  HomotopyReduction = (1<<7),
 };
 
 using DebugOptions = OptionSet<DebugFlags>;
@@ -43,4 +46,4 @@ using DebugOptions = OptionSet<DebugFlags>;
 
 }
 
-#endif
+#endif
diff --git a/lib/AST/RequirementMachine/RequirementMachine.cpp b/lib/AST/RequirementMachine/RequirementMachine.cpp
@@ -448,3 +448,7 @@ void RequirementMachine::computeCompletion() {
 bool RequirementMachine::isComplete() const {
   return Complete;
 }
+
+void RequirementMachine::computeMinimalRequirements(const ProtocolDecl *proto) {
+  System.minimizeRewriteSystem();
+}
diff --git a/lib/AST/RequirementMachine/RequirementMachine.h b/lib/AST/RequirementMachine/RequirementMachine.h
@@ -107,6 +107,8 @@ class RequirementMachine final {
                                                  ProtocolDecl *protocol);
   TypeDecl *lookupNestedType(Type depType, Identifier name) const;
 
+  void computeMinimalRequirements(const ProtocolDecl *proto);
+
   void verify(const MutableTerm &term) const;
   void dump(llvm::raw_ostream &out) const;
 };
diff --git a/lib/AST/RequirementMachine/RewriteContext.cpp b/lib/AST/RequirementMachine/RewriteContext.cpp
@@ -33,6 +33,7 @@ static DebugOptions parseDebugFlags(StringRef debugFlags) {
       .Case("completion", DebugFlags::Completion)
       .Case("concrete-unification", DebugFlags::ConcreteUnification)
       .Case("concretize-nested-types", DebugFlags::ConcretizeNestedTypes)
+      .Case("homotopy-reduction", DebugFlags::HomotopyReduction)
       .Default(None);
     if (!flag) {
       llvm::errs() << "Unknown debug flag in -debug-requirement-machine "
diff --git a/lib/AST/RequirementMachine/RewriteSystem.cpp b/lib/AST/RequirementMachine/RewriteSystem.cpp
@@ -46,18 +46,27 @@ RewriteStep::applyRewriteRule(MutableTerm &term,
   auto lhs = (Inverse ? rule.getRHS() : rule.getLHS());
   auto rhs = (Inverse ? rule.getLHS() : rule.getRHS());
 
-  if (!std::equal(term.begin() + Offset,
-                  term.begin() + Offset + lhs.size(),
-                  lhs.begin())) {
-    llvm::errs() << "Invalid rewrite path\n";
+  auto bug = [&](StringRef msg) {
+    llvm::errs() << msg << "\n";
     llvm::errs() << "- Term: " << term << "\n";
-    llvm::errs() << "- Offset: " << Offset << "\n";
+    llvm::errs() << "- StartOffset: " << StartOffset << "\n";
+    llvm::errs() << "- EndOffset: " << EndOffset << "\n";
     llvm::errs() << "- Expected subterm: " << lhs << "\n";
     abort();
+  };
+
+  if (term.size() != StartOffset + lhs.size() + EndOffset) {
+    bug("Invalid whiskering");
+  }
+
+  if (!std::equal(term.begin() + StartOffset,
+                  term.begin() + StartOffset + lhs.size(),
+                  lhs.begin())) {
+    bug("Invalid subterm");
   }
 
-  MutableTerm prefix(term.begin(), term.begin() + Offset);
-  MutableTerm suffix(term.begin() + Offset + lhs.size(), term.end());
+  MutableTerm prefix(term.begin(), term.begin() + StartOffset);
+  MutableTerm suffix(term.end() - EndOffset, term.end());
 
   term = prefix;
   term.append(rhs);
@@ -69,25 +78,27 @@ RewriteStep::applyRewriteRule(MutableTerm &term,
 MutableTerm RewriteStep::applyAdjustment(MutableTerm &term,
                                          const RewriteSystem &system) const {
   assert(Kind == AdjustConcreteType);
+  assert(EndOffset == 0);
+  assert(RuleID == 0);
 
   auto &ctx = system.getRewriteContext();
-  MutableTerm prefix(term.begin(), term.begin() + Offset);
+  MutableTerm prefix(term.begin(), term.begin() + StartOffset);
 
   // We're either adding or removing the prefix to each concrete substitution.
   term.back() = term.back().transformConcreteSubstitutions(
     [&](Term t) -> Term {
       if (Inverse) {
         if (!std::equal(t.begin(),
-                        t.begin() + Offset,
+                        t.begin() + StartOffset,
                         prefix.begin())) {
           llvm::errs() << "Invalid rewrite path\n";
           llvm::errs() << "- Term: " << term << "\n";
-          llvm::errs() << "- Offset: " << Offset << "\n";
+          llvm::errs() << "- Start offset: " << StartOffset << "\n";
           llvm::errs() << "- Expected subterm: " << prefix << "\n";
           abort();
         }
 
-        MutableTerm mutTerm(t.begin() + Offset, t.end());
+        MutableTerm mutTerm(t.begin() + StartOffset, t.end());
         return Term::get(mutTerm, ctx);
       } else {
         MutableTerm mutTerm(prefix);
@@ -99,6 +110,18 @@ MutableTerm RewriteStep::applyAdjustment(MutableTerm &term,
   return prefix;
 }
 
+void RewriteStep::apply(MutableTerm &term, const RewriteSystem &system) const {
+  switch (Kind) {
+  case ApplyRewriteRule:
+    (void) applyRewriteRule(term, system);
+    break;
+
+  case AdjustConcreteType:
+    (void) applyAdjustment(term, system);
+    break;
+  }
+}
+
 /// Dumps the rewrite step that was applied to \p term. Mutates \p term to
 /// reflect the application of the rule.
 void RewriteStep::dump(llvm::raw_ostream &out,
@@ -264,7 +287,8 @@ bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs,
   if (path) {
     // We have a rewrite path from the simplified lhs to the simplified rhs;
     // add a rewrite step applying the new rule in reverse to close the loop.
-    loop.add(RewriteStep::forRewriteRule(/*offset=*/0, newRuleID, /*inverse=*/true));
+    loop.add(RewriteStep::forRewriteRule(/*startOffset=*/0, /*endOffset=*/0,
+                                         newRuleID, /*inverse=*/true));
     HomotopyGenerators.emplace_back(lhs, loop);
 
     if (Debug.contains(DebugFlags::Add)) {
@@ -322,11 +346,13 @@ bool RewriteSystem::simplify(MutableTerm &term, RewritePath *path) const {
           auto to = from + rule.getLHS().size();
           assert(std::equal(from, to, rule.getLHS().begin()));
 
+          unsigned startOffset = (unsigned)(from - term.begin());
+          unsigned endOffset = term.size() - rule.getLHS().size() - startOffset;
+
           term.rewriteSubTerm(from, to, rule.getRHS());
 
           if (path) {
-            unsigned offset = (unsigned)(from - term.begin());
-            path->add(RewriteStep::forRewriteRule(offset, *ruleID,
+            path->add(RewriteStep::forRewriteRule(startOffset, endOffset, *ruleID,
                                                   /*inverse=*/false));
           }
 
@@ -426,12 +452,12 @@ void RewriteSystem::simplifyRewriteSystem() {
 
     // (2) Next, apply the original rule in reverse to produce the
     // original lhs.
-    loop.add(RewriteStep::forRewriteRule(/*offset=*/0, ruleID,
-                                         /*inverse=*/true));
+    loop.add(RewriteStep::forRewriteRule(/*startOffset=*/0, /*endOffset=*/0,
+                                         ruleID, /*inverse=*/true));
 
     // (3) Finally, apply the new rule to produce the simplified rhs.
-    loop.add(RewriteStep::forRewriteRule(/*offset=*/0, newRuleID,
-                                         /*inverse=*/false));
+    loop.add(RewriteStep::forRewriteRule(/*startOffset=*/0, /*endOffset=*/0,
+                                         newRuleID, /*inverse=*/false));
 
     if (Debug.contains(DebugFlags::Completion)) {
       llvm::dbgs() << "$ Right hand side simplification recorded a loop: ";
@@ -510,14 +536,7 @@ void RewriteSystem::verifyHomotopyGenerators() const {
     auto term = loop.first;
 
     for (const auto &step : loop.second) {
-      switch (step.Kind) {
-      case RewriteStep::ApplyRewriteRule:
-        (void) step.applyRewriteRule(term, *this);
-        break;
-      case RewriteStep::AdjustConcreteType:
-        (void) step.applyAdjustment(term, *this);
-        break;
-      }
+      step.apply(term, *this);
     }
 
     if (term != loop.first) {
diff --git a/lib/AST/RequirementMachine/RewriteSystem.h b/lib/AST/RequirementMachine/RewriteSystem.h
@@ -107,8 +107,13 @@ struct RewriteStep {
   /// The rewrite step kind.
   unsigned Kind : 1;
 
-  /// The position within the term where the rule is being applied.
-  unsigned Offset : 15;
+  /// The size of the left whisker, which is the position within the term where
+  /// the rule is being applied. In A.(X => Y).B, this is |A|=1.
+  unsigned StartOffset : 7;
+
+  /// The size of the right whisker, which is the length of the remaining suffix
+  /// after the rule is applied. In A.(X => Y).B, this is |B|=1.
+  unsigned EndOffset : 7;
 
   /// The index of the rule in the rewrite system.
   unsigned RuleID : 15;
@@ -117,22 +122,27 @@ struct RewriteStep {
   /// with the right hand side. If true, vice versa.
   unsigned Inverse : 1;
 
-  RewriteStep(StepKind kind, unsigned offset, unsigned ruleID, bool inverse) {
+  RewriteStep(StepKind kind, unsigned startOffset, unsigned endOffset,
+              unsigned ruleID, bool inverse) {
     Kind = unsigned(kind);
 
-    Offset = offset;
-    assert(Offset == offset && "Overflow");
+    StartOffset = startOffset;
+    assert(StartOffset == startOffset && "Overflow");
+    EndOffset = endOffset;
+    assert(EndOffset == endOffset && "Overflow");
     RuleID = ruleID;
     assert(RuleID == ruleID && "Overflow");
     Inverse = inverse;
   }
 
-  static RewriteStep forRewriteRule(unsigned offset, unsigned ruleID, bool inverse) {
-    return RewriteStep(ApplyRewriteRule, offset, ruleID, inverse);
+  static RewriteStep forRewriteRule(unsigned startOffset, unsigned endOffset,
+                                    unsigned ruleID, bool inverse) {
+    return RewriteStep(ApplyRewriteRule, startOffset, endOffset, ruleID, inverse);
   }
 
   static RewriteStep forAdjustment(unsigned offset, bool inverse) {
-    return RewriteStep(AdjustConcreteType, offset, /*ruleID=*/0, inverse);
+    return RewriteStep(AdjustConcreteType, offset, /*endOffset=*/0,
+                       /*ruleID=*/0, inverse);
   }
 
   void invert() {
@@ -145,6 +155,8 @@ struct RewriteStep {
   MutableTerm applyAdjustment(MutableTerm &term,
                               const RewriteSystem &system) const;
 
+  void apply(MutableTerm &term, const RewriteSystem &system) const;
+
   void dump(llvm::raw_ostream &out,
             MutableTerm &term,
             const RewriteSystem &system) const;
@@ -158,6 +170,10 @@ struct RewritePath {
     return Steps.empty();
   }
 
+  unsigned size() const {
+    return Steps.size();
+  }
+
   void add(RewriteStep step) {
     Steps.push_back(step);
   }
@@ -223,9 +239,19 @@ class RewriteSystem final {
   /// Pairs of rules which have already been checked for overlap.
   llvm::DenseSet<std::pair<unsigned, unsigned>> CheckedOverlaps;
 
-  /// Homotopy generators (2-cells) for this rewrite system. These are the
-  /// cyclic rewrite paths which rewrite a term back to itself. This
-  /// data informs the generic signature minimization algorithm.
+  /// Homotopy generators for this rewrite system. These are the
+  /// cyclic rewrite paths which rewrite a term back to itself.
+  ///
+  /// In the category theory interpretation, a rewrite rule is a generating
+  /// 2-cell, and a rewrite path is a 2-cell made from a composition of
+  /// generating 2-cells.
+  ///
+  /// Homotopy generators, in turn, are 3-cells. The special case of a
+  /// 3-cell discovered during completion can be viewed as two parallel
+  /// 2-cells; this is actually represented as a single 2-cell forming a
+  /// loop around a base point.
+  ///
+  /// This data informs the generic signature minimization algorithm.
   std::vector<std::pair<MutableTerm, RewritePath>> HomotopyGenerators;
 
   DebugOptions Debug;
diff --git a/lib/AST/RequirementMachine/RewriteSystemCompletion.cpp b/lib/AST/RequirementMachine/RewriteSystemCompletion.cpp
@@ -380,22 +380,31 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
     //
     // In this case, T and V are both empty.
 
+    // Compute the terms T and V.
+    MutableTerm t(lhs.getLHS().begin(), from);
+    MutableTerm v(from + rhs.getLHS().size(), lhs.getLHS().end());
+
     // Compute the term TYV.
-    MutableTerm tyv(lhs.getLHS().begin(), from);
+    MutableTerm tyv(t);
     tyv.append(rhs.getRHS());
-    tyv.append(from + rhs.getLHS().size(), lhs.getLHS().end());
+    tyv.append(v);
 
     MutableTerm x(lhs.getRHS());
 
-    // Compute a path from X to TYV.
+    // Compute a path from X to TYV: (X => TUV) ⊗ T.(U => Y).V
     RewritePath path;
 
-    // (1) First, apply the left hand side rule in the reverse direction.
-    path.add(RewriteStep::forRewriteRule(/*offset=*/0,
+    // (1) First, apply the left hand side rule in the reverse direction:
+    //
+    //     (X => TUV)
+    path.add(RewriteStep::forRewriteRule(/*startOffset=*/0,
+                                         /*endOffset=*/0,
                                          getRuleID(lhs),
                                          /*inverse=*/true));
-    // (2) Now, apply the right hand side in the forward direction.
-    path.add(RewriteStep::forRewriteRule(from - lhs.getLHS().begin(),
+    // (2) Now, apply the right hand side in the forward direction:
+    //
+    //     T.(U => Y).V 
+    path.add(RewriteStep::forRewriteRule(t.size(), v.size(),
                                          getRuleID(rhs),
                                          /*inverse=*/false));
 
@@ -411,52 +420,55 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
   } else {
     // lhs == TU -> X, rhs == UV -> Y.
 
-    // Compute the term T.
+    // Compute the terms T and V.
     MutableTerm t(lhs.getLHS().begin(), from);
+    MutableTerm v(rhs.getLHS().begin() + (lhs.getLHS().end() - from),
+                  rhs.getLHS().end());
 
     // Compute the term XV.
     MutableTerm xv(lhs.getRHS());
-    xv.append(rhs.getLHS().begin() + (lhs.getLHS().end() - from),
-              rhs.getLHS().end());
-
-    if (xv.back().isSuperclassOrConcreteType() &&
-        lhs.getLHS().begin() != from) {
-      xv.back() = xv.back().prependPrefixToConcreteSubstitutions(
-          t, Context);
-    }
+    xv.append(v);
 
     // Compute the term TY.
-    t.append(rhs.getRHS());
+    MutableTerm ty(t);
+    ty.append(rhs.getRHS());
 
-    // Compute a path from XV to TY.
+    // Compute a path from XV to TY: (X => TU).V ⊗ (σ - T) ⊗ T.(UV => Y)
     RewritePath path;
 
-    // (1) First, apply the left hand side rule in the reverse direction.
-    path.add(RewriteStep::forRewriteRule(/*offset=*/0,
+    // (1) First, apply the left hand side rule in the reverse direction:
+    //
+    //     (X => TU).V
+    path.add(RewriteStep::forRewriteRule(/*startOffset=*/0, v.size(),
                                          getRuleID(lhs),
                                          /*inverse=*/true));
 
     // (2) Next, if the right hand side rule ends with a concrete type symbol,
-    // perform the concrete type adjustment.
-    if (xv.back().isSuperclassOrConcreteType() &&
-        lhs.getLHS().begin() != from) {
-      path.add(RewriteStep::forAdjustment(from - lhs.getLHS().begin(),
-                                          /*inverse=*/true));
+    // perform the concrete type adjustment:
+    //
+    //     (σ - T)
+    if (xv.back().isSuperclassOrConcreteType() && t.size() > 0) {
+      path.add(RewriteStep::forAdjustment(t.size(), /*inverse=*/true));
+
+      xv.back() = xv.back().prependPrefixToConcreteSubstitutions(
+          t, Context);
     }
 
-    // (3) Finally, apply the right hand side in the forward direction.
-    path.add(RewriteStep::forRewriteRule(from - lhs.getLHS().begin(),
+    // (3) Finally, apply the right hand side in the forward direction:
+    //
+    //     T.(UV => Y)
+    path.add(RewriteStep::forRewriteRule(t.size(), /*endOffset=*/0,
                                          getRuleID(rhs),
                                          /*inverse=*/false));
 
     // If XV == TY, we have a trivial overlap.
-    if (xv == t) {
+    if (xv == ty) {
       loops.emplace_back(xv, path);
       return false;
     }
 
     // Add the pair (XV, TY).
-    pairs.emplace_back(xv, t);
+    pairs.emplace_back(xv, ty);
     paths.push_back(path);
   }
 

Original file line number	Diff line number	Diff line change
`@@ -448,3 +448,7 @@ void RequirementMachine::computeCompletion() {`
`448`	`448`	`bool RequirementMachine::isComplete() const {`
`449`	`449`	`return Complete;`
`450`	`450`	`}`
	`451`	`+`
	`452`	`+void RequirementMachine::computeMinimalRequirements(const ProtocolDecl *proto) {`
	`453`	`+ System.minimizeRewriteSystem();`
	`454`	`+}`