RequirementMachine: Preliminary plumbing for computing homotopy generators

Author: slavapestov

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -23,6 +23,70 @@
 using namespace swift;
 using namespace rewriting;
 
+void Rule::dump(llvm::raw_ostream &out) const {
+  out << LHS << " => " << RHS;
+  if (deleted)
+    out << " [deleted]";
+}
+
+void RewritePath::invert() {
+  std::reverse(Steps.begin(), Steps.end());
+
+  for (auto &step : Steps)
+    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 {
+  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()));
+
+  MutableTerm prefix(term.begin(), term.begin() + Offset);
+  MutableTerm suffix(term.begin() + Offset + lhs.size(), term.end());
+
+  if (!prefix.empty()) {
+    out << prefix;
+    out << ".";
+  }
+  out << "(" << rule.getLHS();
+  out << (Inverse ? " <= " : " => ");
+  out << rule.getRHS() << ")";
+  if (!suffix.empty()) {
+    out << ".";
+    out << suffix;
+  }
+
+  term = prefix;
+  term.append(rhs);
+  term.append(suffix);
+}
+
+/// Dumps a series of rewrite steps applied to \p term.
+void RewritePath::dump(llvm::raw_ostream &out,
+                       MutableTerm term,
+                       const RewriteSystem &system) const {
+  bool first = true;
+
+  for (const auto &step : Steps) {
+    if (!first) {
+      out << " ⊗ ";
+    } else {
+      first = false;
+    }
+
+    step.dump(out, term, system);
+  }
+}
+
 RewriteSystem::RewriteSystem(RewriteContext &ctx)
     : Context(ctx), Debug(ctx.getDebugOptions()) {}
 
@@ -31,12 +95,6 @@ RewriteSystem::~RewriteSystem() {
                         Context.RuleTrieRootHistogram);
 }
 
-void Rule::dump(llvm::raw_ostream &out) const {
-  out << LHS << " => " << RHS;
-  if (deleted)
-    out << " [deleted]";
-}
-
 void RewriteSystem::initialize(
     std::vector<std::pair<MutableTerm, MutableTerm>> &&rules,
     ProtocolGraph &&graph) {
@@ -89,16 +147,16 @@ bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs) {
     llvm::dbgs() << "## Simplified and oriented rule " << lhs << " => " << rhs << "\n\n";
   }
 
-  unsigned i = Rules.size();
+  unsigned newRuleID = Rules.size();
 
   auto uniquedLHS = Term::get(lhs, Context);
   auto uniquedRHS = Term::get(rhs, Context);
   Rules.emplace_back(uniquedLHS, uniquedRHS);
 
-  auto oldRuleID = Trie.insert(lhs.begin(), lhs.end(), i);
+  auto oldRuleID = Trie.insert(lhs.begin(), lhs.end(), newRuleID);
   if (oldRuleID) {
     llvm::errs() << "Duplicate rewrite rule!\n";
-    const auto &oldRule = Rules[*oldRuleID];
+    const auto &oldRule = getRule(*oldRuleID);
     llvm::errs() << "Old rule #" << *oldRuleID << ": ";
     oldRule.dump(llvm::errs());
     llvm::errs() << "\nTrying to replay what happened when I simplified this term:\n";
@@ -116,11 +174,18 @@ bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs) {
 }
 
 /// Reduce a term by applying all rewrite rules until fixed point.
-bool RewriteSystem::simplify(MutableTerm &term) const {
+///
+/// If \p path is non-null, records the series of rewrite steps taken.
+bool RewriteSystem::simplify(MutableTerm &term, RewritePath *path) const {
   bool changed = false;
 
+  MutableTerm original;
+  RewritePath forDebug;
   if (Debug.contains(DebugFlags::Simplify)) {
-    llvm::dbgs() << "= Term " << term << "\n";
+
+    original = term;
+    if (!path)
+      path = &forDebug;
   }
 
   while (true) {
@@ -131,19 +196,16 @@ bool RewriteSystem::simplify(MutableTerm &term) const {
     while (from < end) {
       auto ruleID = Trie.find(from, end);
       if (ruleID) {
-        const auto &rule = Rules[*ruleID];
+        const auto &rule = getRule(*ruleID);
         if (!rule.isDeleted()) {
-          if (Debug.contains(DebugFlags::Simplify)) {
-            llvm::dbgs() << "== Rule #" << *ruleID << ": " << rule << "\n";
-          }
-
           auto to = from + rule.getLHS().size();
           assert(std::equal(from, to, rule.getLHS().begin()));
 
           term.rewriteSubTerm(from, to, rule.getRHS());
 
-          if (Debug.contains(DebugFlags::Simplify)) {
-            llvm::dbgs() << "=== Result " << term << "\n";
+          if (path) {
+            unsigned offset = (unsigned)(from - term.begin());
+            path->add(RewriteStep(offset, *ruleID, /*inverse=*/false));
           }
 
           changed = true;
@@ -159,6 +221,17 @@ bool RewriteSystem::simplify(MutableTerm &term) const {
       break;
   }
 
+  if (Debug.contains(DebugFlags::Simplify)) {
+    if (changed) {
+      llvm::dbgs() << "= Simplified " << term << ": ";
+      forDebug.dump(llvm::dbgs(), original, *this);
+      llvm::dbgs() << "\n";
+    } else {
+      llvm::dbgs() << "= Irreducible term: " << term << "\n";
+    }
+  }
+
+  assert(path == nullptr || changed != path->empty());
   return changed;
 }
 
@@ -170,7 +243,7 @@ bool RewriteSystem::simplify(MutableTerm &term) const {
 /// rules is only valid to perform if the rewrite system is confluent.
 void RewriteSystem::simplifyRewriteSystem() {
   for (auto ruleID : indices(Rules)) {
-    auto &rule = Rules[ruleID];
+    auto &rule = getRule(ruleID);
     if (rule.isDeleted())
       continue;
 
@@ -186,11 +259,11 @@ void RewriteSystem::simplifyRewriteSystem() {
           continue;
 
         // Ignore other deleted rules.
-        if (Rules[*otherRuleID].isDeleted())
+        if (getRule(*otherRuleID).isDeleted())
           continue;
 
         if (Debug.contains(DebugFlags::Completion)) {
-          const auto &otherRule = Rules[ruleID];
+          const auto &otherRule = getRule(ruleID);
           llvm::dbgs() << "$ Deleting rule " << rule << " because "
                        << "its left hand side contains " << otherRule
                        << "\n";

lib/AST/RequirementMachine/RewriteSystem.h

@@ -31,6 +31,7 @@ namespace rewriting {
 
 class PropertyMap;
 class RewriteContext;
+class RewriteSystem;
 
 /// A rewrite rule that replaces occurrences of LHS with RHS.
 ///
@@ -78,6 +79,67 @@ class Rule final {
   }
 };
 
+/// Records the application of a rewrite rule to a term.
+struct RewriteStep {
+  /// The position within the term where the rule is being applied.
+  unsigned Offset : 16;
+
+  /// The index of the rule in the rewrite system.
+  unsigned RuleID : 15;
+
+  /// If false, the step replaces an occurrence of the rule's left hand side
+  /// with the right hand side. If true, vice versa.
+  unsigned Inverse : 1;
+
+  RewriteStep(unsigned offset, unsigned ruleID, bool inverse) {
+    Offset = offset;
+    assert(Offset == offset && "Overflow");
+    RuleID = ruleID;
+    assert(RuleID == ruleID && "Overflow");
+    Inverse = inverse;
+  }
+
+  void invert() {
+    Inverse = !Inverse;
+  }
+
+  void dump(llvm::raw_ostream &out,
+            MutableTerm &term,
+            const RewriteSystem &system) const;
+};
+
+/// Records a sequence of zero or more rewrite rules applied to a term.
+struct RewritePath {
+  SmallVector<RewriteStep, 3> Steps;
+
+  bool empty() const {
+    return Steps.empty();
+  }
+
+  void add(RewriteStep step) {
+    Steps.push_back(step);
+  }
+
+  // Horizontal composition of paths.
+  void append(RewritePath other) {
+    Steps.append(other.begin(), other.end());
+  }
+
+  decltype(Steps)::const_iterator begin() const {
+    return Steps.begin();
+  }
+
+  decltype(Steps)::const_iterator end() const {
+    return Steps.end();
+  }
+
+  void invert();
+
+  void dump(llvm::raw_ostream &out,
+            MutableTerm term,
+            const RewriteSystem &system) const;
+};
+
 /// A term rewrite system for working with types in a generic signature.
 ///
 /// Out-of-line methods are documented in RewriteSystem.cpp.
@@ -141,9 +203,22 @@ class RewriteSystem final {
 
   Symbol simplifySubstitutionsInSuperclassOrConcreteSymbol(Symbol symbol) const;
 
+  unsigned getRuleID(const Rule &rule) const {
+    assert((unsigned)(&rule - &*Rules.begin()) < Rules.size());
+    return (unsigned)(&rule - &*Rules.begin());
+  }
+
+  Rule &getRule(unsigned ruleID) {
+    return Rules[ruleID];
+  }
+
+  const Rule &getRule(unsigned ruleID) const {
+    return Rules[ruleID];
+  }
+
   bool addRule(MutableTerm lhs, MutableTerm rhs);
 
-  bool simplify(MutableTerm &term) const;
+  bool simplify(MutableTerm &term, RewritePath *path=nullptr) const;
 
   enum class CompletionResult {
     /// Confluent completion was computed successfully.

lib/AST/RequirementMachine/RewriteSystemCompletion.cpp

@@ -235,7 +235,7 @@ void RewriteSystem::processMergedAssociatedTypes() {
 
     // Look for conformance requirements on [P1:T] and [P2:T].
     auto visitRule = [&](unsigned ruleID) {
-      const auto &otherRule = Rules[ruleID];
+      const auto &otherRule = getRule(ruleID);
       const auto &otherLHS = otherRule.getLHS();
       if (otherLHS.size() == 2 &&
           otherLHS[1].getKind() == Symbol::Kind::Protocol) {
@@ -440,7 +440,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
 
     // For every rule, looking for other rules that overlap with this rule.
     for (unsigned i = 0, e = Rules.size(); i < e; ++i) {
-      const auto &lhs = Rules[i];
+      const auto &lhs = getRule(i);
       if (lhs.isDeleted())
         continue;
 
@@ -458,7 +458,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
           if (!CheckedOverlaps.insert(std::make_pair(i, j)).second)
             return;
 
-          const auto &rhs = Rules[j];
+          const auto &rhs = getRule(j);
           if (rhs.isDeleted())
             return;
 
@@ -497,7 +497,7 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
             if (Debug.contains(DebugFlags::Completion)) {
               llvm::dbgs() << "$ Trivially overlapping rules: (#" << i << ") ";
               llvm::dbgs() << lhs << "\n";
-              llvm::dbgs() << "                -vs- (#" << j << ") ";
+              llvm::dbgs() << "                          -vs- (#" << j << ") ";
               llvm::dbgs() << rhs << ":\n";
             }
           }