michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/unifier): reduce the number unify procedure 'flavors'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-03 11:15:43 -07:00
parent d63ccbcf94
commit dd96bb151b
3 changed files with 19 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/apply_tactic.cpp
View file

@ -82,7 +82,7 @@ tactic apply_tactic(expr const & _e) {
e = mk_app(e, meta); e = mk_app(e, meta);
e_t = instantiate(binding_body(e_t), meta); e_t = instantiate(binding_body(e_t), meta);
} }
lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options()); lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), get_noop_unifier_plugin(), ios.get_options());
return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state { return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
name_generator new_ngen(ngen); name_generator new_ngen(ngen);
type_checker tc(env, new_ngen.mk_child()); type_checker tc(env, new_ngen.mk_child());

39
src/library/unifier.cpp
View file

@ -1160,6 +1160,10 @@ struct unifier_fn {
} }
}; };
unifier_plugin get_noop_unifier_plugin() {
return [](constraint const &, name_generator const &) { return lazy_list<constraints>(); }; // NOLINT
}
lazy_list<substitution> unify(std::shared_ptr<unifier_fn> u) { lazy_list<substitution> unify(std::shared_ptr<unifier_fn> u) {
return mk_lazy_list<substitution>([=]() { return mk_lazy_list<substitution>([=]() {
auto s = u->next(); auto s = u->next();
@ -1180,19 +1184,8 @@ lazy_list<substitution> 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)); return unify(env, num_cs, cs, ngen, p, get_unifier_use_exceptions(o), get_unifier_max_steps(o));
} }
lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
bool use_exception, unsigned max_steps) { unifier_plugin const & p, unsigned max_steps) {
return unify(env, num_cs, cs, ngen, [](constraint const &, name_generator const &) { return lazy_list<constraints>(); },
use_exception, max_steps);
}
lazy_list<substitution> 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<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
substitution const & s, unsigned max_steps) {
name_generator new_ngen(ngen); name_generator new_ngen(ngen);
type_checker tc(env, new_ngen.mk_child()); type_checker tc(env, new_ngen.mk_child());
if (!tc.is_def_eq(lhs, rhs)) if (!tc.is_def_eq(lhs, rhs))
@ -1208,19 +1201,9 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
} }
} }
lazy_list<substitution> 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<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
substitution const & s, unsigned max_steps) { substitution const & s, unifier_plugin const & p, options const & o) {
return unify(env, lhs, rhs, ngen, [](constraint const &, name_generator const &) { return lazy_list<constraints>(); }, s, max_steps); return unify(env, lhs, rhs, ngen, s, p, get_unifier_max_steps(o));
}
lazy_list<substitution> 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));
} }
static int unify_simple(lua_State * L) { static int unify_simple(lua_State * L) {
@ -1343,14 +1326,14 @@ static int unify(lua_State * L) {
environment const & env = to_environment(L, 1); environment const & env = to_environment(L, 1);
if (is_expr(L, 2)) { if (is_expr(L, 2)) {
if (nargs == 6 && is_substitution(L, 5)) 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 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 { } else {
buffer<constraint> cs; buffer<constraint> cs;
to_constraint_buffer(L, 2, cs); to_constraint_buffer(L, 2, cs);
if (nargs == 4 && is_options(L, 4)) 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 else
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4), to_options(L, 5)); r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4), to_options(L, 5));
} }

21
src/library/unifier.h
View file

@ -43,22 +43,15 @@ std::pair<unify_status, substitution> unify_simple(substitution const & s, const
*/ */
typedef std::function<lazy_list<constraints>(constraint const &, name_generator const &)> unifier_plugin; typedef std::function<lazy_list<constraints>(constraint const &, name_generator const &)> unifier_plugin;
unifier_plugin get_noop_unifier_plugin();
lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, lazy_list<substitution> 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); unifier_plugin const & p = get_noop_unifier_plugin(), bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, unifier_plugin const & p, options const & o);
bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s = substitution(),
lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, unifier_plugin const & p = get_noop_unifier_plugin(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s,
unifier_plugin const & p, options const & o); unifier_plugin const & p, options const & o);
lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
options const & o);
lazy_list<substitution> 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<substitution> 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<substitution> 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<substitution> 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 { class unifier_exception : public exception {
justification m_jst; justification m_jst;