RequirementMachine: Verify homotopy generators

Author: slavapestov

lib/AST/RequirementMachine/RequirementMachine.cpp

@@ -413,7 +413,8 @@ void RequirementMachine::computeCompletion() {
     checkCompletionResult();
 
     // Check invariants.
-    System.verify();
+    System.verifyRewriteRules();
+    System.verifyHomotopyGenerators();
 
     // Build the property map, which also performs concrete term
     // unification; if this added any new rules, run the completion

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -36,38 +36,49 @@ void RewritePath::invert() {
     step.invert();
 }
 
-/// Dumps the rewrite step that was applied to \p term. Mutates \p term to
-/// reflect the application of the rule.
-void RewriteStep::dump(llvm::raw_ostream &out,
-                       MutableTerm &term,
-                       const RewriteSystem &system) const {
+AppliedRewriteStep RewriteStep::apply(MutableTerm &term,
+                                      const RewriteSystem &system) const {
   const auto &rule = system.getRule(RuleID);
 
   auto lhs = (Inverse ? rule.getRHS() : rule.getLHS());
   auto rhs = (Inverse ? rule.getLHS() : rule.getRHS());
 
-  assert(std::equal(term.begin() + Offset,
-                    term.begin() + Offset + lhs.size(),
-                    lhs.begin()));
+  if (!std::equal(term.begin() + Offset,
+                  term.begin() + Offset + lhs.size(),
+                  lhs.begin())) {
+    llvm::errs() << "Invalid rewrite path\n";
+    llvm::errs() << "- Term: " << term << "\n";
+    llvm::errs() << "- Offset: " << Offset << "\n";
+    llvm::errs() << "- Expected subterm: " << lhs << "\n";
+    abort();
+  }
 
   MutableTerm prefix(term.begin(), term.begin() + Offset);
   MutableTerm suffix(term.begin() + Offset + lhs.size(), term.end());
 
-  if (!prefix.empty()) {
-    out << prefix;
+  term = prefix;
+  term.append(rhs);
+  term.append(suffix);
+
+  return {lhs, rhs, prefix, suffix};
+}
+
+/// Dumps the rewrite step that was applied to \p term. Mutates \p term to
+/// reflect the application of the rule.
+void RewriteStep::dump(llvm::raw_ostream &out,
+                       MutableTerm &term,
+                       const RewriteSystem &system) const {
+  auto result = apply(term, system);
+
+  if (!result.prefix.empty()) {
+    out << result.prefix;
     out << ".";
   }
-  out << "(" << rule.getLHS();
-  out << (Inverse ? " <= " : " => ");
-  out << rule.getRHS() << ")";
-  if (!suffix.empty()) {
+  out << "(" << result.lhs << " => " << result.rhs << ")";
+  if (!result.suffix.empty()) {
     out << ".";
-    out << suffix;
+    out << result.suffix;
   }
-
-  term = prefix;
-  term.append(rhs);
-  term.append(suffix);
 }
 
 /// Dumps a series of rewrite steps applied to \p term.
@@ -377,7 +388,7 @@ void RewriteSystem::simplifyRewriteSystem() {
   }
 }
 
-void RewriteSystem::verify() const {
+void RewriteSystem::verifyRewriteRules() const {
 #ifndef NDEBUG
 
 #define ASSERT_RULE(expr) \
@@ -439,6 +450,25 @@ void RewriteSystem::verify() const {
 #endif
 }
 
+void RewriteSystem::verifyHomotopyGenerators() const {
+#ifndef NDEBUG
+  for (const auto &loop : HomotopyGenerators) {
+    auto term = loop.first;
+
+    for (const auto &step : loop.second) {
+      (void) step.apply(term, *this);
+    }
+
+    if (term != loop.first) {
+      llvm::errs() << "Not a loop: ";
+      loop.second.dump(llvm::errs(), loop.first, *this);
+      llvm::errs() << "\n";
+      abort();
+    }
+  }
+#endif
+}
+
 void RewriteSystem::dump(llvm::raw_ostream &out) const {
   out << "Rewrite system: {\n";
   for (const auto &rule : Rules) {

lib/AST/RequirementMachine/RewriteSystem.h

@@ -79,7 +79,22 @@ class Rule final {
   }
 };
 
+struct AppliedRewriteStep {
+  Term lhs;
+  Term rhs;
+  MutableTerm prefix;
+  MutableTerm suffix;
+};
+
 /// Records the application of a rewrite rule to a term.
+///
+/// Formally, this is a whiskered, oriented rewrite rule. For example, given a
+/// rule (X => Y) and the term A.X.B, the application at offset 1 yields A.Y.B.
+///
+/// This can be represented as A.(X => Y).B.
+///
+/// Similarly, going in the other direction, if we start from A.Y.B and apply
+/// the inverse rule, we get A.(Y => X).B.
 struct RewriteStep {
   /// The position within the term where the rule is being applied.
   unsigned Offset : 16;
@@ -103,6 +118,9 @@ struct RewriteStep {
     Inverse = !Inverse;
   }
 
+  AppliedRewriteStep apply(MutableTerm &term,
+                           const RewriteSystem &system) const;
+
   void dump(llvm::raw_ostream &out,
             MutableTerm &term,
             const RewriteSystem &system) const;
@@ -244,7 +262,9 @@ class RewriteSystem final {
 
   void simplifyRewriteSystem();
 
-  void verify() const;
+  void verifyRewriteRules() const;
+
+  void verifyHomotopyGenerators() const;
 
   std::pair<CompletionResult, unsigned>
   buildPropertyMap(PropertyMap &map,