Merge pull request #40973 from slavapestov/rqm-conditional-requirement-inference

RequirementMachine: Conditional requirement inference

Author: slavapestov

lib/AST/RequirementMachine/Debug.h

@@ -38,17 +38,21 @@ enum class DebugFlags : unsigned {
   /// Print debug output when concretizing nested types in the property map.
   ConcretizeNestedTypes = (1<<5),
 
+  /// Print debug output when inferring conditional requirements in the
+  /// property map.
+  ConditionalRequirements = (1<<6),
+
   /// Print debug output from the homotopy reduction algorithm.
-  HomotopyReduction = (1<<6),
+  HomotopyReduction = (1<<7),
 
   /// Print debug output from the minimal conformances algorithm.
-  MinimalConformances = (1<<7),
+  MinimalConformances = (1<<8),
 
   /// Print debug output from the protocol dependency graph.
-  ProtocolDependencies = (1<<8),
+  ProtocolDependencies = (1<<9),
 
   /// Print debug output from generic signature minimization.
-  Minimization = (1<<9),
+  Minimization = (1<<10),
 };
 
 using DebugOptions = OptionSet<DebugFlags>;

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -386,9 +386,13 @@ findRuleToDelete(llvm::function_ref<bool(unsigned)> isRedundantRuleFn,
 
     const auto &otherRule = getRule(found->second);
 
-    // Prefer to delete "less canonical" rules.
-    if (rule.compare(otherRule, Context) > 0)
+    // If the new rule is conflicting, don't compare the rules at all
+    // and prefer to delete the new rule. Otherwise, prefer to delete
+    // the less canonical of the two rules.
+    if (rule.isConflicting() ||
+        rule.compare(otherRule, Context) > 0) {
       found = pair;
+    }
   }
 
   if (!found)

lib/AST/RequirementMachine/InterfaceType.cpp

@@ -493,3 +493,77 @@ Type PropertyMap::getTypeFromSubstitutionSchema(
     return None;
   });
 }
+
+/// This method takes a concrete type that was derived from a concrete type
+/// produced by RewriteContext::getSubstitutionSchemaFromType() either by
+/// extracting a structural sub-component or performing a (Swift AST)
+/// substitution using subst(). It returns a new concrete substitution schema
+/// and a new list of substitution terms.
+///
+/// For example, suppose we start with the concrete type
+///
+///   Dictionary<τ_0_0, Array<τ_0_1>> with substitutions {X.Y, Z}
+///
+/// We can extract out the structural sub-component Array<τ_0_1>. If we wish
+/// to build a new concrete substitution schema, we call this method with
+/// Array<τ_0_1> and the original substitutions {X.Y, Z}. This will produce
+/// the new schema Array<τ_0_0> with substitutions {Z}.
+///
+/// As another example, consider we start with the schema Bar<τ_0_0> with
+/// original substitutions {X.Y}, and perform a Swift AST subst() to get
+/// Foo<τ_0_0.A.B>. We can then call this method with Foo<τ_0_0.A.B> and
+/// the original substitutions {X.Y} to produce the new schema Foo<τ_0_0>
+/// with substitutions {X.Y.A.B}.
+CanType
+RewriteContext::getRelativeSubstitutionSchemaFromType(
+    CanType concreteType,
+    ArrayRef<Term> substitutions,
+    SmallVectorImpl<Term> &result) {
+  assert(!concreteType->isTypeParameter() && "Must have a concrete type here");
+
+  if (!concreteType->hasTypeParameter())
+    return concreteType;
+
+  return CanType(concreteType.transformRec([&](Type t) -> Optional<Type> {
+    if (!t->isTypeParameter())
+      return None;
+
+    auto term = getRelativeTermForType(CanType(t), substitutions);
+
+    unsigned newIndex = result.size();
+    result.push_back(Term::get(term, *this));
+
+    return CanGenericTypeParamType::get(/*type sequence=*/ false,
+                                        /*depth=*/ 0, newIndex,
+                                        Context);
+  }));
+}
+
+/// Given a concrete type that may contain type parameters in structural positions,
+/// collect all the structural type parameter components, and replace them all with
+/// fresh generic parameters. The fresh generic parameters all have a depth of 0,
+/// and the index is an index into the 'result' array.
+///
+/// For example, given the concrete type Foo<X.Y, Array<Z>>, this produces the
+/// result type Foo<τ_0_0, Array<τ_0_1>>, with result array {X.Y, Z}.
+CanType
+RewriteContext::getSubstitutionSchemaFromType(CanType concreteType,
+                                              const ProtocolDecl *proto,
+                                              SmallVectorImpl<Term> &result) {
+  assert(!concreteType->isTypeParameter() && "Must have a concrete type here");
+
+  if (!concreteType->hasTypeParameter())
+    return concreteType;
+
+  return CanType(concreteType.transformRec([&](Type t) -> Optional<Type> {
+    if (!t->isTypeParameter())
+      return None;
+
+    unsigned index = result.size();
+    result.push_back(getTermForType(CanType(t), proto));
+
+    return CanGenericTypeParamType::get(/*type sequence=*/ false,
+                                        /*depth=*/0, index,
+                                        Context);
+  }));
+}

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -371,36 +371,28 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
 
   // Merging multiple superclass or concrete type rules can induce new rules
   // to unify concrete type constructor arguments.
-  SmallVector<InducedRule, 3> inducedRules;
+  unsigned ruleCount = System.getRules().size();
 
   for (const auto &bucket : properties) {
     for (auto property : bucket) {
       addProperty(property.key, property.symbol,
-                  property.ruleID, inducedRules);
+                  property.ruleID);
     }
   }
 
   // Now, check for conflicts between superclass and concrete type rules.
-  checkConcreteTypeRequirements(inducedRules);
+  checkConcreteTypeRequirements();
 
   // Now, we merge concrete type rules with conformance rules, by adding
   // relations between associated type members of type parameters with
   // the concrete type witnesses in the concrete type's conformance.
-  concretizeNestedTypesFromConcreteParents(inducedRules);
-
-  // Some of the induced rules might be trivial; only count the induced rules
-  // where the left hand side is not already equivalent to the right hand side.
-  unsigned addedNewRules = 0;
-  for (auto pair : inducedRules) {
-    // FIXME: Eventually, all induced rules will have a rewrite path.
-    if (System.addRule(pair.LHS, pair.RHS,
-                       pair.Path.empty() ? nullptr : &pair.Path)) {
-      ++addedNewRules;
-
-      const auto &newRule = System.getRules().back();
-      if (newRule.getDepth() > maxDepth)
-        return std::make_pair(CompletionResult::MaxDepth, addedNewRules);
-    }
+  concretizeNestedTypesFromConcreteParents();
+
+  unsigned addedNewRules = System.getRules().size() - ruleCount;
+  for (unsigned i = ruleCount, e = System.getRules().size(); i < e; ++i) {
+    const auto &newRule = System.getRule(i);
+    if (newRule.getDepth() > maxDepth)
+      return std::make_pair(CompletionResult::MaxDepth, addedNewRules);
   }
 
   // Check invariants of the constructed property map.

lib/AST/RequirementMachine/PropertyMap.h

@@ -44,21 +44,6 @@ namespace rewriting {
 class MutableTerm;
 class Term;
 
-/// A new rule introduced during property map construction, as a result of
-/// unifying two property symbols that apply to the same common suffix term.
-struct InducedRule {
-  MutableTerm LHS;
-  MutableTerm RHS;
-  RewritePath Path;
-
-  InducedRule(MutableTerm LHS, MutableTerm RHS, RewritePath Path)
-    : LHS(LHS), RHS(RHS), Path(Path) {}
-
-  // FIXME: Eventually all induced rules will have a rewrite path.
-  InducedRule(MutableTerm LHS, MutableTerm RHS)
-    : LHS(LHS), RHS(RHS) {}
-};
-
 /// Stores a convenient representation of all "property-like" rewrite rules of
 /// the form T.[p] => T, where [p] is a property symbol, for some term 'T'.
 class PropertyBag {
@@ -258,14 +243,11 @@ class PropertyMap {
   bool checkRuleOnce(unsigned ruleID);
   bool checkRulePairOnce(unsigned firstRuleID, unsigned secondRuleID);
 
-  void addProperty(Term key, Symbol property, unsigned ruleID,
-                   SmallVectorImpl<InducedRule> &inducedRules);
+  void addProperty(Term key, Symbol property, unsigned ruleID);
 
-  void checkConcreteTypeRequirements(
-                   SmallVectorImpl<InducedRule> &inducedRules);
+  void checkConcreteTypeRequirements();
 
-  void concretizeNestedTypesFromConcreteParents(
-                   SmallVectorImpl<InducedRule> &inducedRules);
+  void concretizeNestedTypesFromConcreteParents();
 
   void concretizeNestedTypesFromConcreteParent(
                    Term key, RequirementKind requirementKind,
@@ -274,15 +256,17 @@ class PropertyMap {
                    ArrayRef<Term> substitutions,
                    ArrayRef<unsigned> conformsToRules,
                    ArrayRef<const ProtocolDecl *> conformsTo,
-                   llvm::TinyPtrVector<ProtocolConformance *> &conformances,
-                   SmallVectorImpl<InducedRule> &inducedRules);
+                   llvm::TinyPtrVector<ProtocolConformance *> &conformances);
 
   void concretizeTypeWitnessInConformance(
                    Term key, RequirementKind requirementKind,
                    Symbol concreteConformanceSymbol,
                    ProtocolConformance *concrete,
-                   AssociatedTypeDecl *assocType,
-                   SmallVectorImpl<InducedRule> &inducedRules) const;
+                   AssociatedTypeDecl *assocType) const;
+
+  void inferConditionalRequirements(
+                   ProtocolConformance *concrete,
+                   ArrayRef<Term> substitutions) const;
 
   MutableTerm computeConstraintTermForTypeWitness(
       Term key, RequirementKind requirementKind,
@@ -295,8 +279,7 @@ class PropertyMap {
     unsigned concreteRuleID,
     unsigned conformanceRuleID,
     RequirementKind requirementKind,
-    Symbol concreteConformanceSymbol,
-    SmallVectorImpl<InducedRule> &inducedRules) const;
+    Symbol concreteConformanceSymbol) const;
 
   void verify() const;
 };
@@ -305,4 +288,4 @@ class PropertyMap {
 
 } // end namespace swift
 
-#endif
+#endif