From 24452289ddc3808b8c6ef2e5a0ad2872d109ba03 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Jan 2014 20:30:47 -0800 Subject: [PATCH] feat(library/simplifier): make sure the simplifier can handle meta-variables Signed-off-by: Leonardo de Moura --- src/kernel/free_vars.cpp | 7 +++- src/kernel/free_vars.h | 1 + src/library/hop_match.cpp | 30 +++++++++----- src/library/hop_match.h | 4 ++ src/library/simplifier/simplifier.cpp | 54 +++++++++++++------------- src/library/simplifier/simplifier.h | 9 ++++- src/library/tactic/simplify_tactic.cpp | 2 +- 7 files changed, 68 insertions(+), 39 deletions(-) diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp index 51da33d80..f3e1b0adb 100644 --- a/src/kernel/free_vars.cpp +++ b/src/kernel/free_vars.cpp @@ -365,7 +365,12 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metav return (d && has_free_var(*d, low, high, menv)) || (b && has_free_var(*b, low, high, menv)); } -bool has_free_var_ge(expr const & e, unsigned low, ro_metavar_env const & menv) { return has_free_var(e, low, std::numeric_limits::max(), menv); } +bool has_free_var_ge(expr const & e, unsigned low, ro_metavar_env const & menv) { + return has_free_var(e, low, std::numeric_limits::max(), menv); +} +bool has_free_var_ge(expr const & e, unsigned low, optional const & menv) { + return has_free_var(e, low, std::numeric_limits::max(), menv); +} bool has_free_var_ge(expr const & e, unsigned low) { return has_free_var(e, low, std::numeric_limits::max()); } expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional const & DEBUG_CODE(menv)) { diff --git a/src/kernel/free_vars.h b/src/kernel/free_vars.h index 2c8c537a5..c1ee05dae 100644 --- a/src/kernel/free_vars.h +++ b/src/kernel/free_vars.h @@ -64,6 +64,7 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metav occur in a metavariable. */ bool has_free_var_ge(expr const & e, unsigned low, ro_metavar_env const & menv); +bool has_free_var_ge(expr const & e, unsigned low, optional const & menv); bool has_free_var_ge(expr const & e, unsigned low); /** diff --git a/src/library/hop_match.cpp b/src/library/hop_match.cpp index a762cc52c..088e160be 100644 --- a/src/library/hop_match.cpp +++ b/src/library/hop_match.cpp @@ -21,6 +21,7 @@ class hop_match_fn { buffer> & m_subst; buffer m_vars; optional m_env; + optional m_menv; name_map * m_name_subst; bool is_free_var(expr const & x, unsigned ctx_size) const { @@ -31,6 +32,13 @@ class hop_match_fn { return is_var(x) && var_idx(x) < ctx_size; } + expr lift_free_vars(expr const & e, unsigned d) const { return ::lean::lift_free_vars(e, d, m_menv); } + expr lower_free_vars(expr const & e, unsigned s, unsigned d) const { return ::lean::lower_free_vars(e, s, d, m_menv); } + bool has_free_var(expr const & e, unsigned i) const { return ::lean::has_free_var(e, i, m_menv); } + bool has_free_var(expr const & e, unsigned low, unsigned high) const { return ::lean::has_free_var(e, low, high, m_menv); } + expr apply_beta(expr f, unsigned num_args, expr const * args) const { return ::lean::apply_beta(f, num_args, args, m_menv); } + bool has_free_var_ge(expr const & e, unsigned low) const { return ::lean::has_free_var_ge(e, low, m_menv); } + optional get_subst(expr const & x, unsigned ctx_size) const { lean_assert(is_free_var(x, ctx_size)); unsigned vidx = var_idx(x) - ctx_size; @@ -180,7 +188,7 @@ class hop_match_fn { for_each(p, [&](expr const & v, unsigned offset) { if (!result) return false; - if (is_var(v) && is_free_var(v, ctx_size + offset) && !get_subst(v, ctx_size + offset)) { + if (is_var(v) && this->is_free_var(v, ctx_size + offset) && !get_subst(v, ctx_size + offset)) { result = false; } return true; @@ -201,7 +209,7 @@ class hop_match_fn { if (m_ref.is_free_var(x, real_ctx_sz)) { optional r = m_ref.get_subst(x, real_ctx_sz); lean_assert(r); - return lift_free_vars(*r, real_ctx_sz); + return m_ref.lift_free_vars(*r, real_ctx_sz); } else { return x; } @@ -215,7 +223,7 @@ class hop_match_fn { for (unsigned i = 0; i < num_args(e); i++) new_args.push_back(visit(arg(e, i), ctx)); if (is_lambda(new_args[0])) - return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1); + return m_ref.apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1); else return mk_app(new_args); } else { @@ -310,7 +318,8 @@ class hop_match_fn { } public: hop_match_fn(buffer> & subst, optional const & env, - name_map * name_subst):m_subst(subst), m_env(env), m_name_subst(name_subst) {} + optional const & menv, name_map * name_subst): + m_subst(subst), m_env(env), m_menv(menv), m_name_subst(name_subst) {} bool operator()(expr const & p, expr const & t) { return match(p, t, context(), 0); @@ -318,8 +327,8 @@ public: }; bool hop_match(expr const & p, expr const & t, buffer> & subst, optional const & env, - name_map * name_subst) { - return hop_match_fn(subst, env, name_subst)(p, t); + optional const & menv, name_map * name_subst) { + return hop_match_fn(subst, env, menv, name_subst)(p, t); } static int hop_match_core(lua_State * L, optional const & env) { @@ -327,8 +336,11 @@ static int hop_match_core(lua_State * L, optional const & env) { expr p = to_expr(L, 1); expr t = to_expr(L, 2); int k = 0; - if (nargs >= 4) { - k = luaL_checkinteger(L, 4); + optional menv; + if (nargs >= 4 && !lua_isnil(L, 4)) + menv = to_metavar_env(L, 4); + if (nargs >= 5) { + k = luaL_checkinteger(L, 5); if (k < 0) throw exception("hop_match, arg #4 must be non-negative"); } else { @@ -336,7 +348,7 @@ static int hop_match_core(lua_State * L, optional const & env) { } buffer> subst; subst.resize(k); - if (hop_match(p, t, subst, env)) { + if (hop_match(p, t, subst, env, menv)) { lua_newtable(L); int i = 1; for (auto s : subst) { diff --git a/src/library/hop_match.h b/src/library/hop_match.h index 7263669fc..75f5b0f41 100644 --- a/src/library/hop_match.h +++ b/src/library/hop_match.h @@ -29,12 +29,16 @@ namespace lean { If an environment is provided, then a constant \c c matches a term \c t if \c c is definitionally equal to \c t. + If a metavariable environment is provided, then it is provided to lift/lower + free variables procedures to be able to minimize the size of the local context. + If name_subst is different from nullptr, then the procedure stores in name_subst a mapping for binder names. It maps the binder names used in the pattern \c p into the binder names used in \c t. */ bool hop_match(expr const & p, expr const & t, buffer> & subst, optional const & env = optional(), + optional const & menv = optional(), name_map * name_subst = nullptr); void open_hop_match(lua_State * L); } diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 662a41b27..441f3d0e6 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -156,6 +156,7 @@ class simplifier_cell::imp { unsigned m_num_steps; // number of steps performed unsigned m_depth; // recursion depth name_map m_name_subst; + cached_ro_metavar_env m_menv; std::shared_ptr m_monitor; // Configuration @@ -214,30 +215,22 @@ class simplifier_cell::imp { return mk_lambda(abst_name(abst), abst_domain(abst), new_body); } - bool is_proposition(expr const & e) { - return m_tc.is_proposition(e, m_ctx); - } - - bool is_convertible(expr const & t1, expr const & t2) { - return m_tc.is_convertible(t1, t2, m_ctx); - } - + bool is_proposition(expr const & e) { return m_tc.is_proposition(e, m_ctx, m_menv.to_some_menv()); } + bool is_convertible(expr const & t1, expr const & t2) { return m_tc.is_convertible(t1, t2, m_ctx, m_menv.to_some_menv()); } bool is_definitionally_equal(expr const & t1, expr const & t2) { - return m_tc.is_definitionally_equal(t1, t2, m_ctx); + return m_tc.is_definitionally_equal(t1, t2, m_ctx, m_menv.to_some_menv()); } - - expr infer_type(expr const & e) { - return m_tc.infer_type(e, m_ctx); - } - - expr ensure_pi(expr const & e) { - return m_tc.ensure_pi(e, m_ctx); - } - + expr infer_type(expr const & e) { return m_tc.infer_type(e, m_ctx, m_menv.to_some_menv()); } + expr ensure_pi(expr const & e) { return m_tc.ensure_pi(e, m_ctx, m_menv.to_some_menv()); } expr normalize(expr const & e) { normalizer & proc = m_tc.get_normalizer(); - return proc(e, m_ctx, true); + return proc(e, m_ctx, m_menv.to_some_menv(), true); } + expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); } + expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lower_free_vars(e, s, d, m_menv.to_some_menv()); } + expr instantiate(expr const & e, expr const & s) { return ::lean::instantiate(e, s, m_menv.to_some_menv()); } + expr instantiate(expr const & e, unsigned n, expr const * s) { return ::lean::instantiate(e, n, s, m_menv.to_some_menv()); } + expr head_beta_reduce(expr const & t) { return ::lean::head_beta_reduce(t, m_menv.to_some_menv()); } expr mk_fresh_const(expr const & type) { m_next_idx++; @@ -892,7 +885,8 @@ class simplifier_cell::imp { subst.clear(); subst.resize(num); m_name_subst.clear(); - if (hop_match(rule.get_lhs(), target, subst, optional(m_env), &m_name_subst)) { + if (hop_match(rule.get_lhs(), target, subst, optional(m_env), + m_menv.to_some_menv(), &m_name_subst)) { new_args.clear(); new_args.resize(num+1); if (found_all_args(num, subst, new_args)) { @@ -1508,8 +1502,10 @@ public: m_next_idx = 0; } - expr_pair operator()(expr const & e, context const & ctx) { + expr_pair operator()(expr const & e, context const & ctx, optional const & menv) { set_ctx(ctx); + if (m_menv.update(menv)) + m_cache.clear(); m_num_steps = 0; m_depth = 0; try { @@ -1526,7 +1522,9 @@ simplifier_cell::simplifier_cell(ro_environment const & env, options const & o, m_ptr(new imp(env, o, num_rs, rs, monitor)) { } -expr_pair simplifier_cell::operator()(expr const & e, context const & ctx) { return m_ptr->operator()(e, ctx); } +expr_pair simplifier_cell::operator()(expr const & e, context const & ctx, optional const & menv) { + return m_ptr->operator()(e, ctx, menv); +} void simplifier_cell::clear() { return m_ptr->m_cache.clear(); } unsigned simplifier_cell::get_depth() const { return m_ptr->m_depth; } context const & simplifier_cell::get_context() const { return m_ptr->m_ctx; } @@ -1551,17 +1549,19 @@ ro_simplifier::ro_simplifier(weak_ref const & r) { expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, unsigned num_rs, rewrite_rule_set const * rs, + optional const & menv, std::shared_ptr const & monitor) { - return simplifier(env, opts, num_rs, rs, monitor)(e, ctx); + return simplifier(env, opts, num_rs, rs, monitor)(e, ctx, menv); } expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, unsigned num_ns, name const * ns, + optional const & menv, std::shared_ptr const & monitor) { buffer rules; for (unsigned i = 0; i < num_ns; i++) rules.push_back(get_rewrite_rule_set(env, ns[i])); - return simplify(e, env, ctx, opts, num_ns, rules.data(), monitor); + return simplify(e, env, ctx, opts, num_ns, rules.data(), menv, monitor); } simplifier_stack_space_exception::simplifier_stack_space_exception():stack_space_exception("simplifier") {} @@ -1738,9 +1738,11 @@ static int simplifier_apply(lua_State * L) { int nargs = lua_gettop(L); expr_pair r; if (nargs == 2) - r = to_simplifier(L, 1)(to_expr(L, 2), context()); + r = to_simplifier(L, 1)(to_expr(L, 2), context(), none_ro_menv()); + else if (nargs == 3) + r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), none_ro_menv()); else - r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3)); + r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), some_ro_menv(to_metavar_env(L, 4))); push_expr(L, r.first); push_expr(L, r.second); return 2; diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h index 4de0f34a3..29102d174 100644 --- a/src/library/simplifier/simplifier.h +++ b/src/library/simplifier/simplifier.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "util/lua.h" #include "kernel/environment.h" +#include "kernel/metavar.h" #include "library/expr_pair.h" #include "library/simplifier/rewrite_rule_set.h" @@ -23,7 +24,7 @@ public: simplifier_cell(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, std::shared_ptr const & monitor); - expr_pair operator()(expr const & e, context const & ctx); + expr_pair operator()(expr const & e, context const & ctx, optional const & menv); void clear(); unsigned get_depth() const; @@ -41,7 +42,9 @@ public: std::shared_ptr const & monitor); simplifier_cell * operator->() const { return m_ptr.get(); } simplifier_cell & operator*() const { return *(m_ptr.get()); } - expr_pair operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); } + expr_pair operator()(expr const & e, context const & ctx, optional const & menv) { + return (*m_ptr)(e, ctx, menv); + } }; /** \brief Read only reference to simplifier object */ @@ -115,9 +118,11 @@ public: expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts, unsigned num_rs, rewrite_rule_set const * rs, + optional const & menv = none_ro_menv(), std::shared_ptr const & monitor = std::shared_ptr()); expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, unsigned num_ns, name const * ns, + optional const & menv = none_ro_menv(), std::shared_ptr const & monitor = std::shared_ptr()); void open_simplifier(lua_State * L); } diff --git a/src/library/tactic/simplify_tactic.cpp b/src/library/tactic/simplify_tactic.cpp index 81bff475d..d063f797b 100644 --- a/src/library/tactic/simplify_tactic.cpp +++ b/src/library/tactic/simplify_tactic.cpp @@ -52,7 +52,7 @@ static optional simplify_tactic(ro_environment const & env, io_stat } expr conclusion = g.get_conclusion(); - auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data()); + auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv)); expr new_conclusion = r.first; expr eq_proof = r.second; if (new_conclusion == g.get_conclusion())