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

feat(kernel/level): new universe level datastructure for universe level polymorphism

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-13 18:02:14 -08:00
parent 1b6b33b3f5
commit 9f93b5d97e
5 changed files with 550 additions and 313 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -245,7 +245,7 @@ set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
add_subdirectory(tests/util) add_subdirectory(tests/util)
add_subdirectory(tests/util/numerics) add_subdirectory(tests/util/numerics)
add_subdirectory(tests/util/interval) add_subdirectory(tests/util/interval)
# add_subdirectory(tests/kernel) add_subdirectory(tests/kernel)
# add_subdirectory(tests/library) # add_subdirectory(tests/library)
# add_subdirectory(tests/library/rewriter) # add_subdirectory(tests/library/rewriter)
# add_subdirectory(tests/library/tactic) # add_subdirectory(tests/library/tactic)

626
src/kernel/level.cpp
View file

@ -5,63 +5,215 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include <algorithm> #include <algorithm>
#include <vector>
#include "util/safe_arith.h" #include "util/safe_arith.h"
#include "util/buffer.h" #include "util/buffer.h"
#include "util/rc.h" #include "util/rc.h"
#include "util/list.h"
#include "util/debug.h" #include "util/debug.h"
#include "util/hash.h" #include "util/hash.h"
#include "util/object_serializer.h" #include "util/object_serializer.h"
#include "kernel/level.h" #include "kernel/level.h"
namespace lean { 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 { struct level_cell {
void dealloc(); void dealloc();
MK_LEAN_RC() MK_LEAN_RC()
level_kind m_kind; 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 { unsigned hash(level const & l) { return to_cell(l).m_hash; }
name m_name; level_kind kind(level const & l) { return to_cell(l).m_kind; }
level_uvar(name const & n):level_cell(level_kind::UVar), m_name(n) {}
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 <tt>l + k</tt>, where \c l is a level and \c k a unsigned integer. */
struct level_lift : public level_cell { static bool is_composite(level const & l) {
level m_l; switch (kind(l)) {
unsigned m_k; case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
level_lift(level const & l, unsigned k):level_cell(level_kind::Lift), m_l(l), m_k(k) {} return true;
}; default:
/** \brief Cell for representing the universe <tt>max l_1 ... l_n</tt>, where <tt>n == m_size</tt>. */ return false;
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<level_uvar*>(c); }
level_lift * to_lift(level_cell * c) { return static_cast<level_lift*>(c); }
level_max * to_max(level_cell * c) { return static_cast<level_max*>(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<level_max*>(this)->~level_max(); delete[] reinterpret_cast<char*>(this); break;
} }
} }
static name g_bot_name("bot");
level::level(): m_ptr(new level_uvar(g_bot_name)) { lean_assert_eq(uvar_name(*this), name("bot")); } static level_composite const & to_composite(level const & l) {
level::level(name const & n): m_ptr(new level_uvar(n)) {} lean_assert(is_composite(l));
level::level(level const & l, unsigned k):m_ptr(new level_lift(l, k)) { lean_assert(is_uvar(l)); } return static_cast<level_composite const &>(to_cell(l));
level::level(level_cell * ptr): m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); } }
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<level_succ const &>(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<level_max_core const &>(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<level_param_core const &>(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<level_succ*>(this);
break;
case level_kind::Max: case level_kind::IMax:
delete static_cast<level_max_core*>(this);
break;
case level_kind::Param: case level_kind::Meta:
delete static_cast<level_param_core*>(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): level::level(level const & s):
m_ptr(s.m_ptr) { m_ptr(s.m_ptr) {
if (m_ptr) if (m_ptr)
@ -75,196 +227,88 @@ level::~level() {
if (m_ptr) if (m_ptr)
m_ptr->dec_ref(); 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<level> & 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<level> 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<level> 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<level_uvar*>(l.m_ptr)->m_name; }
level const & lift_of (level const & l) { lean_assert(is_lift(l)); return static_cast<level_lift*>(l.m_ptr)->m_l; }
unsigned lift_offset(level const & l) { lean_assert(is_lift(l)); return static_cast<level_lift*>(l.m_ptr)->m_k; }
unsigned max_size (level const & l) { lean_assert(is_max(l)); return static_cast<level_max*>(l.m_ptr)->m_size; }
level const & max_level (level const & l, unsigned i) { lean_assert(is_max(l)); return static_cast<level_max*>(l.m_ptr)->m_levels[i]; }
level & level::operator=(level const & l) { LEAN_COPY_REF(l); } level & level::operator=(level const & l) { LEAN_COPY_REF(l); }
level & level::operator=(level&& l) { LEAN_MOVE_REF(l); } level & level::operator=(level&& l) { LEAN_MOVE_REF(l); }
bool operator==(level const & l1, level const & l2) { bool operator==(level const & l1, level const & l2) {
if (kind(l1) != kind(l2)) return false; if (kind(l1) != kind(l2)) return false;
if (hash(l1) != hash(l2)) return false;
if (is_eqp(l1, l2)) return true;
switch (kind(l1)) { switch (kind(l1)) {
case level_kind::UVar: return uvar_name(l1) == uvar_name(l2); case level_kind::Zero:
case level_kind::Lift: return lift_of(l1) == lift_of(l2) && lift_offset(l1) == lift_offset(l2); return true;
case level_kind::Max: case level_kind::Param: case level_kind::Meta:
if (max_size(l1) == max_size(l2)) { return to_param_core(l1).m_id == to_param_core(l2).m_id;
for (unsigned i = 0; i < max_size(l1); i++) case level_kind::Max: case level_kind::IMax: case level_kind::Succ:
if (max_level(l1, i) != max_level(l2, i)) if (to_composite(l1).m_depth != to_composite(l2).m_depth ||
return false; 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; return true;
} else { } else {
return false; return succ_of(l1) == succ_of(l2);
} }
} }
lean_unreachable(); // LCOV_EXCL_LINE lean_unreachable(); // LCOV_EXCL_LINE
} }
bool operator<(level const & l1, level const & l2) { bool is_not_zero(level const & l) {
if (kind(l1) != kind(l2)) return kind(l1) < kind(l2); switch (kind(l)) {
switch (kind(l1)) { case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
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);
return false; return false;
} case level_kind::Succ:
lean_unreachable(); // LCOV_EXCL_LINE return true;
}
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::Max: case level_kind::Max:
out << "(max"; return is_not_zero(max_lhs(l)) || is_not_zero(max_rhs(l));
for (unsigned i = 0; i < max_size(l); i++) case level_kind::IMax:
out << " " << max_level(l, i); return is_not_zero(imax_rhs(l));
out << ")";
return out;
} }
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 lean_unreachable(); // LCOV_EXCL_LINE
} }
format pp(level const & l, options const & opts) { // Monotonic total order on universe level terms.
return pp(l, get_pp_unicode(opts)); 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<level> const & l) {
if (l.size() == 1)
return *(l.begin());
return max_core(l.size(), l.begin());
}
class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> { class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> {
typedef object_serializer<level, level::ptr_hash, level::ptr_eq> super; typedef object_serializer<level, level::ptr_hash, level::ptr_eq> super;
public: public:
@ -274,17 +318,17 @@ public:
auto k = kind(l); auto k = kind(l);
s << static_cast<char>(k); s << static_cast<char>(k);
switch (k) { switch (k) {
case level_kind::UVar: case level_kind::Zero:
s << uvar_name(l);
break; break;
case level_kind::Lift: case level_kind::Param: case level_kind::Meta:
s << lift_offset(l); s << to_param_core(l).m_id;
write(lift_of(l));
break; break;
case level_kind::Max: case level_kind::Max: case level_kind::IMax:
s << max_size(l); write(to_max_core(l).m_lhs);
for (unsigned i = 0; i < max_size(l); i++) write(to_max_core(l).m_rhs);
write(max_level(l, i)); break;
case level_kind::Succ:
write(succ_of(l));
break; break;
} }
}); });
@ -299,20 +343,27 @@ public:
deserializer & d = get_owner(); deserializer & d = get_owner();
auto k = static_cast<level_kind>(d.read_char()); auto k = static_cast<level_kind>(d.read_char());
switch (k) { switch (k) {
case level_kind::UVar: case level_kind::Zero:
return level(read_name(d)); return mk_level_zero();
case level_kind::Lift: { case level_kind::Param: {
unsigned offset = d.read_unsigned(); unsigned id = d.read_unsigned();
return read() + offset; return mk_param_univ(id);
}
case level_kind::Meta: {
unsigned id = d.read_unsigned();
return mk_meta_univ(id);
} }
case level_kind::Max: { case level_kind::Max: {
buffer<level> lvls; level lhs = read();
unsigned num = d.read_unsigned(); return mk_max(lhs, read());
for (unsigned i = 0; i < num; i++) { }
lvls.push_back(read()); case level_kind::IMax: {
} level lhs = read();
return max_core(lvls.size(), lvls.data()); return mk_imax(lhs, read());
}} }
case level_kind::Succ:
return mk_succ(read());
}
throw_corrupted_file(); throw_corrupted_file();
}); });
} }
@ -322,10 +373,15 @@ struct level_sd {
unsigned m_s_extid; unsigned m_s_extid;
unsigned m_d_extid; unsigned m_d_extid;
level_sd() { level_sd() {
m_s_extid = serializer::register_extension([](){ return std::unique_ptr<serializer::extension>(new level_serializer()); }); m_s_extid = serializer::register_extension([](){
m_d_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new level_deserializer()); }); return std::unique_ptr<serializer::extension>(new level_serializer());
});
m_d_extid = deserializer::register_extension([](){
return std::unique_ptr<deserializer::extension>(new level_deserializer());
});
} }
}; };
static level_sd g_level_sd; static level_sd g_level_sd;
serializer & operator<<(serializer & s, level const & n) { serializer & operator<<(serializer & s, level const & n) {
@ -336,5 +392,113 @@ serializer & operator<<(serializer & s, level const & n) {
level read_level(deserializer & d) { level read_level(deserializer & d) {
return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read(); return d.get_extension<level_deserializer>(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; } void print(lean::level const & l) { std::cout << l << std::endl; }

125
src/kernel/level.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <iostream> #include <iostream>
#include <algorithm> #include <algorithm>
#include "util/name.h" #include "util/name.h"
#include "util/optional.h"
#include "util/serializer.h" #include "util/serializer.h"
#include "util/sexpr/format.h" #include "util/sexpr/format.h"
#include "util/sexpr/options.h" #include "util/sexpr/options.h"
@ -15,72 +16,118 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
class environment; class environment;
struct level_cell; 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. \brief Universe level.
*/ */
class level { class level {
friend class environment; friend class environment;
level_cell * m_ptr; 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. */ friend level_cell const & to_cell(level const & l);
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);
public: public:
/** \brief Universe 0 */ /** \brief Universe zero */
level(); level();
level(name const & n); level(level_cell * ptr);
level(level const & l); level(level const & l);
level(level&& s); level(level&& s);
~level(); ~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 const & l);
level & operator=(level&& l); level & operator=(level&& l);
friend bool operator==(level const & l1, level const & l2); friend bool is_eqp(level const & l1, level const & l2) { return l1.m_ptr == l2.m_ptr; }
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 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<level_cell*>()(n.m_ptr); } }; struct ptr_hash { unsigned operator()(level const & n) const { return std::hash<level_cell*>()(n.m_ptr); } };
struct ptr_eq { bool operator()(level const & n1, level const & n2) const { return n1.m_ptr == n2.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 const & mk_level_zero();
level max(std::initializer_list<level> const & l); level const & mk_level_one();
level operator+(level const & l, unsigned k); 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(); } bool operator==(level const & l1, level const & l2);
inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar; } inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }
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; }
/** \brief Return a */ /**
inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); } \brief An arbitrary (monotonic) total order on universe level terms.
inline level const * max_end_levels(level const & l) { return max_begin_levels(l) + max_size(l); } */
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. */ unsigned hash(level const & l);
format pp(level const & l, bool unicode); level_kind kind(level const & l);
/** \brief Pretty print the given level expression using the given configuration options. */ inline bool is_zero(level const & l) { return kind(l) == level_kind::Zero; }
format pp(level const & l, options const & opts = options()); 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); serializer & operator<<(serializer & s, level const & l);
level read_level(deserializer & d); level read_level(deserializer & d);
inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return 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); void print(lean::level const & l);

76
src/tests/kernel/CMakeLists.txt
View file

@ -1,41 +1,41 @@
add_executable(expr expr.cpp) # add_executable(expr expr.cpp)
target_link_libraries(expr ${EXTRA_LIBS}) # target_link_libraries(expr ${EXTRA_LIBS})
add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) # add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr)
add_executable(normalizer normalizer.cpp) # add_executable(normalizer normalizer.cpp)
target_link_libraries(normalizer ${EXTRA_LIBS}) # target_link_libraries(normalizer ${EXTRA_LIBS})
add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer) # add_test(normalizer ${CMAKE_CURRENT_BINARY_DIR}/normalizer)
set_tests_properties(normalizer PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # set_tests_properties(normalizer PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(threads threads.cpp) # add_executable(threads threads.cpp)
target_link_libraries(threads ${EXTRA_LIBS}) # target_link_libraries(threads ${EXTRA_LIBS})
add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads) # add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads)
set_tests_properties(threads PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # set_tests_properties(threads PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(free_vars free_vars.cpp) # add_executable(free_vars free_vars.cpp)
target_link_libraries(free_vars ${EXTRA_LIBS}) # target_link_libraries(free_vars ${EXTRA_LIBS})
add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars) # add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars)
add_executable(level level.cpp) add_executable(level level.cpp)
target_link_libraries(level ${EXTRA_LIBS}) target_link_libraries(level ${EXTRA_LIBS})
add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level) add_test(level ${CMAKE_CURRENT_BINARY_DIR}/level)
add_executable(replace replace.cpp) # add_executable(replace replace.cpp)
target_link_libraries(replace ${EXTRA_LIBS}) # target_link_libraries(replace ${EXTRA_LIBS})
add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace) # add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace)
add_executable(type_checker type_checker.cpp) # add_executable(type_checker type_checker.cpp)
target_link_libraries(type_checker ${EXTRA_LIBS}) # target_link_libraries(type_checker ${EXTRA_LIBS})
add_test(type_checker ${CMAKE_CURRENT_BINARY_DIR}/type_checker) # add_test(type_checker ${CMAKE_CURRENT_BINARY_DIR}/type_checker)
set_tests_properties(type_checker PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # set_tests_properties(type_checker PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(environment environment.cpp) # add_executable(environment environment.cpp)
target_link_libraries(environment ${EXTRA_LIBS}) # target_link_libraries(environment ${EXTRA_LIBS})
add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment) # add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)
set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(occurs occurs.cpp) # add_executable(occurs occurs.cpp)
target_link_libraries(occurs ${EXTRA_LIBS}) # target_link_libraries(occurs ${EXTRA_LIBS})
add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) # add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
add_executable(metavar metavar.cpp) # add_executable(metavar metavar.cpp)
target_link_libraries(metavar ${EXTRA_LIBS}) # target_link_libraries(metavar ${EXTRA_LIBS})
add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) # add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)
set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(instantiate instantiate.cpp) # add_executable(instantiate instantiate.cpp)
target_link_libraries(instantiate ${EXTRA_LIBS}) # target_link_libraries(instantiate ${EXTRA_LIBS})
add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate) # add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate)
add_executable(universe_constraints universe_constraints.cpp) # add_executable(universe_constraints universe_constraints.cpp)
target_link_libraries(universe_constraints ${EXTRA_LIBS}) # target_link_libraries(universe_constraints ${EXTRA_LIBS})
add_test(universe_constraints ${CMAKE_CURRENT_BINARY_DIR}/universe_constraints) # add_test(universe_constraints ${CMAKE_CURRENT_BINARY_DIR}/universe_constraints)

34
src/tests/kernel/level.cpp
View file

@ -7,8 +7,7 @@ Author: Leonardo de Moura
#include <locale> #include <locale>
#include "util/test.h" #include "util/test.h"
#include "util/exception.h" #include "util/exception.h"
#include "kernel/environment.h" #include "kernel/level.h"
#include "library/printer.h"
using namespace lean; using namespace lean;
static void check_serializer(level const & l) { static void check_serializer(level const & l) {
@ -19,10 +18,33 @@ static void check_serializer(level const & l) {
deserializer d(in); deserializer d(in);
level l1, l2; level l1, l2;
d >> l1 >> l2; d >> l1 >> l2;
lean_assert(l == l1); lean_assert_eq(l, l1);
lean_assert(l == l2); 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() { static void tst0() {
environment env; environment env;
lean_assert(env->begin_objects() == env->end_objects()); lean_assert(env->begin_objects() == env->end_objects());
@ -123,14 +145,18 @@ static void tst5() {
std::cout << max(l1, max(l2, l1+1)) << "\n"; std::cout << max(l1, max(l2, l1+1)) << "\n";
lean_assert(max(l1, max(l2, l1+1)) == max(l1+1, l2)); lean_assert(max(l1, max(l2, l1+1)) == max(l1+1, l2));
} }
#endif
int main() { int main() {
save_stack_info(); save_stack_info();
tst1();
#if 0
tst0(); tst0();
tst1(); tst1();
tst2(); tst2();
tst3(); tst3();
tst4(); tst4();
tst5(); tst5();
#endif
return has_violations() ? 1 : 0; return has_violations() ? 1 : 0;
} }