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

refactor(kernel): use names instead of unsigned integers to encode level parameters

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-24 11:05:42 -08:00
parent ddbb3a7944
commit eb487e44c1
9 changed files with 238 additions and 199 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/constraint.cpp
View file

@ -76,6 +76,7 @@ bool operator==(constraint const & c1, constraint const & c2) {
cnstr_choice_expr(c1) == cnstr_choice_expr(c2) &&
compare(cnstr_choice_set(c1), cnstr_choice_set(c2), [](expr const & e1, expr const & e2) { return e1 == e2; });
}
lean_unreachable(); // LCOV_EXCL_LINE
}
expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eqc_cnstr(c)); return static_cast<eqc_constraint_cell*>(c.raw())->m_lhs; }

36
src/kernel/environment.cpp
View file

@ -199,10 +199,10 @@ void environment_cell::check_name(name const & n) {
check_name_core(n);
}
void environment_cell::check_level_cnstrs(unsigned num_param, level_cnstrs const & ls) {
if (get_meta_range(ls) > 0)
void environment_cell::check_level_cnstrs(param_names const & ps, level_cnstrs const & ls) {
if (has_meta(ls) > 0)
throw_kernel_exception(env(), "invalid level constraint, it contains level placeholders (aka meta-parameters that must be synthesized by Lean's elaborator");
if (get_param_range(ls) > num_param)
if (auto it = get_undef_param(ls, ps))
throw_kernel_exception(env(), "invalid level constraints, it contains undefined parameters");
}
@ -270,19 +270,19 @@ void environment_cell::check_type(expr const & t) {
}
/** \brief Throw exception if it is not a valid new definition */
void environment_cell::check_new_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) {
void environment_cell::check_new_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) {
check_name(n);
check_level_cnstrs(num_param, cs);
check_level_cnstrs(ps, cs);
check_type(n, t, v);
}
/** \brief Add new definition. */
void environment_cell::add_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) {
void environment_cell::add_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) {
check_no_mlocal(t);
check_no_mlocal(v);
check_new_definition(n, num_param, cs, t, v);
check_new_definition(n, ps, cs, t, v);
unsigned w = get_max_weight(v) + 1;
register_named_object(mk_definition(n, num_param, cs, t, v, w));
register_named_object(mk_definition(n, ps, cs, t, v, w));
}
/**
@ -300,15 +300,15 @@ void environment_cell::add_definition(name const & n, expr const & v) {
v_t = m_type_checker->infer_type(v);
#endif
unsigned w = get_max_weight(v) + 1;
register_named_object(mk_definition(n, 0, level_cnstrs(), v_t, v, w));
register_named_object(mk_definition(n, param_names(), level_cnstrs(), v_t, v, w));
}
/** \brief Add new theorem. */
void environment_cell::add_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) {
void environment_cell::add_theorem(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) {
check_no_mlocal(t);
check_no_mlocal(v);
check_new_definition(n, num_param, cs, t, v);
register_named_object(mk_theorem(n, num_param, cs, t, v));
check_new_definition(n, ps, cs, t, v);
register_named_object(mk_theorem(n, ps, cs, t, v));
}
void environment_cell::set_opaque(name const & n, bool opaque) {
@ -320,21 +320,21 @@ void environment_cell::set_opaque(name const & n, bool opaque) {
}
/** \brief Add new axiom. */
void environment_cell::add_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) {
void environment_cell::add_axiom(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t) {
check_no_mlocal(t);
check_name(n);
check_level_cnstrs(num_param, cs);
check_level_cnstrs(ps, cs);
check_type(t);
register_named_object(mk_axiom(n, num_param, cs, t));
register_named_object(mk_axiom(n, ps, cs, t));
}
/** \brief Add new variable. */
void environment_cell::add_var(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) {
void environment_cell::add_var(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t) {
check_no_mlocal(t);
check_name(n);
check_level_cnstrs(num_param, cs);
check_level_cnstrs(ps, cs);
check_type(t);
register_named_object(mk_var_decl(n, num_param, cs, t));
register_named_object(mk_var_decl(n, ps, cs, t));
}
void environment_cell::add_neutral_object(neutral_object_cell * o) {

20
src/kernel/environment.h
View file

@ -62,7 +62,7 @@ class environment_cell {
void check_name_core(name const & n);
void check_name(name const & n);
void check_level_cnstrs(unsigned num_param, level_cnstrs const & ls);
void check_level_cnstrs(param_names const & ps, level_cnstrs const & ls);
void register_named_object(object const & new_obj);
optional<object> get_object_core(name const & n) const;
@ -70,7 +70,7 @@ class environment_cell {
void check_no_mlocal(expr const & e);
void check_type(name const & n, expr const & t, expr const & v);
void check_type(expr const & t);
void check_new_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v);
void check_new_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v);
bool mark_imported_core(name n);
bool load_core(std::string const & fname, io_state const & ios, optional<std::string> const & mod_name);
@ -108,10 +108,10 @@ public:
It throws an exception if v does not have type t.
It throws an exception if there is already an object with the given name.
*/
void add_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v);
void add_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v);
void add_definition(name const & n, expr const & t, expr const & v) { add_definition(n, 0, level_cnstrs(), t, v); }
void add_theorem(name const & n, expr const & t, expr const & v) { add_theorem(n, 0, level_cnstrs(), t, v); }
void add_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v);
void add_theorem(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v);
void add_definition(name const & n, expr const & t, expr const & v) { add_definition(n, param_names(), level_cnstrs(), t, v); }
void add_theorem(name const & n, expr const & t, expr const & v) { add_theorem(n, param_names(), level_cnstrs(), t, v); }
/**
\brief Add a new definition n : infer_type(v) := v.
@ -130,10 +130,10 @@ public:
\brief Add a new fact (Axiom or Fact) to the environment.
It throws an exception if there is already an object with the given name.
*/
void add_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t);
void add_var(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t);
void add_axiom(name const & n, expr const & t) { add_axiom(n, 0, level_cnstrs(), t); }
void add_var(name const & n, expr const & t) { add_var(n, 0, level_cnstrs(), t); };
void add_axiom(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t);
void add_var(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t);
void add_axiom(name const & n, expr const & t) { add_axiom(n, param_names(), level_cnstrs(), t); }
void add_var(name const & n, expr const & t) { add_var(n, param_names(), level_cnstrs(), t); };
/**
\brief Register the given unanymous object in this environment.

203
src/kernel/level.cpp
View file

@ -30,24 +30,22 @@ struct level_cell {
level_cell(level_kind k, unsigned h):m_rc(1), m_kind(k), m_hash(h) {}
};
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) {}
unsigned m_has_param: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) {}
};
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:
case level_kind::Param: case level_kind::Meta: case level_kind::Zero:
return false;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
static level_composite const & to_composite(level const & l) {
@ -59,7 +57,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, get_param_range(l), get_meta_range(l)),
level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, has_param(l), has_meta(l)),
m_l(l),
m_explicit(is_explicit(l)) {}
};
@ -74,8 +72,8 @@ 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,
std::max(get_param_range(l1), get_param_range(l2)),
std::max(get_meta_range(l1), get_meta_range(l2))),
has_param(l1) || has_param(l2),
has_meta(l1) || has_meta(l2)),
m_lhs(l1), m_rhs(l2) {
lean_assert(!is_explicit(l1) || !is_explicit(l2));
}
@ -92,9 +90,9 @@ level const & imax_lhs(level const & l) { lean_assert(is_imax(l)); return to_max
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)),
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) {}
};
@ -105,8 +103,8 @@ static level_param_core const & to_param_core(level const & 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; }
name const & param_id(level const & l) { lean_assert(is_param(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() {
switch (m_kind) {
@ -135,26 +133,26 @@ unsigned get_depth(level const & l) {
lean_unreachable(); // LCOV_EXCL_LINE
}
unsigned get_param_range(level const & l) {
bool has_param(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Meta:
return 0;
return false;
case level_kind::Param:
return to_param_core(l).m_id + 1;
return true;
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return to_composite(l).m_param_range;
return to_composite(l).m_has_param;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
unsigned get_meta_range(level const & l) {
bool has_meta(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param:
return 0;
return false;
case level_kind::Meta:
return to_param_core(l).m_id + 1;
return true;
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return to_composite(l).m_param_range;
return to_composite(l).m_has_meta;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -199,12 +197,12 @@ level mk_imax(level const & l1, level const & l2) {
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_param_univ(name const & n) {
return level(new level_param_core(true, n));
}
level mk_meta_univ(unsigned i) {
return level(new level_param_core(false, i));
level mk_meta_univ(name const & n) {
return level(new level_param_core(false, n));
}
static level g_zero(new level_cell(level_kind::Zero, 7u));
@ -215,22 +213,13 @@ 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)
m_ptr->inc_ref();
}
level::level(level && s):
m_ptr(s.m_ptr) {
s.m_ptr = nullptr;
}
level::~level() {
if (m_ptr)
m_ptr->dec_ref();
}
level::level(level const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
level::level(level && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
level::~level() { if (m_ptr) m_ptr->dec_ref(); }
level & level::operator=(level const & l) { LEAN_COPY_REF(l); }
level & level::operator=(level&& l) { LEAN_MOVE_REF(l); }
level_kind level::kind() const { return m_ptr->m_kind; }
unsigned level::hash() const { return m_ptr->m_hash; }
bool operator==(level const & l1, level const & l2) {
if (kind(l1) != kind(l2)) return false;
@ -242,9 +231,7 @@ bool operator==(level const & l1, level const & l2) {
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)
if (to_composite(l1).m_depth != to_composite(l2).m_depth)
return false;
break;
}
@ -346,14 +333,10 @@ public:
switch (k) {
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::Param:
return mk_param_univ(read_name(d));
case level_kind::Meta:
return mk_meta_univ(read_name(d));
case level_kind::Max: {
level lhs = read();
return mk_max(lhs, read());
@ -395,58 +378,86 @@ level read_level(deserializer & d) {
}
serializer & operator<<(serializer & s, levels const & ls) {
s << length(ls);
for (auto const & l : ls)
s << l;
return s;
return write_list<level>(s, ls);
}
levels read_levels(deserializer & d) {
unsigned num = d.read_unsigned();
buffer<level> ls;
for (unsigned i = 0; i < num; i++)
ls.push_back(read_level(d));
return to_list(ls.begin(), ls.end());
return read_list<level>(d, read_level);
}
serializer & operator<<(serializer & s, level_cnstrs const & cs) {
s << length(cs);
for (auto const & p : cs)
s << p.first << p.second;
serializer & operator<<(serializer & s, level_cnstr const & c) {
s << c.first << c.second;
return s;
}
level_cnstr read_level_cnstr(deserializer & d) {
level lhs = read_level(d);
level rhs = read_level(d);
return level_cnstr(lhs, rhs);
}
serializer & operator<<(serializer & s, level_cnstrs const & cs) {
return write_list<level_cnstr>(s, cs);
}
level_cnstrs read_level_cnstrs(deserializer & d) {
unsigned num = d.read_unsigned();
buffer<level_cnstr> cs;
for (unsigned i = 0; i < num; i++) {
level lhs = read_level(d);
level rhs = read_level(d);
cs.push_back(level_cnstr(lhs, rhs));
return read_list<level_cnstr>(d, read_level_cnstr);
}
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 to_list(cs.begin(), cs.end());
return false;
}
unsigned get_param_range(level_cnstr const & c) {
return std::max(get_param_range(c.first), get_param_range(c.second));
bool has_meta(level_cnstr const & c) {
return has_meta(c.first) || has_meta(c.second);
}
unsigned get_param_range(level_cnstrs const & cs) {
unsigned r = 0;
for (auto const & c : cs)
r = std::max(r, get_param_range(c));
return r;
bool has_meta(level_cnstrs const & cs) {
for (auto const & c : cs) {
if (has_meta(c))
return true;
}
return false;
}
unsigned get_meta_range(level_cnstr const & c) {
return std::max(get_meta_range(c.first), get_meta_range(c.second));
static optional<name> get_undef_param(level const & l, list<name> const & param_names) {
if (!has_meta(l))
return optional<name>();
switch (l.kind()) {
case level_kind::Succ:
return get_undef_param(succ_of(l), param_names);
case level_kind::Max: case level_kind::IMax:
if (auto it = get_undef_param(to_max_core(l).m_lhs, param_names))
return it;
else
return get_undef_param(to_max_core(l).m_rhs, param_names);
case level_kind::Param:
if (std::find(param_names.begin(), param_names.end(), param_id(l)) == param_names.end())
return optional<name>(param_id(l));
else
return optional<name>();
case level_kind::Zero: case level_kind::Meta:
lean_unreachable(); // LCOV_EXCL_LINE
}
lean_unreachable(); // LCOV_EXCL_LINE
}
unsigned get_meta_range(level_cnstrs const & cs) {
unsigned r = 0;
for (auto const & c : cs)
r = std::max(r, get_meta_range(c));
return r;
optional<name> get_undef_param(level_cnstrs const & cs, list<name> const & param_names) {
for (auto const & c : cs) {
if (auto it = get_undef_param(c.first, param_names))
return it;
if (auto it = get_undef_param(c.second, param_names))
return it;
}
return optional<name>();
}
static void print(std::ostream & out, level l);
@ -470,7 +481,7 @@ static void print(std::ostream & out, level l) {
case level_kind::Zero:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param:
out << "l_" << param_id(l); break;
out << param_id(l); break;
case level_kind::Meta:
out << "?" << meta_id(l); break;
case level_kind::Succ:
@ -509,10 +520,6 @@ static format pp_child(level const & l, bool unicode, unsigned 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);
@ -522,17 +529,7 @@ format pp(level l, bool unicode, unsigned indent) {
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))};
}
return format(param_id(l));
case level_kind::Meta:
return format{format("?"), format(meta_id(l))};
case level_kind::Succ:

43
src/kernel/level.h
View file

@ -30,8 +30,8 @@ struct level_cell;
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.
- Param(n) : A parameter. In Lean, we have universe polymorphic definitions.
- 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.
*/
@ -52,6 +52,9 @@ public:
level(level&& s);
~level();
level_kind kind() const;
unsigned hash() const;
level & operator=(level const & l);
level & operator=(level&& l);
@ -68,8 +71,8 @@ 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);
level mk_param_univ(name const & n);
level mk_meta_univ(name const & n);
bool operator==(level const & l1, level const & l2);
inline bool operator!=(level const & l1, level const & l2) { return !operator==(l1, l2); }
@ -79,8 +82,8 @@ inline bool operator!=(level const & l1, level const & l2) { return !operator==(
*/
bool is_lt(level const & l1, level const & l2);
unsigned hash(level const & l);
level_kind kind(level const & l);
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; }
@ -89,16 +92,14 @@ 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);
name const & param_id(level const & l);
name const & meta_id(level const & l);
/**
\brief Return true iff \c l is an explicit level.
We say a level l is explicit iff
@ -107,10 +108,10 @@ unsigned meta_id(level const & l);
*/
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 Return true iff \c l contains placeholder (aka meta parameters). */
bool has_meta(level const & l);
/** \brief Return true iff \c l contains parameters */
bool has_param(level const & l);
/**
\brief Return true if lhs <= rhs is a trivial constraint.
@ -130,10 +131,16 @@ typedef list<level> levels;
typedef std::pair<level, level> level_cnstr;
typedef list<level_cnstr> level_cnstrs;
unsigned get_param_range(level_cnstr const & c);
unsigned get_param_range(level_cnstrs const & cs);
unsigned get_meta_range(level_cnstr const & c);
unsigned get_meta_range(level_cnstrs const & cs);
bool has_param(level_cnstr const & c);
bool has_param(level_cnstrs const & cs);
bool has_meta(level_cnstr const & c);
bool has_meta(level_cnstrs const & cs);
/**
\brief If \c cs contains a parameter that is not in \c param_names, then return it.
Otherwise, return none.
*/
optional<name> get_undef_param(level_cnstrs const & cs, list<name> const & param_names);
/**
\brief Printer for debugging purposes

78
src/kernel/object.cpp
View file

@ -31,24 +31,32 @@ void read_object(environment const & env, io_state const & ios, std::string cons
neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {}
serializer & operator<<(serializer & s, param_names const & ps) {
return write_list<name>(s, ps);
}
param_names read_params(deserializer & d) {
return read_list<name>(d);
}
/**
\brief Parametric kernel objects.
*/
class parametric_object_cell : public object_cell {
name m_name;
unsigned m_num_params;
param_names m_params;
level_cnstrs m_cnstrs;
expr m_type;
public:
parametric_object_cell(object_kind k, name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t):
object_cell(k), m_name(n), m_num_params(num_params), m_cnstrs(cs), m_type(t) {}
parametric_object_cell(object_kind k, name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
object_cell(k), m_name(n), m_params(params), m_cnstrs(cs), m_type(t) {}
virtual ~parametric_object_cell() {}
virtual bool has_name() const { return true; }
virtual name get_name() const { return m_name; }
virtual expr get_type() const { return m_type; }
virtual unsigned get_num_level_params() const { return m_num_params; }
level_cnstrs const & get_level_cnstrs() const { return m_cnstrs; }
virtual param_names const & get_params() const { return m_params; }
virtual level_cnstrs const & get_level_cnstrs() const { return m_cnstrs; }
};
/**
@ -56,8 +64,8 @@ public:
*/
class postulate_object_cell : public parametric_object_cell {
public:
postulate_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t):
parametric_object_cell(object_kind::Postulate, n, num_params, cs, t) {}
postulate_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
parametric_object_cell(object_kind::Postulate, n, params, cs, t) {}
};
/**
@ -65,18 +73,18 @@ public:
*/
class axiom_object_cell : public postulate_object_cell {
public:
axiom_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t):
postulate_object_cell(n, num_params, cs, t) {}
axiom_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
postulate_object_cell(n, params, cs, t) {}
virtual char const * keyword() const { return "axiom"; }
virtual bool is_axiom() const { return true; }
virtual void write(serializer & s) const { s << "ax" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type(); }
virtual void write(serializer & s) const { s << "ax" << get_name() << get_params() << get_level_cnstrs() << get_type(); }
};
static void read_axiom(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d);
unsigned num = d.read_unsigned();
param_names ps = read_params(d);
level_cnstrs cs = read_level_cnstrs(d);
expr t = read_expr(d);
env->add_axiom(n, num, cs, t);
env->add_axiom(n, ps, cs, t);
}
static object_cell::register_deserializer_fn axiom_ds("ax", read_axiom);
@ -86,18 +94,18 @@ static object_cell::register_deserializer_fn axiom_ds("ax", read_axiom);
*/
class variable_decl_object_cell : public postulate_object_cell {
public:
variable_decl_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t):
postulate_object_cell(n, num_params, cs, t) {}
variable_decl_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t):
postulate_object_cell(n, params, cs, t) {}
virtual char const * keyword() const { return "variable"; }
virtual bool is_var_decl() const { return true; }
virtual void write(serializer & s) const { s << "var" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type(); }
virtual void write(serializer & s) const { s << "var" << get_name() << get_params() << get_level_cnstrs() << get_type(); }
};
static void read_variable(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d);
unsigned num = d.read_unsigned();
param_names ps = read_params(d);
level_cnstrs cs = read_level_cnstrs(d);
expr t = read_expr(d);
env->add_var(n, num, cs, t);
env->add_var(n, ps, cs, t);
}
static object_cell::register_deserializer_fn var_decl_ds("var", read_variable);
@ -109,8 +117,8 @@ class definition_object_cell : public parametric_object_cell {
bool m_opaque;
unsigned m_weight;
public:
definition_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight):
parametric_object_cell(object_kind::Definition, n, num_params, cs, t), m_value(v), m_opaque(false), m_weight(weight) {}
definition_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight):
parametric_object_cell(object_kind::Definition, n, params, cs, t), m_value(v), m_opaque(false), m_weight(weight) {}
virtual ~definition_object_cell() {}
virtual bool is_definition() const { return true; }
@ -120,16 +128,16 @@ public:
virtual char const * keyword() const { return "definition"; }
virtual unsigned get_weight() const { return m_weight; }
virtual void write(serializer & s) const {
s << "def" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type() << get_value();
s << "def" << get_name() << get_params() << get_level_cnstrs() << get_type() << get_value();
}
};
static void read_definition(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d);
unsigned num = d.read_unsigned();
param_names ps = read_params(d);
level_cnstrs cs = read_level_cnstrs(d);
expr t = read_expr(d);
expr v = read_expr(d);
env->add_definition(n, num, cs, t, v);
env->add_definition(n, ps, cs, t, v);
}
static object_cell::register_deserializer_fn definition_ds("def", read_definition);
@ -138,36 +146,36 @@ static object_cell::register_deserializer_fn definition_ds("def", read_definitio
*/
class theorem_object_cell : public definition_object_cell {
public:
theorem_object_cell(name const & n, unsigned num_params, level_cnstrs const & cs, expr const & t, expr const & v):
definition_object_cell(n, num_params, cs, t, v, 0) {
theorem_object_cell(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v):
definition_object_cell(n, params, cs, t, v, 0) {
set_opaque(true);
}
virtual char const * keyword() const { return "theorem"; }
virtual bool is_theorem() const { return true; }
virtual void write(serializer & s) const {
s << "th" << get_name() << get_num_level_params() << get_level_cnstrs() << get_type() << get_value();
s << "th" << get_name() << get_params() << get_level_cnstrs() << get_type() << get_value();
}
};
static void read_theorem(environment const & env, io_state const &, deserializer & d) {
name n = read_name(d);
unsigned num = d.read_unsigned();
param_names ps = read_params(d);
level_cnstrs cs = read_level_cnstrs(d);
expr t = read_expr(d);
expr v = read_expr(d);
env->add_theorem(n, num, cs, t, v);
env->add_theorem(n, ps, cs, t, v);
}
static object_cell::register_deserializer_fn theorem_ds("th", read_theorem);
object mk_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight) {
return object(new definition_object_cell(n, num_param, cs, t, v, weight));
object mk_definition(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight) {
return object(new definition_object_cell(n, ps, cs, t, v, weight));
}
object mk_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v) {
return object(new theorem_object_cell(n, num_param, cs, t, v));
object mk_theorem(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t, expr const & v) {
return object(new theorem_object_cell(n, ps, cs, t, v));
}
object mk_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) {
return object(new axiom_object_cell(n, num_param, cs, t));
object mk_axiom(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t) {
return object(new axiom_object_cell(n, ps, cs, t));
}
object mk_var_decl(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t) {
return object(new variable_decl_object_cell(n, num_param, cs, t));
object mk_var_decl(name const & n, param_names const & ps, level_cnstrs const & cs, expr const & t) {
return object(new variable_decl_object_cell(n, ps, cs, t));
}
}

22
src/kernel/object.h
View file

@ -20,6 +20,8 @@ class io_state;
class object;
enum class object_kind { Definition, Postulate, Neutral };
typedef list<name> param_names;
class object_cell {
protected:
friend class object;
@ -45,7 +47,7 @@ public:
/** \brief Return object name. \pre has_name() */
virtual name get_name() const { lean_unreachable(); } // LCOV_EXCL_LINE
/** \brief Return number of level parameters */
virtual unsigned get_num_level_params() const { lean_unreachable(); }
virtual param_names const & get_params() const { lean_unreachable(); }
/** \brief Return the level constraints associated with a definition/postulate. */
virtual level_cnstrs const & get_level_cnstrs() const { lean_unreachable(); }
@ -103,16 +105,16 @@ public:
object_kind kind() const { return m_ptr->kind(); }
friend object mk_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight);
friend object mk_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v);
friend object mk_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t);
friend object mk_var_decl(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t);
friend object mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight);
friend object mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v);
friend object mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
friend object mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
friend object mk_neutral(neutral_object_cell * c);
char const * keyword() const { return m_ptr->keyword(); }
bool has_name() const { return m_ptr->has_name(); }
name get_name() const { return m_ptr->get_name(); }
unsigned get_num_level_params() const { return m_ptr->get_num_level_params(); }
param_names const & get_params() const { return m_ptr->get_params(); }
level_cnstrs const & get_level_cnstrs() const { return m_ptr->get_level_cnstrs(); }
expr get_type() const { return m_ptr->get_type(); }
bool is_definition() const { return m_ptr->is_definition(); }
@ -132,10 +134,10 @@ inline optional<object> none_object() { return optional<object>(); }
inline optional<object> some_object(object const & o) { return optional<object>(o); }
inline optional<object> some_object(object && o) { return optional<object>(std::forward<object>(o)); }
object mk_definition(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight);
object mk_theorem(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t, expr const & v);
object mk_axiom(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t);
object mk_var_decl(name const & n, unsigned num_param, level_cnstrs const & cs, expr const & t);
object mk_definition(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v, unsigned weight);
object mk_theorem(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t, expr const & v);
object mk_axiom(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
object mk_var_decl(name const & n, param_names const & params, level_cnstrs const & cs, expr const & t);
inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); }
void read_object(environment const & env, io_state const & ios, std::string const & k, deserializer & d);

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

@ -31,7 +31,7 @@ static void tst1() {
lean_assert(mk_imax(two, zero) == zero);
check_serializer(two);
check_serializer(one);
level p = mk_param_univ(0);
level p = mk_param_univ("p");
lean_assert(mk_imax(p, zero) == zero);
lean_assert(mk_max(zero, p) == p);
lean_assert(mk_max(p, zero) == p);
@ -40,16 +40,16 @@ static void tst1() {
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";
std::cout << pp(mk_max(p, mk_max(mk_succ(mk_param_univ("a")), one))) << "\n";
}
static void tst2() {
level zero;
level one = mk_succ(zero);
level two = mk_succ(one);
level p1 = mk_param_univ(0);
level p2 = mk_param_univ(1);
level m1 = mk_meta_univ(0);
level p1 = mk_param_univ("p1");
level p2 = mk_param_univ("p2");
level m1 = mk_meta_univ("m1");
lean_assert(is_trivial(zero, mk_succ(mk_max(p1, p2))));
lean_assert(is_trivial(mk_succ(mk_max(p1, p2)), mk_succ(mk_max(p1, p2))));
lean_assert(is_trivial(p1, mk_succ(mk_max(p1, p2))));

24
src/util/serializer.h
View file

@ -10,6 +10,8 @@ Author: Leonardo de Moura
#include <sstream>
#include <cstring>
#include "util/extensible_object.h"
#include "util/list.h"
#include "util/buffer.h"
namespace lean {
/**
@ -65,4 +67,26 @@ inline deserializer & operator>>(deserializer & d, bool & b) { b = d.read_bool()
inline deserializer & operator>>(deserializer & d, double & b) { b = d.read_double(); return d; }
[[ noreturn ]] void throw_corrupted_file();
template<typename T>
serializer & write_list(serializer & s, list<T> const & ls) {
s << length(ls);
for (auto const & e : ls)
s << e;
return s;
}
template<typename T, typename R>
list<T> read_list(deserializer & d, R && t_reader) {
unsigned num = d.read_unsigned();
buffer<T> ls;
for (unsigned i = 0; i < num; i++)
ls.push_back(t_reader(d));
return to_list(ls.begin(), ls.end());
}
template<typename T>
list<T> read_list(deserializer & d) {
return read_list<T>(d, [](deserializer & d) { T r; d >> r; return r; });
}
}