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

feat(library/tactic/rewrite_tactic): ignore inst_implicit arguments when matching applications of declarations which contain them

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-04 12:14:47 -08:00
parent 0e05c239a5
commit ccae014ef9
1 changed files with 54 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

69
src/library/tactic/rewrite_tactic.cpp
View file

@ -254,6 +254,7 @@ public:
virtual bool on_failure(expr const & p, expr const & t, match_context & ctx) const { virtual bool on_failure(expr const & p, expr const & t, match_context & ctx) const {
try { try {
constraint_seq cs; constraint_seq cs;
// We do not unfold projections.
expr p1 = is_projection_app(p) ? p : m_tc.whnf(p, cs); expr p1 = is_projection_app(p) ? p : m_tc.whnf(p, cs);
expr t1 = is_projection_app(t) ? t : m_tc.whnf(t, cs); expr t1 = is_projection_app(t) ? t : m_tc.whnf(t, cs);
return !cs && (p1 != p || t1 != t) && ctx.match(p1, t1); return !cs && (p1 != p || t1 != t) && ctx.match(p1, t1);
@ -262,32 +263,70 @@ public:
} }
} }
// Return true iff the given declaration contains inst_implicit arguments
bool has_inst_implicit_args(name const & d) const {
if (auto decl = m_tc.env().find(d)) {
expr const * it = &decl->get_type();
while (is_pi(*it)) {
if (binding_info(*it).is_inst_implicit())
return true;
it = &binding_body(*it);
}
return false;
} else {
return false;
}
}
virtual lbool pre(expr const & p, expr const & t, match_context & ctx) const { virtual lbool pre(expr const & p, expr const & t, match_context & ctx) const {
if (!is_app(p) || !is_app(t)) if (!is_app(p) || !is_app(t))
return l_undef; return l_undef;
expr const & p_fn = get_app_fn(p); expr const & p_fn = get_app_fn(p);
if (!is_constant(p_fn)) if (!is_constant(p_fn))
return l_false; return l_undef;
expr const & t_fn = get_app_fn(t); expr const & t_fn = get_app_fn(t);
if (!is_constant(t_fn)) if (!is_constant(t_fn))
return l_false; return l_undef;
if (!ctx.match(p_fn, t_fn)) if (!ctx.match(p_fn, t_fn))
return l_false; return l_undef;
projection_info const * info = get_projection_info(m_tc.env(), const_name(p_fn)); projection_info const * info = get_projection_info(m_tc.env(), const_name(p_fn));
if (!info || !info->m_inst_implicit) if (info && info->m_inst_implicit) {
return l_undef; // use default matcher // Special support for projections
buffer<expr> p_args, t_args; buffer<expr> p_args, t_args;
get_app_args(p, p_args); get_app_args(p, p_args);
get_app_args(t, t_args); get_app_args(t, t_args);
if (p_args.size() != t_args.size()) if (p_args.size() != t_args.size())
return l_false;
for (unsigned i = 0; i < p_args.size(); i++) {
if (i == info->m_nparams)
continue; // skip structure
if (!ctx.match(p_args[i], t_args[i]))
return l_false; return l_false;
for (unsigned i = 0; i < p_args.size(); i++) {
if (i == info->m_nparams)
continue; // skip structure
if (!ctx.match(p_args[i], t_args[i]))
return l_false;
}
return l_true;
} }
return l_true; if (has_inst_implicit_args(const_name(p_fn))) {
// Special support for declarations that contains inst_implicit arguments.
// The idea is to skip them during matching.
buffer<expr> p_args, t_args;
get_app_args(p, p_args);
get_app_args(t, t_args);
if (p_args.size() != t_args.size())
return l_false;
expr const * it = &m_tc.env().get(const_name(p_fn)).get_type();
for (unsigned i = 0; i < p_args.size(); i++) {
if (is_pi(*it) && binding_info(*it).is_inst_implicit()) {
it = &binding_body(*it);
continue; // skip argument
}
if (!ctx.match(p_args[i], t_args[i]))
return to_lbool(on_failure(p, t, ctx)); // try to unfold if possible
if (is_pi(*it))
it = &binding_body(*it);
}
return l_true;
}
return l_undef;
} }
}; };