feat(kernel/abstract): make sure Pi/Fun cache is reset when we enable max-sharing

src/kernel/abstract.cpp

@@ -81,6 +81,11 @@ public:
     expr get_abstract_type(unsigned i) const {
         return *m_abstract_types[i];
     }
+
+    void clear() {
+        m_locals.clear();
+        m_abstract_types.clear();
+    }
 };
 
 MK_THREAD_LOCAL_GET_DEF(mk_binding_cache, get_mk_binding_cache);
@@ -105,4 +110,8 @@ expr mk_binding(unsigned num, expr const * locals, expr const & b, bool use_cach
 
 expr Pi(unsigned num, expr const * locals, expr const & b, bool use_cache) { return mk_binding<false>(num, locals, b, use_cache); }
 expr Fun(unsigned num, expr const * locals, expr const & b, bool use_cache) { return mk_binding<true>(num, locals, b, use_cache); }
+
+void clear_abstract_cache() {
+    get_mk_binding_cache().clear();
+}
 }

src/kernel/abstract.h

@@ -50,4 +50,9 @@ expr Pi(unsigned num, expr const * locals, expr const & b, bool use_cache = true
 inline expr Pi(expr const & local, expr const & b, bool use_cache = true) { return Pi(1, &local, b, use_cache); }
 inline expr Pi(std::initializer_list<expr> const & locals, expr const & b, bool use_cache = true) { return Pi(locals.size(), locals.begin(), b, use_cache); }
 template<typename T> expr Pi(T const & locals, expr const & b, bool use_cache = true) { return Pi(locals.size(), locals.data(), b, use_cache); }
+
+/** \brief Clear thread local caches used by Pi/Fun procedures
+    We clear the caches whenever we enable expression caching (aka max sharing).
+    We do that because the cache may still contain expressions that are not maximally shared. */
+void clear_abstract_cache();
 }

src/kernel/expr.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "kernel/expr_sets.h"
 #include "kernel/free_vars.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/abstract.h"
 
 #ifndef LEAN_INITIAL_EXPR_CACHE_CAPACITY
 #define LEAN_INITIAL_EXPR_CACHE_CAPACITY 1024*16
@@ -314,6 +315,7 @@ bool enable_expr_caching(bool f) {
     g_expr_cache_enabled = f;
     expr_cache new_cache;
     get_expr_cache().swap(new_cache);
+    clear_abstract_cache();
     return r2;
 }
 inline expr cache(expr const & e) {