From 0e2b7973cfd9eb1d3d64eff7858347a0c385c587 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2013 15:49:32 -0800 Subject: [PATCH] feat(kernel/free_vars): improve has_free_vars function, it produces better results for expressions containing metavariables Signed-off-by: Leonardo de Moura --- src/kernel/free_vars.cpp | 43 +++++++++++++++++++++------------- src/kernel/free_vars.h | 32 ++++++++++++++++--------- src/tests/kernel/free_vars.cpp | 33 ++++++++++++++++++++++++++ 3 files changed, 81 insertions(+), 27 deletions(-) diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 94e31e2d0..ecec43f7b 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -233,9 +233,10 @@ unsigned free_var_range(expr const & e, metavar_env const & menv) { */ class has_free_var_in_range_fn { protected: - unsigned m_low; - unsigned m_high; - expr_cell_offset_set m_cached; + unsigned m_low; + unsigned m_high; + expr_cell_offset_set m_cached; + std::unique_ptr m_range_fn; bool apply(optional const & e, unsigned offset) { return e && apply(*e, offset); @@ -251,7 +252,10 @@ protected: case expr_kind::Type: case expr_kind::Value: return false; case expr_kind::MetaVar: - return true; + if (m_range_fn) + break; // it is not cheap + else + return true; // assume that any free variable can occur in the metavariable case expr_kind::Var: return var_idx(e) >= offset + m_low && var_idx(e) < offset + m_high; case expr_kind::App: case expr_kind::Eq: case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Let: @@ -276,9 +280,20 @@ protected: lean_assert(const_type(e)); result = apply(const_type(e), offset); break; - case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: + case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: // easy cases were already handled lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::MetaVar: { + lean_assert(m_range_fn); + unsigned R = (*m_range_fn)(e); + if (R > 0) { + unsigned max_fvar_idx = R - 1; + result = max_fvar_idx >= offset + m_low; + // Remark: Variable #0 may occur in \c e. + // So, we don't have to check the upper bound offset + m_high; + } + break; + } case expr_kind::App: result = std::any_of(begin_args(e), end_args(e), [=](expr const & arg){ return apply(arg, offset); }); break; @@ -301,31 +316,27 @@ protected: return result; } public: - has_free_var_in_range_fn(unsigned low, unsigned high): + has_free_var_in_range_fn(unsigned low, unsigned high, metavar_env const * menv): m_low(low), m_high(high) { lean_assert(low < high); + if (menv) + m_range_fn.reset(new free_var_range_fn(*menv)); } bool operator()(expr const & e) { return apply(e, 0); } }; -bool has_free_var(expr const & e, unsigned vidx) { - return has_free_var_in_range_fn(vidx, vidx+1)(e); +bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const * menv) { + return has_free_var_in_range_fn(low, high, menv)(e); } -bool has_free_var(expr const & e, unsigned low, unsigned high) { - return has_free_var_in_range_fn(low, high)(e); -} - -expr lower_free_vars(expr const & e, unsigned s, unsigned d) { +expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv) { lean_assert(s >= d); - lean_assert(!has_free_var(e, s-d, s)); + lean_assert(!has_free_var(e, s-d, s, menv)); auto f = [=](expr const & e, unsigned offset) -> expr { if (is_var(e) && var_idx(e) >= s + offset) { lean_assert(var_idx(e) >= offset + d); return mk_var(var_idx(e) - d); - } else if (is_metavar(e)) { - lean_unreachable(); // LCOV_EXCL_LINE } else { return e; } diff --git a/src/kernel/free_vars.h b/src/kernel/free_vars.h index 33611e484..9806effcc 100644 --- a/src/kernel/free_vars.h +++ b/src/kernel/free_vars.h @@ -36,26 +36,36 @@ class metavar_env; */ unsigned free_var_range(expr const & e, metavar_env const & menv); -/** - \brief Return true iff \c e contains the free variable (var i). -*/ -bool has_free_var(expr const & e, unsigned i); - /** \brief Return true iff \c e constains a free variable (var i) s.t. \c i in [low, high). \pre low < high + + \remark If menv != nullptr, then we use \c free_var_range to compute the free variables that may + occur in a metavariable. */ -bool has_free_var(expr const & e, unsigned low, unsigned high); +bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const * menv = nullptr); +inline bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv) { + return has_free_var(e, low, high, &menv); +} +/** + \brief Return true iff \c e contains the free variable (var i). +*/ +inline bool has_free_var(expr const & e, unsigned i, metavar_env const * menv = nullptr) { return has_free_var(e, i, i+1, menv); } /** - \brief Lower the free variables >= s in \c e by d. That is, a free variable (var i) s.t. + \brief Lower the free variables >= s in \c e by \c d. That is, a free variable (var i) s.t. i >= s is mapped into (var i-d). - \pre d > 0 - \pre !has_free_var(e, 0, d) + \pre s >= d + \pre !has_free_var(e, s-d, d, menv) + + \remark The parameter menv is only used for debugging purposes */ -expr lower_free_vars(expr const & e, unsigned s, unsigned d); -inline expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, d, d); } +expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const * menv = nullptr); +inline expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { + return lower_free_vars(e, s, d, &menv); +} +inline expr lower_free_vars(expr const & e, unsigned d, metavar_env const * menv = nullptr) { return lower_free_vars(e, d, d, menv); } /** \brief Lift free variables >= s in \c e by d. diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp index be4543153..f980c094b 100644 --- a/src/tests/kernel/free_vars.cpp +++ b/src/tests/kernel/free_vars.cpp @@ -106,11 +106,44 @@ static void tst4() { lean_assert_eq(fn(mk_let("x", Var(2), Var(1), Var(4))), 4); } +static void tst5() { + metavar_env menv; + expr m1 = menv.mk_metavar(); + expr f = Const("f"); + expr a = Const("a"); + expr b = Const("b"); + expr t = Const("t"); + expr x = Const("x"); + lean_assert(has_free_var(mk_lambda("x", t, f(Var(1))), 0, menv)); + lean_assert(!has_free_var(mk_lambda("x", t, f(Var(0))), 1, menv)); + lean_assert(!has_free_var(m1, 0, menv)); + lean_assert(!has_free_var(m1, 1, menv)); + context ctx; + ctx = extend(ctx, name("x"), Bool); + ctx = extend(ctx, name("y"), Bool); + expr m2 = menv.mk_metavar(ctx); + lean_assert(has_free_var(m2, 0, menv)); + lean_assert(has_free_var(m2, 1, menv)); + lean_assert(!has_free_var(m2, 2, menv)); + lean_assert(has_free_var(Fun({x, Bool}, m2), 0, menv)); + lean_assert(!has_free_var(Fun({x, Bool}, m2), 1, menv)); + lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 3), 0, Var(0))), 0, menv)); + lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 1), 0, Var(0))), 0, menv)); + lean_assert(!has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 1), 0, Var(0))), 1, menv)); + lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 1, 3, menv)); + lean_assert(!has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 2, 5, menv)); + lean_assert_eq(lower_free_vars(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 5, 3, menv), + Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0)))); + lean_assert_eq(lower_free_vars(Fun({x, Bool}, Var(6)(add_inst(add_lift(m2, 1, 2), 0, Var(0)))), 5, 3, menv), + Fun({x, Bool}, Var(3)(add_inst(add_lift(m2, 1, 2), 0, Var(0))))); +} + int main() { save_stack_info(); tst1(); tst2(); tst3(); tst4(); + tst5(); return has_violations() ? 1 : 0; }