RequirementMachine: Encapsulate 3-cells in a new HomotopyGenerator data type

Author: slavapestov

lib/AST/RequirementMachine/HomotopyReduction.cpp

@@ -505,12 +505,12 @@ void RewriteSystem::minimizeRewriteSystem() {
       const auto &loop = HomotopyGenerators[loopID];
 
       SmallVector<unsigned> redundancyCandidates =
-          loop.second.findRulesAppearingOnceInEmptyContext();
+          loop.Path.findRulesAppearingOnceInEmptyContext();
       if (redundancyCandidates.empty())
         continue;
 
       auto ruleID = redundancyCandidates.front();
-      RewritePath replacementPath = loop.second.splitCycleAtRule(ruleID);
+      RewritePath replacementPath = loop.Path.splitCycleAtRule(ruleID);
 
       deletedRules.insert(ruleID);
       deletedHomotopyGenerators.insert(loopID);
@@ -538,30 +538,30 @@ void RewriteSystem::minimizeRewriteSystem() {
         continue;
 
       auto &loop = HomotopyGenerators[loopID];
-      bool changed = loop.second.replaceRuleWithPath(ruleID, replacementPath);
+      bool changed = loop.Path.replaceRuleWithPath(ruleID, replacementPath);
 
       if (changed) {
-        unsigned size = loop.second.size();
+        unsigned size = loop.Path.size();
 
         bool changed;
         do {
           changed = false;
-          changed |= loop.second.computeFreelyReducedPath();
-          changed |= loop.second.computeCyclicallyReducedLoop(loop.first, *this);
-          changed |= loop.second.computeLeftCanonicalForm(*this);
+          changed |= loop.Path.computeFreelyReducedPath();
+          changed |= loop.Path.computeCyclicallyReducedLoop(loop.Basepoint, *this);
+          changed |= loop.Path.computeLeftCanonicalForm(*this);
         } while (changed);
 
         if (Debug.contains(DebugFlags::HomotopyReduction)) {
-          if (size != loop.second.size()) {
-            llvm::dbgs() << "** Note: Cyclically reduced the loop to eliminate "
-                         << (size - loop.second.size()) << " steps\n";
+          if (size != loop.Path.size()) {
+            llvm::dbgs() << "** Note: Reducing the loop eliminated "
+                         << (size - loop.Path.size()) << " steps\n";
           }
         }
 
         if (Debug.contains(DebugFlags::HomotopyReduction)) {
           llvm::dbgs() << "** Updated homotopy generator: ";
-          llvm::dbgs() << "- " << loop.first << ": ";
-          loop.second.dump(llvm::dbgs(), loop.first, *this);
+          llvm::dbgs() << "- " << loop.Basepoint << ": ";
+          loop.Path.dump(llvm::dbgs(), loop.Basepoint, *this);
           llvm::dbgs() << "\n";
         }
       }
@@ -587,16 +587,16 @@ void RewriteSystem::minimizeRewriteSystem() {
         continue;
 
       const auto &loop = HomotopyGenerators[loopID];
-      if (loop.second.empty())
+      if (loop.Path.empty())
         continue;
 
       llvm::dbgs() << "(#" << loopID << ") ";
-      llvm::dbgs() << loop.first << ": ";
-      loop.second.dump(llvm::dbgs(), loop.first, *this);
+      llvm::dbgs() << loop.Basepoint << ": ";
+      loop.Path.dump(llvm::dbgs(), loop.Basepoint, *this);
       llvm::dbgs() << "\n";
 
-      MutableTerm basepoint = loop.first;
-      for (auto step : loop.second) {
+      MutableTerm basepoint = loop.Basepoint;
+      for (auto step : loop.Path) {
         step.apply(basepoint, *this);
         llvm::dbgs() << "- " << basepoint << "\n";
       }
@@ -608,15 +608,15 @@ void RewriteSystem::minimizeRewriteSystem() {
 void RewriteSystem::verifyHomotopyGenerators() const {
 #ifndef NDEBUG
   for (const auto &loop : HomotopyGenerators) {
-    auto term = loop.first;
+    auto term = loop.Basepoint;
 
-    for (const auto &step : loop.second) {
+    for (const auto &step : loop.Path) {
       step.apply(term, *this);
     }
 
-    if (term != loop.first) {
+    if (term != loop.Basepoint) {
       llvm::errs() << "Not a loop: ";
-      loop.second.dump(llvm::errs(), loop.first, *this);
+      loop.Path.dump(llvm::errs(), loop.Basepoint, *this);
       llvm::errs() << "\n";
       abort();
     }

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -428,8 +428,8 @@ void RewriteSystem::dump(llvm::raw_ostream &out) const {
   out << "}\n";
   out << "Homotopy generators: {\n";
   for (const auto &loop : HomotopyGenerators) {
-    out << "- " << loop.first << ": ";
-    loop.second.dump(out, loop.first, *this);
+    out << "- " << loop.Basepoint << ": ";
+    loop.Path.dump(out, loop.Basepoint, *this);
     out << "\n";
   }
   out << "}\n";

lib/AST/RequirementMachine/RewriteSystem.h

@@ -266,6 +266,29 @@ struct RewritePath {
             const RewriteSystem &system) const;
 };
 
+/// A loop (3-cell) that rewrites the basepoint back to the basepoint.
+class HomotopyGenerator {
+public:
+  MutableTerm Basepoint;
+  RewritePath Path;
+
+private:
+  bool Deleted;
+
+public:
+  HomotopyGenerator(MutableTerm basepoint, RewritePath path)
+    : Basepoint(basepoint), Path(path), Deleted(false) {}
+
+  bool isDeleted() const {
+    return Deleted;
+  }
+
+  void markDeleted() {
+    assert(!Deleted);
+    Deleted = true;
+  }
+};
+
 /// A term rewrite system for working with types in a generic signature.
 ///
 /// Out-of-line methods are documented in RewriteSystem.cpp.
@@ -320,7 +343,7 @@ class RewriteSystem final {
   /// loop around a base point.
   ///
   /// This data informs the generic signature minimization algorithm.
-  std::vector<std::pair<MutableTerm, RewritePath>> HomotopyGenerators;
+  std::vector<HomotopyGenerator> HomotopyGenerators;
 
   DebugOptions Debug;
 
@@ -401,7 +424,7 @@ class RewriteSystem final {
       const Rule &lhs, const Rule &rhs,
       std::vector<std::pair<MutableTerm, MutableTerm>> &pairs,
       std::vector<RewritePath> &paths,
-      std::vector<std::pair<MutableTerm, RewritePath>> &loops) const;
+      std::vector<HomotopyGenerator> &loops) const;
 
   void processMergedAssociatedTypes();
 

lib/AST/RequirementMachine/RewriteSystemCompletion.cpp

@@ -369,8 +369,7 @@ RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
                                    std::vector<std::pair<MutableTerm,
                                                          MutableTerm>> &pairs,
                                    std::vector<RewritePath> &paths,
-                                   std::vector<std::pair<MutableTerm,
-                                                         RewritePath>> &loops) const {
+                                   std::vector<HomotopyGenerator> &loops) const {
   auto end = lhs.getLHS().end();
   if (from + rhs.getLHS().size() < end) {
     // lhs == TUV -> X, rhs == U -> Y.
@@ -495,7 +494,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
 
   std::vector<std::pair<MutableTerm, MutableTerm>> resolvedCriticalPairs;
   std::vector<RewritePath> resolvedPaths;
-  std::vector<std::pair<MutableTerm, RewritePath>> resolvedLoops;
+  std::vector<HomotopyGenerator> resolvedLoops;
 
   do {
     // For every rule, looking for other rules that overlap with this rule.
@@ -571,7 +570,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
               llvm::dbgs() << rhs << ":\n";
 
               llvm::dbgs() << "$$ Loop: ";
-              loop.second.dump(llvm::dbgs(), loop.first, *this);
+              loop.Path.dump(llvm::dbgs(), loop.Basepoint, *this);
               llvm::dbgs() << "\n\n";
 
               // Record the trivial loop.