RequirementMachine: Add machinery for recording concrete type witnesses

Author: slavapestov

lib/AST/RequirementMachine/PropertyUnification.cpp

@@ -650,6 +650,50 @@ void PropertyMap::concretizeTypeWitnessInConformance(
   }
 }
 
+RewriteSystem::ConcreteTypeWitness::ConcreteTypeWitness(
+    Symbol concreteConformance,
+    Symbol assocType,
+    Symbol concreteType)
+  : ConcreteConformance(concreteConformance),
+    AssocType(assocType),
+    ConcreteType(concreteType) {
+  assert(concreteConformance.getKind() == Symbol::Kind::ConcreteConformance);
+  assert(assocType.getKind() == Symbol::Kind::AssociatedType);
+  assert(concreteType.getKind() == Symbol::Kind::ConcreteType);
+  assert(assocType.getProtocols().size() == 1);
+  assert(assocType.getProtocols()[0] == concreteConformance.getProtocol());
+}
+
+bool swift::rewriting::operator==(
+    const RewriteSystem::ConcreteTypeWitness &lhs,
+    const RewriteSystem::ConcreteTypeWitness &rhs) {
+  return (lhs.ConcreteConformance == rhs.ConcreteConformance &&
+          lhs.AssocType == rhs.AssocType &&
+          lhs.ConcreteType == rhs.ConcreteType);
+}
+
+unsigned RewriteSystem::recordConcreteTypeWitness(
+    RewriteSystem::ConcreteTypeWitness witness) {
+  auto key = std::make_pair(witness.ConcreteConformance,
+                            witness.AssocType);
+  unsigned index = ConcreteTypeWitnesses.size();
+  auto inserted = ConcreteTypeWitnessMap.insert(std::make_pair(key, index));
+
+  if (!inserted.second) {
+    index = inserted.first->second;
+  } else {
+    ConcreteTypeWitnesses.push_back(witness);
+  }
+
+  assert(ConcreteTypeWitnesses[index] == witness);
+  return index;
+}
+
+const RewriteSystem::ConcreteTypeWitness &
+RewriteSystem::getConcreteTypeWitness(unsigned index) const {
+  return ConcreteTypeWitnesses[index];
+}
+
 /// Given the key of a property bag known to have \p concreteType,
 /// together with a \p typeWitness from a conformance on that concrete
 /// type, return the right hand side of a rewrite rule to relate

lib/AST/RequirementMachine/RewriteSystem.h

@@ -197,44 +197,6 @@ class RewriteSystem final {
   /// type is an index into the Rules array defined above.
   Trie<unsigned, MatchKind::Shortest> Trie;
 
-  /// Constructed from a rule of the form X.[P2:T] => X.[P1:T] by
-  /// checkMergedAssociatedType().
-  struct MergedAssociatedType {
-    /// The *right* hand side of the original rule, X.[P1:T].
-    Term rhs;
-
-    /// The associated type symbol appearing at the end of the *left*
-    /// hand side of the original rule, [P2:T].
-    Symbol lhsSymbol;
-
-    /// The merged associated type symbol, [P1&P2:T].
-    Symbol mergedSymbol;
-  };
-
-  /// A list of pending terms for the associated type merging completion
-  /// heuristic. Entries are added by checkMergedAssociatedType(), and
-  /// consumed in processMergedAssociatedTypes().
-  std::vector<MergedAssociatedType> MergedAssociatedTypes;
-
-  /// Pairs of rules which have already been checked for overlap.
-  llvm::DenseSet<std::pair<unsigned, unsigned>> CheckedOverlaps;
-
-  /// Homotopy generators for this rewrite system. These are the
-  /// rewrite loops which rewrite a term back to itself.
-  ///
-  /// In the category theory interpretation, a rewrite rule is a generating
-  /// 2-cell, and a rewrite path is a 2-cell made from a composition of
-  /// generating 2-cells.
-  ///
-  /// Homotopy generators, in turn, are 3-cells. The special case of a
-  /// 3-cell discovered during completion can be viewed as two parallel
-  /// 2-cells; this is actually represented as a single 2-cell forming a
-  /// loop around a base point.
-  ///
-  /// This data is used by the homotopy reduction and generating conformances
-  /// algorithms.
-  std::vector<RewriteLoop> Loops;
-
   DebugOptions Debug;
 
   /// Whether we've initialized the rewrite system with a call to initialize().
@@ -288,10 +250,6 @@ class RewriteSystem final {
     return Rules[ruleID];
   }
 
-  ArrayRef<RewriteLoop> getLoops() const {
-    return Loops;
-  }
-
   bool addRule(MutableTerm lhs, MutableTerm rhs,
                const RewritePath *path=nullptr);
 
@@ -309,6 +267,9 @@ class RewriteSystem final {
   ///
   //////////////////////////////////////////////////////////////////////////////
 
+  /// Pairs of rules which have already been checked for overlap.
+  llvm::DenseSet<std::pair<unsigned, unsigned>> CheckedOverlaps;
+
   std::pair<CompletionResult, unsigned>
   computeConfluentCompletion(unsigned maxIterations,
                              unsigned maxDepth);
@@ -325,21 +286,6 @@ class RewriteSystem final {
   void verifyRewriteRules(ValidityPolicy policy) const;
 
 private:
-  void recordRewriteLoop(RewriteLoop loop) {
-    if (!RecordLoops)
-      return;
-
-    Loops.push_back(loop);
-  }
-
-  void recordRewriteLoop(MutableTerm basepoint,
-                         RewritePath path) {
-    if (!RecordLoops)
-      return;
-
-    Loops.emplace_back(basepoint, path);
-  }
-
   bool
   computeCriticalPair(
       ArrayRef<Symbol>::const_iterator from,
@@ -348,16 +294,96 @@ class RewriteSystem final {
       std::vector<RewritePath> &paths,
       std::vector<RewriteLoop> &loops) const;
 
+  /// Constructed from a rule of the form X.[P2:T] => X.[P1:T] by
+  /// checkMergedAssociatedType().
+  struct MergedAssociatedType {
+    /// The *right* hand side of the original rule, X.[P1:T].
+    Term rhs;
+
+    /// The associated type symbol appearing at the end of the *left*
+    /// hand side of the original rule, [P2:T].
+    Symbol lhsSymbol;
+
+    /// The merged associated type symbol, [P1&P2:T].
+    Symbol mergedSymbol;
+  };
+
+  /// A list of pending terms for the associated type merging completion
+  /// heuristic. Entries are added by checkMergedAssociatedType(), and
+  /// consumed in processMergedAssociatedTypes().
+  std::vector<MergedAssociatedType> MergedAssociatedTypes;
+
   void processMergedAssociatedTypes();
 
   void checkMergedAssociatedType(Term lhs, Term rhs);
 
+  //////////////////////////////////////////////////////////////////////////////
+  ///
+  /// "Pseudo-rules" for the property map
+  ///
+  //////////////////////////////////////////////////////////////////////////////
+
+public:
+  struct ConcreteTypeWitness {
+    Symbol ConcreteConformance;
+    Symbol AssocType;
+    Symbol ConcreteType;
+
+    ConcreteTypeWitness(Symbol concreteConformance,
+                        Symbol assocType,
+                        Symbol concreteType);
+
+    friend bool operator==(const ConcreteTypeWitness &lhs,
+                           const ConcreteTypeWitness &rhs);
+  };
+
+private:
+  /// Cache for concrete type witnesses. The value in the map is an index
+  /// into the vector.
+  llvm::DenseMap<std::pair<Symbol, Symbol>, unsigned> ConcreteTypeWitnessMap;
+  std::vector<ConcreteTypeWitness> ConcreteTypeWitnesses;
+
+public:
+  unsigned recordConcreteTypeWitness(ConcreteTypeWitness witness);
+  const ConcreteTypeWitness &getConcreteTypeWitness(unsigned index) const;
+
   //////////////////////////////////////////////////////////////////////////////
   ///
   /// Homotopy reduction
   ///
   //////////////////////////////////////////////////////////////////////////////
 
+  /// Homotopy generators for this rewrite system. These are the
+  /// rewrite loops which rewrite a term back to itself.
+  ///
+  /// In the category theory interpretation, a rewrite rule is a generating
+  /// 2-cell, and a rewrite path is a 2-cell made from a composition of
+  /// generating 2-cells.
+  ///
+  /// Homotopy generators, in turn, are 3-cells. The special case of a
+  /// 3-cell discovered during completion can be viewed as two parallel
+  /// 2-cells; this is actually represented as a single 2-cell forming a
+  /// loop around a base point.
+  ///
+  /// This data is used by the homotopy reduction and generating conformances
+  /// algorithms.
+  std::vector<RewriteLoop> Loops;
+
+  void recordRewriteLoop(RewriteLoop loop) {
+    if (!RecordLoops)
+      return;
+
+    Loops.push_back(loop);
+  }
+
+  void recordRewriteLoop(MutableTerm basepoint,
+                         RewritePath path) {
+    if (!RecordLoops)
+      return;
+
+    Loops.emplace_back(basepoint, path);
+  }
+
   void propagateExplicitBits();
 
   bool
@@ -377,6 +403,10 @@ class RewriteSystem final {
       llvm::DenseSet<unsigned> &redundantConformances);
 
 public:
+  ArrayRef<RewriteLoop> getLoops() const {
+    return Loops;
+  }
+
   void minimizeRewriteSystem();
 
   bool hadError() const;