From 9f93b5d97e37913f20c423214694498115670ab4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Feb 2014 18:02:14 -0800 Subject: [PATCH] feat(kernel/level): new universe level datastructure for universe level polymorphism Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 +- src/kernel/level.cpp | 626 ++++++++++++++++++++------------ src/kernel/level.h | 125 +++++-- src/tests/kernel/CMakeLists.txt | 76 ++-- src/tests/kernel/level.cpp | 34 +- 5 files changed, 550 insertions(+), 313 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d15e70526..dc9215a82 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -245,7 +245,7 @@ set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS}) add_subdirectory(tests/util) add_subdirectory(tests/util/numerics) add_subdirectory(tests/util/interval) -# add_subdirectory(tests/kernel) +add_subdirectory(tests/kernel) # add_subdirectory(tests/library) # add_subdirectory(tests/library/rewriter) # add_subdirectory(tests/library/tactic) diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 98f86b5f8..0bc143d88 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -5,63 +5,215 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "util/safe_arith.h" #include "util/buffer.h" #include "util/rc.h" +#include "util/list.h" #include "util/debug.h" #include "util/hash.h" #include "util/object_serializer.h" #include "kernel/level.h" namespace lean { -/** \brief Base class for representing universe level cells. */ +level_cell const & to_cell(level const & l) { + return *l.m_ptr; +} + +/** \brief Base class for representing universe level terms. */ struct level_cell { void dealloc(); MK_LEAN_RC() level_kind m_kind; - level_cell(level_kind k):m_rc(1), m_kind(k) {} + unsigned m_hash; + level_cell(level_kind k, unsigned h):m_rc(1), m_kind(k), m_hash(h) {} }; -/** \brief Cell for universe variables. */ -struct level_uvar : public level_cell { - name m_name; - level_uvar(name const & n):level_cell(level_kind::UVar), m_name(n) {} + +unsigned hash(level const & l) { return to_cell(l).m_hash; } +level_kind kind(level const & l) { return to_cell(l).m_kind; } + +struct level_composite : public level_cell { + unsigned m_depth; + unsigned m_param_range; + unsigned m_meta_range; + level_composite(level_kind k, unsigned h, unsigned d, unsigned r1, unsigned r2): + level_cell(k, h), m_depth(d), m_param_range(r1), m_meta_range(r2) {} }; -/** \brief Cell for representing the universe l + k, where \c l is a level and \c k a unsigned integer. */ -struct level_lift : public level_cell { - level m_l; - unsigned m_k; - level_lift(level const & l, unsigned k):level_cell(level_kind::Lift), m_l(l), m_k(k) {} -}; -/** \brief Cell for representing the universe max l_1 ... l_n, where n == m_size. */ -struct level_max : public level_cell { - unsigned m_size; - level m_levels[0]; - level_max(unsigned sz, level const * ls):level_cell(level_kind::Max), m_size(sz) { - for (unsigned i = 0; i < m_size; i++) - new (m_levels + i) level(ls[i]); - } - ~level_max() { - for (unsigned i = 0; i < m_size; i++) - (m_levels+i)->~level(); - } - level const * begin_levels() const { return m_levels; } - level const * end_levels() const { return m_levels + m_size; } -}; -level_uvar * to_uvar(level_cell * c) { return static_cast(c); } -level_lift * to_lift(level_cell * c) { return static_cast(c); } -level_max * to_max(level_cell * c) { return static_cast(c); } -void level_cell::dealloc() { - switch (m_kind) { - case level_kind::UVar: delete to_uvar(this); break; - case level_kind::Lift: delete to_lift(this); break; - case level_kind::Max: static_cast(this)->~level_max(); delete[] reinterpret_cast(this); break; + +static bool is_composite(level const & l) { + switch (kind(l)) { + case level_kind::Succ: case level_kind::Max: case level_kind::IMax: + return true; + default: + return false; } } -static name g_bot_name("bot"); -level::level(): m_ptr(new level_uvar(g_bot_name)) { lean_assert_eq(uvar_name(*this), name("bot")); } -level::level(name const & n): m_ptr(new level_uvar(n)) {} -level::level(level const & l, unsigned k):m_ptr(new level_lift(l, k)) { lean_assert(is_uvar(l)); } -level::level(level_cell * ptr): m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); } + +static level_composite const & to_composite(level const & l) { + lean_assert(is_composite(l)); + return static_cast(to_cell(l)); +} + +struct level_succ : public level_composite { + level m_l; + bool m_explicit; + level_succ(level const & l): + level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, get_param_range(l), get_meta_range(l)), + m_l(l), + m_explicit(is_explicit(l)) {} +}; + +level_succ const & to_level_succ(level const & l) { lean_assert(is_succ(l)); return static_cast(to_cell(l)); } +level const & succ_of(level const & l) { return to_level_succ(l).m_l; } + +struct level_max_core : public level_composite { + level m_lhs; + level m_rhs; + level_max_core(bool imax, level const & l1, level const & l2): + level_composite(imax ? level_kind::IMax : level_kind::Max, + hash(hash(l1), hash(l2)), + std::max(get_depth(l1), get_depth(l2)) + 1, + std::max(get_param_range(l1), get_param_range(l2)), + std::max(get_meta_range(l1), get_meta_range(l2))), + m_lhs(l1), m_rhs(l2) { + lean_assert(!is_explicit(l1) || !is_explicit(l2)); + } +}; + +static level_max_core const & to_max_core(level const & l) { + lean_assert(is_max(l) || is_imax(l)); + return static_cast(to_cell(l)); +} + +level const & max_lhs(level const & l) { lean_assert(is_max(l)); return to_max_core(l).m_lhs; } +level const & max_rhs(level const & l) { lean_assert(is_max(l)); return to_max_core(l).m_rhs; } +level const & imax_lhs(level const & l) { lean_assert(is_imax(l)); return to_max_core(l).m_lhs; } +level const & imax_rhs(level const & l) { lean_assert(is_imax(l)); return to_max_core(l).m_rhs; } + +struct level_param_core : public level_cell { + unsigned m_id; + level_param_core(bool is_param, unsigned id): + level_cell(is_param ? level_kind::Param : level_kind::Meta, hash(id, 11u)), + m_id(id) {} +}; + +static bool is_param_core(level const & l) { return is_param(l) || is_meta(l); } + +static level_param_core const & to_param_core(level const & l) { + lean_assert(is_param_core(l)); + return static_cast(to_cell(l)); +} + +unsigned param_id(level const & l) { lean_assert(is_param(l)); return to_param_core(l).m_id; } +unsigned meta_id(level const & l) { lean_assert(is_meta(l)); return to_param_core(l).m_id; } + +void level_cell::dealloc() { + switch (m_kind) { + case level_kind::Succ: + delete static_cast(this); + break; + case level_kind::Max: case level_kind::IMax: + delete static_cast(this); + break; + case level_kind::Param: case level_kind::Meta: + delete static_cast(this); + break; + case level_kind::Zero: + delete this; + break; + } +} + +unsigned get_depth(level const & l) { + switch (kind(l)) { + case level_kind::Zero: case level_kind::Param: case level_kind::Meta: + return 1; + case level_kind::Succ: case level_kind::Max: case level_kind::IMax: + return to_composite(l).m_depth; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +unsigned get_param_range(level const & l) { + switch (kind(l)) { + case level_kind::Zero: case level_kind::Meta: + return 0; + case level_kind::Param: + return to_param_core(l).m_id + 1; + case level_kind::Succ: case level_kind::Max: case level_kind::IMax: + return to_composite(l).m_param_range; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +unsigned get_meta_range(level const & l) { + switch (kind(l)) { + case level_kind::Zero: case level_kind::Param: + return 0; + case level_kind::Meta: + return to_param_core(l).m_id + 1; + case level_kind::Succ: case level_kind::Max: case level_kind::IMax: + return to_composite(l).m_param_range; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +bool is_explicit(level const & l) { + switch (kind(l)) { + case level_kind::Zero: + return true; + case level_kind::Param: case level_kind::Meta: case level_kind::Max: case level_kind::IMax: + return false; + case level_kind::Succ: + return to_level_succ(l).m_explicit; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +level mk_succ(level const & l) { + return level(new level_succ(l)); +} + +level mk_max(level const & l1, level const & l2) { + if (is_explicit(l1) && is_explicit(l2)) + return get_depth(l1) >= get_depth(l2) ? l1 : l2; + else if (l1 == l2) + return l1; + else if (is_zero(l1)) + return l2; + else if (is_zero(l2)) + return l1; + else + return level(new level_max_core(false, l1, l2)); +} + +level mk_imax(level const & l1, level const & l2) { + if (is_not_zero(l2)) + return mk_max(l1, l2); + else if (is_zero(l2)) + return l2; + else if (l1 == l2) + return l1; + else + return level(new level_max_core(true, l1, l2)); +} + +level mk_param_univ(unsigned i) { + return level(new level_param_core(true, i)); +} + +level mk_meta_univ(unsigned i) { + return level(new level_param_core(false, i)); +} + +static level g_zero(new level_cell(level_kind::Zero, 7u)); +static level g_one(mk_succ(g_zero)); + +level const & mk_level_zero() { return g_zero; } +level const & mk_level_one() { return g_one; } + +level::level():level(g_zero) {} +level::level(level_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); } level::level(level const & s): m_ptr(s.m_ptr) { if (m_ptr) @@ -75,196 +227,88 @@ level::~level() { if (m_ptr) m_ptr->dec_ref(); } -level to_level(level_cell * c) { return level(c); } -level_cell * to_cell(level const & l) { return l.m_ptr; } -level_max * to_max(level const & l) { return to_max(to_cell(l)); } -unsigned level::hash() const { - switch (m_ptr->m_kind) { - case level_kind::UVar: return to_uvar(m_ptr)->m_name.hash(); - case level_kind::Lift: return ::lean::hash(to_lift(m_ptr)->m_l.hash(), to_lift(m_ptr)->m_k); - case level_kind::Max: return ::lean::hash(to_max(m_ptr)->m_size, [&](unsigned i) { return to_max(m_ptr)->m_levels[i].hash(); }); - } - return 0; -} - -bool level::is_bottom() const { - return is_uvar(*this) && uvar_name(*this) == g_bot_name; -} - -level max_core(unsigned sz, level const * ls) { - char * mem = new char[sizeof(level_max) + sz*sizeof(level)]; - return to_level(new (mem) level_max(sz, ls)); -} - -level const & _lift_of(level const & l) { return is_lift(l) ? lift_of(l) : l; } -unsigned _lift_offset(level const & l) { return is_lift(l) ? lift_offset(l) : 0; } - -void push_back(buffer & ls, level const & l) { - if (l.is_bottom()) - return; - for (unsigned i = 0; i < ls.size(); i++) { - if (_lift_of(ls[i]) == _lift_of(l)) { - if (_lift_offset(ls[i]) < _lift_offset(l)) - ls[i] = l; - return; - } - } - ls.push_back(l); -} - -level max_core(unsigned sz1, level const * ls1, unsigned sz2, level const * ls2) { - buffer new_lvls; - std::for_each(ls1, ls1 + sz1, [&](level const & l) { push_back(new_lvls, l); }); - std::for_each(ls2, ls2 + sz2, [&](level const & l) { push_back(new_lvls, l); }); - unsigned sz = new_lvls.size(); - if (sz == 0) - return level(); - else if (sz == 1) - return new_lvls[0]; - else - return max_core(new_lvls.size(), new_lvls.data()); -} - -level max_core(level const & l1, level const & l2) { return max_core(1, &l1, 1, &l2); } -level max_core(level const & l1, level_max * l2) { return max_core(1, &l1, l2->m_size, l2->m_levels); } -level max_core(level_max * l1, level const & l2) { return max_core(l1->m_size, l1->m_levels, 1, &l2); } -level max_core(level_max * l1, level_max * l2) { return max_core(l1->m_size, l1->m_levels, l2->m_size, l2->m_levels); } - -level max(level const & l1, level const & l2) { - if (is_max(l1)) { - if (is_max(l2)) - return max_core(to_max(l1), to_max(l2)); - else - return max_core(to_max(l1), l2); - } else { - if (is_max(l2)) - return max_core(l1, to_max(l2)); - else - return max_core(l1, l2); - } -} - -level operator+(level const & l, unsigned k) { - switch (kind(l)) { - case level_kind::UVar: return level(l, k); - case level_kind::Lift: return level(lift_of(l), safe_add(lift_offset(l), k)); - case level_kind::Max: { - buffer new_lvls; - for (unsigned i = 0; i < max_size(l); i++) - new_lvls.push_back(max_level(l, i) + k); - return max_core(new_lvls.size(), new_lvls.data()); - }} - lean_unreachable(); // LCOV_EXCL_LINE -} - -level_kind kind (level const & l) { lean_assert(l.m_ptr); return l.m_ptr->m_kind; } -name const & uvar_name (level const & l) { lean_assert(is_uvar(l)); return static_cast(l.m_ptr)->m_name; } -level const & lift_of (level const & l) { lean_assert(is_lift(l)); return static_cast(l.m_ptr)->m_l; } -unsigned lift_offset(level const & l) { lean_assert(is_lift(l)); return static_cast(l.m_ptr)->m_k; } -unsigned max_size (level const & l) { lean_assert(is_max(l)); return static_cast(l.m_ptr)->m_size; } -level const & max_level (level const & l, unsigned i) { lean_assert(is_max(l)); return static_cast(l.m_ptr)->m_levels[i]; } level & level::operator=(level const & l) { LEAN_COPY_REF(l); } level & level::operator=(level&& l) { LEAN_MOVE_REF(l); } bool operator==(level const & l1, level const & l2) { if (kind(l1) != kind(l2)) return false; + if (hash(l1) != hash(l2)) return false; + if (is_eqp(l1, l2)) return true; switch (kind(l1)) { - case level_kind::UVar: return uvar_name(l1) == uvar_name(l2); - case level_kind::Lift: return lift_of(l1) == lift_of(l2) && lift_offset(l1) == lift_offset(l2); - case level_kind::Max: - if (max_size(l1) == max_size(l2)) { - for (unsigned i = 0; i < max_size(l1); i++) - if (max_level(l1, i) != max_level(l2, i)) - return false; + case level_kind::Zero: + return true; + case level_kind::Param: case level_kind::Meta: + return to_param_core(l1).m_id == to_param_core(l2).m_id; + case level_kind::Max: case level_kind::IMax: case level_kind::Succ: + if (to_composite(l1).m_depth != to_composite(l2).m_depth || + to_composite(l1).m_param_range != to_composite(l2).m_param_range || + to_composite(l1).m_meta_range != to_composite(l2).m_meta_range) + return false; + break; + } + switch (kind(l1)) { + case level_kind::Zero: case level_kind::Param: case level_kind::Meta: + lean_unreachable(); // LCOV_EXCL_LINE + case level_kind::Max: case level_kind::IMax: + return + to_max_core(l1).m_lhs == to_max_core(l2).m_lhs && + to_max_core(l1).m_rhs == to_max_core(l2).m_rhs; + case level_kind::Succ: + if (is_explicit(l1) != is_explicit(l2)) { + return false; + } else if (is_explicit(l1)) { + lean_assert(get_depth(l1) == get_depth(l2)); + // the depths are equal, then l1 and l2 must be the same universe return true; } else { - return false; + return succ_of(l1) == succ_of(l2); } } lean_unreachable(); // LCOV_EXCL_LINE } -bool operator<(level const & l1, level const & l2) { - if (kind(l1) != kind(l2)) return kind(l1) < kind(l2); - switch (kind(l1)) { - case level_kind::UVar: return uvar_name(l1) < uvar_name(l2); - case level_kind::Lift: - if (lift_of(l1) != lift_of(l2)) - return lift_of(l1) < lift_of(l2); - else - return lift_offset(l1) < lift_offset(l2); - case level_kind::Max: - if (max_size(l1) != max_size(l2)) - return max_size(l1) < max_size(l2); - for (unsigned i = 0; i < max_size(l1); i++) - if (max_level(l1, i) != max_level(l2, i)) - return max_level(l1, i) < max_level(l2, i); +bool is_not_zero(level const & l) { + switch (kind(l)) { + case level_kind::Zero: case level_kind::Param: case level_kind::Meta: return false; - } - lean_unreachable(); // LCOV_EXCL_LINE -} - -std::ostream & operator<<(std::ostream & out, level const & l) { - switch (kind(l)) { - case level_kind::UVar: out << uvar_name(l); return out; - case level_kind::Lift: - if (lift_of(l).is_bottom()) - out << lift_offset(l); - else - out << lift_of(l) << "+" << lift_offset(l); - return out; + case level_kind::Succ: + return true; case level_kind::Max: - out << "(max"; - for (unsigned i = 0; i < max_size(l); i++) - out << " " << max_level(l, i); - out << ")"; - return out; + return is_not_zero(max_lhs(l)) || is_not_zero(max_rhs(l)); + case level_kind::IMax: + return is_not_zero(imax_rhs(l)); } - return out; -} - -format pp(level const & l, bool unicode) { - switch (kind(l)) { - case level_kind::UVar: - if (l.is_bottom()) - return format(0); - else - return pp(uvar_name(l)); - case level_kind::Lift: - if (lift_of(l).is_bottom()) - return format(lift_offset(l)); - else - return format{pp(lift_of(l), unicode), format("+"), format(lift_offset(l))}; - case level_kind::Max: { - if (unicode) { - format r = pp(max_level(l, 0), unicode); - for (unsigned i = 1; i < max_size(l); i++) { - r += format{space(), format("\u2294"), line()}; - r += pp(max_level(l, i), unicode); - } - return group(r); - } else { - format r = format("max"); - for (unsigned i = 0; i < max_size(l); i++) - r += format{line(), pp(max_level(l, i), unicode)}; - return paren(r); - } - }} lean_unreachable(); // LCOV_EXCL_LINE } -format pp(level const & l, options const & opts) { - return pp(l, get_pp_unicode(opts)); +// Monotonic total order on universe level terms. +bool is_lt(level const & a, level const & b) { + if (is_eqp(a, b)) return false; + unsigned da = get_depth(a); + unsigned db = get_depth(b); + if (da < db) return true; + if (da > db) return false; + if (kind(a) != kind(b)) return kind(a) < kind(b); + if (hash(a) < hash(b)) return true; + if (hash(a) > hash(b)) return false; + if (a == b) return false; + switch (kind(a)) { + case level_kind::Zero: + return false; + case level_kind::Param: case level_kind::Meta: + return to_param_core(a).m_id < to_param_core(b).m_id; + case level_kind::Max: case level_kind::IMax: + if (to_max_core(a).m_lhs != to_max_core(b).m_lhs) + return is_lt(to_max_core(a).m_lhs, to_max_core(b).m_lhs); + else + return is_lt(to_max_core(a).m_rhs, to_max_core(b).m_rhs); + case level_kind::Succ: + return is_lt(succ_of(a), succ_of(b)); + } + lean_unreachable(); // LCOV_EXCL_LINE } -level max(std::initializer_list const & l) { - if (l.size() == 1) - return *(l.begin()); - return max_core(l.size(), l.begin()); -} - - class level_serializer : public object_serializer { typedef object_serializer super; public: @@ -274,17 +318,17 @@ public: auto k = kind(l); s << static_cast(k); switch (k) { - case level_kind::UVar: - s << uvar_name(l); + case level_kind::Zero: break; - case level_kind::Lift: - s << lift_offset(l); - write(lift_of(l)); + case level_kind::Param: case level_kind::Meta: + s << to_param_core(l).m_id; break; - case level_kind::Max: - s << max_size(l); - for (unsigned i = 0; i < max_size(l); i++) - write(max_level(l, i)); + case level_kind::Max: case level_kind::IMax: + write(to_max_core(l).m_lhs); + write(to_max_core(l).m_rhs); + break; + case level_kind::Succ: + write(succ_of(l)); break; } }); @@ -299,20 +343,27 @@ public: deserializer & d = get_owner(); auto k = static_cast(d.read_char()); switch (k) { - case level_kind::UVar: - return level(read_name(d)); - case level_kind::Lift: { - unsigned offset = d.read_unsigned(); - return read() + offset; + case level_kind::Zero: + return mk_level_zero(); + case level_kind::Param: { + unsigned id = d.read_unsigned(); + return mk_param_univ(id); + } + case level_kind::Meta: { + unsigned id = d.read_unsigned(); + return mk_meta_univ(id); } case level_kind::Max: { - buffer lvls; - unsigned num = d.read_unsigned(); - for (unsigned i = 0; i < num; i++) { - lvls.push_back(read()); - } - return max_core(lvls.size(), lvls.data()); - }} + level lhs = read(); + return mk_max(lhs, read()); + } + case level_kind::IMax: { + level lhs = read(); + return mk_imax(lhs, read()); + } + case level_kind::Succ: + return mk_succ(read()); + } throw_corrupted_file(); }); } @@ -322,10 +373,15 @@ struct level_sd { unsigned m_s_extid; unsigned m_d_extid; level_sd() { - m_s_extid = serializer::register_extension([](){ return std::unique_ptr(new level_serializer()); }); - m_d_extid = deserializer::register_extension([](){ return std::unique_ptr(new level_deserializer()); }); + m_s_extid = serializer::register_extension([](){ + return std::unique_ptr(new level_serializer()); + }); + m_d_extid = deserializer::register_extension([](){ + return std::unique_ptr(new level_deserializer()); + }); } }; + static level_sd g_level_sd; serializer & operator<<(serializer & s, level const & n) { @@ -336,5 +392,113 @@ serializer & operator<<(serializer & s, level const & n) { level read_level(deserializer & d) { return d.get_extension(g_level_sd.m_d_extid).read(); } + +static void print(std::ostream & out, level l); + +static void print_child(std::ostream & out, level const & l) { + if (is_explicit(l) || is_param(l) || is_meta(l)) { + print(out, l); + } else { + out << "("; + print(out, l); + out << ")"; + } } + +static void print(std::ostream & out, level l) { + if (is_explicit(l)) { + lean_assert(get_depth(l) > 0); + out << get_depth(l) - 1; + } else { + switch (kind(l)) { + case level_kind::Zero: + lean_unreachable(); // LCOV_EXCL_LINE + case level_kind::Param: + out << "l_" << param_id(l); break; + case level_kind::Meta: + out << "?" << meta_id(l); break; + case level_kind::Succ: + out << "succ "; print_child(out, succ_of(l)); break; + case level_kind::Max: case level_kind::IMax: + if (is_max(l)) + out << "max "; + else + out << "imax "; + print_child(out, max_lhs(l)); + // max and imax are right associative + while (kind(max_rhs(l)) == kind(l)) { + l = max_rhs(l); + out << " "; + print_child(out, max_lhs(l)); + } + out << " "; + print_child(out, max_rhs(l)); + break; + } + } +} + +std::ostream & operator<<(std::ostream & out, level const & l) { + print(out, l); + return out; +} + +format pp(level l, bool unicode, unsigned indent); + +static format pp_child(level const & l, bool unicode, unsigned indent) { + if (is_explicit(l) || is_param(l) || is_meta(l)) { + return pp(l, unicode, indent); + } else { + return paren(pp(l, unicode, indent)); + } +} + +static char const * g_sub[10] = { + "\u2080", "\u2081", "\u2082", "\u2083", "\u2084", "\u2085", "\u2086", "\u2087", "\u2088", "\u2089" +}; + +format pp(level l, bool unicode, unsigned indent) { + if (is_explicit(l)) { + lean_assert(get_depth(l) > 0); + return format(get_depth(l) - 1); + } else { + switch (kind(l)) { + case level_kind::Zero: + lean_unreachable(); // LCOV_EXCL_LINE + case level_kind::Param: + if (unicode) { + format r = format("ℓ"); + if (param_id(l) == 0) + return r; + else if (param_id(l) <= 9) + return r + format(g_sub[param_id(l)]); + else + return r + format{format("_"), format(param_id(l))}; + } else { + return format{format("l_"), format(param_id(l))}; + } + case level_kind::Meta: + return format{format("?"), format(meta_id(l))}; + case level_kind::Succ: + return group(compose(format("succ"), nest(indent, compose(line(), pp_child(succ_of(l), unicode, indent))))); + case level_kind::Max: case level_kind::IMax: { + format r = format(is_max(l) ? "max" : "imax"); + r += nest(indent, compose(line(), pp_child(max_lhs(l), unicode, indent))); + // max and imax are right associative + while (kind(max_rhs(l)) == kind(l)) { + l = max_rhs(l); + r += nest(indent, compose(line(), pp_child(max_lhs(l), unicode, indent))); + } + r += nest(indent, compose(line(), pp_child(max_rhs(l), unicode, indent))); + return group(r); + }} + lean_unreachable(); // LCOV_EXCL_LINE + } +} + +format pp(level const & l, options const & opts) { + return pp(l, get_pp_unicode(opts), get_pp_indent(opts)); +} +} + void print(lean::level const & l) { std::cout << l << std::endl; } diff --git a/src/kernel/level.h b/src/kernel/level.h index 6b9a7747a..80531b0a5 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/name.h" +#include "util/optional.h" #include "util/serializer.h" #include "util/sexpr/format.h" #include "util/sexpr/options.h" @@ -15,72 +16,118 @@ Author: Leonardo de Moura namespace lean { class environment; struct level_cell; -enum class level_kind { UVar, Lift, Max }; +/** + \brief Universe level kinds. + + - Zero : Bool/Prop level. In Lean, Bool == (Type zero) + - Succ(l) : successor level + - Max(l1, l2) : maximum of two levels + - IMax(l1, l2) : IMax(x, zero) = zero for all x + IMax(x, succ(y)) = Max(x, succ(y)) for all x, y + + We use IMax to handle Pi-types, and Max for Sigma-types. + Their definitions "mirror" the typing rules for Pi and Sigma. + + - Param(i) : A parameter. In Lean, we have universe polymorphic definitions. + - Meta(i) : Placeholder. It is the equivalent of a metavariable for universe levels. + The elaborator is responsible for replacing Meta with level expressions + that do not contain Meta. +*/ +enum class level_kind { Zero, Succ, Max, IMax, Param, Meta }; + /** \brief Universe level. */ class level { friend class environment; level_cell * m_ptr; - /** \brief Private constructor used by the environment to create a new universe variable named \c n with internal id \c u. */ - level(level const & l, unsigned k); - level(level_cell * ptr); - friend level to_level(level_cell * c); - friend level_cell * to_cell(level const & l); - friend level operator+(level const & l, unsigned k); + friend level_cell const & to_cell(level const & l); public: - /** \brief Universe 0 */ + /** \brief Universe zero */ level(); - level(name const & n); + level(level_cell * ptr); level(level const & l); level(level&& s); ~level(); - unsigned hash() const; - - bool is_bottom() const; - - friend level_kind kind (level const & l); - friend name const & uvar_name (level const & l); - friend level const & lift_of (level const & l); - friend unsigned lift_offset(level const & l); - friend unsigned max_size (level const & l); - friend level const & max_level (level const & l, unsigned i); - level & operator=(level const & l); level & operator=(level&& l); - friend bool operator==(level const & l1, level const & l2); - friend bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); } - friend bool operator<(level const & l1, level const & l2); - friend void swap(level & l1, level & l2) { std::swap(l1, l2); } + friend bool is_eqp(level const & l1, level const & l2) { return l1.m_ptr == l2.m_ptr; } - friend std::ostream & operator<<(std::ostream & out, level const & l); + friend void swap(level & l1, level & l2) { std::swap(l1, l2); } struct ptr_hash { unsigned operator()(level const & n) const { return std::hash()(n.m_ptr); } }; struct ptr_eq { bool operator()(level const & n1, level const & n2) const { return n1.m_ptr == n2.m_ptr; } }; }; -level max(level const & l1, level const & l2); -level max(std::initializer_list const & l); -level operator+(level const & l, unsigned k); +level const & mk_level_zero(); +level const & mk_level_one(); +level mk_max(level const & l1, level const & l2); +level mk_imax(level const & l1, level const & l2); +level mk_succ(level const & l); +level mk_param_univ(unsigned i); +level mk_meta_univ(unsigned i); -inline bool is_bottom(level const & l) { return l.is_bottom(); } -inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar; } -inline bool is_lift(level const & l) { return kind(l) == level_kind::Lift; } -inline bool is_max (level const & l) { return kind(l) == level_kind::Max; } +bool operator==(level const & l1, level const & l2); +inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); } -/** \brief Return a */ -inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); } -inline level const * max_end_levels(level const & l) { return max_begin_levels(l) + max_size(l); } +/** + \brief An arbitrary (monotonic) total order on universe level terms. +*/ +bool is_lt(level const & l1, level const & l2); -/** \brief Pretty print the given level expression, unicode characters are used if \c unicode is \c true. */ -format pp(level const & l, bool unicode); -/** \brief Pretty print the given level expression using the given configuration options. */ -format pp(level const & l, options const & opts = options()); +unsigned hash(level const & l); +level_kind kind(level const & l); +inline bool is_zero(level const & l) { return kind(l) == level_kind::Zero; } +inline bool is_param(level const & l) { return kind(l) == level_kind::Param; } +inline bool is_meta(level const & l) { return kind(l) == level_kind::Meta; } +inline bool is_succ(level const & l) { return kind(l) == level_kind::Succ; } +inline bool is_max(level const & l) { return kind(l) == level_kind::Max; } +inline bool is_imax(level const & l) { return kind(l) == level_kind::IMax; } + +unsigned get_depth(level const & l); +unsigned get_param_range(level const & l); +unsigned get_meta_range(level const & l); + +level const & max_lhs(level const & l); +level const & max_rhs(level const & l); +level const & imax_lhs(level const & l); +level const & imax_rhs(level const & l); +level const & succ_of(level const & l); +unsigned param_id(level const & l); +unsigned meta_id(level const & l); +/** + \brief Return true iff \c l is an explicit level. + We say a level l is explicit iff + 1) l is zero OR + 2) l = succ(l') and l' is explicit +*/ +bool is_explicit(level const & l); + +/** + \brief Return true iff \c l contains placeholder (aka meta parameters). +*/ +inline bool has_meta(level const & l) { return get_meta_range(l) > 0; } + +/** + \brief Printer for debugging purposes +*/ +std::ostream & operator<<(std::ostream & out, level const & l); + +/** + \brief If the result is true, then forall assignments \c A that assigns all parameters and metavariables occuring + in \c l, eval(A, l) != zero. +*/ +bool is_not_zero(level const & l); serializer & operator<<(serializer & s, level const & l); level read_level(deserializer & d); inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; } + +/** \brief Pretty print the given level expression, unicode characters are used if \c unicode is \c true. */ +format pp(level l, bool unicode, unsigned indent); +/** \brief Pretty print the given level expression using the given configuration options. */ +format pp(level const & l, options const & opts = options()); } void print(lean::level const & l); diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index 36144c867..b6bdbe9e6 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -1,41 +1,41 @@ -add_executable(expr expr.cpp) -target_link_libraries(expr ${EXTRA_LIBS}) -add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) -add_executable(normalizer normalizer.cpp) -target_link_libraries(normalizer ${EXTRA_LIBS}) -add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer) -set_tests_properties(normalizer PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") -add_executable(threads threads.cpp) -target_link_libraries(threads ${EXTRA_LIBS}) -add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads) -set_tests_properties(threads PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") -add_executable(free_vars free_vars.cpp) -target_link_libraries(free_vars ${EXTRA_LIBS}) -add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars) +# add_executable(expr expr.cpp) +# target_link_libraries(expr ${EXTRA_LIBS}) +# add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) +# add_executable(normalizer normalizer.cpp) +# target_link_libraries(normalizer ${EXTRA_LIBS}) +# add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer) +# set_tests_properties(normalizer PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") +# add_executable(threads threads.cpp) +# target_link_libraries(threads ${EXTRA_LIBS}) +# add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads) +# set_tests_properties(threads PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") +# add_executable(free_vars free_vars.cpp) +# target_link_libraries(free_vars ${EXTRA_LIBS}) +# add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars) add_executable(level level.cpp) target_link_libraries(level ${EXTRA_LIBS}) add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level) -add_executable(replace replace.cpp) -target_link_libraries(replace ${EXTRA_LIBS}) -add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace) -add_executable(type_checker type_checker.cpp) -target_link_libraries(type_checker ${EXTRA_LIBS}) -add_test(type_checker ${CMAKE_CURRENT_BINARY_DIR}/type_checker) -set_tests_properties(type_checker PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") -add_executable(environment environment.cpp) -target_link_libraries(environment ${EXTRA_LIBS}) -add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment) -set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") -add_executable(occurs occurs.cpp) -target_link_libraries(occurs ${EXTRA_LIBS}) -add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) -add_executable(metavar metavar.cpp) -target_link_libraries(metavar ${EXTRA_LIBS}) -add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) -set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") -add_executable(instantiate instantiate.cpp) -target_link_libraries(instantiate ${EXTRA_LIBS}) -add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate) -add_executable(universe_constraints universe_constraints.cpp) -target_link_libraries(universe_constraints ${EXTRA_LIBS}) -add_test(universe_constraints ${CMAKE_CURRENT_BINARY_DIR}/universe_constraints) +# add_executable(replace replace.cpp) +# target_link_libraries(replace ${EXTRA_LIBS}) +# add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace) +# add_executable(type_checker type_checker.cpp) +# target_link_libraries(type_checker ${EXTRA_LIBS}) +# add_test(type_checker ${CMAKE_CURRENT_BINARY_DIR}/type_checker) +# set_tests_properties(type_checker PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") +# add_executable(environment environment.cpp) +# target_link_libraries(environment ${EXTRA_LIBS}) +# add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment) +# set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") +# add_executable(occurs occurs.cpp) +# target_link_libraries(occurs ${EXTRA_LIBS}) +# add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) +# add_executable(metavar metavar.cpp) +# target_link_libraries(metavar ${EXTRA_LIBS}) +# add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) +# set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") +# add_executable(instantiate instantiate.cpp) +# target_link_libraries(instantiate ${EXTRA_LIBS}) +# add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate) +# add_executable(universe_constraints universe_constraints.cpp) +# target_link_libraries(universe_constraints ${EXTRA_LIBS}) +# add_test(universe_constraints ${CMAKE_CURRENT_BINARY_DIR}/universe_constraints) diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index 4f8c34e65..24923051f 100644 --- a/src/tests/kernel/level.cpp +++ b/src/tests/kernel/level.cpp @@ -7,8 +7,7 @@ Author: Leonardo de Moura #include #include "util/test.h" #include "util/exception.h" -#include "kernel/environment.h" -#include "library/printer.h" +#include "kernel/level.h" using namespace lean; static void check_serializer(level const & l) { @@ -19,10 +18,33 @@ static void check_serializer(level const & l) { deserializer d(in); level l1, l2; d >> l1 >> l2; - lean_assert(l == l1); - lean_assert(l == l2); + lean_assert_eq(l, l1); + lean_assert_eq(l, l2); } +static void tst1() { + level zero; + level one = mk_succ(zero); + level two = mk_succ(one); + lean_assert(mk_max(one, two) == two); + lean_assert(mk_imax(one, two) == two); + lean_assert(mk_imax(two, zero) == zero); + check_serializer(two); + check_serializer(one); + level p = mk_param_univ(0); + lean_assert(mk_imax(p, zero) == zero); + lean_assert(mk_max(zero, p) == p); + lean_assert(mk_max(p, zero) == p); + lean_assert(mk_max(p, one) != p); + check_serializer(mk_max(p, one)); + check_serializer(mk_imax(p, one)); + check_serializer(mk_imax(one, p)); + check_serializer(mk_imax(mk_succ(p), p)); + 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()); @@ -123,14 +145,18 @@ static void tst5() { 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; }