RequirementMachine: Rename Rule::isDeleted() => isSimplified(), and add isPermanent(), isRedundant() bits

Author: slavapestov

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -1040,7 +1040,7 @@ RewriteSystem::buildPropertyMap(PropertyMap &map,
   SmallVector<std::vector<std::pair<Term, Symbol>>, 4> properties;
 
   for (const auto &rule : Rules) {
-    if (rule.isDeleted())
+    if (rule.isSimplified())
       continue;
 
     // Collect all rules of the form T.[p] => T where T is canonical.

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -47,8 +47,12 @@ bool Rule::isProtocolConformanceRule() const {
 
 void Rule::dump(llvm::raw_ostream &out) const {
   out << LHS << " => " << RHS;
-  if (deleted)
-    out << " [deleted]";
+  if (Permanent)
+    out << " [permanent]";
+  if (Simplified)
+    out << " [simplified]";
+  if (Redundant)
+    out << " [redundant]";
 }
 
 RewriteSystem::RewriteSystem(RewriteContext &ctx)
@@ -221,7 +225,7 @@ bool RewriteSystem::simplify(MutableTerm &term, RewritePath *path) const {
       auto ruleID = Trie.find(from, end);
       if (ruleID) {
         const auto &rule = getRule(*ruleID);
-        if (!rule.isDeleted()) {
+        if (!rule.isSimplified()) {
           auto to = from + rule.getLHS().size();
           assert(std::equal(from, to, rule.getLHS().begin()));
 
@@ -271,7 +275,7 @@ bool RewriteSystem::simplify(MutableTerm &term, RewritePath *path) const {
 void RewriteSystem::simplifyRewriteSystem() {
   for (unsigned ruleID = 0, e = Rules.size(); ruleID < e; ++ruleID) {
     auto &rule = getRule(ruleID);
-    if (rule.isDeleted())
+    if (rule.isSimplified())
       continue;
 
     // First, see if the left hand side of this rule can be reduced using
@@ -286,7 +290,7 @@ void RewriteSystem::simplifyRewriteSystem() {
           continue;
 
         // Ignore other deleted rules.
-        if (getRule(*otherRuleID).isDeleted())
+        if (getRule(*otherRuleID).isSimplified())
           continue;
 
         if (Debug.contains(DebugFlags::Completion)) {
@@ -296,13 +300,13 @@ void RewriteSystem::simplifyRewriteSystem() {
                        << "\n";
         }
 
-        rule.markDeleted();
+        rule.markSimplified();
         break;
       }
     }
 
     // If the rule was deleted above, skip the rest.
-    if (rule.isDeleted())
+    if (rule.isSimplified())
       continue;
 
     // Now, try to reduce the right hand side.
@@ -312,7 +316,7 @@ void RewriteSystem::simplifyRewriteSystem() {
       continue;
 
     // We're adding a new rule, so the old rule won't apply anymore.
-    rule.markDeleted();
+    rule.markSimplified();
 
     unsigned newRuleID = Rules.size();
 
@@ -359,7 +363,7 @@ void RewriteSystem::verifyRewriteRules() const {
   }
 
   for (const auto &rule : Rules) {
-    if (rule.isDeleted())
+    if (rule.isSimplified())
       continue;
 
     const auto &lhs = rule.getLHS();

lib/AST/RequirementMachine/RewriteSystem.h

@@ -41,11 +41,37 @@ class RewriteSystem;
 class Rule final {
   Term LHS;
   Term RHS;
-  bool deleted;
+
+  /// Associated type introduction rules are 'permanent', meaning they cannot
+  /// be deleted by homotopy reduction. This is because they do not correspond
+  /// to generic requirements and are re-added when the rewrite system is
+  /// built, so by leaving them in place we can find other redundancies
+  /// instead.
+  unsigned Permanent : 1;
+
+  /// A 'simplified' rule was eliminated by simplifyRewriteSystem() if one of two
+  /// things happen:
+  /// - The rule's left hand side can be reduced via some other rule, in which
+  ///   case completion will have filled in the missing edge if necessary.
+  /// - The rule's right hand side can be reduced, in which case the reduced
+  ///   rule is added when simplifying the rewrite system.
+  ///
+  /// Simplified rules do not participate in term rewriting, because other rules
+  /// can be used to derive an equivalent rewrite path.
+  unsigned Simplified : 1;
+
+  /// A 'redundant' rule was eliminated by homotopy reduction. Redundant rules
+  /// still participate in term rewriting, but they are not part of the minimal
+  /// set of requirements in a generic signature.
+  unsigned Redundant : 1;
 
 public:
   Rule(Term lhs, Term rhs)
-      : LHS(lhs), RHS(rhs), deleted(false) {}
+      : LHS(lhs), RHS(rhs) {
+    Permanent = false;
+    Simplified = false;
+    Redundant = false;
+  }
 
   const Term &getLHS() const { return LHS; }
   const Term &getRHS() const { return RHS; }
@@ -54,19 +80,29 @@ class Rule final {
 
   bool isProtocolConformanceRule() const;
 
-  /// Returns if the rule was deleted.
-  bool isDeleted() const {
-    return deleted;
+  /// See above for an explanation.
+  bool isPermanent() const {
+    return Permanent;
+  }
+
+  /// See above for an explanation.
+  bool isSimplified() const {
+    return Simplified;
+  }
+
+  /// See above for an explanation.
+  bool isRedundant() const {
+    return Redundant;
   }
 
   /// Deletes the rule, which removes it from consideration in term
   /// simplification and completion. Deleted rules are simply marked as
   /// such instead of being physically removed from the rules vector
   /// in the rewrite system, to ensure that indices remain valid across
   /// deletion.
-  void markDeleted() {
-    assert(!deleted);
-    deleted = true;
+  void markSimplified() {
+    assert(!Simplified);
+    Simplified = true;
   }
 
   /// Returns the length of the left hand side.

lib/AST/RequirementMachine/RewriteSystemCompletion.cpp

@@ -501,7 +501,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
     // 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);
-      if (lhs.isDeleted())
+      if (lhs.isSimplified())
         continue;
 
       // Look up every suffix of this rule in the trie using findAll(). This
@@ -519,7 +519,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
             return;
 
           const auto &rhs = getRule(j);
-          if (rhs.isDeleted())
+          if (rhs.isSimplified())
             return;
 
           if (from == lhs.getLHS().begin()) {