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

refactor(library/tactic): cleanup 'revert' and 'clear' tactics

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-26 17:08:14 -08:00
parent 4bee7554a3
commit 2a00647089
6 changed files with 85 additions and 59 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/locals.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
#include "kernel/for_each_fn.h"
#include "kernel/find_fn.h"
#include "library/locals.h"
namespace lean {
void collect_univ_params_core(level const & l, name_set & r) {
@ -76,4 +77,11 @@ bool contains_local(expr const & e, name const & n) {
});
return result;
}
bool depends_on(unsigned sz, expr const * es, expr const & h) {
for (unsigned i = 0; i < sz; i++)
if (depends_on(es[i], h))
return true;
return false;
}
}

8
src/library/locals.h
View file

@ -25,4 +25,12 @@ inline bool contains_local(expr const & local, buffer<expr> const & locals) {
/** \brief Return true iff \c e contains a local constant named \c n (it uses mlocal_name) */
bool contains_local(expr const & e, name const & n);
/** \brief Return true iff \e contains the local constant \c h */
inline bool depends_on(expr const & e, expr const & h) {
return contains_local(e, mlocal_name(h));
}
/** \brief Return true iff one of \c es contains the local constant \c h */
bool depends_on(unsigned sz, expr const * es, expr const & h);
}

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

@ -17,37 +17,26 @@ tactic clear_tactic(name const & n) {
return none_proof_state();
goal g = head(gs);
goals tail_gs = tail(gs);
expr meta = g.get_meta();
buffer<expr> locals;
get_app_args(meta, locals);
unsigned i = locals.size();
while (i > 0) {
--i;
if (local_pp_name(locals[i]) == n) {
// found target
name real_n = mlocal_name(locals[i]);
for (unsigned j = i+1; j < locals.size(); j++) {
if (contains_local(mlocal_type(locals[j]), real_n))
return none_proof_state(); // other variables depends on n
}
if (contains_local(g.get_type(), real_n))
return none_proof_state(); // type depends on n
buffer<expr> new_locals;
for (unsigned j = 0; j < i; j++)
new_locals.push_back(locals[j]);
for (unsigned j = i+1; j < locals.size(); j++)
new_locals.push_back(locals[j]);
name_generator ngen = s.get_ngen();
expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(new_locals, g.get_type())), new_locals);
goal new_g(new_meta, g.get_type());
expr val = Fun(locals, new_meta);
substitution new_subst = s.get_subst();
new_subst.assign(g.get_name(), val);
proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
return some_proof_state(new_s);
}
if (auto p = g.find_hyp(n)) {
expr const & h = p->first;
unsigned i = p->second;
buffer<expr> hyps;
g.get_hyps(hyps);
hyps.erase(hyps.size() - i - 1);
if (depends_on(g.get_type(), h) || depends_on(i, hyps.end() - i, h))
return none_proof_state(); // other hypotheses or result type depend on h
name_generator ngen = s.get_ngen();
expr new_type = g.get_type();
expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps);
goal new_g(new_meta, new_type);
expr val = g.abstract(new_meta);
substitution new_subst = s.get_subst();
new_subst.assign(g.get_name(), val);
proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
return some_proof_state(new_s);
} else {
return none_proof_state();
}
return none_proof_state();
};
return tactic01(fn);
}

17
src/library/tactic/goal.cpp
View file

@ -127,6 +127,23 @@ list<expr> goal::to_context() const {
return to_list(locals.begin(), locals.end());
}
optional<pair<expr, unsigned>> goal::find_hyp(name const & uname) const {
expr const * it = &m_meta;
unsigned i = 0;
while (is_app(*it)) {
expr const & h = app_arg(*it);
if (local_pp_name(h) == uname)
return some(mk_pair(h, i));
i++;
it = &app_fn(*it);
}
return optional<pair<expr, unsigned>>();
}
void goal::get_hyps(buffer<expr> & r) const {
get_app_args(m_meta, r);
}
io_state_stream const & operator<<(io_state_stream const & out, goal const & g) {
options const & opts = out.get_options();
out.get_stream() << mk_pair(g.pp(out.get_formatter()), opts);

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

@ -74,6 +74,20 @@ public:
/** \brief Apply given substitution to goal */
goal instantiate(substitution const & s) const;
/** \brief Return hypothesis (and its position) with "user name" uname (i.e., local_pp_name).
\remark The position is right to left. In the following goal (Ha is 2), (Hb is 1) and (Hc is 0):
Ha : a, Hb : b, Hc : c |- P
*/
optional<pair<expr, unsigned>> find_hyp(name const & uname) const;
/** \brief Store hypotheses in the given buffer.
\remark The hypotheses are stored from left to right.
*/
void get_hyps(buffer<expr> & r) const;
format pp(formatter const & fmt, substitution const & s) const;
format pp(formatter const & fmt) const;
};

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

@ -17,36 +17,26 @@ tactic revert_tactic(name const & n) {
return none_proof_state();
goal g = head(gs);
goals tail_gs = tail(gs);
expr meta = g.get_meta();
buffer<expr> locals;
get_app_args(meta, locals);
unsigned i = locals.size();
while (i > 0) {
--i;
if (local_pp_name(locals[i]) == n) {
// found target
name real_n = mlocal_name(locals[i]);
for (unsigned j = i+1; j < locals.size(); j++) {
if (contains_local(mlocal_type(locals[j]), real_n))
return none_proof_state(); // other variables depends on n
}
buffer<expr> new_locals;
for (unsigned j = 0; j < i; j++)
new_locals.push_back(locals[j]);
for (unsigned j = i+1; j < locals.size(); j++)
new_locals.push_back(locals[j]);
name_generator ngen = s.get_ngen();
expr new_type = Pi(locals[i], g.get_type());
expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(new_locals, new_type)), new_locals);
goal new_g(new_meta, new_type);
expr val = Fun(locals, mk_app(new_meta, locals[i]));
substitution new_subst = s.get_subst();
new_subst.assign(g.get_name(), val);
proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
return some_proof_state(new_s);
}
if (auto p = g.find_hyp(n)) {
expr const & h = p->first;
unsigned i = p->second;
buffer<expr> hyps;
g.get_hyps(hyps);
hyps.erase(hyps.size() - i - 1);
if (depends_on(i, hyps.end() - i, h))
return none_proof_state(); // other hypotheses depend on h
name_generator ngen = s.get_ngen();
expr new_type = Pi(h, g.get_type());
expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps);
goal new_g(new_meta, new_type);
expr val = g.abstract(mk_app(new_meta, h));
substitution new_subst = s.get_subst();
new_subst.assign(g.get_name(), val);
proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
return some_proof_state(new_s);
} else {
return none_proof_state();
}
return none_proof_state();
};
return tactic01(fn);
}