RequirementMachine: Introduce RewriteStep::AbstractTypeWitness

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -101,6 +101,7 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
+    case RewriteStep::AbstractTypeWitness:
       break;
     }
 
@@ -223,6 +224,7 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
+    case RewriteStep::AbstractTypeWitness:
       break;
     }
 
@@ -323,6 +325,7 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
     case RewriteStep::SameTypeWitness:
+    case RewriteStep::AbstractTypeWitness:
       newSteps.push_back(step);
       break;
     }

lib/AST/RequirementMachine/MinimalConformances.cpp

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

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -92,6 +92,13 @@ void RewriteStep::dump(llvm::raw_ostream &out,
                     : "SameTypeWitness");
     break;
   }
+  case AbstractTypeWitness: {
+    evaluator.applyAbstractTypeWitness(*this, system);
+
+    out << (Inverse ? "AbstractTypeWitness⁻¹"
+                    : "AbstractTypeWitness");
+    break;
+  }
 
   }
 }
@@ -561,6 +568,42 @@ void RewritePathEvaluator::applySameTypeWitness(const RewriteStep &step,
   }
 }
 
+void
+RewritePathEvaluator::applyAbstractTypeWitness(const RewriteStep &step,
+                                               const RewriteSystem &system) {
+  checkA();
+  auto &term = A.back();
+
+  const auto &witness = system.getTypeWitness(step.RuleID);
+  auto fail = [&]() {
+    llvm::errs() << "Bad abstract type witness term:\n";
+    llvm::errs() << term << "\n\n";
+    witness.dump(llvm::errs());
+    abort();
+  };
+
+  auto typeWitness = witness.getAbstractType();
+
+  Term origTerm = (step.Inverse ? witness.LHS : typeWitness);
+  Term substTerm = (step.Inverse ? typeWitness : witness.LHS);
+
+  if (term.size() != step.StartOffset + origTerm.size() + step.EndOffset) {
+    fail();
+  }
+
+  if (!std::equal(origTerm.begin(),
+                  origTerm.end(),
+                  term.begin() + step.StartOffset)) {
+    fail();
+  }
+
+  MutableTerm newTerm(term.begin(), term.begin() + step.StartOffset);
+  newTerm.append(substTerm);
+  newTerm.append(term.end() - step.EndOffset, term.end());
+
+  term = newTerm;
+}
+
 void RewritePathEvaluator::apply(const RewriteStep &step,
                                  const RewriteSystem &system) {
   switch (step.Kind) {
@@ -592,5 +635,9 @@ void RewritePathEvaluator::apply(const RewriteStep &step,
   case RewriteStep::SameTypeWitness:
     applySameTypeWitness(step, system);
     break;
+
+  case RewriteStep::AbstractTypeWitness:
+    applyAbstractTypeWitness(step, system);
+    break;
   }
 }

lib/AST/RequirementMachine/RewriteLoop.h

@@ -132,30 +132,39 @@ struct RewriteStep {
     /// The RuleID field is a TypeWitness ID as above.
     /// the step.
     SameTypeWitness,
+
+    /// If not inverted: replaces the abstract type witness term with the
+    /// subject type term.
+    ///
+    /// If inverted: replaces the subject type term with the abstract type
+    /// term.
+    ///
+    /// The RuleID field is a TypeWitness ID as above.
+    AbstractTypeWitness,
   };
 
   /// The rewrite step kind.
-  StepKind Kind : 3;
+  StepKind Kind : 4;
+
+  /// If false, the step replaces an occurrence of the rule's left hand side
+  /// with the right hand side. If true, vice versa.
+  unsigned Inverse : 1;
 
   /// The size of the left whisker, which is the position within the term where
   /// the rule is being applied. In A.(X => Y).B, this is |A|=1.
-  unsigned StartOffset : 14;
+  unsigned StartOffset : 16;
 
   /// The size of the right whisker, which is the length of the remaining suffix
   /// after the rule is applied. In A.(X => Y).B, this is |B|=1.
-  unsigned EndOffset : 14;
+  unsigned EndOffset : 16;
 
   /// If Kind is ApplyRewriteRule, the index of the rule in the rewrite system.
   ///
   /// If Kind is AdjustConcreteType, the length of the prefix to add or remove
   /// at the beginning of each concrete substitution.
   ///
   /// If Kind is Concrete, the number of substitutions to push or pop.
-  unsigned RuleID : 15;
-
-  /// If false, the step replaces an occurrence of the rule's left hand side
-  /// with the right hand side. If true, vice versa.
-  unsigned Inverse : 1;
+  unsigned RuleID : 16;
 
   RewriteStep(StepKind kind, unsigned startOffset, unsigned endOffset,
               unsigned ruleID, bool inverse) {
@@ -211,6 +220,11 @@ struct RewriteStep {
                        /*ruleID=*/witnessID, inverse);
   }
 
+  static RewriteStep forAbstractTypeWitness(unsigned witnessID, bool inverse) {
+    return RewriteStep(AbstractTypeWitness, /*startOffset=*/0, /*endOffset=*/0,
+                       /*ruleID=*/witnessID, inverse);
+  }
+
   bool isInContext() const {
     return StartOffset > 0 || EndOffset > 0;
   }
@@ -400,6 +414,9 @@ struct RewritePathEvaluator {
   void applySameTypeWitness(const RewriteStep &step,
                             const RewriteSystem &system);
 
+  void applyAbstractTypeWitness(const RewriteStep &step,
+                                const RewriteSystem &system);
+
   void dump(llvm::raw_ostream &out) const;
 };