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

feat(kernel/formatter): adjust simple formatter to the new convention for displaying universe levels

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-12 14:42:01 -07:00
parent d4922daedf
commit b18263a014
3 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/formatter.cpp
View file

@ -40,9 +40,11 @@ struct print_expr_fn {
void print_sort(expr const & a) {
if (is_zero(sort_level(a))) {
out () << "Bool";
out() << "Bool";
} else if (is_one(sort_level(a))) {
out() << "Type";
} else {
out() << "(Type " << sort_level(a) << ")";
out() << "Type.{" << sort_level(a) << "}";
}
}

4
src/kernel/level.cpp
View file

@ -248,6 +248,10 @@ level const & mk_level_one() {
return g_one;
}
bool is_one(level const & l) {
return l == mk_level_one();
}
level::level():level(mk_level_zero()) {}
level::level(level_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
level::level(level const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }

1
src/kernel/level.h
View file

@ -95,6 +95,7 @@ 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; }
bool is_one(level const & l);
unsigned get_depth(level const & l);