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

fix(library/tactic): unfold tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-29 12:04:58 -07:00
parent 6d09d82a7c
commit 937d7b2813
1 changed files with 14 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/library/tactic/tactic.cpp
View file

@ -302,12 +302,14 @@ protected:
if (!modified && new_args[i] != arg) if (!modified && new_args[i] != arg)
modified = true; modified = true;
} }
if (is_lambda(f)) if (is_lambda(new_f)) {
return apply_beta(f, new_args.size(), new_args.data()); std::reverse(new_args.begin(), new_args.end());
else if (modified) return apply_beta(new_f, new_args.size(), new_args.data());
return mk_app(f, new_args); } else if (modified) {
else return mk_app(new_f, new_args);
} else {
return e; return e;
}
} else { } else {
return replace_visitor::visit_app(e); return replace_visitor::visit_app(e);
} }
@ -319,20 +321,21 @@ public:
class unfold_fn : public unfold_core_fn { class unfold_fn : public unfold_core_fn {
protected: protected:
name const & m_name; name const & m_name;
expr const & m_def; level_param_names const & m_ps;
expr const & m_def;
virtual expr visit_constant(expr const & c) { virtual expr visit_constant(expr const & c) {
if (const_name(c) == m_name) { if (const_name(c) == m_name) {
m_unfolded = true; m_unfolded = true;
return m_def; return instantiate_params(m_def, m_ps, const_levels(c));
} else { } else {
return c; return c;
} }
} }
public: public:
unfold_fn(name const & n, expr const & d):m_name(n), m_def(d) {} unfold_fn(name const & n, level_param_names const & ps, expr const & d):m_name(n), m_ps(ps), m_def(d) {}
}; };
class unfold_all_fn : public unfold_core_fn { class unfold_all_fn : public unfold_core_fn {
@ -343,7 +346,7 @@ protected:
optional<declaration> d = m_env.find(const_name(c)); optional<declaration> d = m_env.find(const_name(c));
if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) { if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) {
m_unfolded = true; m_unfolded = true;
return d->get_value(); return instantiate_params(d->get_value(), d->get_univ_params(), const_levels(c));
} else { } else {
return c; return c;
} }
@ -374,7 +377,7 @@ tactic unfold_tactic(name const & n) {
optional<declaration> d = env.find(n); optional<declaration> d = env.find(n);
if (!d || !d->is_definition() || (d->is_opaque() && d->get_module_idx() != 0)) if (!d || !d->is_definition() || (d->is_opaque() && d->get_module_idx() != 0))
return none_proof_state(); // tactic failed return none_proof_state(); // tactic failed
unfold_fn fn(n, d->get_value()); unfold_fn fn(n, d->get_univ_params(), d->get_value());
return unfold_tactic_core(fn, s); return unfold_tactic_core(fn, s);
}); });
} }