RequirementMachine: Replace RewriteStep::ConcreteTypeWitness with relations

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -98,7 +98,6 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
       break;
     }
@@ -219,7 +218,6 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
       break;
     }
@@ -318,7 +316,6 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
     case RewriteStep::Relation:
-    case RewriteStep::ConcreteTypeWitness:
     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::ConcreteTypeWitness:
       case RewriteStep::SameTypeWitness:
         break;
       }

lib/AST/RequirementMachine/PropertyRelations.cpp

@@ -90,6 +90,34 @@ unsigned RewriteSystem::recordConcreteConformanceRelation(
       Term::get(rhsTerm, Context));
 }
 
+/// Record a relation ([concrete: C : P].[P:X].[concrete: C.X] =>
+/// [concrete: C : P].[P:X]) which "concretizes" a nested type C.X of a
+/// type parameter conforming to P known to equal the concrete type C.
+unsigned RewriteSystem::recordConcreteTypeWitnessRelation(
+    Symbol concreteConformanceSymbol,
+    Symbol associatedTypeSymbol,
+    Symbol typeWitnessSymbol) {
+  assert(concreteConformanceSymbol.getKind() ==
+         Symbol::Kind::ConcreteConformance);
+  assert(associatedTypeSymbol.getKind() ==
+         Symbol::Kind::AssociatedType);
+  assert(associatedTypeSymbol.getProtocols().size() == 1);
+  assert(concreteConformanceSymbol.getProtocol() ==
+         associatedTypeSymbol.getProtocols()[0]);
+  assert(typeWitnessSymbol.getKind() == Symbol::Kind::ConcreteType);
+
+  MutableTerm rhsTerm;
+  rhsTerm.add(concreteConformanceSymbol);
+  rhsTerm.add(associatedTypeSymbol);
+
+  MutableTerm lhsTerm(rhsTerm);
+  lhsTerm.add(typeWitnessSymbol);
+
+  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

@@ -898,6 +898,15 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
                                      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(
+      concreteConformanceSymbol,
+      associatedTypeSymbol,
+      typeWitnessSymbol);
+
   // Simplify the substitution terms in the type witness symbol.
   RewritePath substPath;
   System.simplifySubstitutions(typeWitnessSymbol, &substPath);
@@ -914,7 +923,7 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
 
     // Add a rule T.[concrete: C : P] => T.[concrete: C : P].[P:X].
     MutableTerm result(key);
-    result.add(witness.getConcreteConformance());
+    result.add(concreteConformanceSymbol);
 
     // ([concrete: C : P] => [concrete: C : P].[P:X].[concrete: C])
     path.add(RewriteStep::forSameTypeWitness(
@@ -924,8 +933,9 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
     path.append(substPath);
 
     // T.([concrete: C : P].[P:X].[concrete: C.X] => [concrete: C : P].[P:X])
-    path.add(RewriteStep::forConcreteTypeWitness(
-        witnessID, /*inverse=*/false));
+    path.add(RewriteStep::forRelation(
+        /*startOffset=*/key.size(), relationID,
+        /*inverse=*/false));
 
     return result;
   }
@@ -944,8 +954,9 @@ MutableTerm PropertyMap::computeConstraintTermForTypeWitness(
   path.append(substPath);
 
   // T.([concrete: C : P].[P:X].[concrete: C.X] => [concrete: C : P].[P:X])
-  path.add(RewriteStep::forConcreteTypeWitness(
-      witnessID, /*inverse=*/false));
+  path.add(RewriteStep::forRelation(
+      /*startOffset=*/key.size(), relationID,
+      /*inverse=*/false));
 
   return constraintType;
 }

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -79,13 +79,6 @@ void RewriteStep::dump(llvm::raw_ostream &out,
 
     break;
   }
-  case ConcreteTypeWitness: {
-    evaluator.applyConcreteTypeWitness(*this, system);
-
-    out << (Inverse ? "ConcreteTypeWitness⁻¹"
-                    : "ConcreteTypeWitness");
-    break;
-  }
   case SameTypeWitness: {
     evaluator.applySameTypeWitness(*this, system);
 
@@ -389,64 +382,6 @@ RewritePathEvaluator::applyRelation(const RewriteStep &step,
   return {lhs, rhs, prefix, suffix};
 }
 
-void RewritePathEvaluator::applyConcreteTypeWitness(const RewriteStep &step,
-                                                  const RewriteSystem &system) {
-  checkPrimary();
-  auto &term = Primary.back();
-
-  const auto &witness = system.getTypeWitness(step.Arg);
-  auto fail = [&]() {
-    llvm::errs() << "Bad concrete type witness term:\n";
-    llvm::errs() << term << "\n\n";
-    witness.dump(llvm::errs());
-    llvm::errs() << "End offset: " << step.EndOffset << "\n";
-    llvm::errs() << "Inverse: " << step.Inverse << "\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.getConcreteConformance() ||
-        *(term.end() - step.EndOffset - 2) != witness.getAssocType() ||
-        *(term.end() - step.EndOffset - 1) != witness.getConcreteType()) {
-      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.getConcreteConformance() ||
-        *(term.end() - step.EndOffset - 1) != witness.getAssocType()) {
-      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.getConcreteType());
-
-    // 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::applySameTypeWitness(const RewriteStep &step,
                                                 const RewriteSystem &system) {
   checkPrimary();
@@ -542,10 +477,6 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
     applyRelation(step, system);
     break;
 
-  case RewriteStep::ConcreteTypeWitness:
-    applyConcreteTypeWitness(step, system);
-    break;
-
   case RewriteStep::SameTypeWitness:
     applySameTypeWitness(step, system);
     break;

lib/AST/RequirementMachine/RewriteLoop.h

@@ -100,17 +100,6 @@ struct RewriteStep {
     /// 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], 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 Arg field stores the result of RewriteSystem::recordTypeWitness().
-    ConcreteTypeWitness,
-
     /// 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.
@@ -184,11 +173,6 @@ struct RewriteStep {
                        /*arg=*/relationID, inverse);
   }
 
-  static RewriteStep forConcreteTypeWitness(unsigned witnessID, bool inverse) {
-    return RewriteStep(ConcreteTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
-                       /*arg=*/witnessID, inverse);
-  }
-
   static RewriteStep forSameTypeWitness(unsigned witnessID, bool inverse) {
     return RewriteStep(SameTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
                        /*arg=*/witnessID, inverse);
@@ -386,9 +370,6 @@ struct RewritePathEvaluator {
   void applyConcreteConformance(const RewriteStep &step,
                                 const RewriteSystem &system);
 
-  void applyConcreteTypeWitness(const RewriteStep &step,
-                                const RewriteSystem &system);
-
   void applySameTypeWitness(const RewriteStep &step,
                             const RewriteSystem &system);
 

lib/AST/RequirementMachine/RewriteSystem.h

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