From 3c71d7eda2013cc5cbc67e4d9a7557d1ef23da10 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 25 Sep 2016 18:34:04 -0700 Subject: [PATCH] feat(frontends/lean,library/tactic/tactic_state): improve error localization --- library/init/meta/tactic.lean | 16 ++++++------ src/frontends/lean/elaborator.cpp | 11 ++++++-- src/library/tactic/tactic_state.cpp | 25 ++++++++++++++----- src/library/tactic/tactic_state.h | 8 +++--- tests/lean/auto_quote_error.lean | 6 +++++ tests/lean/auto_quote_error.lean.expected.out | 6 +++++ 6 files changed, 53 insertions(+), 19 deletions(-) create mode 100644 tests/lean/auto_quote_error.lean create mode 100644 tests/lean/auto_quote_error.lean.expected.out diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 770d054e71..7d0439187e 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -24,7 +24,7 @@ meta instance : has_to_format tactic_state := inductive tactic_result (A : Type) | success : A → tactic_state → tactic_result -| exception : (unit → format) → tactic_state → tactic_result +| exception : (unit → format) → option expr → tactic_state → tactic_result open tactic_result @@ -33,8 +33,8 @@ variables {A : Type} variables [has_to_string A] meta definition tactic_result_to_string : tactic_result A → string -| (success a s) := to_string a -| (exception .A e s) := "Exception: " ++ to_string (e ()) +| (success a s) := to_string a +| (exception .A t ref s) := "Exception: " ++ to_string (t ()) meta instance : has_to_string (tactic_result A) := ⟨tactic_result_to_string⟩ @@ -66,7 +66,7 @@ meta definition tactic_return (a : A) : tactic A := meta definition tactic_orelse {A : Type} (t₁ t₂ : tactic A) : tactic A := λ s, tactic_result.cases_on (t₁ s) success - (λ e₁ s', tactic_result.cases_on (t₂ s) + (λ e₁ ref₁ s', tactic_result.cases_on (t₂ s) success (exception A)) end @@ -75,7 +75,7 @@ meta instance : monad tactic := ⟨@tactic_fmap, @tactic_return, @tactic_bind⟩ meta definition tactic.fail {A B : Type} [has_to_format B] (msg : B) : tactic A := -λ s, exception A (λ u, to_fmt msg) s +λ s, exception A (λ u, to_fmt msg) none s meta definition tactic.failed {A : Type} : tactic A := tactic.fail "failed" @@ -89,7 +89,7 @@ variables {A : Type} meta definition try (t : tactic A) : tactic unit := λ s, tactic_result.cases_on (t s) (λ a, success ()) - (λ e s', success () s) + (λ e ref s', success () s) meta definition skip : tactic unit := success () @@ -116,13 +116,13 @@ repeat_at_most 100000 meta definition returnex (e : exceptional A) : tactic A := λ s, match e with | (exceptional.success a) := tactic_result.success a s -| (exceptional.exception .A f) := tactic_result.exception A (λ u, f options.mk) s -- TODO(Leo): extract options from environment +| (exceptional.exception .A f) := tactic_result.exception A (λ u, f options.mk) none s -- TODO(Leo): extract options from environment end meta definition returnopt (e : option A) : tactic A := λ s, match e with | (some a) := tactic_result.success a s -| none := tactic_result.exception A (λ u, to_fmt "failed") s +| none := tactic_result.exception A (λ u, to_fmt "failed") none s end /- Decorate t's exceptions with msg -/ diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 561a629f17..556342d0d1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2133,8 +2133,15 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) { m_env = new_s->env(); m_ctx.set_env(m_env); m_ctx.set_mctx(mctx); - } else if (optional> ex = is_tactic_exception(S, m_opts, r)) { - throw_unsolved_tactic_state(ex->second, ex->first, ref); + } else if (optional ex = is_tactic_exception(S, r)) { + format fmt = std::get<0>(*ex); + optional ref1 = std::get<1>(*ex); + tactic_state s1 = std::get<2>(*ex); + pos_info_provider * provider = get_pos_info_provider(); + if (ref1 && provider && provider->get_pos_info(*ref1)) + throw elaborator_exception(*ref1, fmt); + else + throw_unsolved_tactic_state(s1, fmt, ref); } else { lean_unreachable(); } diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 91bafce418..90f391e4ac 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -223,12 +223,15 @@ optional is_tactic_success(vm_obj const & o) { } } -optional> is_tactic_exception(vm_state & S, options const & opts, vm_obj const & ex) { +optional is_tactic_exception(vm_state & S, vm_obj const & ex) { if (is_constructor(ex) && cidx(ex) == 1) { - vm_obj fmt = S.invoke(cfield(ex, 0), to_obj(opts)); - return optional>(mk_pair(to_format(fmt), to_tactic_state(cfield(ex, 1)))); + vm_obj fmt = S.invoke(cfield(ex, 0), mk_vm_unit()); + optional ref; + if (!is_none(cfield(ex, 1))) + ref = to_expr(get_some_value(cfield(ex, 1))); + return optional(to_format(fmt), ref, to_tactic_state(cfield(ex, 2))); } else { - return optional>(); + return optional(); } } @@ -241,13 +244,23 @@ vm_obj mk_tactic_success(tactic_state const & s) { } vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s) { - return mk_vm_constructor(1, fn, to_obj(s)); + return mk_vm_constructor(1, fn, 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, fn, ref, to_obj(s)); } vm_obj mk_tactic_exception(throwable const & ex, tactic_state const & s) { vm_obj _ex = to_obj(ex); vm_obj fn = mk_vm_closure(get_throwable_to_format_fun_idx(), 1, &_ex); - return mk_tactic_exception(fn, s); + optional ref; + if (auto kex = dynamic_cast(&ex)) + ref = kex->get_main_expr(); + else if (auto fex = dynamic_cast(&ex)) + ref = fex->get_main_expr(); + vm_obj _ref = ref ? mk_vm_some(to_obj(*ref)) : mk_vm_none(); + return mk_tactic_exception(fn, _ref, s); } vm_obj mk_tactic_exception(format const & fmt, tactic_state const & s) { diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 944f718715..c3b73761f7 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -108,9 +108,11 @@ format pp_indented_expr(tactic_state const & s, expr const & e); /* If r is (base_tactic_result.success a s), then return s */ optional is_tactic_success(vm_obj const & r); -/* If ex is (base_tactic_result.exception fn), then return (fn opts). - The vm_state S is used to execute (fn opts). */ -optional> is_tactic_exception(vm_state & S, options const & opts, vm_obj const & ex); +typedef std::tuple, tactic_state> tactic_exception_info; + +/* If ex is (base_tactic_result.exception fn), then return (fn ()). + The vm_state S is used to execute (fn ()). */ +optional is_tactic_exception(vm_state & S, vm_obj const & ex); type_context mk_type_context_for(tactic_state const & s, transparency_mode m = transparency_mode::Semireducible); type_context mk_type_context_for(tactic_state const & s, local_context const & lctx, transparency_mode m = transparency_mode::Semireducible); diff --git a/tests/lean/auto_quote_error.lean b/tests/lean/auto_quote_error.lean new file mode 100644 index 0000000000..ea2c2851cd --- /dev/null +++ b/tests/lean/auto_quote_error.lean @@ -0,0 +1,6 @@ +example (a b c : nat) : a = b → b = c → c = a := +begin + intro h1, + intro h2, + exact eq.symm (eq.trans h1 _), +end diff --git a/tests/lean/auto_quote_error.lean.expected.out b/tests/lean/auto_quote_error.lean.expected.out new file mode 100644 index 0000000000..b734c1b9ae --- /dev/null +++ b/tests/lean/auto_quote_error.lean.expected.out @@ -0,0 +1,6 @@ +auto_quote_error.lean:5:29: error: don't know how to synthesize placeholder +state: +a b c : ℕ, +h1 : a = b, +h2 : b = c +⊢ b = c