Skip to content

Commit a729beb

Browse files
slavapestovslavapestov
committed
RequirementMachine: Improved rule deletion heuristic
Instead of finding the best redundancy candidate from the first homotopy generator that has one, find the best redundancy candidate from *all* homotopy generators that have one. This correctly minimizes the "Joe Groff monoid" without hitting the assertion guarding against simplified rules being non-redundant. It also brings us closer to being able to correctly minimize the protocol from https://bugs.swift.org/browse/SR-7353.
1 parent 74d944d commit a729beb

File tree

4 files changed

+83
-34
lines changed

4 files changed

+83
-34
lines changed

‎lib/AST/RequirementMachine/HomotopyReduction.cpp

Lines changed: 35 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -849,46 +849,51 @@ findRuleToDelete(bool firstPass,
849849
RewritePath &replacementPath) {
850850
assert(!firstPass || redundantConformances == nullptr);
851851

852-
for (auto &loop : HomotopyGenerators) {
852+
SmallVector<std::pair<unsigned, unsigned>, 2> redundancyCandidates;
853+
for (unsigned loopID : indices(HomotopyGenerators)) {
854+
const auto &loop = HomotopyGenerators[loopID];
853855
if (loop.isDeleted())
854856
continue;
855857

856-
SmallVector<unsigned> redundancyCandidates =
857-
loop.findRulesAppearingOnceInEmptyContext(*this);
858+
for (unsigned ruleID : loop.findRulesAppearingOnceInEmptyContext(*this)) {
859+
redundancyCandidates.emplace_back(loopID, ruleID);
860+
}
861+
}
858862

859-
Optional<unsigned> found;
863+
Optional<std::pair<unsigned, unsigned>> found;
860864

861-
for (unsigned ruleID : redundancyCandidates) {
862-
if (!isCandidateForDeletion(ruleID, firstPass, redundantConformances))
863-
continue;
865+
for (const auto &pair : redundancyCandidates) {
866+
unsigned ruleID = pair.second;
867+
if (!isCandidateForDeletion(ruleID, firstPass, redundantConformances))
868+
continue;
864869

865-
if (!found) {
866-
found = ruleID;
867-
continue;
868-
}
870+
if (!found) {
871+
found = pair;
872+
continue;
873+
}
869874

870-
const auto &rule = getRule(ruleID);
871-
const auto &otherRule = getRule(*found);
875+
const auto &rule = getRule(ruleID);
876+
const auto &otherRule = getRule(found->second);
872877

873-
// Prefer to delete "less canonical" rules.
874-
if (rule.compare(otherRule, Context) > 0)
875-
found = ruleID;
876-
}
878+
// Prefer to delete "less canonical" rules.
879+
if (rule.compare(otherRule, Context) > 0)
880+
found = pair;
881+
}
877882

878-
if (!found)
879-
continue;
883+
if (!found)
884+
return None;
880885

881-
auto ruleID = *found;
882-
assert(replacementPath.empty());
883-
replacementPath = loop.Path.splitCycleAtRule(ruleID);
886+
unsigned loopID = found->first;
887+
unsigned ruleID = found->second;
888+
assert(replacementPath.empty());
884889

885-
loop.markDeleted();
886-
getRule(ruleID).markRedundant();
890+
auto &loop = HomotopyGenerators[loopID];
891+
replacementPath = loop.Path.splitCycleAtRule(ruleID);
887892

888-
return ruleID;
889-
}
893+
loop.markDeleted();
894+
getRule(ruleID).markRedundant();
890895

891-
return None;
896+
return ruleID;
892897
}
893898

894899
/// Delete a rewrite rule that is known to be redundant, replacing all
@@ -1123,11 +1128,13 @@ void RewriteSystem::verifyMinimizedRules() const {
11231128

11241129
// Rules with unresolved name symbols (other than permanent rules for
11251130
// associated type introduction) should be redundant.
1131+
//
1132+
// FIXME: What about invalid code?
11261133
if (rule.getLHS().containsUnresolvedSymbols() ||
11271134
rule.getRHS().containsUnresolvedSymbols()) {
11281135
llvm::errs() << "Unresolved rule is not redundant: " << rule << "\n\n";
11291136
dump(llvm::errs());
11301137
abort();
11311138
}
11321139
}
1133-
}
1140+
}

‎test/Generics/joe_monoid.swift

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
// RUN: %target-swift-frontend -typecheck %s -debug-generic-signatures -requirement-machine-protocol-signatures=on 2>&1 | %FileCheck %s
2+
3+
// This is a funny monoid presentation from Joe Groff.
4+
5+
// CHECK-LABEL: joe_monoid.(file).O1@
6+
// CHECK-LABEL: Requirement signature: <Self where Self == Self.C.C.C.C, Self.C : O1, Self.R : O1, Self.C.C == Self.R.C.C.R, Self.C.R.C == Self.R.C.R>
7+
protocol O1 {
8+
associatedtype R : O1
9+
associatedtype C : O1
10+
where C.C.C.C == Self,
11+
C.C.R.C.C.R == Self,
12+
R.C.R.C.R.C == Self
13+
}
14+
15+
// CHECK-LABEL: joe_monoid.(file).O2@
16+
// CHECK-LABEL: Requirement signature: <Self where Self == Self.C.C.C.C, Self.C : O2, Self.R : O2, Self.C.C == Self.R.C.C.R, Self.C.R.C == Self.R.C.R>
17+
protocol O2 {
18+
associatedtype R : O2
19+
associatedtype C : O2
20+
where Self == C.C.C.C,
21+
C.C.C.C == C.C.R.C.C.R,
22+
C.C.R.C.C.R == R.C.R.C.R.C
23+
}
24+
25+
// The GSB incorrectly minimized this one, dropping all of the same-type requirements.
26+
27+
// CHECK-LABEL: joe_monoid.(file).O3@
28+
// CHECK-LABEL: Requirement signature: <Self where Self == Self.C.C.C.C, Self.C : O3, Self.R : O3, Self.C.C == Self.R.C.C.R, Self.C.R.C == Self.R.C.R>
29+
protocol O3 {
30+
associatedtype R : O3
31+
associatedtype C : O3
32+
where C.C.C.C == C.C.R.C.C.R,
33+
C.C.R.C.C.R == R.C.R.C.R.C,
34+
R.C.R.C.R.C == Self
35+
}
36+
37+
// CHECK-LABEL: joe_monoid.(file).O4@
38+
// CHECK-LABEL: Requirement signature: <Self where Self == Self.C.C.C.C, Self.C : O4, Self.R : O4, Self.C.C == Self.R.C.C.R, Self.C.R.C == Self.R.C.R>
39+
protocol O4 {
40+
associatedtype R : O4
41+
associatedtype C : O4
42+
where Self == C.C.C.C,
43+
C.C == R.C.C.R,
44+
C.R.C == R.C.R
45+
}

‎test/Generics/rdar83308672.swift

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,9 @@ protocol B {
3030

3131
// Note that T.X == T.Y implies T : B, but also T : B implies T.X == T.Y;
3232
// we can drop one requirement but not both.
33-
//
34-
// If T : B was explicitly stated, we drop T.X == T.Y; otherwise we keep
35-
// T.X == T.Y and drop T : B.
3633

3734
// CHECK: rdar83308672.(file).G1@
38-
// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T.X == Self.T.Y>
35+
// CHECK-NEXT: Requirement signature: <Self where Self.T : A, Self.T : B>
3936
protocol G1 {
4037
associatedtype T : A where T.X == T.Y
4138
}

‎test/Generics/sr12120.swift

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// RUN: %target-typecheck-verify-swift -debug-generic-signatures -requirement-machine-protocol-signatures=on 2>&1 | %FileCheck %s
22

33
// CHECK: sr12120.(file).Swappable1@
4-
// CHECK-NEXT: Requirement signature: <Self where Self == Self.Swapped.Swapped, Self.A == Self.Swapped.B, Self.Swapped : Swappable1>
4+
// CHECK-NEXT: Requirement signature: <Self where Self == Self.Swapped.Swapped, Self.B == Self.Swapped.A, Self.Swapped : Swappable1>
55
protocol Swappable1 {
66
associatedtype A
77
associatedtype B
@@ -12,7 +12,7 @@ protocol Swappable1 {
1212
}
1313

1414
// CHECK: sr12120.(file).Swappable2@
15-
// CHECK-NEXT: Requirement signature: <Self where Self == Self.Swapped.Swapped, Self.A == Self.Swapped.B, Self.Swapped : Swappable2>
15+
// CHECK-NEXT: Requirement signature: <Self where Self == Self.Swapped.Swapped, Self.B == Self.Swapped.A, Self.Swapped : Swappable2>
1616
protocol Swappable2 {
1717
associatedtype A
1818
associatedtype B

0 commit comments

Comments
 (0)