From efb9fb0802c3ae22d0e6f7b11b51db261237f41f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Apr 2018 10:55:05 -0700 Subject: [PATCH] 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 | 4 - src/frontends/lean/parser.cpp | 2 - src/kernel/expr.cpp | 158 ++---------------------------- src/kernel/expr.h | 12 --- src/kernel/level.cpp | 43 +------- src/kernel/level.h | 5 - src/kernel/type_checker.cpp | 1 - src/library/deep_copy.cpp | 2 - src/library/max_sharing.cpp | 2 - src/library/module.cpp | 1 - src/library/print.cpp | 1 - src/tests/kernel/expr.cpp | 7 -- src/tests/kernel/max_sharing.cpp | 9 +- 13 files changed, 17 insertions(+), 230 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a2c502ad34..f20dfabfa4 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 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 & es, bool check_unassigned, bool to_simple_metavar, bool collect_local_ctx) { - scoped_expr_caching scope(true); - flush_expr_cache(); name_map to_simple_mvar_cache; for (expr & e : es) { e = instantiate_mvars(e); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 26abc71aa6..e9da6d50ed 100644 --- a/src/frontends/lean/parser.cpp +++ b/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(); diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 309543bd81..f961d56a43 100644 --- a/src/kernel/expr.cpp +++ b/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_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 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)); } // ======================================= diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 29542180d2..36a1b63e7b 100644 --- a/src/kernel/expr.h +++ b/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(); // ======================================= // ======================================= diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 41e14c3b12..a672cd300d 100644 --- a/src/kernel/level.cpp +++ b/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_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(); } diff --git a/src/kernel/level.h b/src/kernel/level.h index 5d9f3983d8..36a8c8a88e 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -78,11 +78,6 @@ inline optional none_level() { return optional(); } inline optional some_level(level const & e) { return optional(e); } inline optional some_level(level && e) { return optional(std::forward(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); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index c9a8873de3..761accb55a 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -779,7 +779,6 @@ certified_declaration check(environment const & env, declaration const & d, bool auto checked_proof = map(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; diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index 0be5977749..683f1f1113 100644 --- a/src/library/deep_copy.cpp +++ b/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)); diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp index b3b34c7d2b..a2c04e77e3 100644 --- a/src/library/max_sharing.cpp +++ b/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); } diff --git a/src/library/module.cpp b/src/library/module.cpp index 798e16e591..d1ee19354c 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -659,7 +659,6 @@ std::shared_ptr 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(file_name)); object_readers & readers = get_object_readers(); unsigned obj_counter = 0; diff --git a/src/library/print.cpp b/src/library/print.cpp index fbe5b374eb..ec65d3e968 100644 --- a/src/library/print.cpp +++ b/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); } }; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 9f12ec840f..f1872b6b74 100644 --- a/src/tests/kernel/expr.cpp +++ b/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); diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp index 73f95d4872..2e6eeccaec 100644 --- a/src/tests/kernel/max_sharing.cpp +++ b/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();