Merge pull request swiftlang#40119 from slavapestov/requirement-machine-explicit-conformances

RequirementMachine: Prefer to eliminate non-explicit conformances, and other fixes

Author: slavapestov

docs/RequirementMachine/Makefile

@@ -0,0 +1,10 @@
+RequirementMachine.pdf:
+	pdflatex RequirementMachine
+	bibtex RequirementMachine
+	pdflatex RequirementMachine
+	pdflatex RequirementMachine
+
+clean:
+	rm *.aux *.bbl *.blg *.idx *.ilg *.ind *.log *.out *.pdf *.toc
+
+.PHONY: clean

docs/RequirementMachine/RequirementMachine.bib

@@ -0,0 +1,75 @@
+@misc{se0142,
+    author    = "David Hart and Jacob Bandes-Storch and Doug Gregor",
+    title     = "{SE-0142}: Permit where clauses to constrain associated types",
+    url       = "https://github.com/apple/swift-evolution/blob/main/proposals/0142-associated-types-constraints.md",
+    year      = {2017}
+}
+@misc{se0157,
+    author    = "Doug Gregor and Erica Sadun and Austin Zheng",
+    title     = "{SE-0157}: Support recursive constraints on associated types",
+    url       = "https://github.com/apple/swift-evolution/blob/main/proposals/0157-recursive-protocol-constraints.md",
+    year      = {2017}
+}
+@misc(gensig,
+    author    = "Doug Gregor",
+    title     = "Generic Signatures",
+    url       = "https://github.com/apple/swift/blob/main/docs/ABI/GenericSignature.md",
+    year      = {2018}
+)
+@article{undecidablegroup,
+author = {Donald J. Collins},
+title = {{A simple presentation of a group with unsolvable word problem}},
+volume = {30},
+journal = {Illinois Journal of Mathematics},
+number = {2},
+publisher = {Duke University Press},
+pages = {230 -- 234},
+year = {1986},
+doi = {10.1215/ijm/1256044631},
+URL = {https://doi.org/10.1215/ijm/1256044631}
+}
+@book{andallthat, place={Cambridge}, title={Term Rewriting and All That}, DOI={10.1017/CBO9781139172752}, publisher={Cambridge University Press}, author={Baader, Franz and Nipkow, Tobias}, year={1998}}
+@Inbook{Knuth1983,
+author="Knuth, D. E.
+and Bendix, P. B.",
+editor="Siekmann, J{\"o}rg H.
+and Wrightson, Graham",
+title="Simple Word Problems in Universal Algebras",
+bookTitle="Automation of Reasoning: 2: Classical Papers on Computational Logic 1967--1970",
+year="1983",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="342--376",
+isbn="978-3-642-81955-1",
+doi="10.1007/978-3-642-81955-1_23",
+url="https://doi.org/10.1007/978-3-642-81955-1_23"
+}
+@article{SQUIER1994271,
+title = {A finiteness condition for rewriting systems},
+journal = {Theoretical Computer Science},
+volume = {131},
+number = {2},
+pages = {271-294},
+year = {1994},
+issn = {0304-3975},
+doi = {https://doi.org/10.1016/0304-3975(94)90175-9},
+url = {https://www.sciencedirect.com/science/article/pii/0304397594901759},
+author = {Craig C. Squier and Friedrich Otto and Yuji Kobayashi}
+}
+@inproceedings{guiraud:hal-00818253,
+  TITLE = {{A Homotopical Completion Procedure with Applications to Coherence of Monoids}},
+  AUTHOR = {Guiraud, Yves and Malbos, Philippe and Mimram, Samuel},
+  URL = {https://hal.inria.fr/hal-00818253},
+  BOOKTITLE = {{RTA - 24th International Conference on Rewriting Techniques and Applications - 2013}},
+  ADDRESS = {Eindhoven, Netherlands},
+  EDITOR = {Van Raamsdonk, Femke},
+  PUBLISHER = {{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}},
+  SERIES = {Leibniz International Proceedings in Informatics (LIPIcs)},
+  VOLUME = {21},
+  PAGES = {223-238},
+  YEAR = {2013},
+  MONTH = Jun,
+  DOI = {10.4230/LIPIcs.RTA.2013.223},
+  HAL_ID = {hal-00818253},
+  HAL_VERSION = {v1},
+}

docs/RequirementMachine/RequirementMachine.tex

@@ -74,17 +74,17 @@ add_swift_host_library(swiftAST STATIC
   ProtocolConformance.cpp
   RawComment.cpp
   RequirementEnvironment.cpp
-  RequirementMachine/HomotopyReduction.cpp
   RequirementMachine/GeneratingConformances.cpp
   RequirementMachine/GenericSignatureQueries.cpp
+  RequirementMachine/HomotopyReduction.cpp
+  RequirementMachine/KnuthBendix.cpp
   RequirementMachine/PropertyMap.cpp
   RequirementMachine/PropertyUnification.cpp
   RequirementMachine/RequirementMachine.cpp
   RequirementMachine/RequirementMachineRequests.cpp
   RequirementMachine/RewriteContext.cpp
   RequirementMachine/RewriteLoop.cpp
   RequirementMachine/RewriteSystem.cpp
-  RequirementMachine/RewriteSystemCompletion.cpp
   RequirementMachine/Symbol.cpp
   RequirementMachine/Term.cpp
   SILLayout.cpp

lib/AST/CMakeLists.txt

@@ -607,8 +607,13 @@ static const ProtocolDecl *getParentConformanceForTerm(Term lhs) {
 /// conformance rules.
 void RewriteSystem::computeGeneratingConformances(
     llvm::DenseSet<unsigned> &redundantConformances) {
-  // All conformance rules, sorted by left hand side.
-  SmallVector<std::pair<unsigned, Term>, 4> conformanceRules;
+  // All conformance rules, sorted by (isExplicit(), getLHS()), with non-explicit
+  // rules with longer left hand sides coming first.
+  //
+  // The idea here is that we want less canonical rules to be eliminated first,
+  // but we prefer to eliminate non-explicit rules, in an attempt to keep protocol
+  // conformance rules in the same protocol as they were originally defined in.
+  SmallVector<unsigned, 4> conformanceRules;
 
   // Maps a conformance rule to a conformance path deriving the subject type's
   // base type. For example, consider the following conformance rule:
@@ -640,8 +645,7 @@ void RewriteSystem::computeGeneratingConformances(
     if (!rule.isProtocolConformanceRule())
       continue;
 
-    auto lhs = rule.getLHS();
-    conformanceRules.emplace_back(ruleID, lhs);
+    conformanceRules.push_back(ruleID);
 
     // Initially, every non-redundant conformance rule can be expressed
     // as itself.
@@ -655,6 +659,8 @@ void RewriteSystem::computeGeneratingConformances(
       continue;
     }
 
+    auto lhs = rule.getLHS();
+
     // Record a parent path if the subject type itself requires a non-trivial
     // conformance path to derive.
     if (auto *parentProto = getParentConformanceForTerm(lhs)) {
@@ -696,14 +702,18 @@ void RewriteSystem::computeGeneratingConformances(
   // Sort the list of conformance rules in reverse order; we're going to try
   // to minimize away less canonical rules first.
   std::sort(conformanceRules.begin(), conformanceRules.end(),
-            [&](const std::pair<unsigned, Term> &lhs,
-                const std::pair<unsigned, Term> &rhs) -> bool {
-              return lhs.second.compare(rhs.second, Context) > 0;
+            [&](unsigned lhs, unsigned rhs) -> bool {
+              const auto &lhsRule = getRule(lhs);
+              const auto &rhsRule = getRule(rhs);
+
+              if (lhsRule.isExplicit() != rhsRule.isExplicit())
+                return !lhsRule.isExplicit();
+
+              return lhsRule.getLHS().compare(rhsRule.getLHS(), Context) > 0;
             });
 
   // Find a minimal set of generating conformances.
-  for (const auto &pair : conformanceRules) {
-    unsigned ruleID = pair.first;
+  for (unsigned ruleID : conformanceRules) {
     const auto &paths = conformancePaths[ruleID];
 
     bool isProtocolRefinement = protocolRefinements.count(ruleID) > 0;