diff --git a/src/library/hop_match.cpp b/src/library/hop_match.cpp index 546398590..a762cc52c 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; + name_map * m_name_subst; bool is_free_var(expr const & x, unsigned ctx_size) const { return is_var(x) && var_idx(x) >= ctx_size; @@ -296,6 +297,8 @@ class hop_match_fn { return true; } case expr_kind::Lambda: case expr_kind::Pi: + if (m_name_subst) + (*m_name_subst)[abst_name(p)] = abst_name(t); return match(abst_domain(p), abst_domain(t), ctx, ctx_size) && match(abst_body(p), abst_body(t), extend(ctx, abst_name(t), abst_domain(t)), ctx_size+1); @@ -306,15 +309,17 @@ class hop_match_fn { lean_unreachable(); } public: - hop_match_fn(buffer> & subst, optional const & env):m_subst(subst), m_env(env) {} + hop_match_fn(buffer> & subst, optional const & env, + name_map * name_subst):m_subst(subst), m_env(env), m_name_subst(name_subst) {} bool operator()(expr const & p, expr const & t) { return match(p, t, context(), 0); } }; -bool hop_match(expr const & p, expr const & t, buffer> & subst, optional const & env) { - return hop_match_fn(subst, env)(p, t); +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); } static int hop_match_core(lua_State * L, optional const & env) { diff --git a/src/library/hop_match.h b/src/library/hop_match.h index 089aac17c..7263669fc 100644 --- a/src/library/hop_match.h +++ b/src/library/hop_match.h @@ -28,8 +28,13 @@ 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 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 & env = 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 005a6ec29..e07d518af 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -64,6 +64,10 @@ Author: Leonardo de Moura #define LEAN_SIMPLIFIER_MEMOIZE true #endif +#ifndef LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES +#define LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES true +#endif + #ifndef LEAN_SIMPLIFIER_MAX_STEPS #define LEAN_SIMPLIFIER_MAX_STEPS std::numeric_limits::max() #endif @@ -79,6 +83,7 @@ static name g_simplifier_unfold {"simplifier", "unfold"}; static name g_simplifier_conditional {"simplifier", "conditional"}; static name g_simplifier_memoize {"simplifier", "memoize"}; static name g_simplifier_max_steps {"simplifier", "max_steps"}; +static name g_simplifier_preserve_binder_names {"simplifier", "preserve_binder_names"}; RegisterBoolOption(g_simplifier_proofs, LEAN_SIMPLIFIER_PROOFS, "(simplifier) generate proofs"); RegisterBoolOption(g_simplifier_contextual, LEAN_SIMPLIFIER_CONTEXTUAL, "(simplifier) contextual simplification"); @@ -89,6 +94,8 @@ RegisterBoolOption(g_simplifier_eval, LEAN_SIMPLIFIER_EVAL, "(simplifier) apply RegisterBoolOption(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD, "(simplifier) unfolds non-opaque definitions"); RegisterBoolOption(g_simplifier_conditional, LEAN_SIMPLIFIER_CONDITIONAL, "(simplifier) conditional rewriting"); RegisterBoolOption(g_simplifier_memoize, LEAN_SIMPLIFIER_MEMOIZE, "(simplifier) memoize/cache intermediate results"); +RegisterBoolOption(g_simplifier_preserve_binder_names, LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES, + "(simplifier) (try to) preserve binder names when applying higher-order rewrite rules"); RegisterUnsignedOption(g_simplifier_max_steps, LEAN_SIMPLIFIER_MAX_STEPS, "(simplifier) maximum number of steps"); bool get_simplifier_proofs(options const & opts) { return opts.get_bool(g_simplifier_proofs, LEAN_SIMPLIFIER_PROOFS); } @@ -100,6 +107,9 @@ bool get_simplifier_eval(options const & opts) { return opts.get_bool(g_simplifi bool get_simplifier_unfold(options const & opts) { return opts.get_bool(g_simplifier_unfold, LEAN_SIMPLIFIER_UNFOLD); } bool get_simplifier_conditional(options const & opts) { return opts.get_bool(g_simplifier_conditional, LEAN_SIMPLIFIER_CONDITIONAL); } bool get_simplifier_memoize(options const & opts) { return opts.get_bool(g_simplifier_memoize, LEAN_SIMPLIFIER_MEMOIZE); } +bool get_simplifier_preserve_binder_names(options const & opts) { + return opts.get_bool(g_simplifier_preserve_binder_names, LEAN_SIMPLIFIER_PRESERVE_BINDER_NAMES); +} unsigned get_simplifier_max_steps(options const & opts) { return opts.get_unsigned(g_simplifier_max_steps, LEAN_SIMPLIFIER_MAX_STEPS); } static name g_local("local"); @@ -145,6 +155,7 @@ class simplifier_cell::imp { unsigned m_next_idx; // index used to create fresh constants unsigned m_num_steps; // number of steps performed unsigned m_depth; // recursion depth + name_map m_name_subst; std::shared_ptr m_monitor; // Configuration @@ -157,6 +168,7 @@ class simplifier_cell::imp { bool m_unfold; bool m_conditional; bool m_memoize; + bool m_preserve_binder_names; unsigned m_max_steps; struct updt_rule_set { @@ -839,6 +851,29 @@ class simplifier_cell::imp { return true; } + struct rename_binder_names_fn : public replace_visitor { + name_map const & m_name_subst; + rename_binder_names_fn(name_map const & s):m_name_subst(s) {} + virtual expr visit_abst(expr const & e, context const & ctx) { + auto it = m_name_subst.find(abst_name(e)); + if (it != m_name_subst.end()) { + if (is_lambda(e)) + return replace_visitor::visit_abst(mk_lambda(it->second, abst_domain(e), abst_body(e)), ctx); + else + return replace_visitor::visit_abst(mk_pi(it->second, abst_domain(e), abst_body(e)), ctx); + } else { + return replace_visitor::visit_abst(e, ctx); + } + } + }; + + expr rename_binder_names(expr const & e, name_map const & name_subst) { + if (m_preserve_binder_names && !name_subst.empty()) + return rename_binder_names_fn(name_subst)(e); + else + return e; + } + /** \brief Given lhs and rhs s.t. lhs = rhs.m_expr with proof rhs.m_proof, this method applies rewrite rules, beta and evaluation to \c rhs.m_expr, @@ -856,12 +891,14 @@ class simplifier_cell::imp { unsigned num = rule.get_num_args(); subst.clear(); subst.resize(num); - if (hop_match(rule.get_lhs(), target, subst, optional(m_env))) { + m_name_subst.clear(); + if (hop_match(rule.get_lhs(), target, subst, optional(m_env), &m_name_subst)) { new_args.clear(); new_args.resize(num+1); if (found_all_args(num, subst, new_args)) { // easy case: all arguments found - new_rhs = instantiate(rule.get_rhs(), num, new_args.data() + 1); + expr rhs = rename_binder_names(rule.get_rhs(), m_name_subst); + new_rhs = instantiate(rhs, num, new_args.data() + 1); if (rule.is_permutation() && !is_lt(new_rhs, target, false)) return false; if (m_proofs_enabled) { @@ -879,7 +916,7 @@ class simplifier_cell::imp { // Conditional rewriting: we try to fill the missing // arguments by trying to find a proof for ones that are // propositions. - expr ceq = rule.get_ceq(); + expr ceq = rename_binder_names(rule.get_ceq(), m_name_subst); buffer & proof_args = new_args; proof_args.clear(); if (m_proofs_enabled) @@ -1452,6 +1489,7 @@ class simplifier_cell::imp { m_conditional = get_simplifier_conditional(o); m_memoize = get_simplifier_memoize(o); m_max_steps = get_simplifier_max_steps(o); + m_preserve_binder_names = get_simplifier_preserve_binder_names(o); } public: diff --git a/tests/lean/nnf.lean.expected.out b/tests/lean/nnf.lean.expected.out index 292466ccb..42aa46a61 100644 --- a/tests/lean/nnf.lean.expected.out +++ b/tests/lean/nnf.lean.expected.out @@ -5,4 +5,4 @@ Assumed: g ¬ (∀ x : ℕ, (∃ y : ℕ, p x y ∨ p (f x) (f y)) ∨ f 0 = 1) ====> -(∃ x : ℕ, (∀ x::1 : ℕ, ¬ p x x::1) ∧ (∀ x::1 : ℕ, ¬ p (f x) (f x::1))) ∧ ¬ f 0 = 1 +(∃ x : ℕ, (∀ y : ℕ, ¬ p x y) ∧ (∀ y : ℕ, ¬ p (f x) (f y))) ∧ ¬ f 0 = 1