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

feat(library/tactic): elaborate 'exact' tactic argument at tactic execution time

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-22 18:34:45 -07:00
parent c50227ea6e
commit 3aec70b92c
2 changed files with 35 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/tools/tactic.lean
View file

@ -57,7 +57,7 @@ notation `intros` := intro_list expr_list.nil
notation `intros` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := intro_list l
opaque definition unfold {B : Type} (b : B) : tactic := builtin
opaque definition exact {B : Type} (b : B) : tactic := builtin
opaque definition exact (e : expr) : tactic := builtin
opaque definition trace (s : string) : tactic := builtin
infixl `;`:15 := and_then
notation `[` h:10 `|`:10 r:(foldl 10 `|` (e r, or_else r e) h) `]` := r

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

@ -5,29 +5,45 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/type_checker.h"
#include "library/unifier.h"
#include "library/reducible.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
namespace lean {
tactic exact_tactic(expr const & _e) {
return tactic01([=](environment const & env, io_state const &, proof_state const & s) {
type_checker tc(env);
tactic exact_tactic(elaborate_fn const & elab, expr const & e) {
return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
name_generator ngen = s.get_ngen();
substitution subst = s.get_subst();
goals const & gs = s.get_goals();
goal const & g = head(gs);
expr e = subst.instantiate(_e);
auto e_t_cs = tc.infer(e);
expr e_t = subst.instantiate(e_t_cs.first);
expr t = subst.instantiate(g.get_type());
auto dcs = tc.is_def_eq(e_t, t);
if (dcs.first && !dcs.second && !e_t_cs.second) {
expr new_p = g.abstract(e);
check_has_no_local(new_p, _e, "exact");
subst.assign(g.get_name(), new_p);
return some(proof_state(s, tail(gs), subst));
} else {
if (empty(gs))
return none_proof_state();
goal const & g = head(gs);
expr new_e;
buffer<constraint> cs;
auto ecs = elab(g, ngen.mk_child(), e);
new_e = ecs.first;
to_buffer(ecs.second, cs);
to_buffer(s.get_postponed(), cs);
unifier_config cfg(ios.get_options());
unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), subst, cfg);
if (auto p = rseq.pull()) {
substitution new_subst = p->first.first;
constraints new_postponed = p->first.second;
new_e = new_subst.instantiate(new_e);
bool relax_main_opaque = true;
auto tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque);
auto e_t_cs = tc->infer(new_e);
expr t = new_subst.instantiate(g.get_type());
auto dcs = tc->is_def_eq(e_t_cs.first, t);
if (dcs.first && !dcs.second && !e_t_cs.second) {
expr new_p = g.abstract(new_e);
check_has_no_local(new_p, e, "exact");
new_subst.assign(g.get_name(), new_p);
return some(proof_state(tail(gs), new_subst, ngen, new_postponed));
}
}
return none_proof_state();
});
}
@ -39,9 +55,9 @@ void initialize_exact_tactic() {
name exact_tac_name({"tactic", "exact"});
g_exact_tac_fn = new expr(Const(exact_tac_name));
register_tac(exact_tac_name,
[](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
// TODO(Leo): use elaborate_fn
return exact_tactic(app_arg(e));
[](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
check_tactic_expr(app_arg(e), "invalid 'exact' tactic, invalid argument");
return exact_tactic(fn, get_tactic_expr_expr(app_arg(e)));
});
}
void finalize_exact_tactic() {