Expose max_sharing_fn object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/max_sharing.cpp

@@ -6,11 +6,11 @@ Author: Leonardo de Moura
 */
 #include <unordered_set>
 #include <vector>
-#include "expr.h"
+#include "max_sharing.h"
 
 namespace lean {
 
-class max_sharing_fn {
+struct max_sharing_fn::imp {
     struct expr_struct_eq { unsigned operator()(expr const & e1, expr const & e2) const { return e1 == e2; }};
     typedef typename std::unordered_set<expr, expr_hash, expr_struct_eq> expr_cache;
 
@@ -73,16 +73,20 @@ class max_sharing_fn {
         lean_unreachable();
         return a;
     }
-
-public:
     expr operator()(expr const & a) { return apply(a); }
 };
 
+
+max_sharing_fn::max_sharing_fn():m_imp(new imp) {}
+max_sharing_fn::~max_sharing_fn() {}
+expr max_sharing_fn::operator()(expr const & a) { return (*m_imp)(a); }
+void max_sharing_fn::clear() { m_imp->m_cache.clear(); }
+
 expr max_sharing(expr const & a) {
     if (a.raw()->max_shared())
         return a;
     else
-        return max_sharing_fn()(a);
+        return max_sharing_fn::imp()(a);
 }
 
 } // namespace lean

src/kernel/max_sharing.h

@@ -5,9 +5,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <memory>
 #include "expr.h"
 
 namespace lean {
+/**
+   \brief Functional object for creating expressions with maximally
+   shared sub-expressions.
+*/
+class max_sharing_fn {
+    struct imp;
+    friend expr max_sharing(expr const & a);
+    std::unique_ptr<imp> m_imp;
+public:
+    max_sharing_fn();
+    ~max_sharing_fn();
+
+    expr operator()(expr const & a);
+
+    /**
+       \brief Clear the cache.
+    */
+    void clear();
+};
+
+
 /**
    \brief The resultant expression is structurally identical to the input one, but
    it uses maximally shared sub-expressions.

src/tests/kernel/expr.cpp

@@ -292,6 +292,18 @@ void tst12() {
     lean_assert(count(F) == count(G));
 }
 
+void tst13() {
+    expr f  = constant("f");
+    expr v  = var(0);
+    expr a1 = max_sharing(f(v,v));
+    expr a2 = max_sharing(f(v,v));
+    lean_assert(!eqp(a1, a2));
+    lean_assert(a1 == a2);
+    max_sharing_fn M;
+    lean_assert(eqp(M(f(v,v)), M(f(v,v))));
+    lean_assert(eqp(M(a1), M(a2)));
+}
+
 int main() {
     continue_on_violation(true);
     std::cout << "sizeof(expr):      " << sizeof(expr) << "\n";
@@ -309,6 +321,7 @@ int main() {
     tst10();
     tst11();
     tst12();
+    tst13();
     std::cout << "done" << "\n";
     return has_violations() ? 1 : 0;
 }