From f5987b7bda3721babf48b63bbda2a47fc091e57d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Aug 2014 17:30:08 -0700 Subject: [PATCH] refactor(library/unifier): make it easier to add new options to the unifier Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 3 +- src/library/unifier.cpp | 84 ++++++++++++++++++----------- src/library/unifier.h | 29 +++++----- tests/lean/run/list_elab1.lean | 2 +- tests/lean/run/over_subst.lean | 2 - tests/lean/slow/list_elab2.lean | 22 ++++---- 7 files changed, 79 insertions(+), 65 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1384aba6e..afaacd70f 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1114,7 +1114,7 @@ public: lazy_list solve(constraint_seq const & cs) { buffer tmp; cs.linearize(tmp); - return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), true, ios().get_options()); + return unify(env(), tmp.size(), tmp.data(), m_ngen.mk_child(), unifier_config(ios().get_options(), true)); } static void collect_metavars(expr const & e, buffer & mvars) { diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index e0b894715..2293a2ea8 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -120,7 +120,8 @@ proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, } } list meta_lst = to_list(metas.begin(), metas.end()); - lazy_list substs = unify(env, t, e_t, ngen.mk_child(), relax_main_opaque, s.get_subst(), ios.get_options()); + lazy_list substs = unify(env, t, e_t, ngen.mk_child(), relax_main_opaque, s.get_subst(), + unifier_config(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 2e624192d..31e1581eb 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -27,13 +27,48 @@ Author: Leonardo de Moura #include "library/unifier_plugin.h" #include "library/kernel_bindings.h" +#ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS +#define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000 +#endif + +#ifndef LEAN_DEFAULT_UNIFIER_COMPUTATION +#define LEAN_DEFAULT_UNIFIER_COMPUTATION true +#endif + +#ifndef LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES +#define LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES false +#endif + namespace lean { static name g_unifier_max_steps {"unifier", "max_steps"}; RegisterUnsignedOption(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps"); unsigned get_unifier_max_steps(options const & opts) { return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); } -static name g_unifier_expensive {"unifier", "expensive"}; -RegisterBoolOption(g_unifier_expensive, LEAN_DEFAULT_UNIFIER_EXPENSIVE, "(unifier) enable/disable expensive (and more complete) procedure"); -bool get_unifier_expensive(options const & opts) { return opts.get_bool(g_unifier_expensive, LEAN_DEFAULT_UNIFIER_EXPENSIVE); } + +static name g_unifier_computation {"unifier", "computation"}; +RegisterBoolOption(g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION, + "(unifier) case-split on reduction/computational steps when solving flex-rigid constraints"); +bool get_unifier_computation(options const & opts) { return opts.get_bool(g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION); } + +static name g_unifier_expensive_classes {"unifier", "expensive_classes"}; +RegisterBoolOption(g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES, + "(unifier) use \"full\" higher-order unification when solving class instances"); +bool get_unifier_expensive_classes(options const & opts) { + return opts.get_bool(g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES); +} + +unifier_config::unifier_config(bool use_exceptions): + m_use_exceptions(use_exceptions), + m_max_steps(LEAN_DEFAULT_UNIFIER_MAX_STEPS), + m_computation(LEAN_DEFAULT_UNIFIER_COMPUTATION), + m_expensive_classes(LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES) { +} + +unifier_config::unifier_config(options const & o, bool use_exceptions): + m_use_exceptions(use_exceptions), + m_max_steps(get_unifier_max_steps(o)), + m_computation(get_unifier_computation(o)), + m_expensive_classes(get_unifier_expensive_classes(o)) { +} // If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where // l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args. @@ -256,10 +291,8 @@ struct unifier_fn { owned_map m_owned_map; // mapping from metavariable name m to delay factor of the choice constraint that owns m unifier_plugin m_plugin; type_checker_ptr m_tc[2]; - bool m_use_exception; //!< True if we should throw an exception when there are no more solutions. - unsigned m_max_steps; + unifier_config m_config; unsigned m_num_steps; - bool m_expensive; bool m_pattern; //!< If true, then only higher-order (pattern) matching is used bool m_first; //!< True if we still have to generate the first solution. unsigned m_next_assumption_idx; //!< Next assumption index. @@ -348,9 +381,9 @@ struct unifier_fn { unifier_fn(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, substitution const & s, - bool use_exception, unsigned max_steps, bool expensive): + unifier_config const & cfg): m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)), - m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0), m_expensive(expensive), m_pattern(false) { + m_config(cfg), m_num_steps(0), m_pattern(false) { m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false); m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true); m_next_assumption_idx = 0; @@ -363,8 +396,8 @@ struct unifier_fn { void check_system() { check_interrupted(); - if (m_num_steps > m_max_steps) - throw exception(sstream() << "unifier maximum number of steps (" << m_max_steps << ") exceeded, " << + if (m_num_steps > m_config.m_max_steps) + throw exception(sstream() << "unifier maximum number of steps (" << m_config.m_max_steps << ") exceeded, " << "the maximum number of steps can be increased by setting the option unifier.max_steps " << "(remark: the unifier uses higher order unification and unification-hints, which may trigger non-termination"); m_num_steps++; @@ -967,7 +1000,7 @@ struct unifier_fn { optional failure() { lean_assert(in_conflict()); - if (m_use_exception) + if (m_config.m_use_exceptions) throw unifier_exception(*m_conflict, m_subst); else return optional(); @@ -1805,7 +1838,7 @@ struct unifier_fn { lean_assert(!m_cnstrs.empty()); auto const * p = m_cnstrs.min(); unsigned cidx = p->second; - if (!m_expensive && cidx >= get_group_first_index(cnstr_group::ClassInstance)) + if (!m_config.m_expensive_classes && cidx >= get_group_first_index(cnstr_group::ClassInstance)) m_pattern = true; // use only higher-order (pattern) matching after we start processing class-instance constraints constraint c = p->first; // std::cout << "process_next: " << c << "\n"; @@ -1907,21 +1940,16 @@ lazy_list unify(std::shared_ptr u) { } lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception, unsigned max_steps, bool expensive) { - return unify(std::make_shared(env, num_cs, cs, ngen, substitution(), use_exception, max_steps, expensive)); -} - -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception, options const & o) { - return unify(env, num_cs, cs, ngen, use_exception, get_unifier_max_steps(o), get_unifier_expensive(o)); + unifier_config const & cfg) { + return unify(std::make_shared(env, num_cs, cs, ngen, substitution(), cfg)); } lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, - bool relax, substitution const & s, unsigned max_steps, bool expensive) { + bool relax, substitution const & s, unifier_config const & cfg) { substitution new_s = s; expr _lhs = new_s.instantiate(lhs); expr _rhs = new_s.instantiate(rhs); - auto u = std::make_shared(env, 0, nullptr, ngen, new_s, false, max_steps, expensive); + auto u = std::make_shared(env, 0, nullptr, ngen, new_s, cfg); constraint_seq cs; if (!u->m_tc[relax]->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) { return lazy_list(); @@ -1930,11 +1958,6 @@ 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, - bool relax, substitution const & s, options const & o) { - return unify(env, lhs, rhs, ngen, relax, s, get_unifier_max_steps(o), get_unifier_expensive(o)); -} - static int unify_simple(lua_State * L) { int nargs = lua_gettop(L); unify_status r; @@ -2055,18 +2078,19 @@ static int unify(lua_State * L) { environment const & env = to_environment(L, 1); if (is_expr(L, 2)) { if (nargs == 7) - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(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), lua_toboolean(L, 5), to_substitution(L, 6), + unifier_config(to_options(L, 7))); else if (nargs == 6) - r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6), options()); + r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5), to_substitution(L, 6)); else r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), lua_toboolean(L, 5)); } else { buffer cs; to_constraint_buffer(L, 2, cs); if (nargs == 4) - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), false, to_options(L, 4)); + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), unifier_config(to_options(L, 4))); else - r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), false, options()); + r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3)); } return push_substitution_seq_it(L, r); } diff --git a/src/library/unifier.h b/src/library/unifier.h index dd87862fd..568625d6e 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -15,17 +15,9 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/metavar.h" -#ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS -#define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000 -#endif - -#ifndef LEAN_DEFAULT_UNIFIER_EXPENSIVE -#define LEAN_DEFAULT_UNIFIER_EXPENSIVE false -#endif - namespace lean { unsigned get_unifier_max_steps(options const & opts); -bool get_unifier_unfold_opaque(options const & opts); +bool get_unifier_computation(options const & opts); bool is_simple_meta(expr const & e); expr mk_aux_metavar_for(name_generator & ngen, expr const & t); @@ -40,16 +32,19 @@ unify_status unify_simple(substitution & s, expr const & lhs, expr const & rhs, unify_status unify_simple(substitution & s, level const & lhs, level const & rhs, justification const & j); unify_status unify_simple(substitution & s, constraint const & c); +struct unifier_config { + bool m_use_exceptions; + unsigned m_max_steps; + bool m_computation; + bool m_expensive_classes; + unifier_config(bool use_exceptions = false); + explicit unifier_config(options const & o, bool use_exceptions = false); +}; + 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, - bool expensive = LEAN_DEFAULT_UNIFIER_EXPENSIVE); -lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception, options const & o); + unifier_config const & c = unifier_config()); lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, bool relax_main_opaque, - substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, - bool expensive = LEAN_DEFAULT_UNIFIER_MAX_STEPS); -lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, - bool relax_main_opaque, substitution const & s, options const & o); + substitution const & s = substitution(), unifier_config const & c = unifier_config()); /** The unifier divides the constraints in 8 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, FlexFlex, MaxDelayed diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean index 8da8526fa..ff34ad1bd 100644 --- a/tests/lean/run/list_elab1.lean +++ b/tests/lean/run/list_elab1.lean @@ -11,7 +11,7 @@ import data.nat using nat eq_proofs -set_option unifier.expensive true + inductive list (T : Type) : Type := | nil {} : list T | cons : T → list T → list T diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean index b53601068..52f49e121 100644 --- a/tests/lean/run/over_subst.lean +++ b/tests/lean/run/over_subst.lean @@ -27,7 +27,5 @@ end int using int using nat -set_option unifier.expensive true - theorem add_lt_left {a b : int} (H : a < b) (c : int) : c + a < c + b := subst (symm (add_assoc c a one)) (add_le_left H c) diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean index a56ff5f76..d2ac48987 100644 --- a/tests/lean/slow/list_elab2.lean +++ b/tests/lean/slow/list_elab2.lean @@ -12,14 +12,12 @@ import logic data.nat -- import congr -set_option unifier.expensive true using nat -- using congr using eq_proofs namespace list - -- Type -- ---- @@ -116,9 +114,9 @@ list_induction_on s assume H : length (concat s t) = length s + length t, calc length (concat (cons x s) t ) = succ (length (concat s t)) : refl _ - ... = succ (length s + length t) : { H } - ... = succ (length s) + length t : {symm (add_succ_left _ _)} - ... = length (cons x s) + length t : refl _) + ... = succ (length s + length t) : { H } + ... = succ (length s) + length t : {symm (add_succ_left _ _)} + ... = length (cons x s) + length t : refl _) -- Reverse -- ------- @@ -141,9 +139,9 @@ list_induction_on s assume H : reverse (concat l t) = concat (reverse t) (reverse l), calc reverse (concat (cons x l) t) = concat (reverse (concat l t)) (cons x nil) : refl _ - ... = concat (concat (reverse t) (reverse l)) (cons x nil) : { H } - ... = concat (reverse t) (concat (reverse l) (cons x nil)) : concat_assoc _ _ _ - ... = concat (reverse t) (reverse (cons x l)) : refl _) + ... = concat (concat (reverse t) (reverse l)) (cons x nil) : { H } + ... = concat (reverse t) (concat (reverse l) (cons x nil)) : concat_assoc _ _ _ + ... = concat (reverse t) (reverse (cons x l)) : refl _) -- -- add_rewrite length_nil length_cons @@ -153,9 +151,9 @@ list_induction_on l (refl _) assume H: reverse (reverse l') = l', show reverse (reverse (cons x l')) = cons x l', from calc - reverse (reverse (cons x l')) = + reverse (reverse (cons x l')) = concat (reverse (cons x nil)) (reverse (reverse l')) : {reverse_concat _ _} - ... = cons x l' : {H}) + ... = cons x l' : {H}) -- Append -- ------ @@ -173,7 +171,6 @@ list_induction_on l (refl _) assume P : append x l = concat l [x], P ▸ refl _) -set_option unifier.expensive false theorem append_eq_reverse_cons (x : T) (l : list T) : append x l = reverse (x :: reverse l) := list_induction_on l (calc @@ -187,7 +184,6 @@ list_induction_on l calc append x (y :: l') = (y :: l') ++ [ x ] : append_eq_concat _ _ ... = concat (reverse (reverse (y :: l'))) [ x ] : {symm (reverse_reverse _)} - ... = reverse (x :: (reverse (y :: l'))) : refl _) + ... = reverse (x :: (reverse (y :: l'))) : refl _) end end list -