RequirementMachine: Replace RewriteStep::SameTypeWitness with a relation

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -98,7 +98,6 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::SameTypeWitness:
       break;
     }
 
@@ -218,7 +217,6 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::SameTypeWitness:
       break;
     }
 
@@ -316,7 +314,6 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::SameTypeWitness:
       newSteps.push_back(step);
       break;
     }

lib/AST/RequirementMachine/MinimalConformances.cpp

@@ -138,7 +138,6 @@ void RewriteLoop::findProtocolConformanceRules(
       case RewriteStep::Shift:
       case RewriteStep::Decompose:
       case RewriteStep::Relation:
-      case RewriteStep::SameTypeWitness:
         break;
       }
     }

lib/AST/RequirementMachine/PropertyRelations.cpp

@@ -118,6 +118,33 @@ unsigned RewriteSystem::recordConcreteTypeWitnessRelation(
       Term::get(rhsTerm, Context));
 }
 
+/// Record a relation ([concrete: C : P].[P:X].[concrete: C] =>
+/// [concrete: C : P].[P:X]) which "ties off" a nested type C.X that is
+/// equivalent to C.
+unsigned RewriteSystem::recordSameTypeWitnessRelation(
+    Symbol concreteConformanceSymbol,
+    Symbol associatedTypeSymbol) {
+  assert(concreteConformanceSymbol.getKind() ==
+         Symbol::Kind::ConcreteConformance);
+  assert(associatedTypeSymbol.getKind() ==
+         Symbol::Kind::AssociatedType);
+
+  MutableTerm rhsTerm;
+  rhsTerm.add(concreteConformanceSymbol);
+
+  auto concreteSymbol = Symbol::forConcreteType(
+      concreteConformanceSymbol.getConcreteType(),
+      concreteConformanceSymbol.getSubstitutions(),
+      Context);
+  MutableTerm lhsTerm(rhsTerm);
+  lhsTerm.add(associatedTypeSymbol);
+  lhsTerm.add(concreteSymbol);
+
+  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

@@ -894,15 +894,11 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
   auto typeWitnessSymbol =
       Symbol::forConcreteType(typeWitnessSchema, result, Context);
 
-  RewriteSystem::TypeWitness witness(Term::get(subjectType, Context),
-                                     typeWitnessSymbol);
-  unsigned witnessID = System.recordTypeWitness(witness);
-
   auto concreteConformanceSymbol = *(subjectType.end() - 2);
   auto associatedTypeSymbol = *(subjectType.end() - 1);
 
   // Record the relation before simplifying typeWitnessSymbol below.
-  unsigned relationID = System.recordConcreteTypeWitnessRelation(
+  unsigned concreteRelationID = System.recordConcreteTypeWitnessRelation(
       concreteConformanceSymbol,
       associatedTypeSymbol,
       typeWitnessSymbol);
@@ -925,16 +921,21 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
     MutableTerm result(key);
     result.add(concreteConformanceSymbol);
 
+    unsigned sameRelationID = System.recordSameTypeWitnessRelation(
+        concreteConformanceSymbol,
+        associatedTypeSymbol);
+
     // ([concrete: C : P] => [concrete: C : P].[P:X].[concrete: C])
-    path.add(RewriteStep::forSameTypeWitness(
-        witnessID, /*inverse=*/true));
+    path.add(RewriteStep::forRelation(
+        /*startOffset=*/key.size(), sameRelationID,
+        /*inverse=*/true));
 
     // [concrete: C : P].[P:X].([concrete: C] => [concrete: C.X])
     path.append(substPath);
 
     // T.([concrete: C : P].[P:X].[concrete: C.X] => [concrete: C : P].[P:X])
     path.add(RewriteStep::forRelation(
-        /*startOffset=*/key.size(), relationID,
+        /*startOffset=*/key.size(), concreteRelationID,
         /*inverse=*/false));
 
     return result;
@@ -955,7 +956,7 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
 
   // T.([concrete: C : P].[P:X].[concrete: C.X] => [concrete: C : P].[P:X])
   path.add(RewriteStep::forRelation(
-      /*startOffset=*/key.size(), relationID,
+      /*startOffset=*/key.size(), concreteRelationID,
       /*inverse=*/false));
 
   return constraintType;

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -79,13 +79,6 @@ void RewriteStep::dump(llvm::raw_ostream &out,
 
     break;
   }
-  case SameTypeWitness: {
-    evaluator.applySameTypeWitness(*this, system);
-
-    out << (Inverse ? "SameTypeWitness⁻¹"
-                    : "SameTypeWitness");
-    break;
-  }
   }
 }
 
@@ -382,78 +375,6 @@ RewritePathEvaluator::applyRelation(const RewriteStep &step,
   return {lhs, rhs, prefix, suffix};
 }
 
-void RewritePathEvaluator::applySameTypeWitness(const RewriteStep &step,
-                                                const RewriteSystem &system) {
-  checkPrimary();
-  auto &term = Primary.back();
-
-  const auto &witness = system.getTypeWitness(step.Arg);
-  auto fail = [&]() {
-    llvm::errs() << "Bad same-type witness term:\n";
-    llvm::errs() << term << "\n\n";
-    witness.dump(llvm::errs());
-    abort();
-  };
-
-  auto concreteConformanceSymbol = witness.getConcreteConformance();
-
-#ifndef NDEBUG
-  if (witness.getConcreteType().getConcreteType() !=
-      concreteConformanceSymbol.getConcreteType()) {
-    fail();
-  }
-#endif
-
-  auto witnessConcreteType = Symbol::forConcreteType(
-      concreteConformanceSymbol.getConcreteType(),
-      concreteConformanceSymbol.getSubstitutions(),
-      system.getRewriteContext());
-
-  if (!step.Inverse) {
-    // Make sure the term takes the following form, where |V| == EndOffset:
-    //
-    //    U.[concrete: C : P].[P:X].[concrete: C].V
-    if (term.size() <= step.EndOffset + 3 ||
-        *(term.end() - step.EndOffset - 3) != concreteConformanceSymbol ||
-        *(term.end() - step.EndOffset - 2) != witness.getAssocType() ||
-        *(term.end() - step.EndOffset - 1) != witnessConcreteType) {
-      fail();
-    }
-
-    // Get the subterm U.[concrete: C : P].
-    MutableTerm newTerm(term.begin(), term.end() - step.EndOffset - 2);
-
-    // 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) != concreteConformanceSymbol) {
-      fail();
-    }
-
-    // Get the subterm U.[concrete: C : P].
-    MutableTerm newTerm(term.begin(), term.end() - step.EndOffset);
-
-    // Add the symbol [P:X].
-    newTerm.add(witness.getAssocType());
-
-    // Add the symbol [concrete: C].
-    newTerm.add(witnessConcreteType);
-
-    // Add the subterm V, to get
-    //
-    //    U.[concrete: C : P].[P:X].[concrete: C].V
-    newTerm.append(term.end() - step.EndOffset, term.end());
-
-    term = newTerm;
-  }
-}
-
 void RewritePathEvaluator::apply(const RewriteStep &step,
                                  const RewriteSystem &system) {
   switch (step.Kind) {
@@ -476,9 +397,5 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
   case RewriteStep::Relation:
     applyRelation(step, system);
     break;
-
-  case RewriteStep::SameTypeWitness:
-    applySameTypeWitness(step, system);
-    break;
   }
 }

lib/AST/RequirementMachine/RewriteLoop.h

@@ -98,16 +98,7 @@ struct RewriteStep {
     ///
     /// The Arg field stores the result of calling
     /// RewriteSystem::recordRelation().
-    Relation,
-
-    /// 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]. The associated type symbol is eliminated.
-    ///
-    /// If inverted: the associated type symbol [P:X] is introduced.
-    ///
-    /// The Arg field stores the result of RewriteSystem::recordTypeWitness().
-    SameTypeWitness,
+    Relation
   };
 
   /// The rewrite step kind.
@@ -173,11 +164,6 @@ struct RewriteStep {
                        /*arg=*/relationID, inverse);
   }
 
-  static RewriteStep forSameTypeWitness(unsigned witnessID, bool inverse) {
-    return RewriteStep(SameTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
-                       /*arg=*/witnessID, inverse);
-  }
-
   bool isInContext() const {
     return StartOffset > 0 || EndOffset > 0;
   }
@@ -370,9 +356,6 @@ struct RewritePathEvaluator {
   void applyConcreteConformance(const RewriteStep &step,
                                 const RewriteSystem &system);
 
-  void applySameTypeWitness(const RewriteStep &step,
-                            const RewriteSystem &system);
-
   void dump(llvm::raw_ostream &out) const;
 };
 

lib/AST/RequirementMachine/RewriteSystem.h

@@ -356,6 +356,10 @@ class RewriteSystem final {
       Symbol associatedTypeSymbol,
       Symbol typeWitnessSymbol);
 
+  unsigned recordSameTypeWitnessRelation(
+      Symbol concreteConformanceSymbol,
+      Symbol associatedTypeSymbol);
+
   /// A type witness has a subject type, stored in LHS, which takes the form:
   ///
   /// T.[concrete: C : P].[P:X]