RequirementMachine: Introduce RewriteStep::ConcreteTypeWitness

Author: slavapestov

lib/AST/RequirementMachine/GeneratingConformances.cpp

@@ -137,6 +137,7 @@ void RewriteLoop::findProtocolConformanceRules(
       case RewriteStep::Decompose:
       case RewriteStep::ConcreteConformance:
       case RewriteStep::SuperclassConformance:
+      case RewriteStep::ConcreteTypeWitness:
         break;
       }
     }

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -92,6 +92,7 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::Decompose:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
+    case RewriteStep::ConcreteTypeWitness:
       break;
     }
 
@@ -208,6 +209,7 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::Decompose:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
+    case RewriteStep::ConcreteTypeWitness:
       break;
     }
 
@@ -306,6 +308,7 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::Decompose:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
+    case RewriteStep::ConcreteTypeWitness:
       newSteps.push_back(step);
       break;
     }

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -78,6 +78,14 @@ void RewriteStep::dump(llvm::raw_ostream &out,
                     : "SuperclassConformance");
     break;
   }
+  case ConcreteTypeWitness: {
+    evaluator.applyConcreteTypeWitness(*this, system);
+
+    out << (Inverse ? "ConcreteTypeWitness⁻¹"
+                    : "ConcreteTypeWitness");
+    break;
+  }
+
   }
 }
 
@@ -416,6 +424,64 @@ RewritePathEvaluator::applyConcreteConformance(const RewriteStep &step,
   }
 }
 
+void RewritePathEvaluator::applyConcreteTypeWitness(const RewriteStep &step,
+                                                  const RewriteSystem &system) {
+  checkA();
+  auto &term = A.back();
+
+  const auto &witness = system.getConcreteTypeWitness(step.RuleID);
+  auto fail = [&]() {
+    llvm::errs() << "Bad concrete type witness term:\n";
+    llvm::errs() << term << "\n\n";
+    llvm::errs() << "Conformance: " << witness.ConcreteConformance << "\n";
+    llvm::errs() << "Assoc type: " << witness.AssocType << "\n";
+    llvm::errs() << "Concrete type: " << witness.ConcreteType << "\n";
+    abort();
+  };
+
+  if (!step.Inverse) {
+    // Make sure the term takes the following form, where |V| == EndOffset:
+    //
+    //    U.[concrete: C : P].[P:X].[concrete: C.X].V
+    if (term.size() <= step.EndOffset + 3 ||
+        *(term.end() - step.EndOffset - 3) != witness.ConcreteConformance ||
+        *(term.end() - step.EndOffset - 2) != witness.AssocType ||
+        *(term.end() - step.EndOffset - 1) != witness.ConcreteType) {
+      fail();
+    }
+
+    // Get the subterm U.[concrete: C : P].[P:X].
+    MutableTerm newTerm(term.begin(), term.end() - step.EndOffset - 1);
+
+    // Add the subterm V, to get U.[concrete: C : P].[P:X].V.
+    newTerm.append(term.end() - step.EndOffset, term.end());
+
+    term = newTerm;
+  } else {
+    // Make sure the term takes the following form, where |V| == EndOffset:
+    //
+    //    U.[concrete: C : P].[P:X].V
+    if (term.size() <= step.EndOffset + 2 ||
+        *(term.end() - step.EndOffset - 2) != witness.ConcreteConformance ||
+        *(term.end() - step.EndOffset - 1) != witness.AssocType) {
+      fail();
+    }
+
+    // Get the subterm U.[concrete: C : P].[P:X].
+    MutableTerm newTerm(term.begin(), term.end() - step.EndOffset);
+
+    // Add the symbol [concrete: C.X].
+    newTerm.add(witness.ConcreteType);
+
+    // Add the subterm V, to get
+    //
+    //    U.[concrete: C : P].[P:X].[concrete: C.X].V
+    newTerm.append(term.end() - step.EndOffset, term.end());
+
+    term = newTerm;
+  }
+}
+
 void RewritePathEvaluator::apply(const RewriteStep &step,
                                  const RewriteSystem &system) {
   switch (step.Kind) {
@@ -439,5 +505,9 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
   case RewriteStep::SuperclassConformance:
     applyConcreteConformance(step, system);
     break;
+
+  case RewriteStep::ConcreteTypeWitness:
+    applyConcreteTypeWitness(step, system);
+    break;
   }
 }

lib/AST/RequirementMachine/RewriteLoop.h

@@ -95,7 +95,21 @@ struct RewriteStep {
     /// concrete conformance symbol [concrete: C : P]. This symbol is replaced
     /// with the superclass symbol [superclass: C] followed by the protocol
     /// symbol [P].
-    SuperclassConformance
+    SuperclassConformance,
+
+    /// If not inverted: the top of the A stack must be a term ending in a
+    /// concrete conformance symbol [concrete: C : P] followed by an associated
+    /// type symbol [P:X], and the concrete type symbol [concrete: C.X] for the
+    /// type witness of 'X' in the conformance 'C : P'. The concrete type symbol
+    /// is eliminated.
+    ///
+    /// If inverted: the concrete type symbol [concrete: C.X] is introduced.
+    ///
+    /// The RuleID field is repurposed to store the result of calling
+    /// RewriteSystem::recordConcreteTypeWitness(). This index is then
+    /// passed in to RewriteSystem::getConcreteTypeWitness() when applying
+    /// the step.
+    ConcreteTypeWitness
   };
 
   /// The rewrite step kind.
@@ -165,6 +179,11 @@ struct RewriteStep {
                        /*ruleID=*/0, inverse);
   }
 
+  static RewriteStep forConcreteTypeWitness(unsigned witnessID, bool inverse) {
+    return RewriteStep(ConcreteTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
+                       /*ruleID=*/witnessID, inverse);
+  }
+
   bool isInContext() const {
     return StartOffset > 0 || EndOffset > 0;
   }
@@ -331,6 +350,9 @@ struct RewritePathEvaluator {
   void applyConcreteConformance(const RewriteStep &step,
                                 const RewriteSystem &system);
 
+  void applyConcreteTypeWitness(const RewriteStep &step,
+                                const RewriteSystem &system);
+
   void dump(llvm::raw_ostream &out) const;
 };