max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic): store tactic_state at failure

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-13 15:24:21 -07:00
parent a9cae34a75
commit 9bcb4e05db
12 changed files with 99 additions and 76 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
library/init/meta/base_tactic.lean
View file

@ -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 -/

51
src/frontends/lean/old_elaborator.cpp
View file

@ -1867,7 +1867,7 @@ optional<expr> 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<tactic_state> 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<tactic_state> new_s = is_tactic_success(r)) {
return *new_s;
} else if (optional<format> ex = is_tactic_exception(S, opts, r)) {
throw_elaborator_exception(tactic, [=](formatter const &) { return *ex; });
return some_tactic_state(*new_s);
} else if (optional<pair<format, tactic_state>> 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<expr> 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<tactic_state> 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;
}

5
src/frontends/lean/old_elaborator.h
View file

@ -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<expr> mvar2meta;
class tactic_state;
/** \brief Helper class for implementing the \c elaborate functions. */
class old_elaborator : public coercion_info_manager {
typedef name_map<expr> local_tactic_hints;
@ -148,6 +148,8 @@ class old_elaborator : public coercion_info_manager {
pair<expr, constraint_seq> 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<expr> get_tactic_for(expr const & mvar);
optional<tactic_state> execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar);
// optional<tactic> 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);

4
src/library/tactic/assumption_tactic.cpp
View file

@ -24,11 +24,11 @@ optional<tactic_state> assumption(tactic_state const & s) {
vm_obj tactic_assumption(vm_obj const & s) {
optional<metavar_decl> 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() {

9
src/library/tactic/clear_tactic.cpp
View file

@ -10,17 +10,18 @@ Author: Leonardo de Moura
namespace lean {
vm_obj clear(name const & n, tactic_state const & s) {
optional<metavar_decl> 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<local_decl> 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<local_decl> 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);

4
src/library/tactic/intro_tactic.cpp
View file

@ -12,14 +12,14 @@ Author: Leonardo de Moura
namespace lean {
vm_obj intro(name const & n, tactic_state const & s) {
optional<metavar_decl> 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)) {

4
src/library/tactic/rename_tactic.cpp
View file

@ -10,11 +10,11 @@ Author: Leonardo de Moura
namespace lean {
vm_obj rename(name const & from, name const & to, tactic_state const & s) {
optional<metavar_decl> 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);

4
src/library/tactic/revert_tactic.cpp
View file

@ -21,14 +21,14 @@ tactic_state revert(buffer<expr> & locals, tactic_state const & s) {
vm_obj revert(list<name> const & ns, tactic_state const & s) {
optional<metavar_decl> 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<expr> locals;
for (name const & n : ns) {
if (optional<local_decl> 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));

48
src/library/tactic/tactic_state.cpp
View file

@ -150,12 +150,12 @@ optional<tactic_state> is_tactic_success(vm_obj const & o) {
}
}
optional<format> is_tactic_exception(vm_state & S, options const & opts, vm_obj const & ex) {
optional<pair<format, tactic_state>> 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<format>(to_format(fmt));
return optional<pair<format, tactic_state>>(mk_pair(to_format(fmt), to_tactic_state(cfield(ex, 1))));
} else {
return optional<format>();
return optional<pair<format, tactic_state>>();
}
}
@ -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<metavar_decl> 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<metavar_decl> 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<local_decl> 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<metavar_decl> 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<expr> r;
lctx.for_each([&](local_decl const & d) { r.push_back(d.mk_ref()); });

14
src/library/tactic/tactic_state.h
View file

@ -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<tactic_state> 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<format> is_tactic_exception(vm_state & S, options const & opts, vm_obj const & ex);
optional<pair<format, tactic_state>> 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);

4
tests/lean/tactic_failure.lean Normal file
View file

@ -0,0 +1,4 @@
open tactic
example (A B : Type) : B → A :=
by do intro "Hb", assumption

8
tests/lean/tactic_failure.lean.expected.out Normal file
View file

@ -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