From 160dc71cb5342b4c8d88f1f123de1296a048377e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jan 2014 17:20:35 -0800 Subject: [PATCH] refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 4 --- src/kernel/metavar.h | 12 +++++++-- src/kernel/type_checker.cpp | 41 ++++++++++++++---------------- src/kernel/type_checker.h | 17 ++++++------- src/library/tactic/proof_state.cpp | 2 +- 5 files changed, 38 insertions(+), 38 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 9070e4e6f..7f9c62d14 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -424,10 +424,6 @@ context metavar_env_cell::instantiate_metavars(context const & ctx) const { return context(new_entries.size(), new_entries.data()); } -metavar_env::metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) { - if (m_ptr) m_ptr->inc_ref(); -} - template bool cached_metavar_env_tpl::update(optional const & menv) { if (!menv) { diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index 507fe8cde..26a7635e4 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -206,8 +206,6 @@ class metavar_env { friend class metavar_env_cell; metavar_env_cell * m_ptr; explicit metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); } - friend class type_checker; - explicit metavar_env(ro_metavar_env const & s); public: metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); } metavar_env(name const & prefix):m_ptr(new metavar_env_cell(prefix)) { m_ptr->inc_ref(); } @@ -251,6 +249,16 @@ class ro_metavar_env { friend class metavar_env; metavar_env_cell * m_ptr; explicit ro_metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); } + friend class type_checker; + /* + \brief (Hack) The following two methods are used by the type_checker. Some methods + in the type checker only need read-only access when unification constraints are not + used. For these methods, we can relax the interface and accept a read-only metavariable + environment. However, the type checker internally uses the read-write version. So, + this constructor is a hack to workaround that. + */ + static optional const & to_rw(optional const & menv) { return reinterpret_cast const &>(menv); } + metavar_env const & to_rw() const { return reinterpret_cast(*this); } public: ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); } ro_metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 1e6362a7e..6ae10f17f 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -479,12 +479,12 @@ expr type_checker::infer_type(expr const & e, context const & ctx, optional & uc) { return m_ptr->infer_type(e, ctx, some_menv(menv), &uc); } -expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv) { - return m_ptr->infer_type(e, ctx, some_menv(menv), nullptr); -} expr type_checker::infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv) { // metavariable environment is not updated when unification constraints are not provided - return infer_type(e, ctx, metavar_env(menv)); + return infer_type(e, ctx, some_menv(menv.to_rw()), nullptr); +} +expr type_checker::infer_type(expr const & e, context const & ctx, optional const & menv) { + return infer_type(e, ctx, ro_metavar_env::to_rw(menv), nullptr); } expr type_checker::infer_type(expr const & e, context const & ctx) { return infer_type(e, ctx, none_menv(), nullptr); @@ -495,8 +495,9 @@ expr type_checker::check(expr const & e, context const & ctx, optional & uc) { return m_ptr->check(e, ctx, some_menv(menv), &uc); } -expr type_checker::check(expr const & e, context const & ctx, metavar_env const & menv) { - return m_ptr->check(e, ctx, some_menv(menv), nullptr); +expr type_checker::check(expr const & e, context const & ctx, ro_metavar_env const & menv) { + // metavariable environment is not updated when unification constraints are not provided + return check(e, ctx, some_menv(menv.to_rw()), nullptr); } expr type_checker::check(expr const & e, context const & ctx) { return check(e, ctx, none_menv(), nullptr); @@ -513,31 +514,27 @@ void type_checker::check_type(expr const & e, context const & ctx) { expr type_checker::ensure_pi(expr const & e, context const & ctx) { return m_ptr->ensure_pi(e, ctx); } -bool type_checker::is_proposition(expr const & e, context const & ctx, optional const & menv) { - return m_ptr->is_proposition(e, ctx, menv); +bool type_checker::is_proposition(expr const & e, context const & ctx, optional const & menv) { + return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv)); } bool type_checker::is_proposition(expr const & e, context const & ctx) { - return is_proposition(e, ctx, none_menv()); -} -bool type_checker::is_proposition(expr const & e, context const & ctx, metavar_env const & menv) { - return is_proposition(e, ctx, some_menv(menv)); + return is_proposition(e, ctx, none_ro_menv()); } bool type_checker::is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) { - // metavariable environment is not updated when unification constraints are not provided - return is_proposition(e, ctx, metavar_env(menv)); + return is_proposition(e, ctx, some_ro_menv(menv)); } -bool type_checker::is_flex_proposition(expr e, context ctx, optional const & menv) { +bool type_checker::is_flex_proposition(expr e, context ctx, optional const & menv) { while (is_pi(e)) { ctx = extend(ctx, abst_name(e), abst_domain(e)); e = abst_body(e); } return is_proposition(e, ctx, menv); } -bool type_checker::is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv) { - return is_flex_proposition(e, ctx, some_menv(menv)); +bool type_checker::is_flex_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) { + return is_flex_proposition(e, ctx, some_ro_menv(menv)); } bool type_checker::is_flex_proposition(expr const & e, context const & ctx) { - return is_flex_proposition(e, ctx, none_menv()); + return is_flex_proposition(e, ctx, none_ro_menv()); } void type_checker::clear() { m_ptr->clear(); } normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); } @@ -547,13 +544,13 @@ expr type_check(expr const & e, ro_environment const & env, context const & ctx bool is_convertible(expr const & given, expr const & expected, ro_environment const & env, context const & ctx) { return type_checker(env).is_convertible(given, expected, ctx); } -bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional const & menv) { +bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional const & menv) { return type_checker(env).is_proposition(e, ctx, menv); } -bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv) { - return is_proposition(e, env, ctx, some_menv(menv)); +bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, ro_metavar_env const & menv) { + return is_proposition(e, env, ctx, some_ro_menv(menv)); } bool is_proposition(expr const & e, ro_environment const & env, context const & ctx) { - return is_proposition(e, env, ctx, none_menv()); + return is_proposition(e, env, ctx, none_ro_menv()); } } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index f37cdc26d..8280580be 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -49,8 +49,8 @@ public: */ expr infer_type(expr const & e, context const & ctx, optional const & menv, buffer * new_constraints); expr infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer & new_constraints); - expr infer_type(expr const & e, context const & ctx, metavar_env const & menv); expr infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv); + expr infer_type(expr const & e, context const & ctx, optional const & menv); /** \brief Return the type of \c e in the context \c ctx. @@ -71,7 +71,7 @@ public: */ expr check(expr const & e, context const & ctx, optional const & menv, buffer * new_constraints); expr check(expr const & e, context const & ctx, metavar_env const & menv, buffer & new_constraints); - expr check(expr const & e, context const & ctx, metavar_env const & menv); + expr check(expr const & e, context const & ctx, ro_metavar_env const & menv); /** \brief Type check the given expression, and return the type of \c e in the context \c ctx. @@ -94,14 +94,13 @@ public: bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx = context()); /** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */ - bool is_proposition(expr const & e, context const & ctx, optional const & menv); - bool is_proposition(expr const & e, context const & ctx, metavar_env const & menv); + bool is_proposition(expr const & e, context const & ctx, optional const & menv); bool is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv); bool is_proposition(expr const & e, context const & ctx = context()); /** \brief Return true iff \c e is a proposition or is a Pi s.t. the range is a flex_proposition */ - bool is_flex_proposition(expr e, context ctx, optional const & menv); - bool is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv); + bool is_flex_proposition(expr e, context ctx, optional const & menv); + bool is_flex_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv); bool is_flex_proposition(expr const & e, context const & ctx = context()); /** \brief Return a Pi if \c e is convertible to Pi. Throw an exception otherwise. */ @@ -122,7 +121,7 @@ public: expr operator()(expr const & e, context const & ctx, metavar_env const & menv, buffer & new_constraints) { return infer_type(e, ctx, menv, new_constraints); } - expr operator()(expr const & e, context const & ctx, metavar_env const & menv) { + expr operator()(expr const & e, context const & ctx, ro_metavar_env const & menv) { return infer_type(e, ctx, menv); } expr operator()(expr const & e, context const & ctx = context()) { @@ -131,7 +130,7 @@ public: }; expr type_check(expr const & e, ro_environment const & env, context const & ctx = context()); bool is_convertible(expr const & t1, expr const & t2, ro_environment const & env, context const & ctx = context()); -bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional const & menv); -bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv); +bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional const & menv); +bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, ro_metavar_env const & menv); bool is_proposition(expr const & e, ro_environment const & env, context const & ctx = context()); } diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index ff3e6bb31..29db6a759 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -90,7 +90,7 @@ void proof_state::get_goal_names(name_set & r) const { } name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, optional const & menv) { - if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx, menv)) + if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx, to_ro_menv(menv))) return name("H"); else return n;