feat(kernel/level): is_trivial predicate for level constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
0b3599851d
commit
aa4a7acccf
3 changed files with 67 additions and 109 deletions
|
|
@ -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; }
|
||||
|
|
|
|||
|
|
@ -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
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue