chore(kernel): remove opportunistic hash consing support

It just adds extra complexity and is in conflict for our plans for
Lean4. Moreover, in our experiments it impacts negatively on
performance: master and lean4 branches. The negative impact has been
confirmed by @kha too.

src/frontends/lean/elaborator.cpp

@@ -3699,7 +3699,6 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
     }
 
     try {
-        scoped_expr_caching scope(true);
         vm_obj r = tactic_evaluator(m_ctx, m_opts, ref, /* allow_profiler */ true)(tactic, s);
         expr val;
         if (auto new_s = tactic::is_success(r)) {
@@ -3978,7 +3977,6 @@ static expr replace_with_simple_metavars(metavar_context mctx, name_map<expr> &
 
 expr elaborator::elaborate(expr const & e) {
     scoped_info_manager scope_infom(&m_info);
-    scoped_expr_caching scope_no_caching(false);
     expr r = visit(e,  none_expr());
     trace_elab_detail(tout() << "result before final checkpoint\n" << r << "\n";);
     synthesize();
@@ -4010,8 +4008,6 @@ expr_pair elaborator::elaborate_with_type(expr const & e, expr const & e_type) {
 
 void elaborator::finalize_core(sanitize_param_names_fn & S, buffer<expr> & es,
                                bool check_unassigned, bool to_simple_metavar, bool collect_local_ctx) {
-    scoped_expr_caching scope(true);
-    flush_expr_cache();
     name_map<expr> to_simple_mvar_cache;
     for (expr & e : es) {
         e = instantiate_mvars(e);

src/frontends/lean/parser.cpp

@@ -2529,8 +2529,6 @@ bool parser::parse_command_like() {
     init_scanner();
     m_error_since_last_cmd = false;
 
-    // We disable hash-consing while parsing to make sure the pos-info are correct.
-    scoped_expr_caching disable(false);
     scope_pos_info_provider scope1(*this);
 
     check_interrupted();

src/kernel/expr.cpp

@@ -374,177 +374,37 @@ expr_macro::~expr_macro() {}
 
 // =======================================
 // Constructors
-LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, false);
-typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_cache;
-/* CACHE_RESET: NO */
-MK_THREAD_LOCAL_GET_DEF(expr_cache, get_expr_cache);
 
-struct cache_expr_insert_fn {
-    expr_cache & m_cache;
-    cache_expr_insert_fn(expr_cache & c):m_cache(c) {}
-
-    expr insert_macro(expr const & e) {
-        buffer<expr> new_args;
-        bool updated = false;
-        unsigned num = macro_num_args(e);
-        for (unsigned i = 0; i < num; i++) {
-            expr const & arg = macro_arg(e, i);
-            new_args.push_back(insert(arg));
-            if (!is_eqp(arg, new_args.back()))
-                updated = true;
-        }
-        if (updated) {
-            char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
-            return expr(new (mem) expr_macro(*to_macro(e), new_args.data()));
-        } else {
-            return e;
-        }
-    }
-
-    expr insert_meta(expr const & e) {
-        expr new_type = insert(mlocal_type(e));
-        if (is_eqp(new_type, mlocal_type(e))) {
-            return e;
-        } else {
-            return expr(new expr_mlocal(*to_mlocal(e), new_type));
-        }
-    }
-
-    expr insert_local(expr const & e) {
-        expr new_type = insert(mlocal_type(e));
-        if (is_eqp(new_type, mlocal_type(e))) {
-            return e;
-        } else {
-            return expr(new expr_local(*to_local(e), new_type));
-        }
-    }
-
-    expr insert_constant(expr const & e) {
-        /* TODO(Leo): similar insert for levels */
-        return e;
-    }
-
-    expr insert_sort(expr const & e) {
-        /* TODO(Leo): similar insert for levels */
-        return e;
-    }
-
-    expr insert_app(expr const & e) {
-        expr new_fn  = insert(app_fn(e));
-        expr new_arg = insert(app_arg(e));
-        if (is_eqp(new_fn, app_fn(e)) && is_eqp(new_arg, app_arg(e))) {
-            return e;
-        } else {
-            return expr(new expr_app(*to_app(e), new_fn, new_arg));
-        }
-    }
-
-    expr insert_binding(expr const & e) {
-        expr new_domain = insert(binding_domain(e));
-        expr new_body   = insert(binding_body(e));
-        if (is_eqp(new_domain, binding_domain(e)) && is_eqp(new_body, binding_body(e))) {
-            return e;
-        } else {
-            return expr(new expr_binding(*to_binding(e), new_domain, new_body));
-        }
-    }
-
-    expr insert_let(expr const & e) {
-        expr new_type  = insert(let_type(e));
-        expr new_value = insert(let_value(e));
-        expr new_body  = insert(let_body(e));
-        if (is_eqp(new_type, let_type(e)) && is_eqp(new_value, let_value(e)) && is_eqp(new_body, let_body(e))) {
-            return e;
-        } else {
-            return expr(new expr_let(*to_let(e), new_type, new_value, new_body));
-        }
-        return e;
-    }
-
-    expr insert(expr const & e) {
-        auto it = m_cache.find(e);
-        if (it != m_cache.end()) {
-            return *it;
-        }
-        expr new_e;
-        switch (e.kind()) {
-        case expr_kind::Var:       new_e = e;                  break;
-        case expr_kind::Macro:     new_e = insert_macro(e);    break;
-        case expr_kind::Meta:      new_e = insert_meta(e);     break;
-        case expr_kind::Local:     new_e = insert_local(e);    break;
-        case expr_kind::Constant:  new_e = insert_constant(e); break;
-        case expr_kind::Sort:      new_e = insert_sort(e);     break;
-        case expr_kind::App:       new_e = insert_app(e);      break;
-        case expr_kind::Lambda:    new_e = insert_binding(e);  break;
-        case expr_kind::Pi:        new_e = insert_binding(e);  break;
-        case expr_kind::Let:       new_e = insert_let(e);      break;
-        }
-        m_cache.insert(new_e);
-        return new_e;
-    }
-
-    expr operator()(expr const & e) { return insert(e); }
-};
-
-inline expr cache(expr const & e) {
-    if (g_expr_cache_enabled)
-        return cache_expr_insert_fn(get_expr_cache())(e);
-    else
-        return e;
-}
-bool enable_expr_caching(bool f) {
-    DEBUG_CODE(bool r1 =) enable_level_caching(f);
-    bool r2 = g_expr_cache_enabled;
-    lean_assert(r1 == r2);
-    cache(mk_Prop());
-    cache(mk_Type());
-    if (f) {
-        clear_abstract_cache();
-        clear_instantiate_cache();
-    }
-    g_expr_cache_enabled = f;
-    return r2;
-}
-bool is_cached(expr const & e) {
-    return get_expr_cache().find(e) != get_expr_cache().end();
-}
-void flush_expr_cache() {
-    flush_level_cache();
-    expr_cache new_cache;
-    get_expr_cache().swap(new_cache);
-    clear_abstract_cache();
-    clear_instantiate_cache();
-}
 expr mk_var(unsigned idx, tag g) {
-    return cache(expr(new expr_var(idx, g)));
+    return expr(new expr_var(idx, g));
 }
 expr mk_constant(name const & n, levels const & ls, tag g) {
-    return cache(expr(new expr_const(n, ls, g)));
+    return expr(new expr_const(n, ls, g));
 }
 expr mk_macro(macro_definition const & m, unsigned num, expr const * args, tag g) {
     char * mem = new char[sizeof(expr_macro) + num*sizeof(expr const *)];
-    return cache(expr(new (mem) expr_macro(m, num, args, g)));
+    return expr(new (mem) expr_macro(m, num, args, g));
 }
 expr mk_metavar(name const & n, name const & pp_n, expr const & t, tag g) {
-    return cache(expr(new expr_mlocal(true, n, pp_n, t, g)));
+    return expr(new expr_mlocal(true, n, pp_n, t, g));
 }
 expr mk_metavar(name const & n, expr const & t, tag g) {
     return mk_metavar(n, n, t, g);
 }
 expr mk_local(name const & n, name const & pp_n, expr const & t, binder_info const & bi, tag g) {
-    return cache(expr(new expr_local(n, pp_n, t, bi, g)));
+    return expr(new expr_local(n, pp_n, t, bi, g));
 }
 expr mk_app(expr const & f, expr const & a, tag g) {
-    return cache(expr(new expr_app(f, a, g)));
+    return expr(new expr_app(f, a, g));
 }
 expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & i, tag g) {
-    return cache(expr(new expr_binding(k, n, t, e, i, g)));
+    return expr(new expr_binding(k, n, t, e, i, g));
 }
 expr mk_let(name const & n, expr const & t, expr const & v, expr const & b, tag g) {
-    return cache(expr(new expr_let(n, t, v, b, g)));
+    return expr(new expr_let(n, t, v, b, g));
 }
 expr mk_sort(level const & l, tag g) {
-    return cache(expr(new expr_sort(l, g)));
+    return expr(new expr_sort(l, g));
 }
 // =======================================
 

src/kernel/expr.h

@@ -516,18 +516,6 @@ inline expr mk_app(expr const & e1, expr const & e2, expr const & e3, expr const
 
 /** \brief Return application (...((f x_{n-1}) x_{n-2}) ... x_0) */
 expr mk_app_vars(expr const & f, unsigned n, tag g = nulltag);
-
-/** \brief Enable hash-consing (caching) for expressions (and universe levels) */
-bool enable_expr_caching(bool f);
-/** \brief Helper class for temporarily enabling/disabling expression caching */
-struct scoped_expr_caching {
-    bool m_old;
-    scoped_expr_caching(bool f) { m_old = enable_expr_caching(f); }
-    ~scoped_expr_caching() { enable_expr_caching(m_old); }
-};
-/** \brief Return true iff \c e is in the cache */
-bool is_cached(expr const & e);
-void flush_expr_cache();
 // =======================================
 
 // =======================================

src/kernel/level.cpp

@@ -19,8 +19,6 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
-level cache(level const & e);
-
 level_cell const & to_cell(level const & l) {
     return *l.m_ptr;
 }
@@ -180,7 +178,7 @@ bool is_explicit(level const & l) {
 }
 
 level mk_succ(level const & l) {
-    return cache(level(new level_succ(l)));
+    return level(new level_succ(l));
 }
 
 /** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
@@ -218,7 +216,7 @@ level mk_max(level const & l1, level const & l2)  {
             lean_assert(p1.second != p2.second);
             return p1.second > p2.second ? l1 : l2;
         } else {
-            return cache(level(new level_max_core(false, l1, l2)));
+            return level(new level_max_core(false, l1, l2));
         }
     }
 }
@@ -233,11 +231,11 @@ level mk_imax(level const & l1, level const & l2) {
     else if (l1 == l2)
         return l1;  // imax u u = u
     else
-        return cache(level(new level_max_core(true,  l1, l2)));
+        return level(new level_max_core(true,  l1, l2));
 }
 
-level mk_param_univ(name const & n)  { return cache(level(new level_param_core(level_kind::Param, n))); }
-level mk_meta_univ(name const & n)   { return cache(level(new level_param_core(level_kind::Meta, n))); }
+level mk_param_univ(name const & n)  { return level(new level_param_core(level_kind::Param, n)); }
+level mk_meta_univ(name const & n)   { return level(new level_param_core(level_kind::Meta, n)); }
 
 static level * g_level_zero = nullptr;
 static level * g_level_one  = nullptr;
@@ -245,37 +243,6 @@ level const & mk_level_zero() { return *g_level_zero; }
 level const & mk_level_one() { return *g_level_one; }
 bool is_one(level const & l) { return l == mk_level_one(); }
 
-typedef typename std::unordered_set<level, level_hash> level_cache;
-LEAN_THREAD_VALUE(bool, g_level_cache_enabled, false);
-/* CACHE_RESET: No */
-MK_THREAD_LOCAL_GET_DEF(level_cache, get_level_cache);
-bool enable_level_caching(bool f) {
-    bool r = g_level_cache_enabled;
-    g_level_cache_enabled = f;
-    get_level_cache().insert(mk_level_zero());
-    get_level_cache().insert(mk_level_one());
-    return r;
-}
-void flush_level_cache() {
-    level_cache new_cache;
-    get_level_cache().swap(new_cache);
-}
-level cache(level const & e) {
-    if (g_level_cache_enabled) {
-        level_cache & cache = get_level_cache();
-        auto it = cache.find(e);
-        if (it != cache.end()) {
-            return *it;
-        } else {
-            cache.insert(e);
-        }
-    }
-    return e;
-}
-bool is_cached(level const & e) {
-    return get_level_cache().find(e) != get_level_cache().end();
-}
-
 level::level():level(mk_level_zero()) {}
 level::level(level_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
 level::level(level const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }

src/kernel/level.h

@@ -78,11 +78,6 @@ inline optional<level> none_level() { return optional<level>(); }
 inline optional<level> some_level(level const & e) { return optional<level>(e); }
 inline optional<level> some_level(level && e) { return optional<level>(std::forward<level>(e)); }
 
-bool enable_level_caching(bool f);
-level cache(level const & l);
-bool is_cached(level const & l);
-void flush_level_cache();
-
 level const & mk_level_zero();
 level const & mk_level_one();
 level mk_max(level const & l1, level const & l2);

src/kernel/type_checker.cpp

@@ -779,7 +779,6 @@ certified_declaration check(environment const & env, declaration const & d, bool
             auto checked_proof =
                     map<expr>(d.get_value_task(),
                               [d, env, memoize, trusted_only] (expr const & val) -> expr {
-                                  scoped_expr_caching disable(false);
                                   type_checker checker(env, memoize, trusted_only);
                                   check_definition(env, d, checker);
                                   return val;

src/library/deep_copy.cpp

@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr copy(expr const & a) {
-    scoped_expr_caching scope(false);
     switch (a.kind()) {
     case expr_kind::Var:      return mk_var(var_idx(a));
     case expr_kind::Constant: return mk_constant(const_name(a), const_levels(a));
@@ -27,7 +26,6 @@ expr copy(expr const & a) {
 }
 
 expr deep_copy(expr const & e) {
-    scoped_expr_caching scope(false);
     return replace(e, [](expr const & e) {
             if (is_atomic(e))
                 return some_expr(copy(e));

src/library/max_sharing.cpp

@@ -96,8 +96,6 @@ struct max_sharing_fn::imp {
     }
 
     expr operator()(expr const & a) {
-        // we must disable approximate/opportunistic hash-consing used in the kernel
-        scoped_expr_caching disable(false);
         return apply(a);
     }
 

src/library/module.cpp

@@ -659,7 +659,6 @@ std::shared_ptr<loaded_module const> cache_preimported_env(
 modification_list parse_olean_modifications(std::string const & olean_code, std::string const & file_name) {
     modification_list ms;
     std::istringstream in(olean_code, std::ios_base::binary);
-    scoped_expr_caching enable_caching(false);
     deserializer d(in, optional<std::string>(file_name));
     object_readers & readers = get_object_readers();
     unsigned obj_counter = 0;

src/library/print.cpp

@@ -258,7 +258,6 @@ struct print_expr_fn {
     print_expr_fn(std::ostream & out):m_out(out) {}
 
     void operator()(expr const & e) {
-        scoped_expr_caching set(false);
         print(e);
     }
 };

src/tests/kernel/expr.cpp

@@ -51,10 +51,6 @@ static void tst1() {
     std::cout << mk_app(fa, a) << "\n";
     lean_assert(is_eqp(app_fn(fa), f));
     lean_assert(is_eqp(app_arg(fa), a));
-    {
-        scoped_expr_caching set(false);
-        lean_assert(!is_eqp(fa, mk_app(f, a)));
-    }
     lean_assert(mk_app(fa, a) == mk_app(f, a, a));
     std::cout << mk_app(fa, fa, fa) << "\n";
     std::cout << mk_lambda("x", ty, Var(0)) << "\n";
@@ -169,7 +165,6 @@ static void tst6() {
 }
 
 static void tst7() {
-    scoped_expr_caching set(false);
     expr f  = Const("f");
     expr v  = Var(0);
     expr a1 = max_sharing(mk_app(f, v, v));
@@ -255,7 +250,6 @@ static void tst11() {
 }
 
 static void tst12() {
-    scoped_expr_caching set(false);
     expr f  = Const("f");
     expr v  = Var(0);
     expr a1 = max_sharing(mk_app(f, v, v));
@@ -311,7 +305,6 @@ static void tst15() {
 }
 
 static void check_copy(expr const & e) {
-    scoped_expr_caching set(false);
     expr c = copy(e);
     lean_assert(!is_eqp(e, c));
     lean_assert(e == c);

src/tests/kernel/max_sharing.cpp

@@ -70,12 +70,9 @@ int main() {
     initialize_library_core_module();
     initialize_library_module();
     init_default_print_fn();
-    {
-        scoped_expr_caching set(false);
-        tst1();
-        tst2();
-        tst3();
-    }
+    tst1();
+    tst2();
+    tst3();
     finalize_library_module();
     finalize_library_core_module();
     finalize_kernel_module();