RequirementMachine: Minimization understands 'relations' among layout requirements

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -88,15 +88,16 @@ RewriteLoop::findRulesAppearingOnceInEmptyContext(
     switch (step.Kind) {
     case RewriteStep::ApplyRewriteRule: {
       if (!step.isInContext() && !evaluator.isInContext())
-        rulesInEmptyContext.insert(step.RuleID);
+        rulesInEmptyContext.insert(step.getRuleID());
 
-      ++ruleMultiplicity[step.RuleID];
+      ++ruleMultiplicity[step.getRuleID()];
       break;
     }
 
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::Relation:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
@@ -207,7 +208,7 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
   for (auto step : Steps) {
     switch (step.Kind) {
     case RewriteStep::ApplyRewriteRule: {
-      if (step.RuleID != ruleID)
+      if (step.getRuleID() != ruleID)
         break;
 
       assert(!sawRule && "Rule appears more than once?");
@@ -220,6 +221,7 @@ RewritePath RewritePath::splitCycleAtRule(unsigned ruleID) const {
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::Relation:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:
@@ -262,7 +264,7 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
 
   for (const auto &step : Steps) {
     if (step.Kind == RewriteStep::ApplyRewriteRule &&
-        step.RuleID == ruleID) {
+        step.getRuleID() == ruleID) {
       foundAny = true;
       break;
     }
@@ -282,7 +284,7 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
   for (const auto &step : Steps) {
     switch (step.Kind) {
     case RewriteStep::ApplyRewriteRule: {
-      if (step.RuleID != ruleID) {
+      if (step.getRuleID() != ruleID) {
         newSteps.push_back(step);
         break;
       }
@@ -321,6 +323,7 @@ bool RewritePath::replaceRuleWithPath(unsigned ruleID,
     case RewriteStep::AdjustConcreteType:
     case RewriteStep::Shift:
     case RewriteStep::Decompose:
+    case RewriteStep::Relation:
     case RewriteStep::ConcreteConformance:
     case RewriteStep::SuperclassConformance:
     case RewriteStep::ConcreteTypeWitness:

lib/AST/RequirementMachine/MinimalConformances.cpp

@@ -113,7 +113,7 @@ void RewriteLoop::findProtocolConformanceRules(
     if (!evaluator.isInContext()) {
       switch (step.Kind) {
       case RewriteStep::ApplyRewriteRule: {
-        const auto &rule = system.getRule(step.RuleID);
+        const auto &rule = system.getRule(step.getRuleID());
 
         if (rule.isIdentityConformanceRule())
           break;
@@ -127,7 +127,7 @@ void RewriteLoop::findProtocolConformanceRules(
             // the prefix term is 'X'.
             const auto &term = evaluator.getCurrentTerm();
             MutableTerm prefix(term.begin(), term.begin() + step.StartOffset);
-            result[proto].RulesInContext.emplace_back(prefix, step.RuleID);
+            result[proto].RulesInContext.emplace_back(prefix, step.getRuleID());
           }
         }
 
@@ -137,6 +137,7 @@ void RewriteLoop::findProtocolConformanceRules(
       case RewriteStep::AdjustConcreteType:
       case RewriteStep::Shift:
       case RewriteStep::Decompose:
+      case RewriteStep::Relation:
       case RewriteStep::ConcreteConformance:
       case RewriteStep::SuperclassConformance:
       case RewriteStep::ConcreteTypeWitness:
@@ -262,7 +263,7 @@ MinimalConformances::decomposeTermIntoConformanceRuleLeftHandSides(
   const auto &step = *steps.begin();
 
 #ifndef NDEBUG
-  const auto &rule = System.getRule(step.RuleID);
+  const auto &rule = System.getRule(step.getRuleID());
   assert(rule.isAnyConformanceRule());
   assert(!rule.isIdentityConformanceRule());
 #endif
@@ -277,9 +278,10 @@ MinimalConformances::decomposeTermIntoConformanceRuleLeftHandSides(
     // Build the term U.
     MutableTerm prefix(term.begin(), term.begin() + step.StartOffset);
 
-    decomposeTermIntoConformanceRuleLeftHandSides(prefix, step.RuleID, result);
+    decomposeTermIntoConformanceRuleLeftHandSides(
+        prefix, step.getRuleID(), result);
   } else {
-    result.push_back(step.RuleID);
+    result.push_back(step.getRuleID());
   }
 }
 

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -319,7 +319,7 @@ Optional<unsigned> PropertyMap::addProperty(
   assert(*System.getRule(ruleID).isPropertyRule() == property);
   auto *props = getOrCreateProperties(key);
   bool debug = Debug.contains(DebugFlags::ConcreteUnification);
-  return props->addProperty(property, ruleID, Context,
+  return props->addProperty(property, ruleID, System,
                             inducedRules, debug);
 }
 

lib/AST/RequirementMachine/PropertyMap.h

@@ -103,7 +103,7 @@ class PropertyBag {
 
   Optional<unsigned> addProperty(Symbol property,
                                  unsigned ruleID,
-                                 RewriteContext &ctx,
+                                 RewriteSystem &system,
                                  SmallVectorImpl<InducedRule> &inducedRules,
                                  bool debug);
   void copyPropertiesFrom(const PropertyBag *next,

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -37,6 +37,82 @@
 using namespace swift;
 using namespace rewriting;
 
+unsigned RewriteSystem::recordRelation(Symbol lhs, Symbol rhs) {
+  auto key = std::make_pair(lhs, rhs);
+  auto found = RelationMap.find(key);
+  if (found != RelationMap.end())
+    return found->second;
+
+  unsigned index = Relations.size();
+  Relations.push_back(key);
+  auto inserted = RelationMap.insert(std::make_pair(key, index));
+  assert(inserted.second);
+  (void) inserted;
+
+  return index;
+}
+
+RewriteSystem::Relation
+RewriteSystem::getRelation(unsigned index) const {
+  return Relations[index];
+}
+
+/// Given two property rules (T.[p1] => T) and (T.[p2] => T) where [p1] < [p2],
+/// record a rewrite loop that makes the second rule redundant from the first.
+static void recordRelation(unsigned lhsRuleID, unsigned rhsRuleID,
+                           RewriteSystem &system,
+                           SmallVectorImpl<InducedRule> &inducedRules,
+                           bool debug) {
+  const auto &lhsRule = system.getRule(lhsRuleID);
+  const auto &rhsRule = system.getRule(rhsRuleID);
+
+  auto lhsProperty = lhsRule.getLHS().back();
+  auto rhsProperty = rhsRule.getLHS().back();
+
+  assert(lhsProperty.isProperty());
+  assert(rhsProperty.isProperty());
+  assert(lhsProperty.getKind() == rhsProperty.getKind());
+
+  if (debug) {
+    llvm::dbgs() << "%% Recording relation: ";
+    llvm::dbgs() << lhsRule.getLHS() << " < " << rhsProperty << "\n";
+  }
+
+  unsigned relationID = system.recordRelation(lhsProperty, rhsProperty);
+
+  /// Build the following rewrite path:
+  ///
+  ///   (T => T.[p1]).[p2] ⊗ T.Relation([p1].[p2] => [p1]) ⊗ (T.[p1] => T).
+  ///
+  RewritePath path;
+
+  /// Starting from T.[p2], the LHS rule in reverse to get T.[p1].[p2].
+  path.add(RewriteStep::forRewriteRule(/*startOffset=*/0,
+                                       /*endOffset=*/1,
+                                       /*ruleID=*/lhsRuleID,
+                                       /*inverse=*/true));
+
+  /// T.Relation([p1].[p2] => [p1]).
+  path.add(RewriteStep::forRelation(relationID, /*inverse=*/false));
+
+  /// (T.[p1] => T).
+  path.add(RewriteStep::forRewriteRule(/*startOffset=*/0,
+                                       /*endOffset=*/0,
+                                       /*ruleID=*/lhsRuleID,
+                                       /*inverse=*/false));
+
+  /// Add the rule (T.[p2] => T) with the above rewrite path.
+  ///
+  /// Since a rule (T.[p2] => T) *already exists*, both sides of the new
+  /// rule will simplify down to T, and the rewrite path will become a loop.
+  ///
+  /// This loop encodes the fact that (T.[p1] => T) makes (T.[p2] => T)
+  /// redundant.
+  inducedRules.emplace_back(MutableTerm(rhsRule.getLHS()),
+                            MutableTerm(rhsRule.getRHS()),
+                            path);
+}
+
 /// This method takes a concrete type that was derived from a concrete type
 /// produced by RewriteSystemBuilder::getConcreteSubstitutionSchema(),
 /// either by extracting a structural sub-component or performing a (Swift AST)
@@ -310,7 +386,7 @@ static std::pair<Symbol, bool> unifySuperclasses(
 /// Returns the old conflicting rule ID if there was a conflict,
 /// otherwise returns None.
 Optional<unsigned> PropertyBag::addProperty(
-    Symbol property, unsigned ruleID, RewriteContext &ctx,
+    Symbol property, unsigned ruleID, RewriteSystem &system,
     SmallVectorImpl<InducedRule> &inducedRules,
     bool debug) {
 
@@ -320,18 +396,41 @@ Optional<unsigned> PropertyBag::addProperty(
     ConformsToRules.push_back(ruleID);
     return None;
 
-  case Symbol::Kind::Layout:
+  case Symbol::Kind::Layout: {
+    auto newLayout = property.getLayoutConstraint();
+
     if (!Layout) {
-      Layout = property.getLayoutConstraint();
+      // If we haven't seen a layout requirement before, just record it.
+      Layout = newLayout;
       LayoutRule = ruleID;
     } else {
+      // Otherwise, compute the intersection.
       assert(LayoutRule.hasValue());
-      Layout = Layout.merge(property.getLayoutConstraint());
-      if (!Layout->isKnownLayout())
+      auto mergedLayout = Layout.merge(property.getLayoutConstraint());
+
+      // If the intersection is invalid, we have a conflict.
+      if (!mergedLayout->isKnownLayout())
         return LayoutRule;
+
+      // If the intersection is equal to the existing layout requirement,
+      // the new layout requirement is redundant.
+      if (mergedLayout == Layout) {
+        recordRelation(*LayoutRule, ruleID, system, inducedRules, debug);
+
+      // If the intersection is equal to the new layout requirement, the
+      // existing layout requirement is redundant.
+      } else if (mergedLayout == newLayout) {
+        recordRelation(ruleID, *LayoutRule, system, inducedRules, debug);
+        LayoutRule = ruleID;
+      } else {
+        llvm::errs() << "Arbitrary intersection of layout requirements is "
+                     << "supported yet\n";
+        abort();
+      }
     }
 
     return None;
+  }
 
   case Symbol::Kind::Superclass: {
     // FIXME: Also handle superclass vs concrete
@@ -342,7 +441,8 @@ Optional<unsigned> PropertyBag::addProperty(
     } else {
       assert(SuperclassRule.hasValue());
       auto pair = unifySuperclasses(*Superclass, property,
-                                    ctx, inducedRules, debug);
+                                    system.getRewriteContext(),
+                                    inducedRules, debug);
       Superclass = pair.first;
       bool conflict = pair.second;
       if (conflict)
@@ -359,7 +459,8 @@ Optional<unsigned> PropertyBag::addProperty(
     } else {
       assert(ConcreteTypeRule.hasValue());
       bool conflict = unifyConcreteTypes(*ConcreteType, property,
-                                         ctx, inducedRules, debug);
+                                         system.getRewriteContext(),
+                                         inducedRules, debug);
       if (conflict)
         return ConcreteTypeRule;
     }