From 8c8bf41e39f29b518f7a0afe83e8f43f08d88922 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 23 Nov 2014 19:03:39 -0800 Subject: [PATCH] feat(frontends/lean/server): do not unfold definitions in FINDG --- src/frontends/lean/server.cpp | 7 ++++- src/library/reducible.cpp | 9 +++++++ src/library/reducible.h | 3 +++ src/library/unifier.cpp | 48 +++++++++++++++++++++++------------ src/library/unifier.h | 3 +++ 5 files changed, 53 insertions(+), 17 deletions(-) diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 49895418b..fb720f8a0 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -760,6 +760,7 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type try { unifier_config cfg; cfg.m_max_steps = LEAN_FINDG_MAX_STEPS; + cfg.m_cheap = true; auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), true, substitution(), cfg); return static_cast(r.pull()); } catch (exception&) { @@ -767,6 +768,10 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type } } +static std::unique_ptr mk_find_goal_type_checker(environment const & env, name_generator const & ngen) { + return mk_opaque_type_checker(env, ngen); +} + static name * g_tmp_prefix = nullptr; void server::find_goal_matches(unsigned line_num, unsigned col_num, std::string const & filters) { buffer pos_names, neg_names; @@ -784,7 +789,7 @@ void server::find_goal_matches(unsigned line_num, unsigned col_num, std::string environment const & env = env_opts->first; options const & opts = env_opts->second; name_generator ngen(*g_tmp_prefix); - std::unique_ptr tc = mk_type_checker(env, ngen, true); + std::unique_ptr tc = mk_find_goal_type_checker(env, ngen); if (auto meta = m_file->infom().get_meta_at(line_num, col_num)) { if (is_meta(*meta)) { if (auto type = m_file->infom().get_type_at(line_num, col_num)) { diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp index 6e120214d..2fde76456 100644 --- a/src/library/reducible.cpp +++ b/src/library/reducible.cpp @@ -136,7 +136,16 @@ std::unique_ptr mk_type_checker(environment const & env, name_gene memoize, pred))); } } + std::unique_ptr mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible) { return mk_type_checker(env, name_generator(*g_tmp_prefix), relax_main_opaque, only_main_reducible); } + +std::unique_ptr mk_opaque_type_checker(environment const & env, name_generator const & ngen) { + extra_opaque_pred pred([=](name const &) { return true; }); // everything is opaque + bool relax_main_opaque = false; + bool memoize = true; + return std::unique_ptr(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque, + memoize, pred))); +} } diff --git a/src/library/reducible.h b/src/library/reducible.h index b915a8bf7..83a1f57a3 100644 --- a/src/library/reducible.h +++ b/src/library/reducible.h @@ -39,6 +39,9 @@ std::unique_ptr mk_type_checker(environment const & env, name_gene bool memoize = true); std::unique_ptr mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible = false); +/** \brief Create a type checker that treats all definitions as opaque. */ +std::unique_ptr mk_opaque_type_checker(environment const & env, name_generator const & ngen); + void initialize_reducible(); void finalize_reducible(); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 95295510f..1accb95cb 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -68,6 +68,7 @@ unifier_config::unifier_config(bool use_exceptions, bool discard): m_computation(LEAN_DEFAULT_UNIFIER_COMPUTATION), m_expensive_classes(LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES), m_discard(discard) { + m_cheap = false; } unifier_config::unifier_config(options const & o, bool use_exceptions, bool discard): @@ -76,6 +77,7 @@ unifier_config::unifier_config(options const & o, bool use_exceptions, bool disc m_computation(get_unifier_computation(o)), m_expensive_classes(get_unifier_expensive_classes(o)), m_discard(discard) { + m_cheap = false; } // If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where @@ -301,7 +303,7 @@ struct unifier_fn { typedef name_map name_to_cnstrs; typedef name_map owned_map; typedef rb_map, expr_quick_cmp> expr_map; - typedef std::unique_ptr type_checker_ptr; + typedef std::shared_ptr type_checker_ptr; environment m_env; name_generator m_ngen; substitution m_subst; @@ -419,11 +421,19 @@ struct unifier_fn { unifier_config const & cfg): m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)), m_config(cfg), m_num_steps(0), m_pattern(false) { - m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false); - m_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true); - if (!cfg.m_computation) { - m_flex_rigid_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, true); - m_flex_rigid_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true, true); + if (m_config.m_cheap) { + m_tc[0] = mk_opaque_type_checker(env, m_ngen.mk_child()); + m_tc[1] = m_tc[0]; + m_flex_rigid_tc[0] = m_tc[0]; + m_flex_rigid_tc[1] = m_tc[0]; + m_config.m_computation = false; + } else { + m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false); + m_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true); + if (!cfg.m_computation) { + m_flex_rigid_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, true); + m_flex_rigid_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true, true); + } } m_next_assumption_idx = 0; m_next_cidx = 0; @@ -1319,7 +1329,7 @@ struct unifier_fn { justification a; bool relax = relax_main_opaque(c); - if (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_reducible_on(m_env, d.get_name())) { + if (!m_config.m_cheap && (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_reducible_on(m_env, d.get_name()))) { // add case_split for t =?= s a = mk_assumption_justification(m_next_assumption_idx); add_case_split(std::unique_ptr(new delta_unfold_case_split(*this, j, c))); @@ -1380,6 +1390,8 @@ struct unifier_fn { optional _has_meta_args; + bool cheap() const { return u.m_config.m_cheap; } + type_checker & tc() { return *u.m_tc[relax]; } @@ -1545,6 +1557,8 @@ struct unifier_fn { if ((!is_local(marg) && !is_local(rhs)) || (is_meta(marg) && is_local(rhs))) { // if rhs is not local, then we only add projections for the nonlocal arguments of lhs mk_simple_nonlocal_projection(i); + if (cheap()) + return; } else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) { // if the argument is local, and rhs is equal to it, then we also add a projection constraint_seq cs; @@ -1552,6 +1566,8 @@ struct unifier_fn { expr v = mk_lambda_for(new_mtype, mk_var(vidx)); cs = cs + mk_eq_cnstr(m, v, j, relax); alts.push_back(cs.to_list()); + if (cheap()) + return; } } } @@ -1592,17 +1608,15 @@ struct unifier_fn { void mk_app_projections() { lean_assert(is_metavar(m)); lean_assert(is_app(rhs)); - if (!u.m_pattern) { + if (!u.m_pattern && !cheap()) { expr const & f = get_app_fn(rhs); lean_assert(is_constant(f) || is_local(f)); if (is_local(f)) { unsigned i = margs.size(); - if (!u.m_pattern) { - while (i > 0) { - --i; - if (!(is_local(margs[i]) && mlocal_name(margs[i]) == mlocal_name(f))) - mk_simple_nonlocal_projection(i); - } + while (i > 0) { + --i; + if (!(is_local(margs[i]) && mlocal_name(margs[i]) == mlocal_name(f))) + mk_simple_nonlocal_projection(i); } } else { mk_simple_projections(); @@ -1789,12 +1803,12 @@ struct unifier_fn { mk_simple_projections(); break; case expr_kind::Sort: case expr_kind::Constant: - if (!u.m_pattern) + if (!u.m_pattern && !cheap()) mk_simple_projections(); mk_simple_imitation(); break; case expr_kind::Pi: case expr_kind::Lambda: - if (!u.m_pattern) + if (!u.m_pattern && !cheap()) mk_simple_projections(); mk_bindings_imitation(); break; @@ -1861,6 +1875,8 @@ struct unifier_fn { */ bool use_flex_rigid_whnf_split(expr const & lhs, expr const & rhs) { lean_assert(is_meta(lhs)); + if (m_config.m_cheap) + return false; if (m_config.m_computation) return true; // if unifier.computation is true, we always consider the additional whnf split buffer locals; diff --git a/src/library/unifier.h b/src/library/unifier.h index 6fbdf59ee..9e1c3fb33 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -40,6 +40,9 @@ struct unifier_config { // If m_discard is true, then constraints that cannot be solved are discarded (or incomplete methods are used) // If m_discard is false, unify returns the set of constraints that could not be handled. bool m_discard; + // If m_cheap is true, then expensive case-analysis is not performed (e.g., delta). + // Default is m_cheap == false + bool m_cheap; unifier_config(bool use_exceptions = false, bool discard = false); explicit unifier_config(options const & o, bool use_exceptions = false, bool discard = false); };