RequirementMachine: Introduce RewriteStep::ConcreteConformance and ::SuperclassConformance

Author: slavapestov

lib/AST/RequirementMachine/GeneratingConformances.cpp

@@ -134,6 +134,8 @@ void RewriteLoop::findProtocolConformanceRules(
       case RewriteStep::AdjustConcreteType:
       case RewriteStep::Shift:
       case RewriteStep::Decompose:
+      case RewriteStep::ConcreteConformance:
+      case RewriteStep::SuperclassConformance:
         break;
       }
     }

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -96,6 +96,8 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::ConcreteConformance:
+    case RewriteStep::SuperclassConformance:
       break;
     }
 
@@ -210,6 +212,8 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::ConcreteConformance:
+    case RewriteStep::SuperclassConformance:
       break;
     }
 
@@ -306,6 +310,8 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::ConcreteConformance:
+    case RewriteStep::SuperclassConformance:
       newSteps.push_back(step);
       break;
     }
@@ -339,6 +345,10 @@ bool RewriteStep::isInverseOf(const RewriteStep &other) const {
 
   case RewriteStep::Decompose:
     return RuleID == other.RuleID;
+
+  case RewriteStep::ConcreteConformance:
+  case RewriteStep::SuperclassConformance:
+    return true;
   }
 
   assert(EndOffset == other.EndOffset && "Bad whiskering?");
@@ -465,7 +475,7 @@ bool RewritePath::computeCyclicallyReducedLoop(MutableTerm &basepoint,
       break;
 
     // Update the basepoint by applying the first step in the path.
-    left.apply(evaluator, system);
+    evaluator.apply(left, system);
 
     ++count;
   }
@@ -522,14 +532,16 @@ bool RewriteLoop::isInContext(const RewriteSystem &system) const {
       case RewriteStep::AdjustConcreteType:
       case RewriteStep::Shift:
       case RewriteStep::Decompose:
+      case RewriteStep::ConcreteConformance:
+      case RewriteStep::SuperclassConformance:
         break;
       }
 
       if (minStartOffset == 0 && minEndOffset == 0)
         break;
     }
 
-    step.apply(evaluator, system);
+    evaluator.apply(step, system);
   }
 
   return (minStartOffset > 0 || minEndOffset > 0);

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -61,6 +61,20 @@ void RewriteStep::dump(llvm::raw_ostream &out,
     out << RuleID << ")";
     break;
   }
+  case ConcreteConformance: {
+    evaluator.applyConcreteConformance(*this, system);
+
+    out << (Inverse ? "ConcreteConformance⁻¹"
+                    : "ConcreteConformance");
+    break;
+  }
+  case SuperclassConformance: {
+    evaluator.applyConcreteConformance(*this, system);
+
+    out << (Inverse ? "SuperclassConformance⁻¹"
+                    : "SuperclassConformance");
+    break;
+  }
   }
 }
 
@@ -312,6 +326,69 @@ void RewritePathEvaluator::applyDecompose(const RewriteStep &step,
   }
 }
 
+void
+RewritePathEvaluator::applyConcreteConformance(const RewriteStep &step,
+                                               const RewriteSystem &system) {
+  checkA();
+  auto &term = A.back();
+
+  auto &ctx = system.getRewriteContext();
+
+  if (!step.Inverse) {
+    assert(term.size() > 2);
+    auto concreteType = *(term.end() - 2);
+    auto proto = *(term.end() - 1);
+    assert(proto.getKind() == Symbol::Kind::Protocol);
+
+    MutableTerm newTerm(term.begin(), term.end() - 2);
+    if (step.Kind == RewriteStep::ConcreteConformance) {
+      assert(concreteType.getKind() == Symbol::Kind::ConcreteType);
+
+      newTerm.add(Symbol::forConcreteConformance(
+          concreteType.getConcreteType(),
+          concreteType.getSubstitutions(),
+          proto.getProtocol(),
+          ctx));
+    } else {
+      assert(step.Kind == RewriteStep::SuperclassConformance);
+      assert(concreteType.getKind() == Symbol::Kind::Superclass);
+
+      newTerm.add(Symbol::forConcreteConformance(
+          concreteType.getSuperclass(),
+          concreteType.getSubstitutions(),
+          proto.getProtocol(),
+          ctx));
+    }
+
+    term = newTerm;
+  } else {
+    assert(term.size() > 1);
+    auto concreteConformance = term.back();
+    assert(concreteConformance.getKind() == Symbol::Kind::ConcreteConformance);
+
+    MutableTerm newTerm(term.begin(), term.end() - 1);
+
+    if (step.Kind == RewriteStep::ConcreteConformance) {
+      newTerm.add(Symbol::forConcreteType(
+          concreteConformance.getConcreteType(),
+          concreteConformance.getSubstitutions(),
+          ctx));
+    } else {
+      assert(step.Kind == RewriteStep::SuperclassConformance);
+      newTerm.add(Symbol::forSuperclass(
+          concreteConformance.getConcreteType(),
+          concreteConformance.getSubstitutions(),
+          ctx));
+    }
+
+    newTerm.add(Symbol::forProtocol(
+        concreteConformance.getProtocol(),
+        ctx));
+
+    term = newTerm;
+  }
+}
+
 void RewritePathEvaluator::apply(const RewriteStep &step,
                                  const RewriteSystem &system) {
   switch (step.Kind) {
@@ -330,5 +407,10 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
   case RewriteStep::Decompose:
     applyDecompose(step, system);
     break;
+
+  case RewriteStep::ConcreteConformance:
+  case RewriteStep::SuperclassConformance:
+    applyConcreteConformance(step, system);
+    break;
   }
 }

lib/AST/RequirementMachine/RewriteLoop.h

@@ -73,19 +73,41 @@ struct RewriteStep {
     /// new substitutions replace the substitutions in that symbol.
     ///
     /// The RuleID field encodes the number of substitutions.
-    Decompose
+    Decompose,
+
+    /// If not inverted: the top of the A stack must be a term ending in a
+    /// concrete type symbol [concrete: C] followed by a protocol symbol [P].
+    /// These two symbols are combined into a single concrete conformance
+    /// symbol [concrete: C : P].
+    ///
+    /// If inverted: the top of the A stack must be a term ending in a
+    /// concrete conformance symbol [concrete: C : P]. This symbol is replaced
+    /// with the concrete type symbol [concrete: C] followed by the protocol
+    /// symbol [P].
+    ConcreteConformance,
+
+    /// If not inverted: the top of the A stack must be a term ending in a
+    /// superclass symbol [superclass: C] followed by a protocol symbol [P].
+    /// These two symbols are combined into a single concrete conformance
+    /// symbol [concrete: C : P].
+    ///
+    /// If inverted: the top of the A stack must be a term ending in a
+    /// concrete conformance symbol [concrete: C : P]. This symbol is replaced
+    /// with the superclass symbol [superclass: C] followed by the protocol
+    /// symbol [P].
+    SuperclassConformance
   };
 
   /// The rewrite step kind.
-  StepKind Kind : 2;
+  StepKind Kind : 3;
 
   /// The size of the left whisker, which is the position within the term where
   /// the rule is being applied. In A.(X => Y).B, this is |A|=1.
-  unsigned StartOffset : 15;
+  unsigned StartOffset : 14;
 
   /// The size of the right whisker, which is the length of the remaining suffix
   /// after the rule is applied. In A.(X => Y).B, this is |B|=1.
-  unsigned EndOffset : 15;
+  unsigned EndOffset : 14;
 
   /// If Kind is ApplyRewriteRule, the index of the rule in the rewrite system.
   ///
@@ -132,6 +154,16 @@ struct RewriteStep {
                        /*ruleID=*/numSubstitutions, inverse);
   }
 
+  static RewriteStep forConcreteConformance(bool inverse) {
+    return RewriteStep(ConcreteConformance, /*startOffset=*/0, /*endOffset=*/0,
+                       /*ruleID=*/0, inverse);
+  }
+
+  static RewriteStep forSuperclassConformance(bool inverse) {
+    return RewriteStep(SuperclassConformance, /*startOffset=*/0, /*endOffset=*/0,
+                       /*ruleID=*/0, inverse);
+  }
+
   bool isInContext() const {
     return StartOffset > 0 || EndOffset > 0;
   }
@@ -303,6 +335,9 @@ struct RewritePathEvaluator {
   void applyDecompose(const RewriteStep &step,
                       const RewriteSystem &system);
 
+  void applyConcreteConformance(const RewriteStep &step,
+                                const RewriteSystem &system);
+
   void dump(llvm::raw_ostream &out) const;
 };