RequirementMachine: Introduce RewriteStep::SameTypeWitness

Author: slavapestov

lib/AST/RequirementMachine/GeneratingConformances.cpp

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

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -93,6 +93,7 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
+    case RewriteStep::SameTypeWitness:
       break;
     }
 
@@ -210,6 +211,7 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
+    case RewriteStep::SameTypeWitness:
       break;
     }
 
@@ -309,6 +311,7 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
+    case RewriteStep::SameTypeWitness:
       newSteps.push_back(step);
       break;
     }

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -85,6 +85,13 @@ void RewriteStep::dump(llvm::raw_ostream &out,
                     : "ConcreteTypeWitness");
     break;
   }
+  case SameTypeWitness: {
+    evaluator.applySameTypeWitness(*this, system);
+
+    out << (Inverse ? "SameTypeWitness⁻¹"
+                    : "SameTypeWitness");
+    break;
+  }
 
   }
 }
@@ -482,6 +489,71 @@ void RewritePathEvaluator::applyConcreteTypeWitness(const RewriteStep &step,
   }
 }
 
+void RewritePathEvaluator::applySameTypeWitness(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();
+  };
+
+#ifndef NDEBUG
+  if ((witness.ConcreteType.getConcreteType() !=
+       witness.ConcreteConformance.getConcreteType()) ||
+      (witness.ConcreteType.getSubstitutions() !=
+       witness.ConcreteConformance.getSubstitutions())) {
+    fail();
+  }
+#endif
+
+  if (!step.Inverse) {
+    // 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].
+    MutableTerm newTerm(term.begin(), term.end() - step.EndOffset - 1);
+
+    // Add the subterm V, to get U.[concrete: C : P].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].V
+    if (term.size() <= step.EndOffset + 1 ||
+        *(term.end() - step.EndOffset - 1) != witness.ConcreteConformance) {
+      fail();
+    }
+
+    // Get the subterm U.[concrete: C : P].
+    MutableTerm newTerm(term.begin(), term.end() - step.EndOffset);
+
+    // Add the symbol [P:X].
+    newTerm.add(witness.AssocType);
+
+    // Add the subterm V, to get
+    //
+    //    U.[concrete: C : P].[P:X].V
+    newTerm.append(term.end() - step.EndOffset, term.end());
+
+    term = newTerm;
+  }
+}
+
 void RewritePathEvaluator::apply(const RewriteStep &step,
                                  const RewriteSystem &system) {
   switch (step.Kind) {
@@ -509,5 +581,9 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
   case RewriteStep::ConcreteTypeWitness:
     applyConcreteTypeWitness(step, system);
     break;
+
+  case RewriteStep::SameTypeWitness:
+    applySameTypeWitness(step, system);
+    break;
   }
 }

lib/AST/RequirementMachine/RewriteLoop.h

@@ -34,6 +34,10 @@ struct RewritePathEvaluator;
 /// Records an evaluation step in a rewrite path.
 struct RewriteStep {
   enum StepKind : unsigned {
+    ///
+    /// *** Rewrite step kinds introduced by Knuth-Bendix completion ***
+    ///
+
     /// Apply a rewrite rule to the term at the top of the A stack.
     ///
     /// Formally, this is a whiskered, oriented rewrite rule. For example,
@@ -60,6 +64,10 @@ struct RewriteStep {
     /// The StartOffset field encodes the length of the prefix.
     AdjustConcreteType,
 
+    ///
+    /// *** Rewrite step kinds introduced by simplifySubstitutions() ***
+    ///
+
     /// Move a term from the A stack to the B stack (if not inverted) or
     /// B stack to A stack (if inverted).
     Shift,
@@ -75,6 +83,10 @@ struct RewriteStep {
     /// The RuleID field encodes the number of substitutions.
     Decompose,
 
+    ///
+    /// *** Rewrite step kinds introduced by the property map ***
+    ///
+
     /// 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
@@ -109,7 +121,19 @@ struct RewriteStep {
     /// RewriteSystem::recordConcreteTypeWitness(). This index is then
     /// passed in to RewriteSystem::getConcreteTypeWitness() when applying
     /// the step.
-    ConcreteTypeWitness
+    ConcreteTypeWitness,
+
+    /// 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]. The associated type symbol is eliminated.
+    ///
+    /// If inverted: the associated type symbol [P: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.
+    SameTypeWitness,
   };
 
   /// The rewrite step kind.
@@ -184,6 +208,11 @@ struct RewriteStep {
                        /*ruleID=*/witnessID, inverse);
   }
 
+  static RewriteStep forSameTypeWitness(unsigned witnessID, bool inverse) {
+    return RewriteStep(SameTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
+                       /*ruleID=*/witnessID, inverse);
+  }
+
   bool isInContext() const {
     return StartOffset > 0 || EndOffset > 0;
   }
@@ -353,6 +382,9 @@ struct RewritePathEvaluator {
   void applyConcreteTypeWitness(const RewriteStep &step,
                                 const RewriteSystem &system);
 
+  void applySameTypeWitness(const RewriteStep &step,
+                            const RewriteSystem &system);
+
   void dump(llvm::raw_ostream &out) const;
 };