From 950f356d9af9ed1183e61d54aeabbf0194d4bf17 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Dec 2015 19:28:45 -0700 Subject: [PATCH] refactor(library/blast,frontends/lean): forward pattern index --- src/frontends/lean/builtin_cmds.cpp | 35 ++-- src/frontends/lean/decl_attributes.cpp | 5 +- src/library/blast/forward/CMakeLists.txt | 2 +- src/library/blast/forward/ematch.cpp | 22 ++- .../blast/forward/forward_lemma_set.cpp | 78 +++++++++ src/library/blast/forward/forward_lemma_set.h | 25 +++ src/library/blast/forward/init_module.cpp | 3 + src/library/blast/forward/pattern.cpp | 159 +++++------------- src/library/blast/forward/pattern.h | 24 +-- src/library/blast/options.cpp | 14 +- tests/lean/pattern_hint1.lean | 9 + tests/lean/pattern_hint1.lean.expected.out | 13 ++ tests/lean/{run => }/redundant_pattern.lean | 0 .../lean/redundant_pattern.lean.expected.out | 4 + 14 files changed, 222 insertions(+), 171 deletions(-) create mode 100644 src/library/blast/forward/forward_lemma_set.cpp create mode 100644 src/library/blast/forward/forward_lemma_set.h create mode 100644 tests/lean/pattern_hint1.lean create mode 100644 tests/lean/pattern_hint1.lean.expected.out rename tests/lean/{run => }/redundant_pattern.lean (100%) create mode 100644 tests/lean/redundant_pattern.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index b09f743f1..5d419a820 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -50,6 +50,7 @@ Author: Leonardo de Moura #include "library/blast/simplifier/simplifier.h" #include "library/blast/backward/backward_rule_set.h" #include "library/blast/forward/pattern.h" +#include "library/blast/forward/forward_lemma_set.h" #include "compiler/preprocess_rec.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" @@ -231,20 +232,26 @@ static void print_metaclasses(parser const & p) { p.regular_stream() << "[" << n << "]" << endl; } -static void print_patterns(io_state_stream const & out, environment const & env, name const & n) { - if (auto lemma = get_hi_lemma(env, n)) { - if (lemma->m_multi_patterns) { - out << "(multi-)patterns:\n"; - for (multi_pattern const & mp : lemma->m_multi_patterns) { - out << "{"; - bool first = true; - for (expr const & p : mp) { - if (first) first = false; else out << ", "; - out << p; +static void print_patterns(parser const & p, name const & n) { + if (is_forward_lemma(p.env(), n)) { + blast::scope_debug scope(p.env(), p.ios()); + try { + // we regenerate the patterns to make sure they reflect the current set of reducible constants + auto lemma = blast::mk_hi_lemma(n, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY); + if (lemma.m_multi_patterns) { + io_state_stream out = p.regular_stream(); + out << "(multi-)patterns:\n"; + for (multi_pattern const & mp : lemma.m_multi_patterns) { + out << "{"; + bool first = true; + for (expr const & p : mp) { + if (first) first = false; else out << ", "; + out << p; + } + out << "}\n"; } - out << "}\n"; } - } + } catch (exception &) {} } } @@ -287,7 +294,7 @@ static void print_attributes(parser const & p, name const & n) { out << " [backward]"; if (is_no_pattern(env, n)) out << " [no_pattern]"; - if (get_hi_lemma(env, n)) + if (is_forward_lemma(env, n)) out << " [forward]"; switch (get_reducible_status(env, n)) { case reducible_status::Reducible: out << " [reducible]"; break; @@ -424,7 +431,7 @@ bool print_id_info(parser const & p, name const & id, bool show_value, pos_info if (show_value) print_definition(p, c, pos); } - print_patterns(out, env, c); + print_patterns(p, c); } return true; } catch (exception & ex) {} diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 2ee998487..d95b7060c 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/blast/simplifier/simp_rule_set.h" #include "library/blast/backward/backward_rule_set.h" #include "library/blast/forward/pattern.h" +#include "library/blast/forward/forward_lemma_set.h" #include "frontends/lean/decl_attributes.h" #include "frontends/lean/parser.h" #include "frontends/lean/tokens.h" @@ -241,9 +242,9 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c } if (forward) { if (m_priority) - env = add_hi_lemma(env, ios.get_options(), d, *m_priority, m_persistent); + env = add_forward_lemma(env, d, *m_priority, m_persistent); else - env = add_hi_lemma(env, ios.get_options(), d, LEAN_HI_LEMMA_DEFAULT_PRIORITY, m_persistent); + env = add_forward_lemma(env, d, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY, m_persistent); } if (m_no_pattern) { env = add_no_pattern(env, d, m_persistent); diff --git a/src/library/blast/forward/CMakeLists.txt b/src/library/blast/forward/CMakeLists.txt index d13aaeeb5..cca97c82c 100644 --- a/src/library/blast/forward/CMakeLists.txt +++ b/src/library/blast/forward/CMakeLists.txt @@ -1,2 +1,2 @@ add_library(forward OBJECT init_module.cpp forward_extension.cpp qcf.cpp pattern.cpp - ematch.cpp) + ematch.cpp forward_lemma_set.cpp) diff --git a/src/library/blast/forward/ematch.cpp b/src/library/blast/forward/ematch.cpp index 8e12a26fa..6e2e29be6 100644 --- a/src/library/blast/forward/ematch.cpp +++ b/src/library/blast/forward/ematch.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/blast/options.h" #include "library/blast/congruence_closure.h" #include "library/blast/forward/pattern.h" +#include "library/blast/forward/forward_lemma_set.h" namespace lean { namespace blast { @@ -45,7 +46,6 @@ struct ematch_branch_extension : public branch_extension { hi_lemma_set m_lemmas; hi_lemma_set m_new_lemmas; rb_map m_apps; - name_set m_initialized; expr_set m_instances; ematch_branch_extension() {} @@ -70,14 +70,6 @@ struct ematch_branch_extension : public branch_extension { case expr_kind::App: { buffer args; expr const & f = get_app_args(e, args); - if (is_constant(f) && !m_initialized.contains(const_name(f))) { - m_initialized.insert(const_name(f)); - if (auto lemmas = get_hi_lemma_index(env()).find(const_name(f))) { - for (hi_lemma const & lemma : *lemmas) { - m_new_lemmas.insert(lemma); - } - } - } if ((is_constant(f) && !is_no_pattern(env(), const_name(f))) || (is_local(f))) { expr_set s; @@ -95,16 +87,22 @@ struct ematch_branch_extension : public branch_extension { void register_lemma(hypothesis const & h) { if (is_pi(h.get_type()) && !is_arrow(h.get_type())) { - blast_tmp_type_context ctx; try { - m_new_lemmas.insert(mk_hi_lemma(*ctx, h.get_self())); + m_new_lemmas.insert(mk_hi_lemma(h.get_self())); } catch (exception &) {} } } virtual ~ematch_branch_extension() {} virtual branch_extension * clone() override { return new ematch_branch_extension(*this); } - virtual void initialized() override {} + virtual void initialized() override { + forward_lemma_set s = get_forward_lemma_set(env()); + s.for_each([&](name const & n, unsigned prio) { + try { + m_new_lemmas.insert(mk_hi_lemma(n, prio)); + } catch (exception &) {} + }); + } virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx) override { collect_apps(h.get_type()); register_lemma(h); diff --git a/src/library/blast/forward/forward_lemma_set.cpp b/src/library/blast/forward/forward_lemma_set.cpp new file mode 100644 index 000000000..904ff43ad --- /dev/null +++ b/src/library/blast/forward/forward_lemma_set.cpp @@ -0,0 +1,78 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/scoped_ext.h" +#include "library/blast/forward/forward_lemma_set.h" + +namespace lean { +static name * g_name = nullptr; +static std::string * g_key = nullptr; + +struct forward_lemma { + name m_name; + unsigned m_priority; + forward_lemma() {} + forward_lemma(name const & n, unsigned p):m_name(n), m_priority(p) {} +}; + +struct forward_lemma_set_config { + typedef forward_lemma entry; + typedef forward_lemma_set state; + + static void add_entry(environment const &, io_state const &, state & s, entry const & e) { + s.insert(e.m_name, e.m_priority); + } + + static name const & get_class_name() { + return *g_name; + } + + static std::string const & get_serialization_key() { + return *g_key; + } + + static void write_entry(serializer & s, entry const & e) { + s << e.m_name << e.m_priority; + } + + static entry read_entry(deserializer & d) { + name n; unsigned p; + d >> n >> p; + return entry(n, p); + } + + static optional get_fingerprint(entry const & e) { + return some(hash(e.m_name.hash(), e.m_priority)); + } +}; + +template class scoped_ext; +typedef scoped_ext forward_lemma_set_ext; + +environment add_forward_lemma(environment const & env, name const & n, unsigned priority, bool persistent) { + return forward_lemma_set_ext::add_entry(env, get_dummy_ios(), forward_lemma(n, priority), persistent); +} + +bool is_forward_lemma(environment const & env, name const & n) { + return forward_lemma_set_ext::get_state(env).contains(n); +} + +forward_lemma_set get_forward_lemma_set(environment const & env) { + return forward_lemma_set_ext::get_state(env); +} + +void initialize_forward_lemma_set() { + g_name = new name("forward"); + g_key = new std::string("FWD"); + forward_lemma_set_ext::initialize(); +} + +void finalize_forward_lemma_set() { + forward_lemma_set_ext::finalize(); + delete g_name; + delete g_key; +} +} diff --git a/src/library/blast/forward/forward_lemma_set.h b/src/library/blast/forward/forward_lemma_set.h new file mode 100644 index 000000000..b357fb9d2 --- /dev/null +++ b/src/library/blast/forward/forward_lemma_set.h @@ -0,0 +1,25 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "util/rb_tree.h" +#include "kernel/expr.h" + +#ifndef LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY +#define LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY 1000 +#endif + +namespace lean { +/** \brief The forward lemma set is actually a mapping from lemma name to priority */ +typedef rb_map forward_lemma_set; + +environment add_forward_lemma(environment const & env, name const & n, unsigned priority, bool persistent); +bool is_forward_lemma(environment const & env, name const & n); +forward_lemma_set get_forward_lemma_set(environment const & env); + +void initialize_forward_lemma_set(); +void finalize_forward_lemma_set(); +} diff --git a/src/library/blast/forward/init_module.cpp b/src/library/blast/forward/init_module.cpp index d44610800..6f715463f 100644 --- a/src/library/blast/forward/init_module.cpp +++ b/src/library/blast/forward/init_module.cpp @@ -5,6 +5,7 @@ Author: Daniel Selsam */ #include "library/blast/forward/init_module.h" #include "library/blast/forward/forward_extension.h" +#include "library/blast/forward/forward_lemma_set.h" #include "library/blast/forward/pattern.h" #include "library/blast/forward/ematch.h" @@ -14,11 +15,13 @@ namespace blast { void initialize_forward_module() { initialize_forward_extension(); initialize_pattern(); + initialize_forward_lemma_set(); initialize_ematch(); } void finalize_forward_module() { finalize_ematch(); + finalize_forward_lemma_set(); finalize_pattern(); finalize_forward_extension(); } diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp index 60f1653a4..c28406d65 100644 --- a/src/library/blast/forward/pattern.cpp +++ b/src/library/blast/forward/pattern.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include #include "util/sstream.h" -#include "util/sexpr/option_declarations.h" #include "library/expr_lt.h" #include "kernel/find_fn.h" #include "kernel/for_each_fn.h" @@ -21,19 +20,11 @@ Author: Leonardo de Moura #include "library/scoped_ext.h" #include "library/idx_metavar.h" #include "library/blast/options.h" +#include "library/blast/blast.h" #include "library/blast/forward/pattern.h" - -#ifndef LEAN_DEFAULT_PATTERN_MAX_STEPS -#define LEAN_DEFAULT_PATTERN_MAX_STEPS 1024 -#endif +#include "library/blast/forward/forward_lemma_set.h" namespace lean { -static name * g_pattern_max_steps = nullptr; - -unsigned get_pattern_max_steps(options const & o) { - return o.get_unsigned(*g_pattern_max_steps, LEAN_DEFAULT_PATTERN_MAX_STEPS); -} - /* Step 1: Selecting which variables we should track. @@ -143,66 +134,19 @@ expr mk_pattern_hint(expr const & e) { return mk_annotation(*g_pattern_hint, e); } -static name * g_hi_name = nullptr; +static name * g_name = nullptr; static std::string * g_key = nullptr; -// "Poor man" union type -struct hi_entry { - optional m_no_pattern; - hi_lemma m_lemma; - hi_entry() {} - hi_entry(name const & n):m_no_pattern(n) {} - hi_entry(hi_lemma const & l):m_lemma(l) {} -}; - -struct hi_state { - name_set m_no_patterns; - name_map m_name_to_lemma; - hi_lemmas m_lemmas; -}; - -serializer & operator<<(serializer & s, multi_pattern const & mp) { - write_list(s, mp); - return s; -} - -deserializer & operator>>(deserializer & d, multi_pattern & mp) { - mp = read_list(d); - return d; -} - -static optional get_hi_lemma_name(expr const & H) { - if (is_lambda(H)) - return get_hi_lemma_name(binding_body(H)); - expr const & f = get_app_fn(H); - if (is_constant(f)) - return optional(const_name(f)); - else - return optional(); -} - -struct hi_config { - typedef hi_entry entry; - typedef hi_state state; +struct no_pattern_config { + typedef name entry; + typedef name_set state; static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - if (e.m_no_pattern) { - s.m_no_patterns.insert(*e.m_no_pattern); - } else { - if (auto n = get_hi_lemma_name(e.m_lemma.m_proof)) - s.m_name_to_lemma.insert(*n, e.m_lemma); - for (multi_pattern const & mp : e.m_lemma.m_multi_patterns) { - for (expr const & p : mp) { - lean_assert(is_app(p)); - lean_assert(is_constant(get_app_fn(p))); - s.m_lemmas.insert(const_name(get_app_fn(p)), e.m_lemma); - } - } - } + s.insert(e); } static name const & get_class_name() { - return *g_hi_name; + return *g_name; } static std::string const & get_serialization_key() { @@ -210,49 +154,36 @@ struct hi_config { } static void write_entry(serializer & s, entry const & e) { - s << e.m_no_pattern; - if (!e.m_no_pattern) { - hi_lemma const & l = e.m_lemma; - s << l.m_num_uvars << l.m_num_mvars << l.m_priority << l.m_prop << l.m_proof; - write_list(s, l.m_mvars); - write_list(s, l.m_is_inst_implicit); - write_list(s, l.m_multi_patterns); - } + s << e; } static entry read_entry(deserializer & d) { entry e; - d >> e.m_no_pattern; - if (!e.m_no_pattern) { - hi_lemma & l = e.m_lemma; - d >> l.m_num_uvars >> l.m_num_mvars >> l.m_priority >> l.m_prop >> l.m_proof; - l.m_mvars = read_list(d); - l.m_is_inst_implicit = read_list(d); - l.m_multi_patterns = read_list(d); - } + d >> e; return e; } static optional get_fingerprint(entry const & e) { - return e.m_no_pattern ? some(e.m_no_pattern->hash()) : some(e.m_lemma.m_prop.hash()); + return some(e.hash()); } }; -template class scoped_ext; -typedef scoped_ext hi_ext; +template class scoped_ext; +typedef scoped_ext no_pattern_ext; bool is_no_pattern(environment const & env, name const & n) { - return hi_ext::get_state(env).m_no_patterns.contains(n); + return no_pattern_ext::get_state(env).contains(n); } environment add_no_pattern(environment const & env, name const & n, bool persistent) { - return hi_ext::add_entry(env, get_dummy_ios(), hi_entry(n), persistent); + return no_pattern_ext::add_entry(env, get_dummy_ios(), n, persistent); } name_set const & get_no_patterns(environment const & env) { - return hi_ext::get_state(env).m_no_patterns; + return no_pattern_ext::get_state(env); } +namespace blast { typedef rb_tree idx_metavar_set; static bool is_higher_order(tmp_type_context & ctx, expr const & e) { @@ -363,7 +294,7 @@ struct mk_hi_lemma_fn { mk_hi_lemma_fn(tmp_type_context & ctx, expr const & H, unsigned num_uvars, unsigned prio, unsigned max_steps): - m_ctx(ctx), m_no_patterns(hi_ext::get_state(ctx.env()).m_no_patterns), + m_ctx(ctx), m_no_patterns(no_pattern_ext::get_state(ctx.env())), m_H(H), m_num_uvars(num_uvars), m_priority(prio), m_max_steps(max_steps) {} struct candidate { @@ -599,7 +530,12 @@ struct mk_hi_lemma_fn { } hi_lemma operator()() { - expr H_type = m_ctx.infer(m_H); + expr H_type; + { + // preserve pattern hints + scope_unfold_macro_pred scope1([](expr const & e) { return !is_pattern_hint(e); }); + H_type = normalize(m_ctx.infer(m_H)); + } buffer inst_implicit_flags; expr B = extract_trackable(m_ctx, H_type, m_mvars, inst_implicit_flags, m_trackable, m_residue); lean_assert(m_mvars.size() == inst_implicit_flags.size()); @@ -652,52 +588,37 @@ hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, expr const & H, unsigned num_u return mk_hi_lemma_fn(ctx, H, num_uvars, priority, max_steps)(); } -namespace blast { -hi_lemma mk_hi_lemma(tmp_type_context & ctx, expr const & H) { +hi_lemma mk_hi_lemma(expr const & H) { + blast_tmp_type_context ctx; unsigned max_steps = get_config().m_pattern_max_steps; - ctx.clear(); - return mk_hi_lemma_core(ctx, H, 0, LEAN_HI_LEMMA_DEFAULT_PRIORITY, max_steps); -}} + return mk_hi_lemma_core(*ctx, H, 0, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY, max_steps); +} -environment add_hi_lemma(environment const & env, options const & o, name const & c, unsigned priority, bool persistent) { - tmp_type_context ctx(env, get_dummy_ios()); - declaration const & d = env.get(c); +hi_lemma mk_hi_lemma(name const & c, unsigned priority) { + blast_tmp_type_context ctx; + unsigned max_steps = get_config().m_pattern_max_steps; + declaration const & d = env().get(c); buffer us; unsigned num_us = d.get_num_univ_params(); for (unsigned i = 0; i < num_us; i++) - us.push_back(ctx.mk_uvar()); - expr H = mk_constant(c, to_list(us)); - unsigned max_steps = get_pattern_max_steps(o); - return hi_ext::add_entry(env, get_dummy_ios(), hi_entry(mk_hi_lemma_core(ctx, H, num_us, priority, max_steps)), - persistent); + us.push_back(ctx->mk_uvar()); + expr H = mk_constant(c, to_list(us)); + return mk_hi_lemma_core(*ctx, H, num_us, priority, max_steps); } - -hi_lemma const * get_hi_lemma(environment const & env, name const & c) { - return hi_ext::get_state(env).m_name_to_lemma.find(c); -} - -hi_lemmas get_hi_lemma_index(environment const & env) { - return hi_ext::get_state(env).m_lemmas; } void initialize_pattern() { - g_hi_name = new name("hi"); - g_key = new std::string("HI"); - hi_ext::initialize(); + g_name = new name("no_pattern"); + g_key = new std::string("NOPAT"); + no_pattern_ext::initialize(); g_pattern_hint = new name("pattern_hint"); register_annotation(*g_pattern_hint); - g_pattern_max_steps = new name{"pattern", "max_steps"}; - register_unsigned_option(*g_pattern_max_steps, LEAN_DEFAULT_PATTERN_MAX_STEPS, - "(pattern) max number of steps performed by pattern inference procedure, " - "we have this threshold because in the worst case this procedure may take " - "an exponetial number of steps"); } void finalize_pattern() { - hi_ext::finalize(); - delete g_hi_name; + no_pattern_ext::finalize(); + delete g_name; delete g_key; delete g_pattern_hint; - delete g_pattern_max_steps; } } diff --git a/src/library/blast/forward/pattern.h b/src/library/blast/forward/pattern.h index 066a4cc86..3b77d75b8 100644 --- a/src/library/blast/forward/pattern.h +++ b/src/library/blast/forward/pattern.h @@ -10,10 +10,6 @@ Author: Leonardo de Moura #include "library/expr_lt.h" #include "library/tmp_type_context.h" -#ifndef LEAN_HI_LEMMA_DEFAULT_PRIORITY -#define LEAN_HI_LEMMA_DEFAULT_PRIORITY 1000 -#endif - namespace lean { /** \brief Annotate \c e as a pattern hint */ expr mk_pattern_hint(expr const & e); @@ -52,27 +48,11 @@ struct hi_lemma_cmp { int operator()(hi_lemma const & l1, hi_lemma const & l2) const { return expr_quick_cmp()(l1.m_prop, l2.m_prop); } }; -/** \brief Mapping c -> S, where c is a constant name and S is a set of hi_lemmas that contain - a pattern where the head symbol is c. */ -typedef rb_multi_map hi_lemmas; - -/** \brief Add the given theorem as a heuristic instantiation lemma in the current environment. */ -environment add_hi_lemma(environment const & env, options const & o, name const & c, unsigned priority, bool persistent); - -/** \brief Return the heuristic instantiation lemma data associated with constant \c c */ -hi_lemma const * get_hi_lemma(environment const & env, name const & c); - -/** \brief Retrieve the active set of heuristic instantiation lemmas. */ -hi_lemmas get_hi_lemma_index(environment const & env); - -hi_lemma mk_hi_lemma(tmp_type_context & ctx, expr const & H, unsigned max_steps); - -unsigned get_pattern_max_steps(options const & o); - namespace blast { /** \brief Create a (local) heuristic instantiation lemma for \c H. The maximum number of steps is extracted from the blast config object. */ -hi_lemma mk_hi_lemma(tmp_type_context & ctx, expr const & H); +hi_lemma mk_hi_lemma(expr const & H); +hi_lemma mk_hi_lemma(name const & n, unsigned prio); } void initialize_pattern(); diff --git a/src/library/blast/options.cpp b/src/library/blast/options.cpp index e14068d19..5488faaeb 100644 --- a/src/library/blast/options.cpp +++ b/src/library/blast/options.cpp @@ -44,7 +44,9 @@ Author: Leonardo de Moura #ifndef LEAN_DEFAULT_BLAST_BACKWARD #define LEAN_DEFAULT_BLAST_BACKWARD true #endif - +#ifndef LEAN_DEFAULT_PATTERN_MAX_STEPS +#define LEAN_DEFAULT_PATTERN_MAX_STEPS 1024 +#endif namespace lean { namespace blast { @@ -61,6 +63,7 @@ static name * g_blast_recursor = nullptr; static name * g_blast_ematch = nullptr; static name * g_blast_backward = nullptr; static name * g_blast_show_failure = nullptr; +static name * g_pattern_max_steps = nullptr; unsigned get_blast_max_depth(options const & o) { return o.get_unsigned(*g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH); @@ -98,6 +101,9 @@ bool get_blast_backward(options const & o) { bool get_blast_show_failure(options const & o) { return o.get_bool(*g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE); } +unsigned get_pattern_max_steps(options const & o) { + return o.get_unsigned(*g_pattern_max_steps, LEAN_DEFAULT_PATTERN_MAX_STEPS); +} config::config(options const & o) { m_max_depth = get_blast_max_depth(o); @@ -145,6 +151,7 @@ void initialize_options() { g_blast_ematch = new name{"blast", "ematch"}; g_blast_backward = new name{"blast", "backward"}; g_blast_show_failure = new name{"blast", "show_failure"}; + g_pattern_max_steps = new name{"pattern", "max_steps"}; register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH, "(blast) max search depth for blast"); @@ -170,6 +177,10 @@ void initialize_options() { "(blast) enable backward chaining"); register_bool_option(*blast::g_blast_show_failure, LEAN_DEFAULT_BLAST_SHOW_FAILURE, "(blast) show failure state"); + register_unsigned_option(*g_pattern_max_steps, LEAN_DEFAULT_PATTERN_MAX_STEPS, + "(pattern) max number of steps performed by pattern inference procedure, " + "we have this threshold because in the worst case this procedure may take " + "an exponetial number of steps"); } void finalize_options() { delete g_blast_max_depth; @@ -184,5 +195,6 @@ void finalize_options() { delete g_blast_ematch; delete g_blast_backward; delete g_blast_show_failure; + delete g_pattern_max_steps; } }} diff --git a/tests/lean/pattern_hint1.lean b/tests/lean/pattern_hint1.lean new file mode 100644 index 000000000..441c46085 --- /dev/null +++ b/tests/lean/pattern_hint1.lean @@ -0,0 +1,9 @@ +constants f g : nat → Prop + +definition foo₁ [forward] : ∀ x, f x ∧ g x := sorry +definition foo₂ [forward] : ∀ x, (: f x :) ∧ g x := sorry +definition foo₃ [forward] : ∀ x, (: f (id x) :) ∧ g x := sorry + +print foo₁ +print foo₂ +print foo₃ -- id is unfolded diff --git a/tests/lean/pattern_hint1.lean.expected.out b/tests/lean/pattern_hint1.lean.expected.out new file mode 100644 index 000000000..5467f0b49 --- /dev/null +++ b/tests/lean/pattern_hint1.lean.expected.out @@ -0,0 +1,13 @@ +definition foo₁ [forward] : ∀ (x : ℕ), f x ∧ g x := +sorry +(multi-)patterns: +{f ?M_1} +{g ?M_1} +definition foo₂ [forward] : ∀ (x : ℕ), (:f x:) ∧ g x := +sorry +(multi-)patterns: +{f ?M_1} +definition foo₃ [forward] : ∀ (x : ℕ), (:f (id x):) ∧ g x := +sorry +(multi-)patterns: +{f ?M_1} diff --git a/tests/lean/run/redundant_pattern.lean b/tests/lean/redundant_pattern.lean similarity index 100% rename from tests/lean/run/redundant_pattern.lean rename to tests/lean/redundant_pattern.lean diff --git a/tests/lean/redundant_pattern.lean.expected.out b/tests/lean/redundant_pattern.lean.expected.out new file mode 100644 index 000000000..3ca6801de --- /dev/null +++ b/tests/lean/redundant_pattern.lean.expected.out @@ -0,0 +1,4 @@ +definition foo [forward] : ∀ (m n k : ℕ), P (f m) → P (g n) → P (f k) → P k ∧ R (g m) (f n) ∧ P (g m) ∧ P (f n) := +λ (m n k : ℕ), sorry +(multi-)patterns: +{P ?M_1, R (g ?M_2) (f ?M_3)}