From 4ddd915886afbed698ca252d4f1698e08783a00b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Sep 2018 21:43:15 -0700 Subject: [PATCH] chore(kernel): remove dummy file --- src/kernel/expr.h | 7 ++++ src/kernel/expr_pair.h | 21 ---------- src/kernel/instantiate.cpp | 84 +++++++++++++++++++------------------- src/kernel/level.h | 1 + src/kernel/type_checker.h | 1 - src/library/expr_pair.h | 1 - 6 files changed, 50 insertions(+), 65 deletions(-) delete mode 100644 src/kernel/expr_pair.h diff --git a/src/kernel/expr.h b/src/kernel/expr.h index cc8b0352a5..ae7cfc3306 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -122,6 +122,7 @@ public: }; typedef list_ref exprs; +typedef pair expr_pair; inline serializer & operator<<(serializer & s, expr const & e) { e.serialize(s); return s; } inline serializer & operator<<(serializer & s, exprs const & es) { es.serialize(s); return s; } @@ -148,6 +149,12 @@ unsigned get_depth(expr const & e); unsigned get_loose_bvar_range(expr const & e); struct expr_hash { unsigned operator()(expr const & e) const { return hash(e); } }; +struct expr_pair_hash { + unsigned operator()(expr_pair const & p) const { return hash(hash(p.first), hash(p.second)); } +}; +struct expr_pair_eq { + bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; } +}; // ======================================= // Testers diff --git a/src/kernel/expr_pair.h b/src/kernel/expr_pair.h deleted file mode 100644 index c08f8dd0e2..0000000000 --- a/src/kernel/expr_pair.h +++ /dev/null @@ -1,21 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/expr.h" -namespace lean { -typedef pair level_pair; -typedef pair expr_pair; -/** \brief Functional object for hashing expression pairs. */ -struct expr_pair_hash { - unsigned operator()(expr_pair const & p) const { return hash(hash(p.first), hash(p.second)); } -}; - -/** \brief Functional object for comparing expression pairs. */ -struct expr_pair_eq { - bool operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; } -}; -} diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index adabf8000d..db6009cf38 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -16,48 +16,6 @@ Author: Leonardo de Moura #endif namespace lean { -class instantiate_univ_cache { - typedef std::tuple entry; - unsigned m_capacity; - std::vector> m_cache; -public: - instantiate_univ_cache(unsigned capacity):m_capacity(capacity) { - if (m_capacity == 0) - m_capacity++; - } - - optional is_cached(constant_info const & d, levels const & ls) { - 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]) { - constant_info info_c; levels ls_c; expr r_c; - std::tie(info_c, ls_c, r_c) = *it; - if (!is_eqp(info_c, d)) - return none_expr(); - if (ls == ls_c) - return some_expr(r_c); - else - return none_expr(); - } - return none_expr(); - } - - void save(constant_info 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()); - } -}; - template struct instantiate_easy_fn { unsigned n; @@ -178,6 +136,48 @@ expr instantiate_lparams(expr const & e, names const & lps, levels const & ls) { }); } +class instantiate_univ_cache { + typedef std::tuple entry; + unsigned m_capacity; + std::vector> m_cache; +public: + instantiate_univ_cache(unsigned capacity):m_capacity(capacity) { + if (m_capacity == 0) + m_capacity++; + } + + optional is_cached(constant_info const & d, levels const & ls) { + 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]) { + constant_info info_c; levels ls_c; expr r_c; + std::tie(info_c, ls_c, r_c) = *it; + if (!is_eqp(info_c, d)) + return none_expr(); + if (ls == ls_c) + return some_expr(r_c); + else + return none_expr(); + } + return none_expr(); + } + + void save(constant_info 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()); + } +}; + MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_CACHE_SIZE); MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE); diff --git a/src/kernel/level.h b/src/kernel/level.h index bfd9783855..da9ee0e251 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -73,6 +73,7 @@ public: }; typedef list_ref levels; +typedef pair level_pair; bool operator==(level const & l1, level const & l2); inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 5ad59d722b..26de303b35 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -14,7 +14,6 @@ Author: Leonardo de Moura #include "util/name_generator.h" #include "kernel/environment.h" #include "kernel/local_ctx.h" -#include "kernel/expr_pair.h" #include "kernel/expr_maps.h" #include "kernel/equiv_manager.h" #include "kernel/abstract_type_context.h" diff --git a/src/library/expr_pair.h b/src/library/expr_pair.h index 34e4ac1769..bbbf819ab4 100644 --- a/src/library/expr_pair.h +++ b/src/library/expr_pair.h @@ -7,7 +7,6 @@ Author: Leonardo de Moura #pragma once #include #include "util/hash.h" -#include "kernel/expr_pair.h" #include "library/expr_lt.h" namespace lean {