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

Add simplification to add_lift

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-17 03:14:02 -07:00
parent 99e8d2feae
commit a26c7d47f2
2 changed files with 22 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/kernel/metavar.cpp
View file

@ -119,10 +119,17 @@ expr instantiate_metavars(expr const & e, metavar_env const & env) {
}
meta_ctx add_lift(meta_ctx const & ctx, unsigned s, unsigned n) {
if (n == 0)
if (n == 0) {
return ctx;
else
return cons(mk_lift(s, n), ctx);
} else if (ctx) {
meta_entry e = head(ctx);
// Simplification rule
// lift:(s1+n1):n2 lift:s1:n1 ---> lift:s1:n1+n2
if (e.is_lift() && s == e.s() + e.n()) {
return add_lift(tail(ctx), e.s(), e.n() + n);
}
}
return cons(mk_lift(s, n), ctx);
}
expr add_lift(expr const & m, unsigned s, unsigned n) {

12
src/tests/kernel/metavar.cpp
View file

@ -432,6 +432,17 @@ static void tst20() {
std::cout << norm(F, ctx) << "\n";
}
static void tst21() {
metavar_env menv;
expr m1 = menv.mk_metavar();
lean_assert(add_lift(add_lift(m1, 0, 1), 1, 1) ==
add_lift(m1, 0, 2));
lean_assert(add_lift(add_lift(m1, 1, 2), 3, 4) ==
add_lift(m1, 1, 6));
lean_assert(add_lift(add_lift(m1, 1, 3), 3, 4) !=
add_lift(m1, 1, 7));
}
int main() {
tst1();
tst2();
@ -453,5 +464,6 @@ int main() {
tst18();
tst19();
tst20();
tst21();
return has_violations() ? 1 : 0;
}