RequirementMachine: Generalize relations so they look more like rules

Author: slavapestov

lib/AST/RequirementMachine/PropertyRelations.cpp

@@ -18,7 +18,15 @@
 using namespace swift;
 using namespace rewriting;
 
-unsigned RewriteSystem::recordRelation(Symbol lhs, Symbol rhs) {
+RewriteSystem::Relation
+RewriteSystem::getRelation(unsigned index) const {
+  return Relations[index];
+}
+
+/// Record a relation that transforms the left hand side when it appears
+/// at the end of a term to the right hand side. Returns the relation ID,
+/// which can be passed to RewriteStep::forRelation().
+unsigned RewriteSystem::recordRelation(Term lhs, Term rhs) {
   auto key = std::make_pair(lhs, rhs);
   auto found = RelationMap.find(key);
   if (found != RelationMap.end())
@@ -33,9 +41,28 @@ unsigned RewriteSystem::recordRelation(Symbol lhs, Symbol rhs) {
   return index;
 }
 
-RewriteSystem::Relation
-RewriteSystem::getRelation(unsigned index) const {
-  return Relations[index];
+/// Given a left-hand side symbol [p1] and a right-hand side symbol
+/// [p2], record a relation ([p1].[p2] => [p1]), which denotes that
+/// the property p1 implies the property p2.
+///
+/// An example is a superclass requirement that implies a layout
+/// requirement.
+unsigned RewriteSystem::recordRelation(Symbol lhsProperty,
+                                       Symbol rhsProperty) {
+  assert(lhsProperty.isProperty());
+  assert(rhsProperty.isProperty());
+
+  MutableTerm lhsTerm;
+  lhsTerm.add(lhsProperty);
+  lhsTerm.add(rhsProperty);
+
+  MutableTerm rhsTerm;
+  rhsTerm.add(lhsProperty);
+
+  // Record a relation ([p1].[p2] => [p1]).
+  return recordRelation(
+      Term::get(lhsTerm, Context),
+      Term::get(rhsTerm, Context));
 }
 
 RewriteSystem::TypeWitness::TypeWitness(

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -77,30 +77,31 @@ static void recordRelation(Term key,
 
   unsigned relationID = system.recordRelation(lhsProperty, rhsProperty);
 
-  /// Build the following rewrite path:
-  ///
-  ///   U.(V => V.[p1]).[p2] ⊗ U.V.Relation([p1].[p2] => [p1]) ⊗ U.(V.[p1] => V).
-  ///
+  // Build the following rewrite path:
+  //
+  //   U.(V => V.[p1]).[p2] ⊗ U.V.Relation([p1].[p2] => [p1]) ⊗ U.(V.[p1] => V).
+  //
   RewritePath path;
 
-  /// Starting from U.V.[p2], apply the rule in reverse to get U.V.[p1].[p2].
+  // Starting from U.V.[p2], apply the rule in reverse to get U.V.[p1].[p2].
   path.add(RewriteStep::forRewriteRule(
       /*startOffset=*/key.size() - lhsRule.getRHS().size(),
       /*endOffset=*/1,
       /*ruleID=*/lhsRuleID,
       /*inverse=*/true));
 
-  /// U.V.Relation([p1].[p2] => [p1]).
-  path.add(RewriteStep::forRelation(relationID, /*inverse=*/false));
+  // U.V.Relation([p1].[p2] => [p1]).
+  path.add(RewriteStep::forRelation(/*startOffset=*/key.size(),
+                                    relationID, /*inverse=*/false));
 
-  /// U.(V.[p1] => V).
+  // U.(V.[p1] => V).
   path.add(RewriteStep::forRewriteRule(
       /*startOffset=*/key.size() - lhsRule.getRHS().size(),
       /*endOffset=*/0,
       /*ruleID=*/lhsRuleID,
       /*inverse=*/false));
 
-  /// Add the rule (T.[p2] => T) with the above rewrite path.
+  // Add the rule (T.[p2] => T) with the above rewrite path.
   MutableTerm lhs(key);
   lhs.add(rhsProperty);
 

lib/AST/RequirementMachine/RewriteLoop.cpp

@@ -65,16 +65,18 @@ void RewriteStep::dump(llvm::raw_ostream &out,
     break;
   }
   case Relation: {
-    evaluator.applyRelation(*this, system);
+    auto result = evaluator.applyRelation(*this, system);
 
-    auto relation = system.getRelation(Arg);
-    out << "Relation(";
-    if (Inverse) {
-      out << relation.second << " > " << relation.first;
-    } else {
-      out << relation.first << " < " << relation.second;
+    if (!result.prefix.empty()) {
+      out << result.prefix;
+      out << ".";
+    }
+    out << "(" << result.lhs << " =>> " << result.rhs << ")";
+    if (!result.suffix.empty()) {
+      out << ".";
+      out << result.suffix;
     }
-    out << ")";
+
     break;
   }
   case ConcreteConformance: {
@@ -293,41 +295,6 @@ void RewritePathEvaluator::applyShift(const RewriteStep &step,
   }
 }
 
-void RewritePathEvaluator::applyRelation(const RewriteStep &step,
-                                         const RewriteSystem &system) {
-  assert(step.Kind == RewriteStep::Relation);
-
-  auto relation = system.getRelation(step.Arg);
-  auto &term = getCurrentTerm();
-
-  if (!step.Inverse) {
-    // Given a term T.[p1].[p2].U where |U| == EndOffset, build the
-    // term T.[p1].U.
-
-    auto lhsProperty = *(term.end() - step.EndOffset - 2);
-    auto rhsProperty = *(term.end() - step.EndOffset - 1);
-    assert(lhsProperty == relation.first);
-    assert(rhsProperty == relation.second);
-
-    MutableTerm result(term.begin(), term.end() - step.EndOffset - 1);
-    result.append(term.end() - step.EndOffset, term.end());
-
-    term = result;
-  } else {
-    // Given a term T.[p1].U where |U| == EndOffset, build the
-    // term T.[p1].[p2].U.
-
-    auto lhsProperty = *(term.end() - step.EndOffset - 1);
-    assert(lhsProperty == relation.first);
-
-    MutableTerm result(term.begin(), term.end() - step.EndOffset);
-    result.add(relation.second);
-    result.append(term.end() - step.EndOffset, term.end());
-
-    term = result;
-  }
-}
-
 void RewritePathEvaluator::applyDecompose(const RewriteStep &step,
                                           const RewriteSystem &system) {
   assert(step.Kind == RewriteStep::Decompose);
@@ -404,6 +371,46 @@ void RewritePathEvaluator::applyDecompose(const RewriteStep &step,
   }
 }
 
+AppliedRewriteStep
+RewritePathEvaluator::applyRelation(const RewriteStep &step,
+                                    const RewriteSystem &system) {
+  assert(step.Kind == RewriteStep::Relation);
+
+  auto relation = system.getRelation(step.Arg);
+  auto &term = getCurrentTerm();
+
+  auto lhs = (step.Inverse ? relation.second : relation.first);
+  auto rhs = (step.Inverse ? relation.first : relation.second);
+
+  auto bug = [&](StringRef msg) {
+    llvm::errs() << msg << "\n";
+    llvm::errs() << "- Term: " << term << "\n";
+    llvm::errs() << "- StartOffset: " << step.StartOffset << "\n";
+    llvm::errs() << "- EndOffset: " << step.EndOffset << "\n";
+    llvm::errs() << "- Expected subterm: " << lhs << "\n";
+    abort();
+  };
+
+  if (term.size() != step.StartOffset + lhs.size() + step.EndOffset) {
+    bug("Invalid whiskering");
+  }
+
+  if (!std::equal(term.begin() + step.StartOffset,
+                  term.begin() + step.StartOffset + lhs.size(),
+                  lhs.begin())) {
+    bug("Invalid subterm");
+  }
+
+  MutableTerm prefix(term.begin(), term.begin() + step.StartOffset);
+  MutableTerm suffix(term.end() - step.EndOffset, term.end());
+
+  term = prefix;
+  term.append(rhs);
+  term.append(suffix);
+
+  return {lhs, rhs, prefix, suffix};
+}
+
 void
 RewritePathEvaluator::applyConcreteConformance(const RewriteStep &step,
                                                const RewriteSystem &system) {

lib/AST/RequirementMachine/RewriteLoop.h

@@ -209,8 +209,9 @@ struct RewriteStep {
                        /*arg=*/numSubstitutions, inverse);
   }
 
-  static RewriteStep forRelation(unsigned relationID, bool inverse) {
-    return RewriteStep(Relation, /*startOffset=*/0, /*endOffset=*/0,
+  static RewriteStep forRelation(unsigned startOffset, unsigned relationID,
+                                 bool inverse) {
+    return RewriteStep(Relation, startOffset, /*endOffset=*/0,
                        /*arg=*/relationID, inverse);
   }
 
@@ -420,12 +421,13 @@ struct RewritePathEvaluator {
   void applyShift(const RewriteStep &step,
                   const RewriteSystem &system);
 
-  void applyRelation(const RewriteStep &step,
-                     const RewriteSystem &system);
-
   void applyDecompose(const RewriteStep &step,
                       const RewriteSystem &system);
 
+  AppliedRewriteStep
+  applyRelation(const RewriteStep &step,
+                const RewriteSystem &system);
+
   void applyConcreteConformance(const RewriteStep &step,
                                 const RewriteSystem &system);
 

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -699,6 +699,11 @@ void RewriteSystem::dump(llvm::raw_ostream &out) const {
     out << "- " << rule << "\n";
   }
   out << "}\n";
+  out << "Relations: {\n";
+  for (const auto &relation : Relations) {
+    out << "- " << relation.first << " =>> " << relation.second << "\n";
+  }
+  out << "}\n";
   out << "Rewrite loops: {\n";
   for (const auto &loop : Loops) {
     if (loop.isDeleted())

lib/AST/RequirementMachine/RewriteSystem.h

@@ -329,22 +329,24 @@ class RewriteSystem final {
 
   //////////////////////////////////////////////////////////////////////////////
   ///
-  /// "Pseudo-rules" for the property map
+  /// Relations are "pseudo-rules" introduced by the property map
   ///
   //////////////////////////////////////////////////////////////////////////////
 
 public:
   /// The left hand side is known to be smaller than the right hand side.
-  using Relation = std::pair<Symbol, Symbol>;
+  using Relation = std::pair<Term, Term>;
 
 private:
   llvm::DenseMap<Relation, unsigned> RelationMap;
   std::vector<Relation> Relations;
 
 public:
-  unsigned recordRelation(Symbol lhs, Symbol rhs);
+  unsigned recordRelation(Term lhs, Term rhs);
   Relation getRelation(unsigned index) const;
 
+  unsigned recordRelation(Symbol lhs, Symbol rhs);
+
   /// A type witness has a subject type, stored in LHS, which takes the form:
   ///
   /// T.[concrete: C : P].[P:X]

test/Generics/generic_objc_superclass.swift

@@ -16,8 +16,6 @@ func foo<T : Generic<U>, U>(_: T, _: U) {
 // CHECK-NEXT: - τ_0_0.[superclass: Generic<τ_0_0> with <τ_0_1>] => τ_0_0
 // CHECK-NEXT: - τ_0_0.[layout: AnyObject] => τ_0_0
 // CHECK-NEXT: }
-// CHECK-NEXT: Rewrite loops: {
-// CHECK-NEXT: }
-// CHECK-NEXT: Property map: {
+// CHECK: Property map: {
 // CHECK-NEXT:   τ_0_0 => { layout: AnyObject superclass: [superclass: Generic<τ_0_0> with <τ_0_1>] }
 // CHECK-NEXT: }

test/Generics/rdar79564324.swift

@@ -35,9 +35,7 @@ public func test<T : P>(_ t: T) where T == T.A {
 // CHECK-NEXT: - τ_0_1.A => τ_0_0
 // CHECK-NEXT: - τ_0_0.A => τ_0_0
 // CHECK-NEXT: }
-// CHECK-NEXT: Rewrite loops: {
-// CHECK:      }
-// CHECK-NEXT: Property map: {
+// CHECK: Property map: {
 // CHECK-NEXT:   [P] => { conforms_to: [P] }
 // CHECK-NEXT:   [P:A] => { conforms_to: [P] }
 // CHECK-NEXT:   τ_0_1 => { conforms_to: [P] }

test/Generics/unify_superclass_types_1.swift

@@ -23,9 +23,7 @@ extension P where Self : Derived {
 // CHECK-NEXT: - [P].[layout: _NativeClass] => [P]
 // CHECK-NEXT: - τ_0_0.[layout: _NativeClass] => τ_0_0
 // CHECK-NEXT: }
-// CHECK-NEXT: Rewrite loops: {
-// CHECK:      }
-// CHECK-NEXT: Property map: {
+// CHECK: Property map: {
 // CHECK-NEXT:   [P] => { conforms_to: [P] layout: _NativeClass superclass: [superclass: Base] }
 // CHECK-NEXT:   τ_0_0 => { conforms_to: [P] layout: _NativeClass superclass: [superclass: Derived] }
 // CHECK-NEXT: }

test/Generics/unify_superclass_types_2.swift

@@ -41,9 +41,7 @@ func unifySuperclassTest<T : P1 & P2>(_: T) {
 // CHECK-NEXT: - τ_0_0.[P1:A1].[concrete: String] => τ_0_0.[P1:A1]
 // CHECK-NEXT: - τ_0_0.[P2:B2] => τ_0_0.[P1:B1]
 // CHECK:      }
-// CHECK-NEXT: Rewrite loops: {
-// CHECK:      }
-// CHECK-NEXT: Property map: {
+// CHECK: Property map: {
 // CHECK-NEXT:   [P1] => { conforms_to: [P1] }
 // CHECK-NEXT:   [P2] => { conforms_to: [P2] }
 // CHECK-NEXT:   [P1:X] => { layout: _NativeClass superclass: [superclass: Generic<Int, τ_0_0, τ_0_1> with <[P1:A1], [P1:B1]>] }