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

refactor(kernel/instantiate): cleanup beta-reduce

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-17 20:19:51 -07:00
parent 1ce3b83d79
commit 2369388629
1 changed files with 13 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/kernel/instantiate.cpp
View file

@ -91,18 +91,7 @@ expr instantiate_rev(expr const & a, unsigned n, expr const * subst) {
} }
bool is_head_beta(expr const & t) { bool is_head_beta(expr const & t) {
expr const * it = &t; return is_app(t) && is_lambda(get_app_fn(t));
while (is_app(*it)) {
expr const & f = app_fn(*it);
if (is_lambda(f)) {
return true;
} else if (is_app(f)) {
it = &f;
} else {
return false;
}
}
return false;
} }
expr apply_beta(expr f, unsigned num_args, expr const * args) { expr apply_beta(expr f, unsigned num_args, expr const * args) {
@ -126,33 +115,28 @@ expr head_beta_reduce(expr const & t) {
return t; return t;
} else { } else {
buffer<expr> args; buffer<expr> args;
expr const * it = &t; expr const & f = get_app_rev_args(t, args);
while (true) { lean_assert(is_lambda(f));
lean_assert(is_app(*it)); return apply_beta(f, args.size(), args.data());
expr const & f = app_fn(*it);
args.push_back(app_arg(*it));
if (is_lambda(f)) {
return apply_beta(f, args.size(), args.data());
} else {
lean_assert(is_app(f));
it = &f;
}
}
} }
} }
expr beta_reduce(expr t) { expr beta_reduce(expr t) {
auto f = [=](expr const & m, unsigned) -> optional<expr> { bool reduced = false;
if (is_head_beta(m)) auto f = [&](expr const & m, unsigned) -> optional<expr> {
if (is_head_beta(m)) {
reduced = true;
return some_expr(head_beta_reduce(m)); return some_expr(head_beta_reduce(m));
else if (is_local(m) || is_metavar(m)) } else if (is_local(m) || is_metavar(m)) {
return some_expr(m); // do not simplify local constants and metavariables types. return some_expr(m); // do not simplify local constants and metavariables types.
else } else {
return none_expr(); return none_expr();
}
}; };
while (true) { while (true) {
reduced = false;
expr new_t = replace(t, f); expr new_t = replace(t, f);
if (new_t == t) if (!reduced)
return new_t; return new_t;
else else
t = new_t; t = new_t;