fix(frontends/lean, library/tactic): error position in auto quoted terms

This commit also gets rid of the redundant "elaborator failed" error
message.

src/frontends/lean/CMakeLists.txt

@@ -5,7 +5,7 @@ notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmds.cpp dependencies.cpp
 pp.cpp structure_cmd.cpp structure_instance.cpp
 init_module.cpp type_util.cpp decl_attributes.cpp
-prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
+prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp tactic_evaluator.cpp
 parser_state.cpp)

src/frontends/lean/elaborator.cpp

@@ -768,8 +768,8 @@ static expr get_ref_for_child(expr const & arg, expr const & ref) {
 }
 
 expr elaborator::visit_typed_expr(expr const & e) {
-    expr ref          = e;
     expr val          = get_typed_expr_expr(e);
+    expr ref          = val;
     expr type         = get_typed_expr_type(e);
     expr new_type;
     expr ref_type     = get_ref_for_child(type, e);
@@ -3020,17 +3020,16 @@ void elaborator::ensure_no_unassigned_metavars(expr & e) {
             if (!has_expr_metavar(e)) return false;
             if (is_metavar_decl_ref(e) && !m_ctx.is_assigned(e)) {
                 tactic_state s = mk_tactic_state_for(e);
-                report_error(s, "context:", "don't know how to synthesize placeholder", e);
-
                 if (m_recover_from_errors) {
+                    report_error(s, "context:", "don't know how to synthesize placeholder", e);
                     auto ty = m_ctx.mctx().get_metavar_decl(e).get_type();
                     m_ctx.assign(e, copy_tag(e, mk_sorry(ty)));
                     ensure_no_unassigned_metavars(ty);
 
                     auto val = instantiate_mvars(e);
                     ensure_no_unassigned_metavars(val);
                 } else {
-                    throw elaborator_exception(e, "elaborator failed");
+                    throw failed_to_synthesize_placeholder_exception(e, s);
                 }
             }
             return true;

src/frontends/lean/elaborator.h

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/elaborate.h"
-#include "frontends/lean/elaborator_exception.h"
+#include "library/tactic/elaborator_exception.h"
 #include "frontends/lean/info_manager.h"
 #include "library/sorry.h"
 

src/frontends/lean/structure_cmd.cpp

@@ -47,7 +47,7 @@ Author: Leonardo de Moura
 #include "library/constructions/projection.h"
 #include "library/constructions/no_confusion.h"
 #include "library/inductive_compiler/add_decl.h"
-#include "frontends/lean/elaborator_exception.h"
+#include "library/tactic/elaborator_exception.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/decl_util.h"

src/frontends/lean/tactic_evaluator.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_list.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/tactic/smt/smt_state.h"
-#include "frontends/lean/elaborator_exception.h"
+#include "library/tactic/elaborator_exception.h"
 #include "frontends/lean/tactic_evaluator.h"
 #include "frontends/lean/tactic_notation.h"
 
@@ -36,15 +36,6 @@ elaborator_exception unsolved_tactic_state(tactic_state const & ts, char const *
     throw_unsolved_tactic_state(ts, format(msg), ref);
 }
 
-[[noreturn]] void throw_unsolved_smt_tactic_state(vm_obj const & ss, tactic_state const & ts, format const & fmt, expr const & ref) {
-    format msg = fmt + line() + format("state:") + line() + smt_state_pp(ss, ts);
-    throw elaborator_exception(ref, msg);
-}
-
-[[noreturn]] void throw_unsolved_smt_tactic_state(vm_obj const & ss, tactic_state const & ts, char const * msg, expr const & ref) {
-    throw_unsolved_smt_tactic_state(ss, ts, format(msg), ref);
-}
-
 /* Compile tactic into bytecode */
 environment tactic_evaluator::compile_tactic(name const & tactic_name, expr const & tactic) {
     pos_info_provider * provider = get_pos_info_provider();

src/library/tactic/CMakeLists.txt

@@ -8,4 +8,5 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
   hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp
   simp_result.cpp user_attribute.cpp eval.cpp
   simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp
-  vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp)
+  vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp
+  elaborator_exception.cpp)

src/library/tactic/elaborate.cpp

@@ -7,8 +7,11 @@ Author: Leonardo de Moura
 #include <frontends/lean/elaborator.h>
 #include "kernel/for_each_fn.h"
 #include "library/annotation.h"
+#include "library/scope_pos_info_provider.h"
+#include "library/message_builder.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/elaborate.h"
+#include "library/tactic/elaborator_exception.h"
 #include "library/tactic/tactic_state.h"
 
 namespace lean {
@@ -18,6 +21,22 @@ expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); }
 bool is_by(expr const & e) { return is_annotation(e, *g_by_name); }
 expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); }
 
+static bool report_failure(elaborator_exception const & ex, expr const & mvar, char const * header, tactic_state const & s) {
+    auto pip = get_pos_info_provider();
+    if (!pip) return false;
+    optional<expr> ref = ex.get_main_expr();
+    if (!ref) return false;
+    optional<metavar_decl> d = s.mctx().find_metavar_decl(mvar);
+    if (!d) return false;
+    auto tc = std::make_shared<type_context>(s.env(), s.get_options(), s.mctx(), d->get_context());
+    message_builder out(pip, tc, s.env(), get_global_ios(), pip->get_file_name(),
+                        pip->get_pos_info_or_some(*ref), ERROR);
+    out.set_exception(ex);
+    out << line() + format(header) + line() + s.pp();
+    out.report();
+    return true;
+}
+
 vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj const & _s) {
     tactic_state const & s = to_tactic_state(_s);
     optional<metavar_decl> g = s.get_main_goal_decl();
@@ -52,6 +71,16 @@ vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj con
         } else {
             return mk_tactic_success(to_obj(r), set_env_mctx(s, env, mctx));
         }
+    } catch (failed_to_synthesize_placeholder_exception & ex) {
+        if (report_failure(ex, ex.get_mvar(), "context:", ex.get_tactic_state()))
+            return mk_tactic_silent_exception(s);
+        else
+            return mk_tactic_exception(ex, s);
+    } catch (elaborator_exception & ex) {
+        if (report_failure(ex, *s.get_main_goal(), "state:", s))
+            return mk_tactic_silent_exception(s);
+        else
+            return mk_tactic_exception(ex, s);
     } catch (exception & ex) {
         return mk_tactic_exception(ex, s);
     }

src/frontends/lean/elaborator_exception.cpp → src/library/tactic/elaborator_exception.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/scope_pos_info_provider.h"
-#include "frontends/lean/elaborator_exception.h"
+#include "library/tactic/elaborator_exception.h"
 
 namespace lean {
 throwable * elaborator_exception::clone() const {

src/frontends/lean/elaborator_exception.h → src/library/tactic/elaborator_exception.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/sstream.h"
 #include "library/io_state.h"
+#include "library/tactic/tactic_state.h"
 
 namespace lean {
 class elaborator_exception : public formatted_exception {
@@ -19,6 +20,20 @@ class elaborator_exception : public formatted_exception {
     virtual void rethrow() const override { throw *this; }
 };
 
+class failed_to_synthesize_placeholder_exception : public elaborator_exception {
+    tactic_state m_state;
+public:
+    failed_to_synthesize_placeholder_exception(expr const & e, tactic_state const & s):
+        elaborator_exception(e, "don't know how to synthesize placeholder"),
+        m_state(s) {}
+    virtual throwable * clone() const override {
+        return new failed_to_synthesize_placeholder_exception(*m_expr, m_state);
+    }
+    virtual void rethrow() const override { throw *this; }
+    expr const & get_mvar() const { return *m_expr; }
+    tactic_state const & get_tactic_state() const { return m_state; }
+};
+
 class nested_elaborator_exception : public elaborator_exception {
     std::shared_ptr<elaborator_exception> m_exception;
     nested_elaborator_exception(optional<expr> const & ref, format const & fmt,

src/library/tactic/tactic_state.cpp

@@ -323,6 +323,10 @@ vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s) {
     return mk_vm_constructor(1, mk_vm_some(fn), mk_vm_none(), to_obj(s));
 }
 
+vm_obj mk_tactic_silent_exception(tactic_state const & s) {
+    return mk_vm_constructor(1, mk_vm_none(), mk_vm_none(), to_obj(s));
+}
+
 vm_obj mk_tactic_exception(vm_obj const & fn, vm_obj const & ref, tactic_state const & s) {
     return mk_vm_constructor(1, mk_vm_some(fn), ref, to_obj(s));
 }

src/library/tactic/tactic_state.h

@@ -142,6 +142,7 @@ vm_obj mk_tactic_exception(format const & fmt, tactic_state const & s);
 vm_obj mk_tactic_exception(sstream const & strm, tactic_state const & s);
 vm_obj mk_tactic_exception(char const * msg, tactic_state const & s);
 vm_obj mk_tactic_exception(std::function<format()> const & thunk, tactic_state const & s);
+vm_obj mk_tactic_silent_exception(tactic_state const & s);
 vm_obj mk_no_goals_exception(tactic_state const & s);
 
 format pp_expr(tactic_state const & s, expr const & e);

tests/lean/auto_quote_error.lean.expected.out

@@ -4,9 +4,3 @@ a b c : ℕ,
 h1 : a = b,
 h2 : b = c
 ⊢ b = c
-auto_quote_error.lean:5:2: error: elaborator failed
-state:
-a b c : ℕ,
-h1 : a = b,
-h2 : b = c
-⊢ c = a

tests/lean/auto_quote_error2.lean.expected.out

@@ -32,9 +32,3 @@ a b c : ℕ,
 h1 : a = b,
 h2 : b = c
 ⊢ b = c
-auto_quote_error2.lean:37:4: error: elaborator failed
-state:
-a b c : ℕ,
-h1 : a = b,
-h2 : b = c
-⊢ a = c

tests/lean/elab_error_recovery.lean.expected.out

@@ -19,7 +19,7 @@ half_baked : ℕ → ℕ
 elab_error_recovery.lean:10:11: error: failed to add declaration '_tactic' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   …
-elab_error_recovery.lean:12:14: error: invalid type ascription, expression has type
+elab_error_recovery.lean:12:20: error: invalid type ascription, expression has type
   list ?m_1
 but is expected to have type
   ℕ

tests/lean/exact_error_pos.lean

@@ -0,0 +1,16 @@
+constant f : nat → nat → nat
+
+
+def ex1 : nat :=
+begin
+  exact 10 +
+        (f 1 (f 0 tt))
+
+end
+
+
+def ex₂ : nat :=
+begin
+  apply 10 +
+        (f 1 (f 0 tt))
+end

tests/lean/exact_error_pos.lean.expected.out

@@ -0,0 +1,22 @@
+exact_error_pos.lean:7:14: error: type mismatch at application
+  f 0 tt
+term
+  tt
+has type
+  bool
+but is expected to have type
+  ℕ
+state:
+⊢ ℕ
+exact_error_pos.lean:4:4: warning: declaration 'ex1' uses sorry
+exact_error_pos.lean:15:14: error: type mismatch at application
+  f 0 tt
+term
+  tt
+has type
+  bool
+but is expected to have type
+  ℕ
+state:
+⊢ ℕ
+exact_error_pos.lean:12:4: warning: declaration 'ex₂' uses sorry

tests/lean/num2.lean.expected.out

@@ -3,7 +3,7 @@ z : N
 eq a gz : Prop
 num2.lean:24:7: error: failed to synthesize type class instance for
 ⊢ has_zero G
-num2.lean:24:6: error: invalid type ascription, expression has type
+num2.lean:24:7: error: invalid type ascription, expression has type
   N
 but is expected to have type
   G

tests/lean/num3.lean.expected.out

@@ -1,5 +1,5 @@
 @eq N a z : Prop
-num3.lean:14:10: error: invalid type ascription, expression has type
+num3.lean:14:11: error: invalid type ascription, expression has type
   N
 but is expected to have type
   num