From 028ef47c8460bdf7b53368b22fa7110303c13c24 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Dec 2015 22:36:10 -0800 Subject: [PATCH] feat(frontends/lean,library/blast/forward/pattern): check whether patterns can be inferred at declaration time --- src/frontends/lean/builtin_cmds.cpp | 6 ++---- src/frontends/lean/decl_attributes.cpp | 1 + src/library/blast/forward/pattern.cpp | 9 ++++++++- src/library/blast/forward/pattern.h | 3 +++ tests/lean/bad_pattern.lean | 3 +++ tests/lean/bad_pattern.lean.expected.out | 3 ++- 6 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 6909e2500..2d9cae490 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -234,14 +234,12 @@ static void print_metaclasses(parser const & p) { static void print_patterns(parser & p, name const & n) { if (is_forward_lemma(p.env(), n)) { - blast::scope_debug scope(p.env(), p.ios()); // we regenerate the patterns to make sure they reflect the current set of reducible constants try { - auto lemma = blast::mk_hi_lemma(n, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY); - if (lemma.m_multi_patterns) { + if (auto mps = mk_multipatterns(p.env(), p.ios(), n)) { io_state_stream out = p.regular_stream(); out << "(multi-)patterns:\n"; - for (multi_pattern const & mp : lemma.m_multi_patterns) { + for (multi_pattern const & mp : mps) { out << "{"; bool first = true; for (expr const & p : mp) { diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index d95b7060c..aaad2084d 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -241,6 +241,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent); } if (forward) { + mk_multipatterns(env, ios, d); // try to create patterns if (m_priority) env = add_forward_lemma(env, d, *m_priority, m_persistent); else diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp index 3e119c41d..deabf091d 100644 --- a/src/library/blast/forward/pattern.cpp +++ b/src/library/blast/forward/pattern.cpp @@ -130,7 +130,7 @@ expr mk_pattern_hint(expr const & e) { if (has_pattern_hints(e)) throw exception("invalid pattern hint, nested patterns hints are not allowed"); if (!is_app(e)) - throw_generic_exception("invalid pattern hint, pattern must be applications", e); + throw_generic_exception("invalid pattern hint, pattern hints must be applications", e); return mk_annotation(*g_pattern_hint, e); } @@ -630,6 +630,13 @@ hi_lemma mk_hi_lemma(name const & c, unsigned priority) { } } +list mk_multipatterns(environment const & env, io_state const & ios, name const & c) { + blast::scope_debug scope(env, ios); + // we regenerate the patterns to make sure they reflect the current set of reducible constants + auto lemma = blast::mk_hi_lemma(c, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY); + return lemma.m_multi_patterns; +} + void initialize_pattern() { g_name = new name("no_pattern"); g_key = new std::string("NOPAT"); diff --git a/src/library/blast/forward/pattern.h b/src/library/blast/forward/pattern.h index 3b77d75b8..66a1ed1b6 100644 --- a/src/library/blast/forward/pattern.h +++ b/src/library/blast/forward/pattern.h @@ -48,6 +48,9 @@ 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 Try to compute multipatterns for declaration \c c using the current environment configuration. */ +list mk_multipatterns(environment const & env, io_state const & ios, name const & c); + namespace blast { /** \brief Create a (local) heuristic instantiation lemma for \c H. The maximum number of steps is extracted from the blast config object. */ diff --git a/tests/lean/bad_pattern.lean b/tests/lean/bad_pattern.lean index fab09cc29..c90c0769e 100644 --- a/tests/lean/bad_pattern.lean +++ b/tests/lean/bad_pattern.lean @@ -16,3 +16,6 @@ reveal tst₀ tst₁ tst₃ print tst₀ print tst₁ print tst₃ + +definition tst₄ [forward] : ∀ x : nat, (: id x :) = x := +λ x, rfl diff --git a/tests/lean/bad_pattern.lean.expected.out b/tests/lean/bad_pattern.lean.expected.out index 237a8efbf..05f0463ab 100644 --- a/tests/lean/bad_pattern.lean.expected.out +++ b/tests/lean/bad_pattern.lean.expected.out @@ -1,4 +1,4 @@ -bad_pattern.lean:9:33: error: invalid pattern hint, pattern must be applications +bad_pattern.lean:9:33: error: invalid pattern hint, pattern hints must be applications theorem tst₀ [forward] : ∀ (x : ℕ), P x := sorry (multi-)patterns: @@ -11,3 +11,4 @@ theorem tst₃ [forward] : ∀ (x : ℕ), P (:id x:) := sorry (multi-)patterns: {P ?M_1} +bad_pattern.lean:20:0: error: pattern inference failed for [forward] annotation, (solution: provide pattern hints using the notation '(: t :)' )