RequirementMachine: Compute critical pairs directly

Previously if the left hand side of two rules overlapped, we would
compute the overlapped term and apply both rules to obtain a
critical pair.

But it is actually possible to compute the critical pair directly.
For now this has no effect other than possibly being more efficient,
but for concrete type terms we will need this formulation for the
completion procedure to work.

Author: slavapestov

include/swift/AST/RewriteSystem.h

@@ -186,6 +186,16 @@ class Atom final {
   }
 };
 
+/// See the implementation of MutableTerm::checkForOverlap() for a discussion.
+enum class OverlapKind {
+  /// Terms do not overlap.
+  None,
+  /// First kind of overlap (TUV vs U).
+  First,
+  /// Second kind of overlap (TU vs UV).
+  Second
+};
+
 /// A term is a sequence of one or more atoms.
 ///
 /// The Term type is a uniqued, permanently-allocated representation,
@@ -248,6 +258,10 @@ class MutableTerm final {
   /// to become valid.
   MutableTerm() {}
 
+  explicit MutableTerm(decltype(Atoms)::const_iterator begin,
+                       decltype(Atoms)::const_iterator end)
+    : Atoms(begin, end) {}
+
   explicit MutableTerm(llvm::SmallVector<Atom, 3> &&atoms)
     : Atoms(std::move(atoms)) {}
 
@@ -261,8 +275,14 @@ class MutableTerm final {
     Atoms.push_back(atom);
   }
 
+  void append(const MutableTerm &other) {
+    Atoms.append(other.begin(), other.end());
+  }
+
   int compare(const MutableTerm &other, const ProtocolGraph &protos) const;
 
+  bool empty() const { return Atoms.empty(); }
+
   size_t size() const { return Atoms.size(); }
 
   decltype(Atoms)::const_iterator begin() const { return Atoms.begin(); }
@@ -300,7 +320,9 @@ class MutableTerm final {
 
   bool rewriteSubTerm(const MutableTerm &lhs, const MutableTerm &rhs);
 
-  bool checkForOverlap(const MutableTerm &other, MutableTerm &result) const;
+  OverlapKind checkForOverlap(const MutableTerm &other,
+                              MutableTerm &t,
+                              MutableTerm &v) const;
 
   void dump(llvm::raw_ostream &out) const;
 };
@@ -359,8 +381,10 @@ class Rule final {
     return term.rewriteSubTerm(LHS, RHS);
   }
 
-  bool checkForOverlap(const Rule &other, MutableTerm &result) const {
-    return LHS.checkForOverlap(other.LHS, result);
+  OverlapKind checkForOverlap(const Rule &other,
+                              MutableTerm &t,
+                              MutableTerm &v) const {
+    return LHS.checkForOverlap(other.LHS, t, v);
   }
 
   bool canReduceLeftHandSide(const Rule &other) const {
@@ -478,6 +502,9 @@ class RewriteSystem final {
   void dump(llvm::raw_ostream &out) const;
 
 private:
+  Optional<std::pair<MutableTerm, MutableTerm>>
+  computeCriticalPair(const Rule &lhs, const Rule &rhs) const;
+
   Atom mergeAssociatedTypes(Atom lhs, Atom rhs) const;
   void processMergedAssociatedTypes();
 };

lib/AST/RewriteSystem.cpp

@@ -779,20 +779,25 @@ bool MutableTerm::rewriteSubTerm(const MutableTerm &lhs,
 ///
 /// An overlap occurs if one of the following two cases holds:
 ///
-/// 1) If this == TUV and other == U, then \p result is TUV.
-/// 2) If this == TU and other == UV, then \p result is TUV.
-/// 3) If neither holds, we return false.
+/// 1) If this == TUV and other == U.
+/// 2) If this == TU and other == UV.
+///
+/// In both cases, we return the subterms T and V, together with
+/// an 'overlap kind' identifying the first or second case.
+///
+/// If both rules have identical left hand sides, either case could
+/// apply, but we arbitrarily pick case 1.
 ///
 /// Note that this relation is not commutative; we need to check
 /// for overlap between both (X and Y) and (Y and X).
-bool MutableTerm::checkForOverlap(const MutableTerm &other,
-                                  MutableTerm &result) const {
-  assert(result.size() == 0);
-
+OverlapKind
+MutableTerm::checkForOverlap(const MutableTerm &other,
+                             MutableTerm &t,
+                             MutableTerm &v) const {
   // If the other term is longer than this term, there's no way
   // we can overlap.
   if (other.size() > size())
-    return false;
+    return OverlapKind::None;
 
   auto first1 = begin();
   auto last1 = end();
@@ -806,12 +811,15 @@ bool MutableTerm::checkForOverlap(const MutableTerm &other,
   // X.Y.Z
   //   X.Y.Z
   //     X.Y.Z
-  while (last2 - first2 <= last1 - first1) {
+  while (last1 - first1 >= last2 - first2) {
     if (std::equal(first2, last2, first1)) {
-      // If this == TUV and other == U, the overlap is TUV, so just
-      // copy this term over.
-      result = *this;
-      return true;
+      // We have an overlap of the first kind, where
+      // this == TUV and other == U.
+      //
+      // Get the subterms for T and V.
+      t = MutableTerm(begin(), first1);
+      v = MutableTerm(first1 + other.size(), end());
+      return OverlapKind::First;
     }
 
     ++first1;
@@ -827,21 +835,21 @@ bool MutableTerm::checkForOverlap(const MutableTerm &other,
     --last2;
 
     if (std::equal(first1, last1, first2)) {
-      // If this == TU and other == UV, the overlap is the term
-      // TUV, which can be formed by concatenating a prefix of this
-      // term with the entire other term.
-      std::copy(begin(), first1,
-                std::back_inserter(result.Atoms));
-      std::copy(other.begin(), other.end(),
-                std::back_inserter(result.Atoms));
-      return true;
+      // We have an overlap of the second kind, where
+      // this == TU and other == UV.
+      //
+      // Get the subterms for T and V.
+      t = MutableTerm(begin(), first1);
+      assert(!t.empty());
+      v = MutableTerm(last2, other.end());
+      return OverlapKind::Second;
     }
 
     ++first1;
   }
 
   // No overlap found.
-  return false;
+  return OverlapKind::None;
 }
 
 void MutableTerm::dump(llvm::raw_ostream &out) const {
@@ -1230,6 +1238,63 @@ void RewriteSystem::processMergedAssociatedTypes() {
   MergedAssociatedTypes.clear();
 }
 
+/// Compute a critical pair from two rewrite rules.
+///
+/// There are two cases:
+///
+/// 1) lhs == TUV -> X, rhs == U -> Y. The overlapped term is TUV;
+///    applying lhs and rhs, respectively, yields the critical pair
+///    (X, TYV).
+///
+/// 2) lhs == TU -> X, rhs == UV -> Y. The overlapped term is once
+///    again TUV; applying lhs and rhs, respectively, yields the
+///    critical pair (XV, TY).
+///
+/// If lhs and rhs have identical left hand sides, either case could
+/// apply, but we arbitrarily pick case 1.
+///
+/// There is also an additional wrinkle. If we're in case 2, and the
+/// last atom of V is a superclass or concrete type atom A, we prepend
+/// T to each substitution of A.
+Optional<std::pair<MutableTerm, MutableTerm>>
+RewriteSystem::computeCriticalPair(const Rule &lhs, const Rule &rhs) const {
+  MutableTerm t, v;
+
+  switch (lhs.checkForOverlap(rhs, t, v)) {
+  case OverlapKind::None:
+    return None;
+
+  case OverlapKind::First: {
+    // lhs == TUV -> X, rhs == U -> Y.
+
+    // Note: This includes the case where the two rules have exactly
+    // equal left hand sides; that is, lhs == U -> X, rhs == U -> Y.
+    //
+    // In this case, T and V are both empty.
+
+    // Compute the term TYV.
+    t.append(rhs.getRHS());
+    t.append(v);
+    return std::make_pair(lhs.getRHS(), t);
+  }
+
+  case OverlapKind::Second: {
+    // lhs == TU -> X, rhs == UV -> Y.
+
+    // Compute the term XV.
+    MutableTerm xv;
+    xv.append(lhs.getRHS());
+    xv.append(v);
+
+    // Compute the term TY.
+    t.append(rhs.getRHS());
+    return std::make_pair(xv, t);
+  }
+  }
+
+  llvm_unreachable("Bad overlap kind");
+}
+
 /// Computes the confluent completion using the Knuth-Bendix algorithm
 /// (https://en.wikipedia.org/wiki/Knuth–Bendix_completion_algorithm).
 ///
@@ -1254,50 +1319,33 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
   // that we resolve all overlaps among the initial set of rules before
   // moving on to overlaps between rules introduced by completion.
   while (!Worklist.empty()) {
-    auto pair = Worklist.front();
+    auto next = Worklist.front();
     Worklist.pop_front();
 
-    MutableTerm first;
-
-    const auto &lhs = Rules[pair.first];
-    const auto &rhs = Rules[pair.second];
+    const auto &lhs = Rules[next.first];
+    const auto &rhs = Rules[next.second];
 
     if (DebugCompletion) {
-      llvm::dbgs() << "$ Check for overlap: (#" << pair.first << ") ";
+      llvm::dbgs() << "$ Check for overlap: (#" << next.first << ") ";
       lhs.dump(llvm::dbgs());
       llvm::dbgs() << "\n";
-      llvm::dbgs() << "                -vs- (#" << pair.second << ") ";
+      llvm::dbgs() << "                -vs- (#" << next.second << ") ";
       rhs.dump(llvm::dbgs());
-      llvm::dbgs() << ":";
+      llvm::dbgs() << ":\n";
     }
 
-    if (!lhs.checkForOverlap(rhs, first)) {
+    auto pair = computeCriticalPair(lhs, rhs);
+    if (!pair) {
       if (DebugCompletion) {
         llvm::dbgs() << " no overlap\n\n";
       }
       continue;
     }
 
-    if (DebugCompletion) {
-      llvm::dbgs() << "\n";
-      llvm::dbgs() << "$$ Overlapping term is ";
-      first.dump(llvm::dbgs());
-      llvm::dbgs() << "\n";
-    }
-
-    assert(first.size() > 0);
+    MutableTerm first, second;
 
-    // We have two rules whose left hand sides overlap. This means
-    // one of the following two cases is true:
-    //
-    // 1) lhs == TUV and rhs == U
-    // 2) lhs == TU and rhs == UV
-    MutableTerm second = first;
-
-    // In both cases, rewrite the term TUV using both rules to
-    // produce two new terms X and Y.
-    lhs.apply(first);
-    rhs.apply(second);
+    // We have a critical pair (X, Y).
+    std::tie(first, second) = *pair;
 
     if (DebugCompletion) {
       llvm::dbgs() << "$$ First term of critical pair is ";