fix(library/blast,frontends/lean): handling pattern hints after unfolding

src/frontends/lean/builtin_cmds.cpp

@@ -232,11 +232,11 @@ static void print_metaclasses(parser const & p) {
         p.regular_stream() << "[" << n << "]" << endl;
 }
 
-static void print_patterns(parser const & p, name const & n) {
+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 {
-            // 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();
@@ -251,7 +251,9 @@ static void print_patterns(parser const & p, name const & n) {
                     out << "}\n";
                 }
             }
-        } catch (exception &) {}
+        } catch (exception & ex) {
+            p.display_error(ex);
+        }
     }
 }
 
@@ -387,7 +389,7 @@ static bool print_constant(parser const & p, char const * kind, declaration cons
     return true;
 }
 
-bool print_id_info(parser const & p, name const & id, bool show_value, pos_info const & pos) {
+bool print_id_info(parser & p, name const & id, bool show_value, pos_info const & pos) {
     // declarations
     try {
         environment const & env = p.env();

src/frontends/lean/builtin_cmds.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "frontends/lean/cmd_table.h"
 namespace lean {
-bool print_id_info(parser const & p, name const & id, bool show_value, pos_info const & pos);
+bool print_id_info(parser & p, name const & id, bool show_value, pos_info const & pos);
 bool print_token_info(parser const & p, name const & tk);
 
 cmd_table get_builtin_cmds();

src/frontends/lean/parser.h

@@ -164,7 +164,6 @@ class parser {
     void display_error_pos(pos_info p);
     void display_error(char const * msg, unsigned line, unsigned pos);
     void display_error(char const * msg, pos_info p);
-    void display_error(throwable const & ex);
     void display_error(script_exception const & ex);
     void throw_parser_exception(char const * msg, pos_info p);
     void throw_nested_exception(throwable const & ex, pos_info p);
@@ -277,6 +276,8 @@ public:
            info_manager * im = nullptr, keep_theorem_mode tmode = keep_theorem_mode::All);
     ~parser();
 
+    void display_error(throwable const & ex);
+
     bool ignore_noncomputable() const { return m_ignore_noncomputable; }
     void set_ignore_noncomputable() { m_ignore_noncomputable = true; }
 

src/library/blast/blast.cpp

@@ -792,10 +792,12 @@ void scope_assignment::commit() {
 scope_unfold_macro_pred::scope_unfold_macro_pred(unfold_macro_pred const & pred):
     m_old_pred(g_blastenv->m_unfold_macro_pred) {
     g_blastenv->m_unfold_macro_pred = pred;
+    g_blastenv->m_norm_cache.clear(); // TODO(Leo): check if we need better solution
 }
 
 scope_unfold_macro_pred::~scope_unfold_macro_pred() {
     g_blastenv->m_unfold_macro_pred = m_old_pred;
+    g_blastenv->m_norm_cache.clear();
 }
 
 struct scope_debug::imp {

src/library/blast/forward/pattern.cpp

@@ -321,7 +321,12 @@ struct mk_hi_lemma_fn {
     void collect_pattern_hints(expr const & e, candidate_set & s) {
         for_each(e, [&](expr const & e, unsigned) {
                 if (is_pattern_hint(e)) {
-                    s.insert(candidate(get_pattern_hint_arg(e)));
+                    expr hint = get_pattern_hint_arg(e);
+                    // TODO(Leo): if hint was unfolded and is not an application anymore, we should
+                    // report to user this fact.
+                    if (is_app(hint)) {
+                        s.insert(candidate(hint));
+                    }
                     return false;
                 }
                 return true;
@@ -529,9 +534,13 @@ struct mk_hi_lemma_fn {
         }
     }
 
-    hi_lemma operator()() {
+    struct try_again_without_hints {};
+
+    hi_lemma operator()(bool erase_hints) {
         expr H_type;
-        {
+        if (erase_hints) {
+            H_type = normalize(m_ctx.infer(m_H));
+        } else {
             // preserve pattern hints
             scope_unfold_macro_pred scope1([](expr const & e) { return !is_pattern_hint(e); });
             H_type = normalize(m_ctx.infer(m_H));
@@ -548,6 +557,9 @@ struct mk_hi_lemma_fn {
         if (!hints.empty()) {
             mps = mk_multi_patterns_using(hints, false);
         } else {
+            if (has_pattern_hints(H_type)) {
+                throw try_again_without_hints();
+            }
             buffer<expr> places;
             candidate_set B_candidates = collect(B);
             if (auto r1 = mk_multi_patterns_using(B_candidates, true)) {
@@ -585,7 +597,18 @@ struct mk_hi_lemma_fn {
 
 hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, expr const & H, unsigned num_uvars,
                           unsigned priority, unsigned max_steps) {
-    return mk_hi_lemma_fn(ctx, H, num_uvars, priority, max_steps)();
+    try {
+        bool erase_hints = false;
+        return mk_hi_lemma_fn(ctx, H, num_uvars, priority, max_steps)(erase_hints);
+    } catch (mk_hi_lemma_fn::try_again_without_hints &) {
+        ctx.clear();
+        try {
+            bool erase_hints = true;
+            return mk_hi_lemma_fn(ctx, H, num_uvars, priority, max_steps)(erase_hints);
+        } catch (mk_hi_lemma_fn::try_again_without_hints &) {
+            lean_unreachable();
+        }
+    }
 }
 
 hi_lemma mk_hi_lemma(expr const & H) {

tests/lean/bad_pattern.lean

@@ -1,7 +1,18 @@
 constant P : nat → Prop
 
+lemma tst₀ [forward] : ∀ x, P x := -- Fine
+sorry
+
 lemma tst₁ [forward] : ∀ x, (: P x :) := -- Fine
 sorry
 
 lemma tst₂ [forward] : ∀ x, P (: x :) := -- Error
 sorry
+
+lemma tst₃ [forward] : ∀ x, P (: id x :) :=
+sorry
+
+reveal tst₀ tst₁ tst₃
+print tst₀
+print tst₁
+print tst₃

tests/lean/bad_pattern.lean.expected.out

@@ -1 +1,13 @@
-bad_pattern.lean:6:33: error: invalid pattern hint, pattern must be applications
+bad_pattern.lean:9:33: error: invalid pattern hint, pattern must be applications
+theorem tst₀ [forward] : ∀ (x : ℕ), P x :=
+sorry
+(multi-)patterns:
+{P ?M_1}
+theorem tst₁ [forward] : ∀ (x : ℕ), (:P x:) :=
+sorry
+(multi-)patterns:
+{P ?M_1}
+theorem tst₃ [forward] : ∀ (x : ℕ), P (:id x:) :=
+sorry
+(multi-)patterns:
+{P ?M_1}