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

refactor(beta_reduction): add function apply_beta

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-23 16:01:05 -07:00
parent f1e0d6ec29
commit 873e56844a
2 changed files with 22 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/kernel/instantiate.cpp
View file

@ -69,31 +69,31 @@ bool is_head_beta(expr const & t) {
return is_app(t) && is_lambda(arg(t, 0));
}
expr apply_beta(expr f, unsigned num_args, expr const * args) {
lean_assert(is_lambda(f));
unsigned m = 1;
while (is_lambda(abst_body(f)) && m < num_args) {
f = abst_body(f);
m++;
}
lean_assert(m <= num_args);
expr r = instantiate(abst_body(f), m, args);
if (m == num_args) {
return r;
} else {
buffer<expr> new_args;
new_args.push_back(r);
for (; m < num_args; m++)
new_args.push_back(args[m]);
return mk_app(new_args.size(), new_args.data());
}
}
expr head_beta_reduce(expr const & t) {
if (!is_head_beta(t)) {
return t;
} else {
unsigned num = num_args(t);
unsigned num1 = num - 1;
expr const * f = &arg(t, 0);
lean_assert(is_lambda(*f));
unsigned m = 1;
while (is_lambda(abst_body(*f)) && m < num1) {
f = &abst_body(*f);
m++;
}
lean_assert(m <= num1);
expr r = instantiate(abst_body(*f), m, &arg(t, 1));
if (m == num1) {
return r;
} else {
buffer<expr> args;
args.push_back(r);
m++;
for (; m < num; m++)
args.push_back(arg(t, m));
return mk_app(args.size(), args.data());
}
return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1));
}
}

1
src/kernel/instantiate.h
View file

@ -30,6 +30,7 @@ inline expr instantiate(expr const & e, expr const & s) { return instantiate(e,
*/
expr instantiate(expr const & e, unsigned i, expr const & s);
expr apply_beta(expr f, unsigned num_args, expr const * args);
bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t);
expr beta_reduce(expr t);