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

feat(kernel): add global universe level

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-06 16:13:29 -07:00
parent 8095783c36
commit 503d8dfa9e
3 changed files with 77 additions and 87 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

139
src/kernel/level.cpp
View file

@ -33,16 +33,17 @@ struct level_cell {
struct level_composite : public level_cell {
unsigned m_depth;
unsigned m_has_param:1;
unsigned m_has_global:1;
unsigned m_has_meta:1;
level_composite(level_kind k, unsigned h, unsigned d, bool has_param, bool has_meta):
level_cell(k, h), m_depth(d), m_has_param(has_param), m_has_meta(has_meta) {}
level_composite(level_kind k, unsigned h, unsigned d, bool has_param, bool has_global, bool has_meta):
level_cell(k, h), m_depth(d), m_has_param(has_param), m_has_global(has_global), m_has_meta(has_meta) {}
};
bool is_composite(level const & l) {
switch (kind(l)) {
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return true;
case level_kind::Param: case level_kind::Meta: case level_kind::Zero:
case level_kind::Param: case level_kind::Global: case level_kind::Meta: case level_kind::Zero:
return false;
}
lean_unreachable(); // LCOV_EXCL_LINE
@ -57,7 +58,7 @@ 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, has_param(l), has_meta(l)),
level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, has_param(l), has_global(l), has_meta(l)),
m_l(l),
m_explicit(is_explicit(l)) {}
};
@ -72,8 +73,9 @@ struct level_max_core : public level_composite {
level_composite(imax ? level_kind::IMax : level_kind::Max,
hash(hash(l1), hash(l2)),
std::max(get_depth(l1), get_depth(l2)) + 1,
has_param(l1) || has_param(l2),
has_meta(l1) || has_meta(l2)),
has_param(l1) || has_param(l2),
has_global(l1) || has_global(l2),
has_meta(l1) || has_meta(l2)),
m_lhs(l1), m_rhs(l2) {
lean_assert(!is_explicit(l1) || !is_explicit(l2));
}
@ -91,9 +93,11 @@ level const & imax_rhs(level const & l) { lean_assert(is_imax(l)); return to_max
struct level_param_core : public level_cell {
name m_id;
level_param_core(bool is_param, name const & id):
level_cell(is_param ? level_kind::Param : level_kind::Meta, hash(id.hash(), is_param ? 11u : 13u)),
m_id(id) {}
level_param_core(level_kind k, name const & id):
level_cell(k, hash(id.hash(), is_param ? 11u : 13u)),
m_id(id) {
lean_assert(k == level_kind::Meta || k == level_kind::Param || k == level_kind::Global);
}
};
bool is_param_core(level const & l) { return is_param(l) || is_meta(l); }
@ -104,6 +108,7 @@ static level_param_core const & to_param_core(level const & l) {
}
name const & param_id(level const & l) { lean_assert(is_param(l)); return to_param_core(l).m_id; }
name const & global_id(level const & l) { lean_assert(is_global(l)); return to_param_core(l).m_id; }
name const & meta_id(level const & l) { lean_assert(is_meta(l)); return to_param_core(l).m_id; }
void level_cell::dealloc() {
@ -114,7 +119,7 @@ void level_cell::dealloc() {
case level_kind::Max: case level_kind::IMax:
delete static_cast<level_max_core*>(this);
break;
case level_kind::Param: case level_kind::Meta:
case level_kind::Param: case level_kind::Global: case level_kind::Meta:
delete static_cast<level_param_core*>(this);
break;
case level_kind::Zero:
@ -125,7 +130,7 @@ void level_cell::dealloc() {
unsigned get_depth(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
return 1;
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return to_composite(l).m_depth;
@ -135,7 +140,7 @@ unsigned get_depth(level const & l) {
bool has_param(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Meta:
case level_kind::Zero: case level_kind::Meta: case level_kind::Global:
return false;
case level_kind::Param:
return true;
@ -145,9 +150,21 @@ bool has_param(level const & l) {
lean_unreachable(); // LCOV_EXCL_LINE
}
bool has_global(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
return false;
case level_kind::Global:
return true;
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return to_composite(l).m_has_param;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
bool has_meta(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param:
case level_kind::Zero: case level_kind::Param: case level_kind::Global:
return false;
case level_kind::Meta:
return true;
@ -161,7 +178,7 @@ 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:
case level_kind::Param: case level_kind::Global: 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;
@ -197,13 +214,9 @@ level mk_imax(level const & l1, level const & l2) {
return level(new level_max_core(true, l1, l2));
}
level mk_param_univ(name const & n) {
return level(new level_param_core(true, n));
}
level mk_meta_univ(name const & n) {
return level(new level_param_core(false, n));
}
level mk_param_univ(name const & n) { return level(new level_param_core(level_kind::Param, n)); }
level mk_global_univ(name const & n) { return level(new level_param_core(level_kind::Global, n)); }
level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
level const & mk_level_zero() {
static level g_zero(new level_cell(level_kind::Zero, 7u));
@ -232,7 +245,7 @@ bool operator==(level const & l1, level const & l2) {
switch (kind(l1)) {
case level_kind::Zero:
return true;
case level_kind::Param: case level_kind::Meta:
case level_kind::Param: case level_kind::Global: 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)
@ -240,7 +253,7 @@ bool operator==(level const & l1, level const & l2) {
break;
}
switch (kind(l1)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Max: case level_kind::IMax:
return
@ -262,7 +275,7 @@ bool operator==(level const & l1, level const & l2) {
bool is_not_zero(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
return false;
case level_kind::Succ:
return true;
@ -288,7 +301,7 @@ bool is_lt(level const & a, level const & b) {
switch (kind(a)) {
case level_kind::Zero:
return false;
case level_kind::Param: case level_kind::Meta:
case level_kind::Param: case level_kind::Global: 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)
@ -312,7 +325,7 @@ public:
switch (k) {
case level_kind::Zero:
break;
case level_kind::Param: case level_kind::Meta:
case level_kind::Param: case level_kind::Global: case level_kind::Meta:
s << to_param_core(l).m_id;
break;
case level_kind::Max: case level_kind::IMax:
@ -339,6 +352,8 @@ public:
return mk_level_zero();
case level_kind::Param:
return mk_param_univ(read_name(d));
case level_kind::Global:
return mk_global_univ(read_name(d));
case level_kind::Meta:
return mk_meta_univ(read_name(d));
case level_kind::Max: {
@ -377,17 +392,11 @@ serializer & operator<<(serializer & s, level const & n) {
return s;
}
level read_level(deserializer & d) {
return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read();
}
level read_level(deserializer & d) { return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read(); }
serializer & operator<<(serializer & s, levels const & ls) {
return write_list<level>(s, ls);
}
serializer & operator<<(serializer & s, levels const & ls) { return write_list<level>(s, ls); }
levels read_levels(deserializer & d) {
return read_list<level>(d, read_level);
}
levels read_levels(deserializer & d) { return read_list<level>(d, read_level); }
serializer & operator<<(serializer & s, level_cnstr const & c) {
s << c.first << c.second;
@ -404,52 +413,22 @@ serializer & operator<<(serializer & s, level_cnstrs const & cs) {
return write_list<level_cnstr>(s, cs);
}
level_cnstrs read_level_cnstrs(deserializer & d) {
return read_list<level_cnstr>(d, read_level_cnstr);
}
level_cnstrs read_level_cnstrs(deserializer & d) { return read_list<level_cnstr>(d, read_level_cnstr); }
bool has_meta(levels const & ls) {
for (auto const & l : ls) {
if (has_meta(l))
return true;
}
return false;
}
bool has_param(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_param(l); }); }
bool has_param(level_cnstr const & c) { return has_param(c.first) || has_param(c.second); }
bool has_param(level_cnstrs const & cs) { return std::any_of(cs.begin(), cs.end(), [](level_cnstr const & c) { return has_param(c); }); }
bool has_param(levels const & ls) {
for (auto const & l : ls) {
if (has_param(l))
return true;
}
return false;
}
bool has_global(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_global(l); }); }
bool has_global(level_cnstr const & c) { return has_global(c.first) || has_global(c.second); }
bool has_global(level_cnstrs const & cs) { return std::any_of(cs.begin(), cs.end(), [](level_cnstr const & c) { return has_global(c); }); }
bool has_param(level_cnstr const & c) {
return has_param(c.first) || has_param(c.second);
}
bool has_param(level_cnstrs const & cs) {
for (auto const & c : cs) {
if (has_param(c))
return true;
}
return false;
}
bool has_meta(level_cnstr const & c) {
return has_meta(c.first) || has_meta(c.second);
}
bool has_meta(level_cnstrs const & cs) {
for (auto const & c : cs) {
if (has_meta(c))
return true;
}
return false;
}
bool has_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_meta(l); }); }
bool has_meta(level_cnstr const & c) { return has_meta(c.first) || has_meta(c.second); }
bool has_meta(level_cnstrs const & cs) { return std::any_of(cs.begin(), cs.end(), [](level_cnstr const & c) { return has_meta(c); }); }
static optional<name> get_undef_param(level const & l, param_names const & ps) {
if (!has_meta(l))
if (!has_param(l))
return optional<name>();
switch (l.kind()) {
case level_kind::Succ:
@ -464,7 +443,7 @@ static optional<name> get_undef_param(level const & l, param_names const & ps) {
return optional<name>(param_id(l));
else
return optional<name>();
case level_kind::Zero: case level_kind::Meta:
case level_kind::Zero: case level_kind::Meta: case level_kind::Global:
lean_unreachable(); // LCOV_EXCL_LINE
}
lean_unreachable(); // LCOV_EXCL_LINE
@ -505,7 +484,7 @@ level replace_level_fn::apply(level const & l) {
return update_succ(l, apply(succ_of(l)));
case level_kind::Max: case level_kind::IMax:
return update_max(l, apply(to_max_core(l).m_lhs), apply(to_max_core(l).m_rhs));
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Meta: case level_kind::Global:
return l;
}
lean_unreachable(); // LCOV_EXCL_LINE
@ -553,7 +532,7 @@ static void print(std::ostream & out, level l) {
switch (kind(l)) {
case level_kind::Zero:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param:
case level_kind::Param: case level_kind::Global:
out << param_id(l); break;
case level_kind::Meta:
out << "?" << meta_id(l); break;
@ -601,7 +580,7 @@ format pp(level l, bool unicode, unsigned indent) {
switch (kind(l)) {
case level_kind::Zero:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param:
case level_kind::Param: case level_kind::Global:
return format(param_id(l));
case level_kind::Meta:
return format{format("?"), format(meta_id(l))};

24
src/kernel/level.h
View file

@ -31,11 +31,12 @@ struct level_cell;
Their definitions "mirror" the typing rules for Pi and Sigma.
- Param(n) : A parameter. In Lean, we have universe polymorphic definitions.
- Global(n) : A global level.
- Meta(n) : 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 };
enum class level_kind { Zero, Succ, Max, IMax, Param, Global, Meta };
/**
\brief Universe level.
@ -82,6 +83,7 @@ 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(name const & n);
level mk_global_univ(name const & n);
level mk_meta_univ(name const & n);
/** \brief An arbitrary (monotonic) total order on universe level terms. */
@ -89,12 +91,13 @@ bool is_lt(level const & l1, level const & l2);
inline unsigned hash(level const & l) { return l.hash(); }
inline level_kind kind(level const & l) { return l.kind(); }
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; }
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_global(level const & l) { return kind(l) == level_kind::Global; }
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);
@ -104,6 +107,7 @@ level const & imax_lhs(level const & l);
level const & imax_rhs(level const & l);
level const & succ_of(level const & l);
name const & param_id(level const & l);
name const & global_id(level const & l);
name const & meta_id(level const & l);
/**
\brief Return true iff \c l is an explicit level.
@ -115,9 +119,12 @@ bool is_explicit(level const & l);
/** \brief Return true iff \c l contains placeholder (aka meta parameters). */
bool has_meta(level const & l);
/** \brief Return true iff \c l contains globals */
bool has_global(level const & l);
/** \brief Return true iff \c l contains parameters */
bool has_param(level const & l);
/**
\brief Return a new level expression based on <tt>l == succ(arg)</tt>, where \c arg is replaced with
\c new_arg.
@ -145,6 +152,7 @@ bool is_trivial(level const & lhs, level const & rhs);
typedef list<level> levels;
bool has_meta(levels const & ls);
bool has_global(levels const & ls);
bool has_param(levels const & ls);
/**
@ -156,6 +164,8 @@ typedef list<level_cnstr> level_cnstrs;
bool has_param(level_cnstr const & c);
bool has_param(level_cnstrs const & cs);
bool has_global(level_cnstr const & c);
bool has_global(level_cnstrs const & cs);
bool has_meta(level_cnstr const & c);
bool has_meta(level_cnstrs const & cs);

1
src/library/expr_lt.cpp
View file

@ -20,6 +20,7 @@ bool is_lt(level const & a, level const & b, bool use_hash) {
case level_kind::Zero: return true;
case level_kind::Succ: return is_lt(succ_of(a), succ_of(b), use_hash);
case level_kind::Param: return param_id(a) < param_id(b);
case level_kind::Global: return global_id(a) < global_id(b);
case level_kind::Meta: return meta_id(a) < meta_id(b);
case level_kind::Max:
if (max_lhs(a) != max_lhs(b))