RequirementMachine: Stub out logic for property map to record rewrite loops

For homotopy reduction to properly deal with new rules introduced
while bulding the property map, rewrite loops must be recorded
relating these to existing rules.

Author: slavapestov

lib/AST/RequirementMachine/PropertyMap.cpp

@@ -311,7 +311,7 @@ void PropertyMap::clear() {
 /// key. Must be called in monotonically non-decreasing key order.
 void PropertyMap::addProperty(
     Term key, Symbol property, unsigned ruleID,
-    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules) {
+    SmallVectorImpl<InducedRule> &inducedRules) {
   assert(property.isProperty());
   assert(*System.getRule(ruleID).isPropertyRule() == property);
   auto *props = getOrCreateProperties(key);
@@ -371,7 +371,7 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
 
   // Merging multiple superclass or concrete type rules can induce new rules
   // to unify concrete type constructor arguments.
-  SmallVector<std::pair<MutableTerm, MutableTerm>, 3> inducedRules;
+  SmallVector<InducedRule, 3> inducedRules;
 
   for (const auto &bucket : properties) {
     for (auto property : bucket) {
@@ -392,7 +392,9 @@ PropertyMap::buildPropertyMap(unsigned maxIterations,
   // where the left hand side is not already equivalent to the right hand side.
   unsigned addedNewRules = 0;
   for (auto pair : inducedRules) {
-    if (System.addRule(pair.first, pair.second)) {
+    // 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();

lib/AST/RequirementMachine/PropertyMap.h

@@ -43,6 +43,21 @@ 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 {
@@ -88,7 +103,7 @@ class PropertyBag {
   void addProperty(Symbol property,
                    unsigned ruleID,
                    RewriteContext &ctx,
-                   SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules,
+                   SmallVectorImpl<InducedRule> &inducedRules,
                    bool debug);
   void copyPropertiesFrom(const PropertyBag *next,
                           RewriteContext &ctx);
@@ -186,18 +201,18 @@ class PropertyMap {
 private:
   void clear();
   void addProperty(Term key, Symbol property, unsigned ruleID,
-                   SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules);
+                   SmallVectorImpl<InducedRule> &inducedRules);
 
   void computeConcreteTypeInDomainMap();
   void concretizeNestedTypesFromConcreteParents(
-                   SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules) const;
+                   SmallVectorImpl<InducedRule> &inducedRules) const;
 
   void concretizeNestedTypesFromConcreteParent(
                    Term key, RequirementKind requirementKind,
                    CanType concreteType, ArrayRef<Term> substitutions,
                    ArrayRef<const ProtocolDecl *> conformsTo,
                    llvm::TinyPtrVector<ProtocolConformance *> &conformances,
-                   SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules) const;
+                   SmallVectorImpl<InducedRule> &inducedRules) const;
 
   MutableTerm computeConstraintTermForTypeWitness(
       Term key, CanType concreteType, CanType typeWitness,

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -90,15 +90,14 @@ namespace {
     ArrayRef<Term> lhsSubstitutions;
     ArrayRef<Term> rhsSubstitutions;
     RewriteContext &ctx;
-    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules;
+    SmallVectorImpl<InducedRule> &inducedRules;
     bool debug;
 
   public:
     ConcreteTypeMatcher(ArrayRef<Term> lhsSubstitutions,
                         ArrayRef<Term> rhsSubstitutions,
                         RewriteContext &ctx,
-                        SmallVectorImpl<std::pair<MutableTerm,
-                                                  MutableTerm>> &inducedRules,
+                        SmallVectorImpl<InducedRule> &inducedRules,
                         bool debug)
         : lhsSubstitutions(lhsSubstitutions),
           rhsSubstitutions(rhsSubstitutions),
@@ -205,7 +204,7 @@ namespace {
 /// Returns true if a conflict was detected.
 static bool unifyConcreteTypes(
     Symbol lhs, Symbol rhs, RewriteContext &ctx,
-    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules,
+    SmallVectorImpl<InducedRule> &inducedRules,
     bool debug) {
   auto lhsType = lhs.getConcreteType();
   auto rhsType = rhs.getConcreteType();
@@ -253,7 +252,7 @@ static bool unifyConcreteTypes(
 /// that gets recorded in the property map.
 static Symbol unifySuperclasses(
     Symbol lhs, Symbol rhs, RewriteContext &ctx,
-    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules,
+    SmallVectorImpl<InducedRule> &inducedRules,
     bool debug) {
   if (debug) {
     llvm::dbgs() << "% Unifying " << lhs << " with " << rhs << "\n";
@@ -310,7 +309,7 @@ static Symbol unifySuperclasses(
 
 void PropertyBag::addProperty(
     Symbol property, unsigned ruleID, RewriteContext &ctx,
-    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules,
+    SmallVectorImpl<InducedRule> &inducedRules,
     bool debug) {
 
   switch (property.getKind()) {
@@ -395,7 +394,7 @@ void PropertyMap::computeConcreteTypeInDomainMap() {
 }
 
 void PropertyMap::concretizeNestedTypesFromConcreteParents(
-    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules) const {
+    SmallVectorImpl<InducedRule> &inducedRules) const {
   for (const auto &props : Entries) {
     if (props->getConformsTo().empty())
       continue;
@@ -478,7 +477,7 @@ void PropertyMap::concretizeNestedTypesFromConcreteParent(
     CanType concreteType, ArrayRef<Term> substitutions,
     ArrayRef<const ProtocolDecl *> conformsTo,
     llvm::TinyPtrVector<ProtocolConformance *> &conformances,
-    SmallVectorImpl<std::pair<MutableTerm, MutableTerm>> &inducedRules) const {
+    SmallVectorImpl<InducedRule> &inducedRules) const {
   assert(requirementKind == RequirementKind::SameType ||
          requirementKind == RequirementKind::Superclass);