RequirementMachine: Record homotopy generators when adding new rules during completion

slavapestov · slavapestov · commit a75327e6b182 · 2021-09-24T08:59:50.000-04:00
diff --git a/lib/AST/RequirementMachine/RewriteSystem.cpp b/lib/AST/RequirementMachine/RewriteSystem.cpp
@@ -116,30 +116,76 @@ Symbol RewriteSystem::simplifySubstitutionsInSuperclassOrConcreteSymbol(
     }, Context);
 }
 
-bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs) {
+/// Adds a rewrite rule, returning true if the new rule was non-trivial.
+///
+/// If both sides simplify to the same term, the rule is trivial and discarded,
+/// and this method returns false.
+///
+/// If \p path is non-null, the new rule is derived from existing rules in the
+/// rewrite system; the path records a series of rewrite steps which transform
+/// \p lhs to \p rhs.
+bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs,
+                            const RewritePath *path) {
   assert(!lhs.empty());
   assert(!rhs.empty());
 
   if (Debug.contains(DebugFlags::Add)) {
-    llvm::dbgs() << "# Adding rule " << lhs << " == " << rhs << "\n";
+    llvm::dbgs() << "# Adding rule " << lhs << " == " << rhs << "\n\n";
   }
 
   // Now simplify both sides as much as possible with the rules we have so far.
   //
   // This avoids unnecessary work in the completion algorithm.
-  simplify(lhs);
-  simplify(rhs);
+  RewritePath lhsPath;
+  RewritePath rhsPath;
+
+  simplify(lhs, &lhsPath);
+  simplify(rhs, &rhsPath);
+
+  RewritePath loop;
+  if (path) {
+    // Produce a path from the simplified lhs to the simplified rhs.
+
+    // (1) First, apply lhsPath in reverse to produce the original lhs.
+    lhsPath.invert();
+    loop.append(lhsPath);
+
+    // (2) Now, apply the path from the original lhs to the original rhs
+    // given to us by the completion procedure.
+    loop.append(*path);
+
+    // (3) Finally, apply rhsPath to produce the simplified rhs, which
+    // is the same as the simplified lhs.
+    loop.append(rhsPath);
+  }
 
   // If the left hand side and right hand side are already equivalent, we're
   // done.
   int result = lhs.compare(rhs, Protos);
-  if (result == 0)
+  if (result == 0) {
+    // If this rule is a consequence of existing rules, add a homotopy
+    // generator.
+    if (path) {
+      // We already have a loop, since the simplified lhs is identical to the
+      // simplified rhs.
+      HomotopyGenerators.emplace_back(lhs, loop);
+
+      if (Debug.contains(DebugFlags::Add)) {
+        llvm::dbgs() << "## Recorded trivial loop at " << lhs << ": ";
+        loop.dump(llvm::dbgs(), lhs, *this);
+        llvm::dbgs() << "\n\n";
+      }
+    }
+
     return false;
+  }
 
   // Orient the two terms so that the left hand side is greater than the
   // right hand side.
-  if (result < 0)
+  if (result < 0) {
     std::swap(lhs, rhs);
+    loop.invert();
+  }
 
   assert(lhs.compare(rhs, Protos) > 0);
 
@@ -153,6 +199,19 @@ bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs) {
   auto uniquedRHS = Term::get(rhs, Context);
   Rules.emplace_back(uniquedLHS, uniquedRHS);
 
+  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(/*offset=*/0, newRuleID, /*inverse=*/true));
+    HomotopyGenerators.emplace_back(lhs, loop);
+
+    if (Debug.contains(DebugFlags::Add)) {
+      llvm::dbgs() << "## Recorded non-trivial loop at " << lhs << ": ";
+      loop.dump(llvm::dbgs(), lhs, *this);
+      llvm::dbgs() << "\n\n";
+    }
+  }
+
   auto oldRuleID = Trie.insert(lhs.begin(), lhs.end(), newRuleID);
   if (oldRuleID) {
     llvm::errs() << "Duplicate rewrite rule!\n";
@@ -279,8 +338,9 @@ void RewriteSystem::simplifyRewriteSystem() {
       continue;
 
     // Now, try to reduce the right hand side.
+    RewritePath rhsPath;
     MutableTerm rhs(rule.getRHS());
-    if (!simplify(rhs))
+    if (!simplify(rhs, &rhsPath))
       continue;
 
     // We're adding a new rule, so the old rule won't apply anymore.
@@ -293,6 +353,27 @@ void RewriteSystem::simplifyRewriteSystem() {
     auto oldRuleID = Trie.insert(lhs.begin(), lhs.end(), newRuleID);
     assert(oldRuleID == ruleID);
     (void) oldRuleID;
+
+    // Produce a loop at the simplified rhs.
+    RewritePath loop;
+
+    // (1) First, apply rhsPath in reverse to produce the original rhs.
+    rhsPath.invert();
+    loop.append(rhsPath);
+
+    // (2) Next, apply the original rule in reverse to produce the
+    // original lhs.
+    loop.add(RewriteStep(/*offset=*/0, ruleID, /*inverse=*/true));
+
+    // (3) Finally, apply the new rule to produce the simplified rhs.
+    loop.add(RewriteStep(/*offset=*/0, newRuleID, /*inverse=*/false));
+
+    if (Debug.contains(DebugFlags::Completion)) {
+      llvm::dbgs() << "$ Right hand side simplification recorded a loop: ";
+      loop.dump(llvm::dbgs(), rhs, *this);
+    }
+
+    HomotopyGenerators.emplace_back(rhs, loop);
   }
 }
 
@@ -364,4 +445,11 @@ void RewriteSystem::dump(llvm::raw_ostream &out) const {
     out << "- " << rule << "\n";
   }
   out << "}\n";
+  out << "Homotopy generators: {\n";
+  for (const auto &loop : HomotopyGenerators) {
+    out << "- " << loop.first << ": ";
+    loop.second.dump(out, loop.first, *this);
+    out << "\n";
+  }
+  out << "}\n";
 }
diff --git a/lib/AST/RequirementMachine/RewriteSystem.h b/lib/AST/RequirementMachine/RewriteSystem.h
@@ -181,6 +181,11 @@ 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.
+  std::vector<std::pair<MutableTerm, RewritePath>> HomotopyGenerators;
+
   DebugOptions Debug;
 
 public:
@@ -216,7 +221,8 @@ class RewriteSystem final {
     return Rules[ruleID];
   }
 
-  bool addRule(MutableTerm lhs, MutableTerm rhs);
+  bool addRule(MutableTerm lhs, MutableTerm rhs,
+               const RewritePath *path=nullptr);
 
   bool simplify(MutableTerm &term, RewritePath *path=nullptr) const;
 
@@ -249,10 +255,12 @@ class RewriteSystem final {
 
 private:
   bool
-  computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
-                      const Rule &lhs, const Rule &rhs,
-                      std::vector<std::pair<MutableTerm,
-                                            MutableTerm>> &result) const;
+  computeCriticalPair(
+      ArrayRef<Symbol>::const_iterator from,
+      const Rule &lhs, const Rule &rhs,
+      std::vector<std::pair<MutableTerm, MutableTerm>> &pairs,
+      std::vector<RewritePath> &paths,
+      std::vector<std::pair<MutableTerm, RewritePath>> &loops) const;
 
   void processMergedAssociatedTypes();
 
diff --git a/lib/AST/RequirementMachine/RewriteSystemCompletion.cpp b/lib/AST/RequirementMachine/RewriteSystemCompletion.cpp
@@ -367,7 +367,10 @@ bool
 RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
                                    const Rule &lhs, const Rule &rhs,
                                    std::vector<std::pair<MutableTerm,
-                                                         MutableTerm>> &result) const {
+                                                         MutableTerm>> &pairs,
+                                   std::vector<RewritePath> &paths,
+                                   std::vector<std::pair<MutableTerm,
+                                                         RewritePath>> &loops) const {
   auto end = lhs.getLHS().end();
   if (from + rhs.getLHS().size() < end) {
     // lhs == TUV -> X, rhs == U -> Y.
@@ -378,17 +381,33 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
     // In this case, T and V are both empty.
 
     // Compute the term TYV.
-    MutableTerm t(lhs.getLHS().begin(), from);
-    t.append(rhs.getRHS());
-    t.append(from + rhs.getLHS().size(), lhs.getLHS().end());
-
-    if (lhs.getRHS().size() == t.size() &&
-        std::equal(lhs.getRHS().begin(), lhs.getRHS().end(),
-                   t.begin())) {
+    MutableTerm tyv(lhs.getLHS().begin(), from);
+    tyv.append(rhs.getRHS());
+    tyv.append(from + rhs.getLHS().size(), lhs.getLHS().end());
+
+    MutableTerm x(lhs.getRHS());
+
+    // Compute a path from X to TYV.
+    RewritePath path;
+
+    // (1) First, apply the left hand side rule in the reverse direction.
+    path.add(RewriteStep(/*offset=*/0,
+                         getRuleID(lhs),
+                         /*inverse=*/true));
+    // (2) Now, apply the right hand side in the forward direction.
+    path.add(RewriteStep(from - lhs.getLHS().begin(),
+                         getRuleID(rhs),
+                         /*inverse=*/false));
+
+    // If X == TYV, we have a trivial overlap.
+    if (x == tyv) {
+      loops.emplace_back(x, path);
       return false;
     }
 
-    result.emplace_back(MutableTerm(lhs.getRHS()), t);
+    // Add the pair (X, TYV).
+    pairs.emplace_back(x, tyv);
+    paths.push_back(path);
   } else {
     // lhs == TU -> X, rhs == UV -> Y.
 
@@ -408,10 +427,27 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
     // Compute the term TY.
     t.append(rhs.getRHS());
 
-    if (xv == t)
+    // Compute a path from XV to TY.
+    RewritePath path;
+
+    // (1) First, apply the left hand side rule in the reverse direction.
+    path.add(RewriteStep(/*offset=*/0,
+                         getRuleID(lhs),
+                         /*inverse=*/true));
+    // (2) Now, apply the right hand side in the forward direction.
+    path.add(RewriteStep(from - lhs.getLHS().begin(),
+                         getRuleID(rhs),
+                         /*inverse=*/false));
+
+    // If XV == TY, we have a trivial overlap.
+    if (xv == t) {
+      loops.emplace_back(xv, path);
       return false;
+    }
 
-    result.emplace_back(xv, t);
+    // Add the pair (XV, TY).
+    pairs.emplace_back(xv, t);
+    paths.push_back(path);
   }
 
   return true;
@@ -435,9 +471,11 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
 
   bool again = false;
 
-  do {
-    std::vector<std::pair<MutableTerm, MutableTerm>> resolvedCriticalPairs;
+  std::vector<std::pair<MutableTerm, MutableTerm>> resolvedCriticalPairs;
+  std::vector<RewritePath> resolvedPaths;
+  std::vector<std::pair<MutableTerm, RewritePath>> resolvedLoops;
 
+  do {
     // For every rule, looking for other rules that overlap with this rule.
     for (unsigned i = 0, e = Rules.size(); i < e; ++i) {
       const auto &lhs = getRule(i);
@@ -480,9 +518,13 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
           }
 
           // Try to repair the confluence violation by adding a new rule.
-          if (computeCriticalPair(from, lhs, rhs, resolvedCriticalPairs)) {
+          if (computeCriticalPair(from, lhs, rhs,
+                                  resolvedCriticalPairs,
+                                  resolvedPaths,
+                                  resolvedLoops)) {
             if (Debug.contains(DebugFlags::Completion)) {
               const auto &pair = resolvedCriticalPairs.back();
+              const auto &path = resolvedPaths.back();
 
               llvm::dbgs() << "$ Overlapping rules: (#" << i << ") ";
               llvm::dbgs() << lhs << "\n";
@@ -492,13 +534,26 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
                            << pair.first << "\n";
               llvm::dbgs() << "$$ Second term of critical pair is "
                            << pair.second << "\n\n";
+
+              llvm::dbgs() << "$$ Resolved via path: ";
+              path.dump(llvm::dbgs(), pair.first, *this);
+              llvm::dbgs() << "\n\n";
             }
           } else {
             if (Debug.contains(DebugFlags::Completion)) {
+              const auto &loop = resolvedLoops.back();
+
               llvm::dbgs() << "$ Trivially overlapping rules: (#" << i << ") ";
               llvm::dbgs() << lhs << "\n";
               llvm::dbgs() << "                          -vs- (#" << j << ") ";
               llvm::dbgs() << rhs << ":\n";
+
+              llvm::dbgs() << "$$ Loop: ";
+              loop.second.dump(llvm::dbgs(), loop.first, *this);
+              llvm::dbgs() << "\n\n";
+
+              // Record the trivial loop.
+              HomotopyGenerators.push_back(loop);
             }
           }
         });
@@ -509,13 +564,18 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
 
     simplifyRewriteSystem();
 
+    assert(resolvedCriticalPairs.size() == resolvedPaths.size());
+
     again = false;
-    for (const auto &pair : resolvedCriticalPairs) {
+    for (unsigned index : indices(resolvedCriticalPairs)) {
+      const auto &pair = resolvedCriticalPairs[index];
+      const auto &path = resolvedPaths[index];
+
       // Check if we've already done too much work.
       if (Rules.size() > maxIterations)
         return std::make_pair(CompletionResult::MaxIterations, steps);
 
-      if (!addRule(pair.first, pair.second))
+      if (!addRule(pair.first, pair.second, &path))
         continue;
 
       // Check if the new rule is too long.
@@ -527,6 +587,9 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
       again = true;
     }
 
+    resolvedCriticalPairs.clear();
+    resolvedPaths.clear();
+
     // If the added rules merged any associated types, process the merges now
     // before we continue with the completion procedure. This is important
     // to perform incrementally since merging is required to repair confluence
