Merge pull request #41614 from slavapestov/rqm-left-canonical-form

RequirementMachine: Reduce replacement paths for redundant rules to left-canonical normal form

Author: slavapestov

include/swift/Basic/LangOptions.h

@@ -545,6 +545,10 @@ namespace swift {
     /// enabled. It can be disabled for debugging and testing.
     bool EnableRequirementMachineConcreteContraction = true;
 
+    /// Enable the stronger minimization algorithm. This is just for debugging;
+    /// if you have a testcase which requires this, please submit a bug report.
+    bool EnableRequirementMachineLoopNormalization = false;
+
     /// Enables dumping type witness systems from associated type inference.
     bool DumpTypeWitnessSystems = false;
 

include/swift/Option/FrontendOptions.td

@@ -359,6 +359,9 @@ def disable_requirement_machine_concrete_contraction : Flag<["-"], "disable-requ
   HelpText<"Disable preprocessing pass to eliminate conformance requirements "
            "on generic parameters which are made concrete">;
 
+def enable_requirement_machine_loop_normalization : Flag<["-"], "enable-requirement-machine-loop-normalization">,
+  HelpText<"Enable stronger minimization algorithm, for debugging only">;
+
 def dump_type_witness_systems : Flag<["-"], "dump-type-witness-systems">,
   HelpText<"Enables dumping type witness systems from associated type inference">;
 

lib/AST/CMakeLists.txt

@@ -83,6 +83,7 @@ add_swift_host_library(swiftAST STATIC
   RequirementMachine/InterfaceType.cpp
   RequirementMachine/KnuthBendix.cpp
   RequirementMachine/MinimalConformances.cpp
+  RequirementMachine/NormalizeRewritePath.cpp
   RequirementMachine/PropertyMap.cpp
   RequirementMachine/PropertyRelations.cpp
   RequirementMachine/PropertyUnification.cpp

lib/AST/GenericSignature.cpp

@@ -827,6 +827,9 @@ void GenericSignature::verify(ArrayRef<Requirement> reqts) const {
   // We collect conformance requirements to check that they're minimal.
   llvm::SmallDenseMap<CanType, SmallVector<ProtocolDecl *, 2>, 2> conformances;
 
+  // We collect same-type requirements to check that they're minimal.
+  llvm::SmallDenseMap<CanType, SmallVector<Type, 2>, 2> sameTypeComponents;
+
   // Check that the requirements satisfy certain invariants.
   for (unsigned idx : indices(reqts)) {
     const auto &reqt = reqts[idx].getCanonical();
@@ -873,6 +876,10 @@ void GenericSignature::verify(ArrayRef<Requirement> reqts) const {
 
       auto firstType = reqt.getFirstType();
       auto secondType = reqt.getSecondType();
+
+      auto canType = canSig->getCanonicalTypeInContext(firstType);
+      auto &component = sameTypeComponents[canType];
+
       if (!hasCanonicalOrConcreteParent(firstType)) {
         llvm::errs() << "Left hand side does not have a canonical parent: ";
         reqt.dump(llvm::errs());
@@ -893,13 +900,34 @@ void GenericSignature::verify(ArrayRef<Requirement> reqts) const {
           llvm::errs() << "\n";
           abort();
         }
+
+        if (component.empty()) {
+          component.push_back(firstType);
+        } else if (!component.back()->isEqual(firstType)) {
+          llvm::errs() << "Same-type requirement within an equiv. class "
+                       << "is out-of-order: ";
+          reqt.dump(llvm::errs());
+          llvm::errs() << "\n";
+          abort();
+        }
+
+        component.push_back(secondType);
       } else {
         if (!canSig->isCanonicalTypeInContext(secondType)) {
           llvm::errs() << "Right hand side is not canonical: ";
           reqt.dump(llvm::errs());
           llvm::errs() << "\n";
           abort();
         }
+
+        if (component.empty()) {
+          component.push_back(secondType);
+        } else if (!component.back()->isEqual(secondType)) {
+          llvm::errs() << "Inconsistent concrete requirement in equiv. class: ";
+          reqt.dump(llvm::errs());
+          llvm::errs() << "\n";
+          abort();
+        }
       }
       break;
     }
@@ -925,33 +953,6 @@ void GenericSignature::verify(ArrayRef<Requirement> reqts) const {
       abort();
     }
 
-    // If we have two same-type requirements where the left-hand sides differ
-    // but fall into the same equivalence class, we can check the form.
-    if (compareLHS < 0 && reqt.getKind() == RequirementKind::SameType &&
-        prevReqt.getKind() == RequirementKind::SameType &&
-        canSig->areSameTypeParameterInContext(prevReqt.getFirstType(),
-                                              reqt.getFirstType())) {
-      // If it's a it's a type parameter, make sure the equivalence class is
-      // wired together sanely.
-      if (prevReqt.getSecondType()->isTypeParameter()) {
-        if (!prevReqt.getSecondType()->isEqual(reqt.getFirstType())) {
-          llvm::errs() << "Same-type requirement within an equiv. class "
-                       << "is out-of-order: ";
-          reqt.dump(llvm::errs());
-          llvm::errs() << "\n";
-          abort();
-        }
-      } else {
-        // Otherwise, the concrete types must match up.
-        if (!prevReqt.getSecondType()->isEqual(reqt.getSecondType())) {
-          llvm::errs() << "Inconsistent concrete requirement in equiv. class: ";
-          reqt.dump(llvm::errs());
-          llvm::errs() << "\n";
-          abort();
-        }
-      }
-    }
-
     // If we have a concrete same-type requirement, we shouldn't have any
     // other requirements on the same type.
     if (reqt.getKind() == RequirementKind::SameType &&
@@ -974,7 +975,7 @@ void GenericSignature::verify(ArrayRef<Requirement> reqts) const {
   }
 
   // Make sure we don't have redundant protocol conformance requirements.
-  for (auto pair : conformances) {
+  for (const auto &pair : conformances) {
     const auto &protos = pair.second;
     auto canonicalProtos = protos;
 
@@ -992,6 +993,18 @@ void GenericSignature::verify(ArrayRef<Requirement> reqts) const {
       abort();
     }
   }
+
+  // Check same-type components for consistency.
+  for (const auto &pair : sameTypeComponents) {
+    if (pair.second.front()->isTypeParameter() &&
+        !canSig->isCanonicalTypeInContext(pair.second.front())) {
+      llvm::errs() << "Abstract same-type requirement involving concrete types\n";
+      llvm::errs() << "Canonical type: " << pair.first << "\n";
+      llvm::errs() << "Left hand side of first requirement: "
+                   << pair.second.front() << "\n";
+      abort();
+    }
+  }
 }
 
 static Type stripBoundDependentMemberTypes(Type t) {

lib/AST/RequirementMachine/ConcreteTypeWitness.cpp

@@ -483,14 +483,29 @@ void PropertyMap::recordConcreteConformanceRule(
 
   auto protocolSymbol = *conformanceRule.isPropertyRule();
 
-  // Now, transform T''.[concrete: C].[P] into T''.[concrete: C : P].
+  // Now, transform T''.[concrete: C].[P] into T''.[concrete: C].[concrete: C : P].
   unsigned relationID = System.recordConcreteConformanceRelation(
       concreteSymbol, protocolSymbol, concreteConformanceSymbol);
 
   path.add(RewriteStep::forRelation(
       /*startOffset=*/rhs.size(), relationID,
       /*inverse=*/false));
 
+  // If T' is a suffix of T, prepend the prefix to the concrete type's
+  // substitutions.
+  if (prefixLength > 0 &&
+      !concreteConformanceSymbol.getSubstitutions().empty()) {
+    path.add(RewriteStep::forPrefixSubstitutions(prefixLength, /*endOffset=*/1,
+                                                 /*inverse=*/true));
+  }
+
+  // Finally, apply the concrete type rule to obtain T''.[concrete: C : P].
+  path.add(RewriteStep::forRewriteRule(
+      /*startOffset=*/rhs.size() - concreteRule.getRHS().size(),
+      /*endOffset=*/1,
+      /*ruleID=*/concreteRuleID,
+      /*inverse=*/false));
+
   MutableTerm lhs(rhs);
   lhs.add(concreteConformanceSymbol);
 

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -55,15 +55,18 @@
 #include "swift/Basic/Range.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/DenseSet.h"
+#include "llvm/ADT/SmallVector.h"
 #include "llvm/Support/Debug.h"
 #include "llvm/Support/raw_ostream.h"
 #include <algorithm>
+#include "RewriteContext.h"
 #include "RewriteSystem.h"
 
 using namespace swift;
 using namespace rewriting;
 
-/// Recompute RulesInEmptyContext and DecomposeCount if needed.
+/// Recompute Useful, RulesInEmptyContext, ProjectionCount and DecomposeCount
+/// if needed.
 void RewriteLoop::recompute(const RewriteSystem &system) {
   if (!Dirty)
     return;
@@ -109,6 +112,8 @@ void RewriteLoop::recompute(const RewriteSystem &system) {
     evaluator.apply(step, system);
   }
 
+  Useful = !rulesInEmptyContext.empty();
+
   RulesInEmptyContext.clear();
 
   // Collect all rules that we saw exactly once in empty context.
@@ -146,6 +151,14 @@ unsigned RewriteLoop::getDecomposeCount(
   return DecomposeCount;
 }
 
+/// The number of Decompose steps, used by the elimination order to prioritize
+/// loops that are not concrete simplifications.
+bool RewriteLoop::isUseful(
+    const RewriteSystem &system) const {
+  const_cast<RewriteLoop *>(this)->recompute(system);
+  return Useful;
+}
+
 /// If a rewrite loop contains an explicit rule in empty context, propagate the
 /// explicit bit to all other rules appearing in empty context within the same
 /// loop.
@@ -418,16 +431,22 @@ findRuleToDelete(llvm::function_ref<bool(unsigned)> isRedundantRuleFn) {
     if (loop.isDeleted())
       continue;
 
-    bool foundAny = false;
+    // Delete loops that don't contain any rewrite rules in empty context,
+    // since such loops do not yield any elimination candidates.
+    if (!loop.isUseful(*this)) {
+      if (Debug.contains(DebugFlags::HomotopyReduction)) {
+        llvm::dbgs() << "** Deleting useless loop #" << loopID << ": ";
+        loop.dump(llvm::dbgs(), *this);
+        llvm::dbgs() << "\n";
+      }
+
+      loop.markDeleted();
+      continue;
+    }
+
     for (unsigned ruleID : loop.findRulesAppearingOnceInEmptyContext(*this)) {
       redundancyCandidates.emplace_back(loopID, ruleID);
-      foundAny = true;
     }
-
-    // Delete loops that don't contain any rewrite rules in empty context,
-    // since such loops do not give us useful information.
-    if (!foundAny)
-      loop.markDeleted();
   }
 
   Optional<std::pair<unsigned, unsigned>> found;
@@ -609,6 +628,10 @@ void RewriteSystem::deleteRule(unsigned ruleID,
     if (!changed)
       continue;
 
+    if (Context.getASTContext().LangOpts.EnableRequirementMachineLoopNormalization) {
+      loop.computeNormalForm(*this);
+    }
+
     // The loop's path has changed, so we must invalidate the cached
     // result of findRulesAppearingOnceInEmptyContext().
     loop.markDirty();
@@ -658,6 +681,34 @@ void RewriteSystem::performHomotopyReduction(
   }
 }
 
+void RewriteSystem::normalizeRedundantRules() {
+  for (auto &pair : RedundantRules) {
+    pair.second.computeNormalForm(*this);
+  }
+
+  if (Debug.contains(DebugFlags::RedundantRules)) {
+    llvm::dbgs() << "\nRedundant rules:\n";
+    for (const auto &pair : RedundantRules) {
+      const auto &rule = getRule(pair.first);
+      llvm::dbgs() << "- ("
+                   << rule.getLHS() << " => "
+                   << rule.getRHS() << ") ::== ";
+
+      MutableTerm lhs(rule.getLHS());
+      pair.second.dump(llvm::dbgs(), lhs, *this);
+
+      llvm::dbgs() << "\n";
+
+      if (Debug.contains(DebugFlags::RedundantRulesDetail)) {
+        llvm::dbgs() << "\n";
+        pair.second.dumpLong(llvm::dbgs(), lhs, *this);
+
+        llvm::dbgs() << "\n\n";
+      }
+    }
+  }
+}
+
 /// Use the loops to delete redundant rewrite rules via a series of Tietze
 /// transformations, updating and simplifying existing loops as each rule
 /// is deleted.
@@ -677,6 +728,12 @@ void RewriteSystem::minimizeRewriteSystem() {
   propagateExplicitBits();
   processConflicts();
 
+  if (Context.getASTContext().LangOpts.EnableRequirementMachineLoopNormalization) {
+    for (auto &loop : Loops) {
+      loop.computeNormalForm(*this);
+    }
+  }
+
   // First pass:
   // - Eliminate all LHS-simplified non-conformance rules.
   // - Eliminate all RHS-simplified and substitution-simplified rules.
@@ -753,25 +810,7 @@ void RewriteSystem::minimizeRewriteSystem() {
   verifyRedundantConformances(redundantConformances);
   verifyMinimizedRules(redundantConformances);
 
-  if (Debug.contains(DebugFlags::RedundantRules)) {
-    llvm::dbgs() << "\nRedundant rules:\n";
-    for (const auto &pair : RedundantRules) {
-      const auto &rule = getRule(pair.first);
-      llvm::dbgs() << "- " << rule << " ::== ";
-
-      MutableTerm lhs(rule.getLHS());
-      pair.second.dump(llvm::dbgs(), lhs, *this);
-
-      llvm::dbgs() << "\n";
-
-      if (Debug.contains(DebugFlags::RedundantRulesDetail)) {
-        llvm::dbgs() << "\n";
-        pair.second.dumpLong(llvm::dbgs(), lhs, *this);
-
-        llvm::dbgs() << "\n\n";
-      }
-    }
-  }
+  normalizeRedundantRules();
 }
 
 /// In a conformance-valid rewrite system, any rule with unresolved symbols on