diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index d7e6a1d14..136b9145b 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "util/debug.h" #include "util/hash.h" #include "util/object_serializer.h" +#include "util/interrupt.h" #include "kernel/level.h" namespace lean { @@ -499,6 +500,33 @@ format pp(level l, bool unicode, unsigned indent) { format pp(level const & l, options const & opts) { return pp(l, get_pp_unicode(opts), get_pp_indent(opts)); } -} +bool is_trivial(level const & lhs, level const & rhs) { + check_system("level constraints"); + if (is_zero(lhs) || lhs == rhs) { + // 0 <= l + // l <= l + return true; + } else if (is_succ(lhs) && is_succ(rhs)) { + // is_trivial(l <= r) implies is_trivial(succ l <= succ r) + return is_trivial(succ_of(lhs), succ_of(rhs)); + } else if (is_succ(rhs)) { + // is_trivial(l <= r) implies is_trivial(l <= succ^k r) + lean_assert(!is_succ(lhs)); + level it = succ_of(rhs); + while (is_succ(it)) + it = succ_of(it); + return is_trivial(lhs, it); + } else if (is_max(rhs)) { + // is_trivial(l <= l1) implies is_trivial(l <= max(l1, l2)) + // is_trivial(l <= l2) implies is_trivial(l <= max(l1, l2)) + return is_trivial(lhs, max_lhs(rhs)) || is_trivial(lhs, max_rhs(rhs)); + } else if (is_imax(rhs)) { + // is_trivial(l <= l2) implies is_trivial(l <= imax(l1, l2)) + return is_trivial(lhs, imax_rhs(rhs)); + } else { + return false; + } +} +} void print(lean::level const & l) { std::cout << l << std::endl; } diff --git a/src/kernel/level.h b/src/kernel/level.h index de4d6b0a4..3b56663ba 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -110,6 +110,16 @@ bool is_explicit(level const & l); */ inline bool has_meta(level const & l) { return get_meta_range(l) > 0; } +/** + \brief Return true if lhs <= rhs is a trivial constraint. + That is, it is a constraint that is always valid, and can be discarded. + This is not a complete procedure. It only "catches" the easy cases. + + \remark The type checker produces many trivial constraints. +*/ +bool is_trivial(level const & lhs, level const & rhs); + + /** \brief Printer for debugging purposes */ diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index 24923051f..eb883fa1b 100644 --- a/src/tests/kernel/level.cpp +++ b/src/tests/kernel/level.cpp @@ -43,120 +43,40 @@ static void tst1() { std::cout << pp(mk_max(p, mk_max(mk_succ(mk_param_univ(1)), one))) << "\n"; } - -#if 0 -static void tst0() { - environment env; - lean_assert(env->begin_objects() == env->end_objects()); - std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) { - std::cout << obj.keyword() << "\n"; - }); - level l1 = env->add_uvar_cnstr(name(name("l1"), "suffix"), level()); - lean_assert(env->begin_objects() != env->end_objects()); - std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) { - std::cout << obj.keyword() << "\n"; - }); - std::cout << env; -} - -static void tst1() { - environment env; - level l1 = env->add_uvar_cnstr(name(name("l1"), "suffix"), level()); - level l2 = env->add_uvar_cnstr("l2", l1 + 10); - level l3 = env->add_uvar_cnstr("l3", max(l2, l1 + 3)); - level l4 = env->add_uvar_cnstr("l4", max(l1 + 8, max(l2 + 2, l3 + 20))); - check_serializer(l1); - check_serializer(l2); - check_serializer(l3); - check_serializer(l4); - std::cout << pp(max(l1 + 8, max(l2 + 2, l3 + 20))) << "\n"; - std::cout << pp(level()) << "\n"; - std::cout << pp(level()+1) << "\n"; - std::cout << env; - lean_assert(env->is_ge(l4 + 10, l3 + 30)); - lean_assert(!env->is_ge(l4 + 9, l3 + 30)); -} - static void tst2() { - environment env; - level l1 = env->add_uvar_cnstr("l1", level()); - level l2 = env->add_uvar_cnstr("l1", level()); + level zero; + level one = mk_succ(zero); + level two = mk_succ(one); + level p1 = mk_param_univ(0); + level p2 = mk_param_univ(1); + level m1 = mk_meta_univ(0); + lean_assert(is_trivial(zero, mk_succ(mk_max(p1, p2)))); + lean_assert(is_trivial(mk_succ(mk_max(p1, p2)), mk_succ(mk_max(p1, p2)))); + lean_assert(is_trivial(p1, mk_succ(mk_max(p1, p2)))); + lean_assert(!is_trivial(p1, mk_succ(mk_imax(p1, p2)))); + lean_assert(is_trivial(p2, mk_succ(mk_max(p1, p2)))); + lean_assert(is_trivial(mk_succ(p2), mk_succ(mk_max(p1, p2)))); + lean_assert(is_trivial(p2, mk_succ(mk_imax(p1, p2)))); + lean_assert(is_trivial(mk_succ(p2), mk_succ(mk_imax(p1, p2)))); + lean_assert(!is_trivial(mk_succ(mk_succ(p2)), mk_succ(mk_max(p1, p2)))); + lean_assert(!is_trivial(mk_succ(mk_max(p1, p2)), zero)); + lean_assert(is_trivial(mk_succ(mk_succ(p1)), mk_succ(mk_succ(mk_succ(p1))))); + lean_assert(!is_trivial(mk_succ(mk_succ(p1)), mk_succ(mk_succ(mk_succ(p2))))); + lean_assert(!is_trivial(mk_succ(mk_succ(mk_succ(p1))), mk_succ(mk_succ(p1)))); + lean_assert(is_trivial(p1, mk_max(m1, mk_max(p1, p2)))); + lean_assert(!is_trivial(p1, mk_imax(m1, mk_imax(p1, p2)))); + lean_assert(is_trivial(p2, mk_imax(m1, mk_imax(p1, p2)))); + lean_assert(is_trivial(zero, one)); + lean_assert(is_trivial(one, two)); + lean_assert(!is_trivial(one, zero)); + lean_assert(!is_trivial(two, one)); + lean_assert(!is_trivial(m1, p1)); + lean_assert(!is_trivial(p1, m1)); } -static void tst3() { - environment env; - level l1 = env->add_uvar_cnstr("l1", level()); - level l2 = env->add_uvar_cnstr("l2", l1 + ((1<<30) + 1024)); - check_serializer(l2); - try { - level l3 = env->add_uvar_cnstr("l3", l2 + (1<<30)); - lean_unreachable(); - } - catch (exception & ex) { - std::cout << "ok\n"; - } -} - -static void tst4() { - environment env; - level l1 = env->add_uvar_cnstr("l1", level() + 1); - level l2 = env->add_uvar_cnstr("l2", level() + 1); - level l3 = env->add_uvar_cnstr("l3", max(l1, l2) + 1); - level l4 = env->add_uvar_cnstr("l4", l3 + 1); - level l5 = env->add_uvar_cnstr("l5", l3 + 1); - level l6 = env->add_uvar_cnstr("l6", max(l4, l5) + 1); - check_serializer(l1); - check_serializer(l2); - check_serializer(l3); - check_serializer(l4); - check_serializer(l5); - check_serializer(l6); - lean_assert(!env->is_ge(l5 + 1, l6)); - lean_assert(env->is_ge(l6, l5)); - lean_assert(env->is_ge(l6, max({l1, l2, l3, l4, l5}))); - lean_assert(env->is_ge(l6, l6)); - lean_assert(!env->is_ge(l5, l4)); - lean_assert(env->is_ge(max({l1, l2, l4, l5}), max({l1, l2, l3, l4, l5}))); - lean_assert(env->is_ge(max({l4, l5}), max({l1, l2, l3}))); - lean_assert(!env->is_ge(max({l1, l2, l5}), max({l1, l2, l3, l4, l5}))); - lean_assert(!env->is_ge(max({l2, l4}), max({l1, l2, l3, l4, l5}))); - lean_assert(env->is_ge(max(l2, l3) + 1, max(l1, l1+1))); - lean_assert(env->is_ge(max(l2, l3) + 1, max(l1+2, l1+1))); - lean_assert(env->is_ge(max(l2, l3) + 1, max(l2+2, l1+1))); - lean_assert(!env->is_ge(max(l4, l5) + 1, max(l2+4, l1+1))); - lean_assert(!env->is_ge(max(l6, l5), max(l2+4, l1+1))); - lean_assert(env->is_ge(max(l6, l5), max(l2+3, l1+1))); - lean_assert(!env->is_ge(max(l6, l5), max(l2, l1+1)+3)); - lean_assert(env->is_ge(max(l6+1, l5), max(l2, l1+1)+3)); - std::cout << env; -} - -static void tst5() { - environment env; - level l1 = env->add_uvar_cnstr("l1", level() + 1); - level l2 = env->add_uvar_cnstr("l2", level() + 1); - std::cout << max(l1, l1) << "\n"; - lean_assert(max(l1, l1) == l1); - lean_assert(max(l1+1, l1+1) == l1+1); - std::cout << max(l1, l1+1) << "\n"; - std::cout << max(l2, max(l1, l1+1)) << "\n"; - lean_assert(max(l1, l1+1) == l1+1); - lean_assert(max(l2, max(l1, l1+1)) == max(l2, l1+1)); - std::cout << max(l1, max(l2, l1+1)) << "\n"; - lean_assert(max(l1, max(l2, l1+1)) == max(l1+1, l2)); -} -#endif - int main() { save_stack_info(); tst1(); -#if 0 - tst0(); - tst1(); tst2(); - tst3(); - tst4(); - tst5(); -#endif return has_violations() ? 1 : 0; }