From 05b4d8411b79afc7f8eeb5245ece3f1b2ac2f2cf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jan 2014 17:03:30 -0800 Subject: [PATCH] refactor(kernel/normalizer): normalizer only needs read access to metavariable environment Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 7 +++++-- src/kernel/metavar.h | 38 ++++++++++++++++++++++++------------- src/kernel/normalizer.cpp | 16 ++++++++-------- src/kernel/normalizer.h | 6 +++--- src/kernel/type_checker.cpp | 2 +- 5 files changed, 42 insertions(+), 27 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index ad7edea6d..9070e4e6f 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -428,9 +428,10 @@ metavar_env::metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } -bool cached_metavar_env::update(optional const & menv) { +template +bool cached_metavar_env_tpl::update(optional const & menv) { if (!menv) { - m_menv = none_menv(); + m_menv = optional(); if (m_timestamp != 0) { m_timestamp = 0; return true; @@ -448,6 +449,8 @@ bool cached_metavar_env::update(optional const & menv) { } } } +template class cached_metavar_env_tpl; +template class cached_metavar_env_tpl; local_context add_lift(local_context const & lctx, unsigned s, unsigned n) { if (n == 0) diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index fd5fa5970..507fe8cde 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -221,6 +221,7 @@ public: metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); } friend bool is_eqp(metavar_env const & menv1, metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; } friend bool operator==(metavar_env const & menv1, metavar_env const & menv2) { return is_eqp(menv1, menv2); } + typedef metavar_env_cell * ptr; }; SPECIALIZE_OPTIONAL_FOR_SMART_PTR(metavar_env) @@ -263,6 +264,7 @@ public: metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); } friend bool is_eqp(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; } friend bool operator==(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return is_eqp(menv1, menv2); } + typedef metavar_env_cell const * ptr; }; SPECIALIZE_OPTIONAL_FOR_SMART_PTR(ro_metavar_env) @@ -272,29 +274,39 @@ inline optional some_ro_menv(ro_metavar_env && e) { return optio inline optional const & to_ro_menv(optional const & menv) { return reinterpret_cast const &>(menv); } /** - \brief A cached weak reference to a metavariable environment + timestamp at the time of - the caching. This object may also cache optional references. + \brief Template for creating a cached reference to a metavariable + environment + timestamp at the time of the caching. This object may + also cache optional references. + + We use this template for cached_metavar_env and cached_ro_metavar_env */ -class cached_metavar_env { - optional m_menv; - unsigned m_timestamp; +template +class cached_metavar_env_tpl { + optional m_menv; + unsigned m_timestamp; public: - cached_metavar_env():m_timestamp(0) {} - void clear() { m_menv = none_menv(); m_timestamp = 0; } + cached_metavar_env_tpl():m_timestamp(0) {} + void clear() { m_menv = optional(); m_timestamp = 0; } /** \brief Updated the cached value with menv. Return true if menv is different from the the cached metavar_env, or if the timestamp is different. */ - bool update(optional const & menv); - bool update(metavar_env const & menv) { return update(some(menv)); } + bool update(optional const & menv); + bool update(MEnv const & menv) { return update(optional(menv)); } explicit operator bool() const { return static_cast(m_menv); } - optional const & to_some_menv() const { return m_menv; } - optional const & to_some_ro_menv() const { return to_ro_menv(m_menv); } - metavar_env operator*() const { return *m_menv; } - metavar_env_cell * operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); } + optional const & to_some_menv() const { return m_menv; } + MEnv operator*() const { return *m_menv; } + typename MEnv::ptr operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); } }; +class cached_metavar_env : public cached_metavar_env_tpl { +public: + optional const & to_some_ro_menv() const { return to_ro_menv(to_some_menv()); } +}; + +typedef cached_metavar_env_tpl cached_ro_metavar_env; + /** \brief Apply the changes in \c lctx to \c a. */ diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 4b3d6f2bb..965553755 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -78,7 +78,7 @@ class normalizer::imp { ro_environment::weak_ref m_env; context m_ctx; - cached_metavar_env m_menv; + cached_ro_metavar_env m_menv; cache m_cache; bool m_unfold_opaque; unsigned m_max_depth; @@ -87,11 +87,11 @@ class normalizer::imp { ro_environment env() const { return ro_environment(m_env); } expr instantiate(expr const & e, unsigned n, expr const * s) { - return ::lean::instantiate(e, n, s, m_menv.to_some_ro_menv()); + return ::lean::instantiate(e, n, s, m_menv.to_some_menv()); } expr add_lift(expr const & m, unsigned s, unsigned n) { - return ::lean::add_lift(m, s, n, m_menv.to_some_ro_menv()); + return ::lean::add_lift(m, s, n, m_menv.to_some_menv()); } expr lookup(value_stack const & s, unsigned i) { @@ -338,7 +338,7 @@ public: m_unfold_opaque = false; } - expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque) { + expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque) { if (m_unfold_opaque != unfold_opaque) m_cache.clear(); m_unfold_opaque = unfold_opaque; @@ -356,14 +356,14 @@ normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits::max()) {} normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} normalizer::~normalizer() {} -expr normalizer::operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque) { +expr normalizer::operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque) { return (*m_ptr)(e, ctx, menv, unfold_opaque); } -expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque) { - return operator()(e, ctx, some_menv(menv), unfold_opaque); +expr normalizer::operator()(expr const & e, context const & ctx, ro_metavar_env const & menv, bool unfold_opaque) { + return operator()(e, ctx, some_ro_menv(menv), unfold_opaque); } expr normalizer::operator()(expr const & e, context const & ctx, bool unfold_opaque) { - return operator()(e, ctx, none_menv(), unfold_opaque); + return operator()(e, ctx, none_ro_menv(), unfold_opaque); } void normalizer::clear() { m_ptr->clear(); } diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h index ebbc46fa7..5b19900b2 100644 --- a/src/kernel/normalizer.h +++ b/src/kernel/normalizer.h @@ -13,7 +13,7 @@ Author: Leonardo de Moura namespace lean { class environment; class options; -class metavar_env; +class ro_metavar_env; /** \brief Functional object for normalizing expressions */ class normalizer { class imp; @@ -24,8 +24,8 @@ public: normalizer(ro_environment const & env, options const & opts); ~normalizer(); - expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque = false); - expr operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque = false); + expr operator()(expr const & e, context const & ctx, optional const & menv, bool unfold_opaque = false); + expr operator()(expr const & e, context const & ctx, ro_metavar_env const & menv, bool unfold_opaque = false); expr operator()(expr const & e, context const & ctx = context(), bool unfold_opaque = false); void clear(); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 9276e1846..1e6362a7e 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -48,7 +48,7 @@ class type_checker::imp { expr lower_free_vars(expr const & e, unsigned s, unsigned n) { return ::lean::lower_free_vars(e, s, n, m_menv.to_some_ro_menv()); } expr instantiate_with_closed(expr const & e, expr const & v) { return ::lean::instantiate_with_closed(e, v, m_menv.to_some_ro_menv()); } expr instantiate(expr const & e, expr const & v) { return ::lean::instantiate(e, v, m_menv.to_some_ro_menv()); } - expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque); } + expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { return m_normalizer(e, ctx, m_menv.to_some_ro_menv(), unfold_opaque); } expr check_type(expr const & e, expr const & s, context const & ctx) { if (is_type(e) || is_bool(e))