RequirementMachine: Replace RewriteStep::{Superclass,Concrete}Conformance with relations

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -98,8 +98,6 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::ConcreteConformance:
-    case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
     case RewriteStep::AbstractTypeWitness:
@@ -222,8 +220,6 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::ConcreteConformance:
-    case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
     case RewriteStep::AbstractTypeWitness:
@@ -324,8 +320,6 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::ConcreteConformance:
-    case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
     case RewriteStep::AbstractTypeWitness:

lib/AST/RequirementMachine/MinimalConformances.cpp

@@ -138,8 +138,6 @@ void RewriteLoop::findProtocolConformanceRules(
       case RewriteStep::Shift:
       case RewriteStep::Decompose:
       case RewriteStep::Relation:
-      case RewriteStep::ConcreteConformance:
-      case RewriteStep::SuperclassConformance:
       case RewriteStep::ConcreteTypeWitness:
       case RewriteStep::SameTypeWitness:
       case RewriteStep::AbstractTypeWitness:

lib/AST/RequirementMachine/PropertyRelations.cpp

@@ -65,6 +65,31 @@ unsigned RewriteSystem::recordRelation(Symbol lhsProperty,
       Term::get(rhsTerm, Context));
 }
 
+/// Record a relation ([concrete: C].[P] => [concrete: C : P])
+/// or ([superclass: C].[P] => [concrete: C : P]) which combines a
+/// concrete type symbol (or a superclass symbol) with a protocol
+/// symbol to form a single a concrete conformance symbol.
+unsigned RewriteSystem::recordConcreteConformanceRelation(
+    Symbol concreteSymbol, Symbol protocolSymbol,
+    Symbol concreteConformanceSymbol) {
+  assert(protocolSymbol.getKind() == Symbol::Kind::Protocol);
+  assert(protocolSymbol.getProtocol() ==
+         concreteConformanceSymbol.getProtocol());
+  assert(concreteSymbol.getKind() == Symbol::Kind::Superclass ||
+         concreteSymbol.getKind() == Symbol::Kind::ConcreteType);
+
+  MutableTerm lhsTerm;
+  lhsTerm.add(concreteSymbol);
+  lhsTerm.add(protocolSymbol);
+
+  MutableTerm rhsTerm;
+  rhsTerm.add(concreteConformanceSymbol);
+
+  return recordRelation(
+      Term::get(lhsTerm, Context),
+      Term::get(rhsTerm, Context));
+}
+
 RewriteSystem::TypeWitness::TypeWitness(
     Term lhs, llvm::PointerUnion<Symbol, Term> rhs)
   : LHS(lhs), RHS(rhs) {

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -957,23 +957,6 @@ void PropertyMap::recordConcreteConformanceRule(
   const auto &concreteRule = System.getRule(concreteRuleID);
   const auto &conformanceRule = System.getRule(conformanceRuleID);
 
-#ifndef NDEBUG
-  {
-    auto conformanceSymbol = *conformanceRule.isPropertyRule();
-    assert(conformanceSymbol.getKind() == Symbol::Kind::Protocol);
-    assert(conformanceSymbol.getProtocol() ==
-           concreteConformanceSymbol.getProtocol());
-
-    auto concreteSymbol = *concreteRule.isPropertyRule();
-    if (concreteSymbol.getKind() == Symbol::Kind::Superclass)
-      assert(requirementKind == RequirementKind::Superclass);
-    else {
-      assert(concreteSymbol.getKind() == Symbol::Kind::ConcreteType);
-      assert(requirementKind == RequirementKind::SameType);
-    }
-  }
-#endif
-
   RewritePath path;
 
   // We have a pair of rules T.[P] and T'.[concrete: C].
@@ -1000,20 +983,28 @@ void PropertyMap::recordConcreteConformanceRule(
 
   // Apply a concrete type adjustment to the concrete symbol if T' is shorter
   // than T.
+  auto concreteSymbol = *concreteRule.isPropertyRule();
   unsigned adjustment = rhs.size() - concreteRule.getRHS().size();
+
   if (adjustment > 0 &&
       !concreteConformanceSymbol.getSubstitutions().empty()) {
     path.add(RewriteStep::forAdjustment(adjustment, /*endOffset=*/1,
                                         /*inverse=*/false));
+
+    MutableTerm prefix(rhs.begin(), rhs.begin() + adjustment);
+    concreteSymbol = concreteSymbol.prependPrefixToConcreteSubstitutions(
+        prefix, Context);
   }
 
+  auto protocolSymbol = *conformanceRule.isPropertyRule();
+
   // Now, transform T''.[concrete: C].[P] into T''.[concrete: C : P].
-  if (requirementKind == RequirementKind::Superclass) {
-    path.add(RewriteStep::forSuperclassConformance(/*inverse=*/false));
-  } else {
-    assert(requirementKind == RequirementKind::SameType);
-    path.add(RewriteStep::forConcreteConformance(/*inverse=*/false));
-  }
+  unsigned relationID = System.recordConcreteConformanceRelation(
+      concreteSymbol, protocolSymbol, concreteConformanceSymbol);
+
+  path.add(RewriteStep::forRelation(
+      /*startOffset=*/rhs.size(), relationID,
+      /*inverse=*/false));
 
   MutableTerm lhs(rhs);
   lhs.add(concreteConformanceSymbol);

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -79,20 +79,6 @@ void RewriteStep::dump(llvm::raw_ostream &out,
 
     break;
   }
-  case ConcreteConformance: {
-    evaluator.applyConcreteConformance(*this, system);
-
-    out << (Inverse ? "ConcreteConformance⁻¹"
-                    : "ConcreteConformance");
-    break;
-  }
-  case SuperclassConformance: {
-    evaluator.applyConcreteConformance(*this, system);
-
-    out << (Inverse ? "SuperclassConformance⁻¹"
-                    : "SuperclassConformance");
-    break;
-  }
   case ConcreteTypeWitness: {
     evaluator.applyConcreteTypeWitness(*this, system);
 
@@ -411,88 +397,6 @@ RewritePathEvaluator::applyRelation(const RewriteStep &step,
   return {lhs, rhs, prefix, suffix};
 }
 
-void
-RewritePathEvaluator::applyConcreteConformance(const RewriteStep &step,
-                                               const RewriteSystem &system) {
-  checkPrimary();
-  auto &term = Primary.back();
-  Symbol *last = term.end() - step.EndOffset;
-
-  auto &ctx = system.getRewriteContext();
-
-  if (!step.Inverse) {
-    // The input term takes one of the following forms, where |V| == EndOffset:
-    // - U.[concrete: C].[P].V
-    // - U.[superclass: C].[P].V
-    assert(term.size() > step.EndOffset + 2);
-    auto concreteType = *(last - 2);
-    auto proto = *(last - 1);
-    assert(proto.getKind() == Symbol::Kind::Protocol);
-
-    // Get the prefix U.
-    MutableTerm newTerm(term.begin(), last - 2);
-
-    // Build the term U.[concrete: C : P].
-    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));
-    }
-
-    // Add the suffix V to get the final term U.[concrete: C : P].V.
-    newTerm.append(last, term.end());
-    term = newTerm;
-  } else {
-    // The input term takes the form U.[concrete: C : P].V, where
-    // |V| == EndOffset.
-    assert(term.size() > step.EndOffset + 1);
-    auto concreteConformance = *(last - 1);
-    assert(concreteConformance.getKind() == Symbol::Kind::ConcreteConformance);
-
-    // Build the term U.
-    MutableTerm newTerm(term.begin(), last - 1);
-
-    // Add the symbol [concrete: C] or [superclass: C] to get the term
-    // U.[concrete: C] or U.[superclass: C].
-    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));
-    }
-
-    // Add the symbol [P] to get the term U.[concrete: C].[P] or
-    // U.[superclass: C].[P].
-    newTerm.add(Symbol::forProtocol(
-        concreteConformance.getProtocol(),
-        ctx));
-
-    // Add the suffix V to get the final term U.[concrete: C].[P].V or
-    // U.[superclass: C].[P].V.
-    newTerm.append(last, term.end());
-    term = newTerm;
-  }
-}
-
 void RewritePathEvaluator::applyConcreteTypeWitness(const RewriteStep &step,
                                                   const RewriteSystem &system) {
   checkPrimary();
@@ -682,11 +586,6 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
     applyRelation(step, system);
     break;
 
-  case RewriteStep::ConcreteConformance:
-  case RewriteStep::SuperclassConformance:
-    applyConcreteConformance(step, system);
-    break;
-
   case RewriteStep::ConcreteTypeWitness:
     applyConcreteTypeWitness(step, system);
     break;

lib/AST/RequirementMachine/RewriteLoop.h

@@ -100,28 +100,6 @@ struct RewriteStep {
     /// RewriteSystem::recordRelation().
     Relation,
 
-    /// If not inverted: the top of the primary 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 primary 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 primary 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 primary 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,
-
     /// If not inverted: the top of the primary 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
@@ -215,16 +193,6 @@ struct RewriteStep {
                        /*arg=*/relationID, inverse);
   }
 
-  static RewriteStep forConcreteConformance(bool inverse) {
-    return RewriteStep(ConcreteConformance, /*startOffset=*/0, /*endOffset=*/0,
-                       /*arg=*/0, inverse);
-  }
-
-  static RewriteStep forSuperclassConformance(bool inverse) {
-    return RewriteStep(SuperclassConformance, /*startOffset=*/0, /*endOffset=*/0,
-                       /*arg=*/0, inverse);
-  }
-
   static RewriteStep forConcreteTypeWitness(unsigned witnessID, bool inverse) {
     return RewriteStep(ConcreteTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
                        /*arg=*/witnessID, inverse);

lib/AST/RequirementMachine/RewriteSystem.h

@@ -346,6 +346,9 @@ class RewriteSystem final {
   Relation getRelation(unsigned index) const;
 
   unsigned recordRelation(Symbol lhs, Symbol rhs);
+  unsigned recordConcreteConformanceRelation(
+    Symbol concreteSymbol, Symbol protocolSymbol,
+    Symbol concreteConformanceSymbol);
 
   /// A type witness has a subject type, stored in LHS, which takes the form:
   ///