michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel/normalizer): normalizer only needs read access to metavariable environment

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-27 17:03:30 -08:00
parent 3b152d1a9e
commit 05b4d8411b
5 changed files with 42 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/kernel/metavar.cpp
View file

@ -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<metavar_env> const & menv) {
template<typename MEnv>
bool cached_metavar_env_tpl<MEnv>::update(optional<MEnv> const & menv) {
if (!menv) {
m_menv = none_menv();
m_menv = optional<MEnv>();
if (m_timestamp != 0) {
m_timestamp = 0;
return true;
@ -448,6 +449,8 @@ bool cached_metavar_env::update(optional<metavar_env> const & menv) {
}
}
}
template class cached_metavar_env_tpl<metavar_env>;
template class cached_metavar_env_tpl<ro_metavar_env>;
local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
if (n == 0)

36
src/kernel/metavar.h
View file

@ -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<ro_metavar_env> some_ro_menv(ro_metavar_env && e) { return optio
inline optional<ro_metavar_env> const & to_ro_menv(optional<metavar_env> const & menv) { return reinterpret_cast<optional<ro_metavar_env> 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<metavar_env> m_menv;
template<typename MEnv>
class cached_metavar_env_tpl {
optional<MEnv> 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<MEnv>(); 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<metavar_env> const & menv);
bool update(metavar_env const & menv) { return update(some(menv)); }
bool update(optional<MEnv> const & menv);
bool update(MEnv const & menv) { return update(optional<MEnv>(menv)); }
explicit operator bool() const { return static_cast<bool>(m_menv); }
optional<metavar_env> const & to_some_menv() const { return m_menv; }
optional<ro_metavar_env> 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<MEnv> 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<metavar_env> {
public:
optional<ro_metavar_env> const & to_some_ro_menv() const { return to_ro_menv(to_some_menv()); }
};
typedef cached_metavar_env_tpl<ro_metavar_env> cached_ro_metavar_env;
/**
\brief Apply the changes in \c lctx to \c a.
*/

16
src/kernel/normalizer.cpp
View file

@ -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<metavar_env> const & menv, bool unfold_opaque) {
expr operator()(expr const & e, context const & ctx, optional<ro_metavar_env> 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<unsigned>::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<metavar_env> const & menv, bool unfold_opaque) {
expr normalizer::operator()(expr const & e, context const & ctx, optional<ro_metavar_env> 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(); }

6
src/kernel/normalizer.h
View file

@ -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<metavar_env> 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<ro_metavar_env> 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();

2
src/kernel/type_checker.cpp
View file

@ -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))