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

feat(library/match): match modulo eta

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-12 00:30:44 -07:00
parent a7af8e7c71
commit a9fa0fead9
1 changed files with 30 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/library/match.cpp
View file

@ -311,9 +311,38 @@ class match_fn : public match_context {
return try_plugin(p, t);
}
static expr eta(expr const & e) {
unsigned num = 0;
expr it = e;
while (is_lambda(it)) {
num++;
it = binding_body(it);
}
if (num == 0)
return e;
for (unsigned i = 0; i < num; i++) {
if (!is_app(it))
return e;
if (!is_var(app_arg(it), i)) {
return e;
}
it = app_fn(it);
}
if (!closed(it))
return e;
return it;
}
bool match_core(expr const & p, expr const & t) {
if (p.kind() != t.kind())
if (p.kind() != t.kind()) {
if (is_lambda(p) != is_lambda(t)) {
expr new_p = eta(p);
expr new_t = eta(t);
if (is_lambda(new_p) == is_lambda(new_t))
return _match(new_p, new_t);
}
return try_plugin(p, t);
}
if (m_plugin) {
switch (m_plugin->pre(p, t, *this)) {