From 57035d31623bd11ccc6a254926c9b8d837f9ca9d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Sep 2015 13:31:42 -0700 Subject: [PATCH] feat(kernel/level,library/blast/expr): add universe level hash consing support in the kernel, simplify blast/expr even more --- src/kernel/expr.cpp | 6 ++++-- src/kernel/expr.h | 1 + src/kernel/level.cpp | 42 ++++++++++++++++++++++++++++++++------ src/kernel/level.h | 4 ++++ src/library/blast/expr.cpp | 42 ++++++++------------------------------ src/library/blast/expr.h | 23 +-------------------- 6 files changed, 55 insertions(+), 63 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 6feb4cf14..6a3dae107 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -307,10 +307,12 @@ expr_macro::~expr_macro() { LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, true); MK_THREAD_LOCAL_GET_DEF(expr_struct_set, get_expr_cache); bool enable_expr_caching(bool f) { - bool r = g_expr_cache_enabled; + bool r1 = enable_level_caching(f); + bool r2 = g_expr_cache_enabled; + lean_verify(r1 == r2); g_expr_cache_enabled = f; get_expr_cache().clear(); - return r; + return r2; } inline expr cache(expr const & e) { if (g_expr_cache_enabled) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 9845b9099..5f387f654 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -477,6 +477,7 @@ 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 { diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 9d067c028..d26c4a12a 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "util/safe_arith.h" #include "util/buffer.h" #include "util/rc.h" @@ -18,6 +19,8 @@ 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; } @@ -192,7 +195,7 @@ bool is_explicit(level const & l) { } level mk_succ(level const & l) { - return level(new level_succ(l)); + return cache(level(new level_succ(l))); } /** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */ @@ -230,7 +233,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 level(new level_max_core(false, l1, l2)); + return cache(level(new level_max_core(false, l1, l2))); } } } @@ -245,12 +248,12 @@ level mk_imax(level const & l1, level const & l2) { else if (l1 == l2) return l1; // imax u u = u else - return level(new level_max_core(true, l1, l2)); + return cache(level(new level_max_core(true, l1, l2))); } -level mk_param_univ(name const & n) { return level(new level_param_core(level_kind::Param, n)); } -level mk_global_univ(name const & n) { return level(new level_param_core(level_kind::Global, n)); } -level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); } +level mk_param_univ(name const & n) { return cache(level(new level_param_core(level_kind::Param, n))); } +level mk_global_univ(name const & n) { return cache(level(new level_param_core(level_kind::Global, n))); } +level mk_meta_univ(name const & n) { return cache(level(new level_param_core(level_kind::Meta, n))); } static level * g_level_zero = nullptr; static level * g_level_one = nullptr; @@ -258,6 +261,33 @@ 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_table; +LEAN_THREAD_VALUE(bool, g_level_cache_enabled, true); +MK_THREAD_LOCAL_GET_DEF(level_table, get_level_cache); +bool enable_level_caching(bool f) { + bool r = g_level_cache_enabled; + g_level_cache_enabled = f; + get_level_cache().clear(); + get_level_cache().insert(mk_level_zero()); + get_level_cache().insert(mk_level_one()); + return r; +} +level cache(level const & e) { + if (g_level_cache_enabled) { + level_table & 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 7d44bc00a..251a02c59 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -79,6 +79,10 @@ 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); + level const & mk_level_zero(); level const & mk_level_one(); level mk_max(level const & l1, level const & l2); diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index e2953abd4..8e5b10003 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -19,54 +19,30 @@ Author: Leonardo de Moura namespace lean { namespace blast { -typedef typename std::unordered_set level_table; -typedef typename std::vector expr_array; - -LEAN_THREAD_PTR(level_table, g_level_table); +typedef typename std::vector expr_array; LEAN_THREAD_PTR(expr_array, g_var_array); LEAN_THREAD_PTR(expr_array, g_mref_array); LEAN_THREAD_PTR(expr_array, g_href_array); -scope_hash_consing::scope_hash_consing() { - lean_assert(g_level_table == nullptr); +scope_hash_consing::scope_hash_consing(): + scoped_expr_caching(true) { lean_assert(g_var_array == nullptr); lean_assert(g_mref_array == nullptr); lean_assert(g_href_array == nullptr); - g_level_table = new level_table(); g_var_array = new expr_array(); g_mref_array = new expr_array(); g_href_array = new expr_array(); - g_level_table->insert(lean::mk_level_zero()); - g_level_table->insert(lean::mk_level_one()); } scope_hash_consing::~scope_hash_consing() { - delete g_level_table; delete g_var_array; delete g_mref_array; delete g_href_array; - g_level_table = nullptr; g_var_array = nullptr; g_mref_array = nullptr; g_href_array = nullptr; } -#ifdef LEAN_DEBUG -static bool is_cached(level const & l) { - lean_assert(g_level_table); - return g_level_table->find(l) != g_level_table->end(); -} -#endif - -static level cache(level const & l) { - lean_assert(g_level_table); - auto r = g_level_table->find(l); - if (r != g_level_table->end()) - return *r; - g_level_table->insert(l); - return l; -} - level mk_level_zero() { return lean::mk_level_zero(); } @@ -78,30 +54,30 @@ level mk_level_one() { level mk_max(level const & l1, level const & l2) { lean_assert(is_cached(l1)); lean_assert(is_cached(l2)); - return cache(lean::mk_max(l1, l2)); + return lean::mk_max(l1, l2); } level mk_imax(level const & l1, level const & l2) { lean_assert(is_cached(l1)); lean_assert(is_cached(l2)); - return cache(lean::mk_max(l1, l2)); + return lean::mk_max(l1, l2); } level mk_succ(level const & l) { lean_assert(is_cached(l)); - return cache(lean::mk_succ(l)); + return lean::mk_succ(l); } level mk_param_univ(name const & n) { - return cache(lean::mk_param_univ(n)); + return lean::mk_param_univ(n); } level mk_global_univ(name const & n) { - return cache(lean::mk_global_univ(n)); + return lean::mk_global_univ(n); } level mk_meta_univ(name const & n) { - return cache(lean::mk_meta_univ(n)); + return lean::mk_meta_univ(n); } level update_succ(level const & l, level const & new_arg) { diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h index 103efba2f..2cb1150a9 100644 --- a/src/library/blast/expr.h +++ b/src/library/blast/expr.h @@ -20,7 +20,7 @@ namespace blast { // Auxiliary object for resetting the the thread local hash-consing tables. // It also uses an assertion to make sure it is not being used in a recursion. -class scope_hash_consing { +class scope_hash_consing : public scoped_expr_caching { public: scope_hash_consing(); ~scope_hash_consing(); @@ -81,8 +81,6 @@ bool has_local(expr const & e); level update_succ(level const & l, level const & new_arg); level update_max(level const & l, level const & new_lhs, level const & new_rhs); -level replace(level const & l, std::function(level const & l)> const & f); - expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); expr update_metavar(expr const & e, expr const & new_type); expr update_binding(expr const & e, expr const & new_domain, expr const & new_body); @@ -90,25 +88,6 @@ expr update_sort(expr const & e, level const & new_level); expr update_constant(expr const & e, levels const & new_levels); expr update_macro(expr const & e, unsigned num, expr const * args); -expr replace(expr const & e, std::function(expr const &, unsigned)> const & f); -inline expr replace(expr const & e, std::function(expr const &)> const & f) { - return blast::replace(e, [&](expr const & e, unsigned) { return f(e); }); -} - -expr lift_free_vars(expr const & e, unsigned s, unsigned d); -expr lift_free_vars(expr const & e, unsigned d); - -expr instantiate(expr const & e, unsigned n, expr const * s); -expr instantiate_rev(expr const & e, unsigned n, expr const * s); - -level instantiate(level const & l, level_param_names const & ps, levels const & ls); -expr instantiate_univ_params(expr const & e, level_param_names const & ps, levels const & ls); -expr instantiate_type_univ_params(declaration const & d, levels const & ls); -expr instantiate_value_univ_params(declaration const & d, levels const & ls); - -expr abstract_hrefs(expr const & e, unsigned n, expr const * s); -expr abstract_locals(expr const & e, unsigned n, expr const * s); - void initialize_expr(); void finalize_expr(); }