From aa3292eb364a5598889ca9428a4edce2e58ef88e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Sep 2018 20:50:53 -0700 Subject: [PATCH] feat(kernel/type_checker): remove `m_memoize` It is always `true` --- src/kernel/environment.cpp | 25 +++++++++---------- src/kernel/inductive.cpp | 2 +- src/kernel/type_checker.cpp | 37 +++++++++++------------------ src/kernel/type_checker.h | 10 ++++---- src/library/compiler/preprocess.cpp | 3 +-- 5 files changed, 31 insertions(+), 46 deletions(-) diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index acb84ba665..f36b234738 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -78,8 +78,7 @@ static void check_constant_val(environment const & env, constant_val const & v, } static void check_constant_val(environment const & env, constant_val const & v, bool non_meta_only) { - bool memoize = true; - type_checker checker(env, memoize, non_meta_only); + type_checker checker(env, non_meta_only); check_constant_val(env, v, checker); } @@ -96,14 +95,14 @@ environment environment::add_definition(declaration const & d, bool check) const /* Meta definition can be recursive. So, we check the header, add, and then type check the body. */ if (check) { - bool memoize = true; bool non_meta_only = false; - type_checker checker(*this, memoize, non_meta_only); + bool non_meta_only = false; + type_checker checker(*this, non_meta_only); check_constant_val(*this, v.to_constant_val(), checker); } environment new_env = add(constant_info(d)); if (check) { - bool memoize = true; bool non_meta_only = false; - type_checker checker(new_env, memoize, non_meta_only); + bool non_meta_only = false; + type_checker checker(new_env, non_meta_only); expr val_type = checker.check(v.get_value(), v.get_lparams()); if (!checker.is_def_eq(val_type, v.get_type())) throw definition_type_mismatch_exception(new_env, d, val_type); @@ -111,8 +110,7 @@ environment environment::add_definition(declaration const & d, bool check) const return new_env; } else { if (check) { - bool memoize = true; - type_checker checker(*this, memoize); + type_checker checker(*this); check_constant_val(*this, v.to_constant_val(), checker); expr val_type = checker.check(v.get_value(), v.get_lparams()); if (!checker.is_def_eq(val_type, v.get_type())) @@ -126,8 +124,7 @@ environment environment::add_theorem(declaration const & d, bool check) const { theorem_val const & v = d.to_theorem_val(); if (check) { // TODO(Leo): we must add support for handling tasks here - bool memoize = true; - type_checker checker(*this, memoize); + type_checker checker(*this); check_constant_val(*this, v.to_constant_val(), checker); expr val_type = checker.check(v.get_value(), v.get_lparams()); if (!checker.is_def_eq(val_type, v.get_type())) @@ -140,8 +137,8 @@ environment environment::add_mutual(declaration const & d, bool check) const { definition_vals const & vs = d.to_definition_vals(); /* Check declarations header */ if (check) { - bool memoize = true; bool non_meta_only = false; - type_checker checker(*this, memoize, non_meta_only); + bool non_meta_only = false; + type_checker checker(*this, non_meta_only); for (definition_val const & v : vs) { if (!v.is_meta()) throw kernel_exception(*this, "invalid mutual definition, declaration is not tagged as meta"); @@ -155,8 +152,8 @@ environment environment::add_mutual(declaration const & d, bool check) const { } /* Check actual definitions */ if (check) { - bool memoize = true; bool non_meta_only = false; - type_checker checker(new_env, memoize, non_meta_only); + bool non_meta_only = false; + type_checker checker(new_env, non_meta_only); for (definition_val const & v : vs) { expr val_type = checker.check(v.get_value(), v.get_lparams()); if (!checker.is_def_eq(val_type, v.get_type())) diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index 8cd5f62ad9..93cbc9035e 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -116,7 +116,7 @@ public: to_buffer(decl.get_types(), m_ind_types); } - type_checker tc() { return type_checker(m_env, m_lctx, true, !m_is_meta); } + type_checker tc() { return type_checker(m_env, m_lctx, !m_is_meta); } /** Return type of the parameter at position `i` */ expr get_param_type(unsigned i) const { diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 1e068b7223..c98feb8a93 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -233,11 +233,9 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) { lean_assert(!has_loose_bvars(e)); check_system("type checker"); - if (m_memoize) { - auto it = m_infer_type_cache[infer_only].find(e); - if (it != m_infer_type_cache[infer_only].end()) - return it->second; - } + auto it = m_infer_type_cache[infer_only].find(e); + if (it != m_infer_type_cache[infer_only].end()) + return it->second; expr r; switch (e.kind()) { @@ -268,8 +266,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) { } } - if (m_memoize) - m_infer_type_cache[infer_only].insert(mk_pair(e, r)); + m_infer_type_cache[infer_only].insert(mk_pair(e, r)); return r; } @@ -368,11 +365,9 @@ expr type_checker::whnf_core(expr const & e) { } // check cache - if (m_memoize) { - auto it = m_whnf_core_cache.find(e); - if (it != m_whnf_core_cache.end()) - return it->second; - } + auto it = m_whnf_core_cache.find(e); + if (it != m_whnf_core_cache.end()) + return it->second; // do the actual work expr r; @@ -422,8 +417,7 @@ expr type_checker::whnf_core(expr const & e) { break; } - if (m_memoize) - m_whnf_core_cache.insert(mk_pair(e, r)); + m_whnf_core_cache.insert(mk_pair(e, r)); return r; } @@ -485,11 +479,9 @@ expr type_checker::whnf(expr const & e) { } // check cache - if (m_memoize) { - auto it = m_whnf_cache.find(e); - if (it != m_whnf_cache.end()) - return it->second; - } + auto it = m_whnf_cache.find(e); + if (it != m_whnf_cache.end()) + return it->second; expr t = e; while (true) { @@ -498,8 +490,7 @@ expr type_checker::whnf(expr const & e) { t = *next_t; } else { auto r = t1; - if (m_memoize) - m_whnf_cache.insert(mk_pair(e, r)); + m_whnf_cache.insert(mk_pair(e, r)); return r; } } @@ -800,9 +791,9 @@ bool type_checker::is_def_eq(expr const & t, expr const & s) { return r; } -type_checker::type_checker(environment const & env, local_ctx const & lctx, bool memoize, bool non_meta_only): +type_checker::type_checker(environment const & env, local_ctx const & lctx, bool non_meta_only): m_env(env), m_lctx(lctx), m_name_generator(*g_kernel_fresh), - m_memoize(memoize), m_non_meta_only(non_meta_only), m_lparams(nullptr) { + m_non_meta_only(non_meta_only), m_lparams(nullptr) { } type_checker::~type_checker() {} diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index f39975434a..5ad59d722b 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -32,7 +32,6 @@ class type_checker : public abstract_type_context { environment m_env; local_ctx m_lctx; name_generator m_name_generator; - bool m_memoize; bool m_non_meta_only; cache m_infer_type_cache[2]; expr_map m_whnf_core_cache; @@ -84,11 +83,10 @@ class type_checker : public abstract_type_context { expr check_ignore_undefined_universes(expr const & e); public: - /** \brief Create a type checker for the given environment. - memoize: if true, then inferred types are memoized/cached. */ - type_checker(environment const & env, local_ctx const & lctx, bool memoize = true, bool non_meta_only = true); - type_checker(environment const & env, bool memoize = true, bool non_meta_only = true): - type_checker(env, local_ctx(), memoize, non_meta_only) {} + /** \brief Create a type checker for the given environment. */ + type_checker(environment const & env, local_ctx const & lctx, bool non_meta_only = true); + type_checker(environment const & env, bool non_meta_only = true): + type_checker(env, local_ctx(), non_meta_only) {} ~type_checker(); virtual environment const & env() const { return m_env; } diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index 7d77fcf1b5..2b4a811fdf 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -170,9 +170,8 @@ class preprocess_fn { name_set m_decl_names; /* name of the functions being compiled */ bool check(constant_info const & d, expr const & v) { - bool memoize = true; bool non_meta_only = false; - type_checker tc(m_env, memoize, non_meta_only); + type_checker tc(m_env, non_meta_only); expr t = tc.check(v, d.get_lparams()); if (!tc.is_def_eq(d.get_type(), t)) throw exception("preprocess failed");