From 9bcb4e05dbfb24bd41566484adc98eabc5b27ebf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jun 2016 15:24:21 -0700 Subject: [PATCH] feat(library/tactic): store tactic_state at failure --- library/init/meta/base_tactic.lean | 20 ++++---- src/frontends/lean/old_elaborator.cpp | 51 ++++++++++++--------- src/frontends/lean/old_elaborator.h | 5 +- src/library/tactic/assumption_tactic.cpp | 4 +- src/library/tactic/clear_tactic.cpp | 9 ++-- src/library/tactic/intro_tactic.cpp | 4 +- src/library/tactic/rename_tactic.cpp | 4 +- src/library/tactic/revert_tactic.cpp | 4 +- src/library/tactic/tactic_state.cpp | 48 +++++++++---------- src/library/tactic/tactic_state.h | 14 +++--- tests/lean/tactic_failure.lean | 4 ++ tests/lean/tactic_failure.lean.expected.out | 8 ++++ 12 files changed, 99 insertions(+), 76 deletions(-) create mode 100644 tests/lean/tactic_failure.lean create mode 100644 tests/lean/tactic_failure.lean.expected.out diff --git a/library/init/meta/base_tactic.lean b/library/init/meta/base_tactic.lean index 3344c81ac4..4a7186fca9 100644 --- a/library/init/meta/base_tactic.lean +++ b/library/init/meta/base_tactic.lean @@ -13,7 +13,7 @@ We "merge" them for performance reasons. -/ inductive base_tactic_result (S : Type) (A : Type) := | success : A → S → base_tactic_result S A -| exception : (options → format) → base_tactic_result S A +| exception : (options → format) → S → base_tactic_result S A section open base_tactic_result @@ -22,7 +22,7 @@ variables [has_to_string A] protected meta_definition base_tactic_result.to_string : base_tactic_result S A → string | (success a s) := to_string a -| (exception S A e) := "Exception: " + to_string (e options.mk) +| (exception A e s) := "Exception: " + to_string (e options.mk) protected meta_definition base_tactic_result.has_to_string [instance] : has_to_string (base_tactic_result S A) := has_to_string.mk base_tactic_result.to_string @@ -38,12 +38,12 @@ open base_tactic_result inline protected meta_definition fmap (f : A → B) (t : base_tactic S A) : base_tactic S B := λ s, base_tactic_result.cases_on (t s) (λ a s', success (f a) s') - (λ e, !exception e) + (λ e s', exception B e s') inline protected meta_definition bind (t₁ : base_tactic S A) (t₂ : A → base_tactic S B) : base_tactic S B := λ s : S, base_tactic_result.cases_on (t₁ s) (λ a s', t₂ a s') - (λ e, !exception e) + (λ e s', exception B e s') inline protected meta_definition return (a : A) : base_tactic S A := λ s, success a s @@ -58,19 +58,19 @@ variables {S A : Type} open base_tactic_result meta_definition fail (e : format) : base_tactic S unit := -λ s, !exception (λ u, e) +λ s, exception unit (λ u, e) s meta_definition try (t : base_tactic S A) : base_tactic S unit := λ s, base_tactic_result.cases_on (t s) (λ a, success ()) - (λ e, success () s) + (λ e s', success () s) meta_definition or_else (t₁ t₂ : base_tactic S A) : base_tactic S A := λ s, base_tactic_result.cases_on (t₁ s) success - (λ e₁, base_tactic_result.cases_on (t₂ s) + (λ e₁ s', base_tactic_result.cases_on (t₂ s) success - (λ e₂, !exception (λ u, e₁ u + format.line + e₂ u))) + (exception A)) infix `<|>`:1 := or_else @@ -95,8 +95,8 @@ meta_definition repeat_exactly : nat → base_tactic S unit → base_tactic S un meta_definition returnex (e : exceptional A) : base_tactic S A := λ s, match e with -| exceptional.success a := base_tactic_result.success a s -| !exceptional.exception f := !base_tactic_result.exception f +| exceptional.success a := base_tactic_result.success a s +| exceptional.exception A f := base_tactic_result.exception A f s end /- Decorate t's exceptions with msg -/ diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index 72df572cc9..91ed09091d 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -1867,7 +1867,7 @@ optional old_elaborator::get_tactic_for(expr const & mvar) { } } -void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, char const * msg, +void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, format const & fmt, expr const & pos) { lean_assert(is_metavar(mvar)); if (!m_displayed_errors.contains(mlocal_name(mvar))) { @@ -1876,11 +1876,16 @@ void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_sta flycheck_error err(ios()); if (!err.enabled() || save_error(pip(), pos)) { display_error_pos(out.get_stream(), out.get_options(), pip(), pos); - out << " " << msg << "\n" << ts.pp(ios().get_formatter_factory()) << endl; + out << " " << fmt << "\n" << ts.pp(ios().get_formatter_factory()) << endl; } } } +void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, char const * msg, + expr const & pos) { + return display_unsolved_tactic_state(mvar, ts, format(msg), pos); +} + void old_elaborator::display_unsolved_tactic_state(expr const & mvar, tactic_state const & ps, char const * msg) { display_unsolved_tactic_state(mvar, ps, msg, mvar); } @@ -1901,14 +1906,14 @@ static tactic_state to_tactic_state(environment const & env, options const & opt return mk_tactic_state_for(env, opts, lctx, new_type); } -static tactic_state execute_tactic(environment const & env, options const & opts, expr const & tactic, - tactic_state const & s) { +optional old_elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar) { name tactic_name("_tactic"); - expr tactic_type = mk_app(mk_constant("tactic", {mk_level_one()}), mk_constant("unit")); + expr tactic_type = ::lean::mk_app(mk_constant("tactic", {mk_level_one()}), mk_constant("unit")); /* compile tactic */ - bool use_conv_opt = true; - bool is_trusted = false; - environment new_env = env; + environment new_env = env(); + options const & opts = ios().get_options(); + bool use_conv_opt = true; + bool is_trusted = false; auto cd = check(new_env, mk_definition(new_env, tactic_name, {}, tactic_type, tactic, use_conv_opt, is_trusted)); new_env = new_env.add(cd); new_env = vm_compile(new_env, new_env.get(tactic_name)); @@ -1924,11 +1929,12 @@ static tactic_state execute_tactic(environment const & env, options const & opts } vm_obj r = S.top(); if (optional new_s = is_tactic_success(r)) { - return *new_s; - } else if (optional ex = is_tactic_exception(S, opts, r)) { - throw_elaborator_exception(tactic, [=](formatter const &) { return *ex; }); + return some_tactic_state(*new_s); + } else if (optional> ex = is_tactic_exception(S, opts, r)) { + display_unsolved_tactic_state(mvar, ex->second, ex->first, mvar); + return none_tactic_state(); } else { - lean_unreachable(); + return none_tactic_state(); } } @@ -1955,17 +1961,18 @@ void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name tactic_state ts = to_tactic_state(env(), opts, *meta, type, new_locals); if (optional tac = get_tactic_for(mvar)) { expr tactic = subst.instantiate(*tac); - tactic_state new_ts = execute_tactic(env(), opts, tactic, ts); - metavar_context mctx = new_ts.mctx(); - expr r = mctx.instantiate(new_ts.main()); - if (has_expr_metavar(r)) { - display_unsolved_tactic_state(mvar, new_ts, "tactic failed, result contains meta-variables"); - throw_elaborator_exception("tactic failed, result contains meta-variables", r); + if (optional new_ts = execute_tactic(tactic, ts, mvar)) { + metavar_context mctx = new_ts->mctx(); + expr r = mctx.instantiate(new_ts->main()); + if (has_expr_metavar(r)) { + display_unsolved_tactic_state(mvar, *new_ts, "tactic failed, result contains meta-variables"); + throw_elaborator_exception("tactic failed, result contains meta-variables", r); + } + metavar_decl main_decl = *mctx.get_metavar_decl(new_ts->main()); + type_context aux_ctx(env(), opts, mctx, main_decl.get_context()); + r = aux_ctx.mk_lambda(new_locals, r); + subst.assign(mvar, r); } - metavar_decl main_decl = *mctx.get_metavar_decl(new_ts.main()); - type_context aux_ctx(env(), opts, mctx, main_decl.get_context()); - r = aux_ctx.mk_lambda(new_locals, r); - subst.assign(mvar, r); } return; } diff --git a/src/frontends/lean/old_elaborator.h b/src/frontends/lean/old_elaborator.h index 22d364015f..d7e2930090 100644 --- a/src/frontends/lean/old_elaborator.h +++ b/src/frontends/lean/old_elaborator.h @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/old_local_context.h" #include "library/old_type_checker.h" +#include "library/tactic/tactic_state.h" #include "frontends/lean/elaborator_context.h" #include "frontends/lean/coercion_elaborator.h" #include "frontends/lean/util.h" @@ -21,7 +22,6 @@ Author: Leonardo de Moura namespace lean { /** \brief Mapping from metavariable names to metavariable applications (?M ...) */ typedef name_map mvar2meta; -class tactic_state; /** \brief Helper class for implementing the \c elaborate functions. */ class old_elaborator : public coercion_info_manager { typedef name_map local_tactic_hints; @@ -148,6 +148,8 @@ class old_elaborator : public coercion_info_manager { pair visit(expr const & e); expr visit(expr const & e, constraint_seq & cs); unify_result_seq solve(constraint_seq const & cs); + void display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, format const & fmt, + expr const & pos); void display_unsolved_tactic_state(expr const & mvar, tactic_state const & ts, char const * msg, expr const & pos); void display_unsolved_tactic_state(expr const & mvar, tactic_state const & ps, char const * msg); @@ -155,6 +157,7 @@ class old_elaborator : public coercion_info_manager { // void display_unsolved_subgoals(expr const & mvar, proof_state const & ps); // void display_tactic_exception(tactic_exception const & ex, proof_state const & ps, expr const & pre_tac); optional get_tactic_for(expr const & mvar); + optional execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar); // optional pre_tactic_to_tactic(expr const & pre_tac); // bool try_using(substitution & subst, expr const & mvar, proof_state const & ps, // expr const & pre_tac, tactic const & tac, bool show_failure); diff --git a/src/library/tactic/assumption_tactic.cpp b/src/library/tactic/assumption_tactic.cpp index b7acd7a20e..7813c2f497 100644 --- a/src/library/tactic/assumption_tactic.cpp +++ b/src/library/tactic/assumption_tactic.cpp @@ -24,11 +24,11 @@ optional assumption(tactic_state const & s) { vm_obj tactic_assumption(vm_obj const & s) { optional g = to_tactic_state(s).get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(to_tactic_state(s)); if (auto r = assumption(to_tactic_state(s))) return mk_tactic_success(*r); else - return mk_tactic_exception("assumption tactic failed"); + return mk_tactic_exception("assumption tactic failed", to_tactic_state(s)); } void initialize_assumption_tactic() { diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index 0375771979..c6e65d3634 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -10,17 +10,18 @@ Author: Leonardo de Moura namespace lean { vm_obj clear(name const & n, tactic_state const & s) { optional g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(s); metavar_context mctx = s.mctx(); local_context lctx = g->get_context(); optional d = lctx.get_local_decl_from_user_name(n); if (!d) - return mk_tactic_exception(sstream() << "clear tactic failed, unknown '" << n << "' hypothesis"); + return mk_tactic_exception(sstream() << "clear tactic failed, unknown '" << n << "' hypothesis", s); expr l = d->mk_ref(); if (depends_on(g->get_type(), 1, &l)) - return mk_tactic_exception(sstream() << "clear tactic failed, result type depends on '" << n << "'"); + return mk_tactic_exception(sstream() << "clear tactic failed, result type depends on '" << n << "'", s); if (optional d2 = lctx.has_dependencies(*d)) - return mk_tactic_exception(sstream() << "clear tactic failed, '" << d2->get_pp_name() << "' depends on '" << n << "'"); + return mk_tactic_exception(sstream() << "clear tactic failed, '" << d2->get_pp_name() << "' depends on '" + << n << "'", s); lctx.clear(*d); expr new_g = mctx.mk_metavar_decl(lctx, g->get_type()); mctx.assign(head(s.goals()), new_g); diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp index bf4c392e5b..0a2de7d3ce 100644 --- a/src/library/tactic/intro_tactic.cpp +++ b/src/library/tactic/intro_tactic.cpp @@ -12,14 +12,14 @@ Author: Leonardo de Moura namespace lean { vm_obj intro(name const & n, tactic_state const & s) { optional g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(s); metavar_context mctx = s.mctx(); type_context ctx = mk_type_context_for(s, mctx); expr type = g->get_type(); if (!is_pi(type) && !is_let(type)) { type = ctx.whnf(type); if (!is_pi(type)) - return mk_tactic_exception("intro tactic failed, Pi/let expression expected"); + return mk_tactic_exception("intro tactic failed, Pi/let expression expected", s); } local_context lctx = g->get_context(); if (is_pi(type)) { diff --git a/src/library/tactic/rename_tactic.cpp b/src/library/tactic/rename_tactic.cpp index d681f49fbd..6a1b9d827c 100644 --- a/src/library/tactic/rename_tactic.cpp +++ b/src/library/tactic/rename_tactic.cpp @@ -10,11 +10,11 @@ Author: Leonardo de Moura namespace lean { vm_obj rename(name const & from, name const & to, tactic_state const & s) { optional g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(s); metavar_context mctx = s.mctx(); local_context lctx = g->get_context(); if (!lctx.rename_user_name(from, to)) { - return mk_tactic_exception(sstream() << "rename tactic failed, unknown '" << from << "' hypothesis"); + return mk_tactic_exception(sstream() << "rename tactic failed, unknown '" << from << "' hypothesis", s); } expr new_g = mctx.mk_metavar_decl(lctx, g->get_type()); mctx.assign(head(s.goals()), new_g); diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/tactic/revert_tactic.cpp index 7336b577e7..ecb895558f 100644 --- a/src/library/tactic/revert_tactic.cpp +++ b/src/library/tactic/revert_tactic.cpp @@ -21,14 +21,14 @@ tactic_state revert(buffer & locals, tactic_state const & s) { vm_obj revert(list const & ns, tactic_state const & s) { optional g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(s); local_context lctx = g->get_context(); buffer locals; for (name const & n : ns) { if (optional const & d = lctx.get_local_decl_from_user_name(n)) { locals.push_back(d->mk_ref()); } else { - return mk_tactic_exception(sstream() << "revert tactic failed, unknown '" << n << "' hypothesis"); + return mk_tactic_exception(sstream() << "revert tactic failed, unknown '" << n << "' hypothesis", s); } } return mk_tactic_success(revert(locals, s)); diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 2001a5676e..b24b73269f 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -150,12 +150,12 @@ 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, options const & opts, vm_obj const & ex) { if (is_constructor(ex) && cidx(ex) == 1) { vm_obj fmt = S.invoke(cfield(ex, 0), to_obj(opts)); - return optional(to_format(fmt)); + return optional>(mk_pair(to_format(fmt), to_tactic_state(cfield(ex, 1)))); } else { - return optional(); + return optional>(); } } @@ -167,32 +167,32 @@ vm_obj mk_tactic_success(tactic_state const & s) { return mk_tactic_success(mk_vm_unit(), s); } -vm_obj mk_tactic_exception(vm_obj const & fn) { - return mk_vm_constructor(1, fn); +vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s) { + return mk_vm_constructor(1, fn, to_obj(s)); } -vm_obj mk_tactic_exception(throwable const & ex) { +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); + return mk_tactic_exception(fn, s); } -vm_obj mk_tactic_exception(format const & fmt) { - vm_state const & s = get_vm_state(); - vm_decl K = *s.get_decl(get_combinator_K_name()); - return mk_tactic_exception(mk_vm_closure(K.get_idx(), to_obj(fmt), mk_vm_unit(), mk_vm_unit())); +vm_obj mk_tactic_exception(format const & fmt, tactic_state const & s) { + vm_state const & S = get_vm_state(); + vm_decl K = *S.get_decl(get_combinator_K_name()); + return mk_tactic_exception(mk_vm_closure(K.get_idx(), to_obj(fmt), mk_vm_unit(), mk_vm_unit()), s); } -vm_obj mk_tactic_exception(char const * msg) { - return mk_tactic_exception(format(msg)); +vm_obj mk_tactic_exception(char const * msg, tactic_state const & s) { + return mk_tactic_exception(format(msg), s); } -vm_obj mk_tactic_exception(sstream const & s) { - return mk_tactic_exception(s.str().c_str()); +vm_obj mk_tactic_exception(sstream const & strm, tactic_state const & s) { + return mk_tactic_exception(strm.str().c_str(), s); } -vm_obj mk_no_goals_exception() { - return mk_tactic_exception("tactic failed, there are no goals to be solved"); +vm_obj mk_no_goals_exception(tactic_state const & s) { + return mk_tactic_exception("tactic failed, there are no goals to be solved", s); } vm_obj tactic_result(vm_obj const & o) { @@ -216,7 +216,7 @@ vm_obj tactic_format_result(vm_obj const & o) { vm_obj tactic_target(vm_obj const & o) { tactic_state const & s = to_tactic_state(o); optional g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(s); return mk_tactic_success(to_obj(g->get_type()), s); } @@ -257,7 +257,7 @@ vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) { try { return mk_tactic_success(to_obj(ctx.infer(to_expr(e))), s); } catch (exception & ex) { - return mk_tactic_exception(ex); + return mk_tactic_exception(ex, s); } } @@ -268,7 +268,7 @@ vm_obj tactic_whnf(vm_obj const & e, vm_obj const & s0) { try { return mk_tactic_success(to_obj(ctx.whnf(to_expr(e))), s); } catch (exception & ex) { - return mk_tactic_exception(ex); + return mk_tactic_exception(ex, s); } } @@ -280,24 +280,24 @@ vm_obj tactic_unify_core(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, bool r = ctx.is_def_eq(to_expr(e1), to_expr(e2)); return mk_tactic_success(mk_vm_bool(r), set_mctx(s, mctx)); } catch (exception & ex) { - return mk_tactic_exception(ex); + return mk_tactic_exception(ex, s); } } vm_obj tactic_get_local(vm_obj const & n, vm_obj const & s0) { tactic_state const & s = to_tactic_state(s0); optional g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(s); local_context lctx = g->get_context(); optional d = lctx.get_local_decl_from_user_name(to_name(n)); - if (!d) return mk_tactic_exception(sstream() << "get_local tactic failed, unknown '" << to_name(n) << "' local"); + if (!d) return mk_tactic_exception(sstream() << "get_local tactic failed, unknown '" << to_name(n) << "' local", s); return mk_tactic_success(to_obj(d->mk_ref()), s); } vm_obj tactic_local_context(vm_obj const & s0) { tactic_state const & s = to_tactic_state(s0); optional g = s.get_main_goal_decl(); - if (!g) return mk_no_goals_exception(); + if (!g) return mk_no_goals_exception(s); local_context lctx = g->get_context(); buffer r; lctx.for_each([&](local_decl const & d) { r.push_back(d.mk_ref()); }); diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index cd9ed4372a..cffe46444b 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -86,19 +86,19 @@ vm_obj to_obj(transparency_mode m); vm_obj mk_tactic_success(vm_obj const & a, tactic_state const & s); vm_obj mk_tactic_success(tactic_state const & s); -vm_obj mk_tactic_exception(vm_obj const & fn); -vm_obj mk_tactic_exception(throwable const & ex); -vm_obj mk_tactic_exception(format const & fmt); -vm_obj mk_tactic_exception(sstream const & s); -vm_obj mk_tactic_exception(char const * msg); -vm_obj mk_no_goals_exception(); +vm_obj mk_tactic_exception(vm_obj const & fn, tactic_state const & s); +vm_obj mk_tactic_exception(throwable const & ex, tactic_state const & s); +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_no_goals_exception(tactic_state const & s); /* 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); +optional> is_tactic_exception(vm_state & S, options const & opts, vm_obj const & ex); type_context_cache & get_type_context_cache_for(environment const & env, options const & o); type_context_cache & get_type_context_cache_for(tactic_state const & s); diff --git a/tests/lean/tactic_failure.lean b/tests/lean/tactic_failure.lean new file mode 100644 index 0000000000..b57ca827cb --- /dev/null +++ b/tests/lean/tactic_failure.lean @@ -0,0 +1,4 @@ +open tactic + +example (A B : Type) : B → A := +by do intro "Hb", assumption diff --git a/tests/lean/tactic_failure.lean.expected.out b/tests/lean/tactic_failure.lean.expected.out new file mode 100644 index 0000000000..9c1b674dba --- /dev/null +++ b/tests/lean/tactic_failure.lean.expected.out @@ -0,0 +1,8 @@ +tactic_failure.lean:4:0: error: assumption tactic failed +A : Type, +B : Type, +Hb : B +⊢ A +tactic_failure.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + ?M_1