michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/elaborator) add trick for improving error messages when mixing tactics, elaboration and exact tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-02 18:58:32 -07:00
parent c3abf81382
commit 138267b53a
3 changed files with 20 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/frontends/lean/elaborator.cpp
View file

@ -640,10 +640,25 @@ public:
}
}
// For each occurrence of \c exact_tac in \c pre_tac, display its unassigned metavariables.
// This is a trick to improve the quality of the error messages.
void check_exact_tacs(expr const & pre_tac, substitution const & s) {
for_each(pre_tac, [&](expr const & e, unsigned) {
expr const & f = get_app_fn(e);
if (is_constant(f) && const_name(f) == get_exact_tac_name()) {
display_unassigned_mvars(e, s);
return false;
} else {
return true;
}
});
}
optional<expr> get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) {
if (auto it = m_tactic_hints.find(mlocal_name(mvar))) {
expr pre_tac = subst.instantiate(*it);
pre_tac = solve_unassigned_mvars(subst, pre_tac, visited);
check_exact_tacs(pre_tac, subst);
return some_expr(pre_tac);
} else {
// TODO(Leo): m_env tactic hints

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

@ -81,6 +81,8 @@ register_unary_tac::register_unary_tac(name const & n, std::function<tactic(tact
}
static name g_tac("tactic");
static name g_exact_tac_name(g_tac, "exact");
name const & get_exact_tac_name() { return g_exact_tac_name; }
static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); });
static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); });
static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { return assumption_tactic(); });
@ -110,7 +112,7 @@ static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr c
static register_tac reg_apply(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) {
return apply_tactic(app_arg(e));
});
static register_tac reg_exact(name(g_tac, "exact"), [](type_checker &, expr const & e, pos_info_provider const *) {
static register_tac reg_exact(g_exact_tac_name, [](type_checker &, expr const & e, pos_info_provider const *) {
return exact_tactic(app_arg(e));
});
static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) {

2
src/library/tactic/expr_to_tactic.h
View file

@ -28,6 +28,8 @@ struct register_unary_tac {
register_unary_tac(name const & n, std::function<tactic(tactic const &)> f);
};
name const & get_exact_tac_name();
tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p);
expr mk_by(expr const & e);
bool is_by(expr const & e);