feat(kernel/instantiate): make sure instantiate_type_univ_params and instantiate_value_univ_params caches are reset when we enable max-sharing

src/kernel/expr.cpp

@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
+#include "kernel/instantiate.h"
 
 #ifndef LEAN_INITIAL_EXPR_CACHE_CAPACITY
 #define LEAN_INITIAL_EXPR_CACHE_CAPACITY 1024*16
@@ -312,10 +313,13 @@ bool enable_expr_caching(bool f) {
     bool r1 = enable_level_caching(f);
     bool r2 = g_expr_cache_enabled;
     lean_verify(r1 == r2);
-    g_expr_cache_enabled = f;
     expr_cache new_cache;
     get_expr_cache().swap(new_cache);
-    clear_abstract_cache();
+    if (f) {
+        clear_abstract_cache();
+        clear_instantiate_cache();
+    }
+    g_expr_cache_enabled = f;
     return r2;
 }
 inline expr cache(expr const & e) {

src/kernel/instantiate.cpp

@@ -166,4 +166,9 @@ expr instantiate_value_univ_params(declaration const & d, levels const & ls) {
     cache.save(d, ls, r);
     return r;
 }
+
+void clear_instantiate_cache() {
+    get_type_univ_cache().clear();
+    get_value_univ_cache().clear();
+}
 }

src/kernel/instantiate.h

@@ -39,4 +39,9 @@ expr instantiate_type_univ_params(declaration const & d, levels const & ls);
     \pre d.get_num_univ_params() == length(ls)
 */
 expr instantiate_value_univ_params(declaration const & d, levels const & ls);
+
+/** \brief Clear thread local caches used by instantiate_value_univ_params and instantiate_type_univ_params.
+    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_instantiate_cache();
 }

src/kernel/instantiate_univ_cache.h

@@ -13,14 +13,19 @@ Author: Leonardo de Moura
 namespace lean {
 class instantiate_univ_cache {
     typedef std::tuple<declaration, levels, expr> entry;
+    unsigned                     m_capacity;
     std::vector<optional<entry>> m_cache;
 public:
-    instantiate_univ_cache(unsigned capacity) {
-        m_cache.resize(capacity);
+    instantiate_univ_cache(unsigned capacity):m_capacity(capacity) {
+        if (m_capacity == 0)
+            m_capacity++;
     }
 
     optional<expr> is_cached(declaration const & d, levels const & ls) {
-        unsigned idx = d.get_name().hash() % m_cache.size();
+        if (m_cache.empty())
+            return none_expr();
+        lean_assert(m_cache.size() == m_capacity);
+        unsigned idx = d.get_name().hash() % m_capacity;
         if (auto it = m_cache[idx]) {
             declaration d_c; levels ls_c; expr r_c;
             std::tie(d_c, ls_c, r_c) = *it;
@@ -35,8 +40,16 @@ public:
     }
 
     void save(declaration const & d, levels const & ls, expr const & r) {
+        if (m_cache.empty())
+            m_cache.resize(m_capacity);
+        lean_assert(m_cache.size() == m_capacity);
         unsigned idx = d.get_name().hash() % m_cache.size();
         m_cache[idx] = entry(d, ls, r);
     }
+
+    void clear() {
+        m_cache.clear();
+        lean_assert(m_cache.empty());
+    }
 };
 }