RequirementMachine: Don't normalize replacement paths for redundant rules

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -459,60 +459,6 @@ void RewriteSystem::performHomotopyReduction(
   propagateRedundantRequirementIDs();
 }
 
-void RewriteSystem::normalizeRedundantRules() {
-  llvm::DenseMap<unsigned, unsigned> RedundantRuleMap;
-
-  // A redundant path in the range [0, i-1] might contain rewrite steps naming
-  // rules that subsequently became redundant in the range [i, e-1].
-  //
-  // We back-substitute later rules into earlier paths here.
-  for (unsigned i = 0, e = RedundantRules.size(); i < e; ++i) {
-    // Pre-condition: Redundant paths in the range [i+1, e-1] do not involve
-    // any other redundant rules.
-    unsigned j = e - i - 1;
-
-    // Replace all occurrences of redundant rules with their path at
-    // RedundantRules[i].
-    auto &pair = RedundantRules[j];
-    pair.second.replaceRulesWithPaths(
-        [&](unsigned ruleID) -> RewritePath * {
-          auto found = RedundantRuleMap.find(ruleID);
-          if (found != RedundantRuleMap.end())
-            return &RedundantRules[found->second].second;
-
-          return nullptr;
-        });
-    pair.second.computeNormalForm(*this);
-
-    RedundantRuleMap[RedundantRules[j].first] = j;
-
-    // Post-condition: the path for RedundantRules[i] does not contain any
-    // redundant rules.
-  }
-
-  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.
@@ -644,12 +590,32 @@ void RewriteSystem::minimizeRewriteSystem() {
     return false;
   });
 
-  normalizeRedundantRules();
-
   // Check invariants after homotopy reduction.
   verifyRewriteLoops();
   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.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";
+      }
+    }
+  }
 }
 
 /// Returns flags indicating if the rewrite system has unresolved or
@@ -849,7 +815,11 @@ void RewriteSystem::verifyMinimizedRules(
     abort();
   }
 
-  for (const auto &pair : RedundantRules) {
+  // Replacement paths for redundant rules can only reference other redundant
+  // rules if those redundant rules were made redundant later, ie if they
+  // appear later in the array.
+  llvm::DenseSet<unsigned> laterRedundantRules;
+  for (const auto &pair : llvm::reverse(RedundantRules)) {
     const auto &rule = getRule(pair.first);
     if (!rule.isRedundant()) {
       llvm::errs() << "Recorded replacement path for non-redundant rule "
@@ -860,14 +830,19 @@ void RewriteSystem::verifyMinimizedRules(
 
     for (const auto &step : pair.second) {
       if (step.Kind == RewriteStep::Rule) {
-        const auto &rule = getRule(step.getRuleID());
-        if (rule.isRedundant()) {
+        unsigned otherRuleID = step.getRuleID();
+        const auto &otherRule = getRule(otherRuleID);
+        if (otherRule.isRedundant() &&
+            !laterRedundantRules.count(otherRuleID)) {
           llvm::errs() << "Redundant requirement path contains a redundant "
-                          "rule " << rule << "\n";
+                          "rule " << otherRule << "\n";
           dump(llvm::errs());
           abort();
         }
       }
     }
+
+    laterRedundantRules.insert(pair.first);
   }
+
 }

lib/AST/RequirementMachine/RewriteSystem.h

@@ -367,8 +367,6 @@ class RewriteSystem final {
   void computeMinimalConformances(
       llvm::DenseSet<unsigned> &redundantConformances);
 
-  void normalizeRedundantRules();
-
 public:
   void recordRewriteLoop(MutableTerm basepoint,
                          RewritePath path);