From dd96bb151b54a370af1df6c88432c7f9cf2ba9dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 3 Jul 2014 11:15:43 -0700 Subject: [PATCH] refactor(library/unifier): reduce the number unify procedure 'flavors' Signed-off-by: Leonardo de Moura --- src/library/tactic/apply_tactic.cpp | 2 +- src/library/unifier.cpp | 39 ++++++++--------------------- src/library/unifier.h | 21 ++++++---------- 3 files changed, 19 insertions(+), 43 deletions(-) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index f3b3bccff7..ddc5d2ca62 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -82,7 +82,7 @@ tactic apply_tactic(expr const & _e) { e = mk_app(e, meta); e_t = instantiate(binding_body(e_t), meta); } - lazy_list substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options()); + lazy_list substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), get_noop_unifier_plugin(), ios.get_options()); return map2(substs, [=](substitution const & subst) -> proof_state { name_generator new_ngen(ngen); type_checker tc(env, new_ngen.mk_child()); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 89c6f47437..7582522480 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1160,6 +1160,10 @@ struct unifier_fn { } }; +unifier_plugin get_noop_unifier_plugin() { + return [](constraint const &, name_generator const &) { return lazy_list(); }; // NOLINT +} + lazy_list unify(std::shared_ptr u) { return mk_lazy_list([=]() { auto s = u->next(); @@ -1180,19 +1184,8 @@ lazy_list unify(environment const & env, unsigned num_cs, constra return unify(env, num_cs, cs, ngen, p, get_unifier_use_exceptions(o), get_unifier_max_steps(o)); } -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception, unsigned max_steps) { - return unify(env, num_cs, cs, ngen, [](constraint const &, name_generator const &) { return lazy_list(); }, - use_exception, max_steps); -} - -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - options const & o) { - return unify(env, num_cs, cs, ngen, get_unifier_use_exceptions(o), get_unifier_max_steps(o)); -} - -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p, - substitution const & s, unsigned max_steps) { +lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, + unifier_plugin const & p, unsigned max_steps) { name_generator new_ngen(ngen); type_checker tc(env, new_ngen.mk_child()); if (!tc.is_def_eq(lhs, rhs)) @@ -1208,19 +1201,9 @@ lazy_list unify(environment const & env, expr const & lhs, expr co } } -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p, - substitution const & s, options const & o) { - return unify(env, lhs, rhs, ngen, p, s, get_unifier_max_steps(o)); -} - lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, - substitution const & s, unsigned max_steps) { - return unify(env, lhs, rhs, ngen, [](constraint const &, name_generator const &) { return lazy_list(); }, s, max_steps); -} - -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, - substitution const & s, options const & o) { - return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o)); + substitution const & s, unifier_plugin const & p, options const & o) { + return unify(env, lhs, rhs, ngen, s, p, get_unifier_max_steps(o)); } static int unify_simple(lua_State * L) { @@ -1343,14 +1326,14 @@ static int unify(lua_State * L) { environment const & env = to_environment(L, 1); if (is_expr(L, 2)) { if (nargs == 6 && is_substitution(L, 5)) - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_options(L, 6)); + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), get_noop_unifier_plugin(), to_options(L, 6)); else - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_unifier_plugin(L, 5), to_substitution(L, 6), to_options(L, 7)); + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_unifier_plugin(L, 6), to_options(L, 7)); } else { buffer cs; to_constraint_buffer(L, 2, cs); if (nargs == 4 && is_options(L, 4)) - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_options(L, 4)); + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), get_noop_unifier_plugin(), to_options(L, 4)); else r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4), to_options(L, 5)); } diff --git a/src/library/unifier.h b/src/library/unifier.h index 9d933041d4..4c92f4a12a 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -43,22 +43,15 @@ std::pair unify_simple(substitution const & s, const */ typedef std::function(constraint const &, name_generator const &)> unifier_plugin; +unifier_plugin get_noop_unifier_plugin(); + lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - unifier_plugin const & p, bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, + unifier_plugin const & p = get_noop_unifier_plugin(), bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); +lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, unifier_plugin const & p, options const & o); +lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s = substitution(), + unifier_plugin const & p = get_noop_unifier_plugin(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); +lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, unifier_plugin const & p, options const & o); -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - options const & o); -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p, - substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, - substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p, - substitution const & s, options const & o); -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, - substitution const & s, options const & o); class unifier_exception : public exception { justification m_jst;