RequirementMachine: Add Rule::isExplicit() bit

Eventually I might upgrade this to a SourceLoc, for redundancy
diagnostics.

Author: slavapestov

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -101,6 +101,8 @@ void Rule::dump(llvm::raw_ostream &out) const {
   out << LHS << " => " << RHS;
   if (Permanent)
     out << " [permanent]";
+  if (Explicit)
+    out << " [explicit]";
   if (Simplified)
     out << " [simplified]";
   if (Redundant)
@@ -133,7 +135,7 @@ void RewriteSystem::initialize(
     addPermanentRule(rule.first, rule.second);
 
   for (const auto &rule : requirementRules)
-    addRule(rule.first, rule.second);
+    addExplicitRule(rule.first, rule.second);
 }
 
 /// Reduce a term by applying all rewrite rules until fixed point.
@@ -412,6 +414,15 @@ bool RewriteSystem::addPermanentRule(MutableTerm lhs, MutableTerm rhs) {
   return added;
 }
 
+/// Add a new rule, marking it explicit.
+bool RewriteSystem::addExplicitRule(MutableTerm lhs, MutableTerm rhs) {
+  bool added = addRule(std::move(lhs), std::move(rhs));
+  if (added)
+    Rules.back().markExplicit();
+
+  return added;
+}
+
 /// Delete any rules whose left hand sides can be reduced by other rules,
 /// and reduce the right hand sides of all remaining rules as much as
 /// possible.

lib/AST/RequirementMachine/RewriteSystem.h

@@ -42,13 +42,14 @@ class Rule final {
   Term LHS;
   Term RHS;
 
-  /// 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.
+  /// A 'permanent' rule cannot be deleted by homotopy reduction. These
+  /// do not correspond to generic requirements and are re-added when the
+  /// rewrite system is built.
   unsigned Permanent : 1;
 
+  /// An 'explicit' rule is a generic requirement written by the user.
+  unsigned Explicit : 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
@@ -69,6 +70,7 @@ class Rule final {
   Rule(Term lhs, Term rhs)
       : LHS(lhs), RHS(rhs) {
     Permanent = false;
+    Explicit = false;
     Simplified = false;
     Redundant = false;
   }
@@ -84,36 +86,40 @@ class Rule final {
 
   bool isProtocolRefinementRule() const;
 
-  /// See above for an explanation.
+  /// See above for an explanation of these predicates.
   bool isPermanent() const {
     return Permanent;
   }
 
-  /// See above for an explanation.
+  bool isExplicit() const {
+    return Explicit;
+  }
+
   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 markSimplified() {
     assert(!Simplified);
     Simplified = true;
   }
 
   void markPermanent() {
-    assert(!Permanent);
+    assert(!Explicit && !Permanent &&
+           "Permanent and explicit are mutually exclusive");
     Permanent = true;
   }
 
+  void markExplicit() {
+    assert(!Explicit && !Permanent &&
+           "Permanent and explicit are mutually exclusive");
+    Explicit = true;
+  }
+
   void markRedundant() {
     assert(!Redundant);
     Redundant = true;
@@ -255,6 +261,8 @@ class RewriteSystem final {
 
   bool addPermanentRule(MutableTerm lhs, MutableTerm rhs);
 
+  bool addExplicitRule(MutableTerm lhs, MutableTerm rhs);
+
   bool simplify(MutableTerm &term, RewritePath *path=nullptr) const;
 
   void simplifySubstitutions(MutableTerm &term, RewritePath &path) const;