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

feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression

Browse source 
Actually, the elaborator is the one reporting the unassigned
placeholders. The 'exact' tactic just makes the request.
To implement this feature we had to extend the elaboration interface
expected by the tactic framework.
This commit is contained in:
Leonardo de Moura 2014-11-28 14:59:35 -08:00
parent 04dfda99ab
commit 9516cd9ee3
7 changed files with 21 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -961,12 +961,12 @@ optional<expr> elaborator::get_pre_tactic_for(expr const & mvar) {
optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
try {
bool relax = m_relax_main_opaque;
auto fn = [=](goal const & g, name_generator const & ngen, expr const & e) {
auto fn = [=](goal const & g, name_generator const & ngen, expr const & e, bool report_unassigned) {
elaborator aux_elaborator(m_ctx, ngen);
// Disable tactic hints when processing expressions nested in tactics.
// We must do it otherwise, it is easy to make the system loop.
bool use_tactic_hints = false;
return aux_elaborator.elaborate_nested(g.to_context(), e, relax, use_tactic_hints);
return aux_elaborator.elaborate_nested(g.to_context(), e, relax, use_tactic_hints, report_unassigned);
};
return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
} catch (expr_to_tactic_exception & ex) {
@ -1274,7 +1274,7 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
/** \brief Elaborate expression \c e in context \c ctx. */
pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, expr const & n,
bool relax, bool use_tactic_hints) {
bool relax, bool use_tactic_hints, bool report_unassigned) {
if (infom()) {
if (auto ps = get_info_tactic_proof_state()) {
save_proof_state_info(*ps, n);
@ -1295,6 +1295,8 @@ pair<expr, constraints> elaborator::elaborate_nested(list<expr> const & ctx, exp
r = s.instantiate_all(r);
r = solve_unassigned_mvars(s, r);
copy_info_to_manager(s);
if (report_unassigned)
display_unassigned_mvars(r, s);
return mk_pair(r, rcs);
}

2
src/frontends/lean/elaborator.h
View file

@ -150,7 +150,7 @@ class elaborator : public coercion_info_manager {
expr apply(substitution & s, expr const & e, name_set & univ_params, buffer<name> & new_params);
std::tuple<expr, level_param_names> apply(substitution & s, expr const & e);
pair<expr, constraints> elaborate_nested(list<expr> const & g, expr const & e,
bool relax, bool use_tactic_hints);
bool relax, bool use_tactic_hints, bool report_unassigned);
public:
elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false);
std::tuple<expr, level_param_names> operator()(list<expr> const & ctx, expr const & e, bool _ensure_type,

2
src/frontends/lean/info_tactic.cpp
View file

@ -36,7 +36,7 @@ tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) {
// create dummy variable just to communicate position to the elaborator
expr dummy = mk_sort(mk_level_zero(), e.get_tag());
scoped_info_tactic_proof_state scope(ps);
fn(goal(), name_generator("dummy"), dummy);
fn(goal(), name_generator("dummy"), dummy, false);
return ps;
});
}

2
src/library/tactic/apply_tactic.cpp
View file

@ -158,7 +158,7 @@ tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool rev) {
name_generator ngen = s.get_ngen();
expr new_e;
buffer<constraint> cs;
auto ecs = elab(g, ngen.mk_child(), e);
auto ecs = elab(g, ngen.mk_child(), e, false);
new_e = ecs.first;
to_buffer(ecs.second, cs);
to_buffer(s.get_postponed(), cs);

5
src/library/tactic/elaborate.cpp
View file

@ -30,13 +30,14 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
}
optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
proof_state & s, expr const & e, optional<expr> const & expected_type) {
proof_state & s, expr const & e, optional<expr> const & expected_type,
bool report_unassigned) {
name_generator ngen = s.get_ngen();
substitution subst = s.get_subst();
goals const & gs = s.get_goals();
if (empty(gs))
return none_expr();
auto ecs = elab(head(gs), ngen.mk_child(), e);
auto ecs = elab(head(gs), ngen.mk_child(), e, report_unassigned);
expr new_e = ecs.first;
buffer<constraint> cs;
to_buffer(ecs.second, cs);

10
src/library/tactic/elaborate.h
View file

@ -12,8 +12,13 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
/** \brief Function for elaborating expressions nested in tactics.
Some tactics contain nested expression (aka pre-terms) that need to be elaborated.
The arguments are:
1- goal that will provide the context where the expression will be elaborated
2- name generator
3- expression to be elaborated
4- a flag indicating whether the elaborator should report unassigned/unsolved placeholders
*/
typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &)> elaborate_fn;
typedef std::function<pair<expr, constraints>(goal const &, name_generator const &, expr const &, bool)> elaborate_fn;
/** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed
with respect to (local context of) the first goal in \c s. The constraints generated during elaboration
@ -26,5 +31,6 @@ typedef std::function<pair<expr, constraints>(goal const &, name_generator const
is not modified.
*/
optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
proof_state & s, expr const & e, optional<expr> const & expected_type = optional<expr>());
proof_state & s, expr const & e, optional<expr> const & expected_type = optional<expr>(),
bool report_unassigned = false);
}

3
src/library/tactic/exact_tactic.cpp
View file

@ -17,7 +17,8 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
if (!gs)
return none_proof_state();
expr t = head(gs).get_type();
if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t))) {
bool report_unassigned = true;
if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), report_unassigned)) {
goals const & gs = new_s.get_goals();
goal const & g = head(gs);
expr new_p = g.abstract(*new_e);