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

feat(library/tactic/intro_tactic): improve low-level intron

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-05 13:50:21 -07:00
parent 07388479e6
commit 34fc12eda0
2 changed files with 17 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -23,8 +23,9 @@ static name mk_aux_name(list<name> & given_names, name const & default_name) {
}
}
optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & given_names, buffer<name> & new_Hns) {
optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & given_names, buffer<name> & new_Hns) {
lean_assert(is_metavar(mvar));
metavar_context mctx = ctx.mctx();
optional<metavar_decl> g = mctx.get_metavar_decl(mvar);
if (!g) return none_expr();
expr type = g->get_type();
@ -38,7 +39,8 @@ optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & m
}
lean_assert(is_pi(type) || is_let(type));
if (is_pi(type)) {
expr H = new_locals.push_local(mk_aux_name(given_names, binding_name(type)), binding_domain(type), binding_info(type));
expr H = new_locals.push_local(mk_aux_name(given_names, binding_name(type)), binding_domain(type),
binding_info(type));
type = instantiate(binding_body(type), H);
new_Hs.push_back(H);
new_Hns.push_back(mlocal_name(H));
@ -52,7 +54,6 @@ optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & m
}
}
local_context lctx = ctx.lctx();
mctx = ctx.mctx();
expr new_M = mctx.mk_metavar_decl(lctx, type);
lean_assert(!mctx.is_assigned(new_M));
expr new_val = abstract_locals(mk_lazy_abstraction_with_locals(new_M, new_Hs), new_Hs.size(), new_Hs.data());
@ -71,12 +72,18 @@ optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & m
}
lean_assert(!mctx.is_assigned(new_M));
mctx.assign(mvar, new_val);
ctx.set_mctx(mctx);
return some_expr(new_M);
}
optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & given_names) {
optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & given_names) {
buffer<name> tmp;
return intron(ctx, mctx, mvar, n, given_names, tmp);
return intron(ctx, mvar, n, given_names, tmp);
}
optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n) {
list<name> empty;
return intron(ctx, mvar, n, empty);
}
optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hns) {
@ -84,11 +91,10 @@ optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> &
optional<expr> mvar = s.get_main_goal();
if (!mvar) return none_tactic_state();
type_context ctx = mk_type_context_for(s);
metavar_context mctx = s.mctx();
list<name> new_names;
if (optional<expr> new_M = intron(ctx, mctx, *mvar, n, new_names, new_Hns)) {
if (optional<expr> new_M = intron(ctx, *mvar, n, new_names, new_Hns)) {
list<expr> new_gs(*new_M, tail(s.goals()));
return some_tactic_state(set_mctx_goals(s, mctx, new_gs));
return some_tactic_state(set_mctx_goals(s, ctx.mctx(), new_gs));
} else {
return none_tactic_state();
}

6
src/library/tactic/intro_tactic.h
View file

@ -14,9 +14,9 @@ optional<tactic_state> intron(unsigned n, tactic_state const & s);
After execution, the buffer \c new_Hns stores the new interal names for the new hypotheses.
\remark new_hs_names is an input/output parameter. The procedure will "consume" n elements from the list. */
optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & new_hs_names);
optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n);
optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & new_hs_names);
optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n);
void initialize_intro_tactic();
void finalize_intro_tactic();