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

Use level at kernel expressions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-29 19:44:26 -07:00
parent 537e2c101c
commit 6452c69b96
7 changed files with 78 additions and 93 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/kernel/environment.cpp
View file

@ -14,10 +14,12 @@ Author: Leonardo de Moura
namespace lean {
constexpr unsigned uninit = std::numeric_limits<int>::max();
/** \brief Implementation of the Lean environment. */
struct environment::imp {
std::vector<std::vector<unsigned>> m_uvar_distances;
std::vector<level> m_uvars;
/** \brief Return v - k. It throws an exception if there is a underflow. */
static int sub(int v, unsigned k) {
long long r = static_cast<long long>(v) - static_cast<long long>(k);
if (r < std::numeric_limits<int>::min())
@ -25,6 +27,7 @@ struct environment::imp {
return static_cast<int>(r);
}
/** \brief Return v + k. It throws an exception if there is an overflow. */
static int add(int v, unsigned k) {
long long r = static_cast<long long>(v) + static_cast<long long>(k);
if (r > std::numeric_limits<int>::max() - 1)
@ -32,6 +35,7 @@ struct environment::imp {
return static_cast<int>(r);
}
/** \brief Return v + k. It throws an exception if there is an overflow. */
static unsigned add(unsigned v, unsigned k) {
unsigned long long r = static_cast<unsigned long long>(v) + static_cast<unsigned long long>(k);
if (r > std::numeric_limits<int>::max() - 1)

1
src/kernel/environment.h
View file

@ -38,6 +38,7 @@ public:
*/
bool is_ge(level const & l1, level const & l2) const;
/** \brief Display universal variables, and their constraints */
void display_uvars(std::ostream & out) const;
};
}

37
src/kernel/expr.cpp
View file

@ -15,10 +15,6 @@ unsigned hash_args(unsigned size, expr const * args) {
return hash(size, [&args](unsigned i){ return args[i].hash(); });
}
unsigned hash_vars(unsigned size, uvar const * vars) {
return hash(size, [&vars](unsigned i){ return vars[i].second.hash(); });
}
expr_cell::expr_cell(expr_kind k, unsigned h):
m_kind(static_cast<unsigned>(k)),
m_flags(0),
@ -84,21 +80,12 @@ expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):
expr_pi::expr_pi(name const & n, expr const & t, expr const & e):
expr_abstraction(expr_kind::Pi, n, t, e) {}
expr_type::expr_type(unsigned size, uvar const * vars):
expr_cell(expr_kind::Type, hash_vars(size, vars)),
m_size(size) {
for (unsigned i = 0; i < m_size; i++)
new (m_vars + i) uvar(vars[i]);
expr_type::expr_type(level const & l):
expr_cell(expr_kind::Type, l.hash()),
m_level(l) {
}
expr_type::~expr_type() {
for (unsigned i = 0; i < m_size; i++)
(m_vars+i)->~uvar();
}
expr type(unsigned size, uvar const * vars) {
char * mem = new char[sizeof(expr_type) + size*sizeof(uvar)];
return expr(new (mem) expr_type(size, vars));
}
expr_numeral::expr_numeral(mpz const & n):
expr_cell(expr_kind::Numeral, n.hash()),
m_numeral(n) {}
@ -111,12 +98,11 @@ void expr_cell::dealloc() {
case expr_kind::Lambda: delete static_cast<expr_lambda*>(this); break;
case expr_kind::Pi: delete static_cast<expr_pi*>(this); break;
case expr_kind::Prop: delete static_cast<expr_prop*>(this); break;
case expr_kind::Type: static_cast<expr_type*>(this)->~expr_type(); delete[] reinterpret_cast<char*>(this); break;
case expr_kind::Type: delete static_cast<expr_type*>(this); break;
case expr_kind::Numeral: delete static_cast<expr_numeral*>(this); break;
}
}
class eq_fn {
expr_cell_pair_set m_eq_visited;
@ -148,16 +134,7 @@ class eq_fn {
// Remark: we ignore get_abs_name because we want alpha-equivalence
return apply(abst_type(a), abst_type(b)) && apply(abst_body(a), abst_body(b));
case expr_kind::Prop: lean_unreachable(); return true;
case expr_kind::Type:
if (ty_num_vars(a) != ty_num_vars(b))
return false;
for (unsigned i = 0; i < ty_num_vars(a); i++) {
uvar v1 = ty_var(a, i);
uvar v2 = ty_var(b, i);
if (v1.first != v2.first || v1.second != v2.second)
return false;
}
return true;
case expr_kind::Type: return ty_level(a) == ty_level(b);
case expr_kind::Numeral: return num_value(a) == num_value(b);
}
lean_unreachable();
@ -189,7 +166,7 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Pi: out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_body(a) << ")"; break;
case expr_kind::Prop: out << "Prop"; break;
case expr_kind::Type: out << "Type"; break;
case expr_kind::Type: out << "(Type " << ty_level(a) << ")"; break;
case expr_kind::Numeral: out << num_value(a); break;
}
return out;
@ -200,7 +177,7 @@ expr copy(expr const & a) {
case expr_kind::Var: return var(var_idx(a));
case expr_kind::Constant: return constant(const_name(a), const_pos(a));
case expr_kind::Prop: return prop();
case expr_kind::Type: return type(ty_num_vars(a), begin_ty_vars(a));
case expr_kind::Type: return type(ty_level(a));
case expr_kind::Numeral: return numeral(num_value(a));
case expr_kind::App: return app(num_args(a), begin_args(a));
case expr_kind::Lambda: return lambda(abst_name(a), abst_type(a), abst_body(a));

40
src/kernel/expr.h
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "rc.h"
#include "name.h"
#include "mpz.h"
#include "level.h"
#include "hash.h"
namespace lean {
@ -62,21 +63,6 @@ public:
unsigned hash() const { return m_hash; }
};
/**
\brief Instead of fixed universes, we use universe variables with
explicit user-declared constraints between universe variables.
Each universe variable is associated with a name.
If the Boolean in the following pair is true, then we are taking
the successor of the universe variable.
For additional information, see:
Explicit universes for the calculus of constructions, Courant J (2002).
*/
typedef std::pair<bool, name> universe_variable;
typedef universe_variable uvar;
/**
\brief Exprs for encoding formulas/expressions, types and proofs.
*/
@ -121,8 +107,7 @@ public:
friend expr lambda(name const & n, expr const & t, expr const & e);
friend expr pi(name const & n, expr const & t, expr const & e);
friend expr prop();
friend expr type(unsigned size, uvar const * vars);
friend expr type(std::initializer_list<uvar> const & l);
friend expr type(level const & l);
friend expr numeral(mpz const & n);
friend bool eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
@ -193,14 +178,11 @@ public:
};
/** \brief Type */
class expr_type : public expr_cell {
unsigned m_size;
uvar m_vars[0];
level m_level;
public:
expr_type(unsigned size, uvar const * vars);
expr_type(level const & l);
~expr_type();
unsigned size() const { return m_size; }
uvar const & get_var(unsigned idx) const { lean_assert(idx < m_size); return m_vars[idx]; }
uvar const * get_vars() const { return m_vars; }
level const & get_level() const { return m_level; }
};
/** \brief Numerals (efficient encoding using GMP numbers) */
class expr_numeral : public expr_cell {
@ -253,9 +235,7 @@ inline expr lambda(char const * n, expr const & t, expr const & e) { return lamb
inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
inline expr pi(char const * n, expr const & t, expr const & e) { return pi(name(n), t, e); }
inline expr prop() { return expr(new expr_prop()); }
expr type(unsigned size, uvar const * vars);
inline expr type(uvar const & uv) { return type(1, &uv); }
inline expr type(std::initializer_list<uvar> const & l) { return type(l.size(), l.begin()); }
inline expr type(level const & l) { return expr(new expr_type(l)); }
inline expr numeral(mpz const & n) { return expr(new expr_numeral(n)); }
inline expr numeral(int n) { return numeral(mpz(n)); }
@ -301,8 +281,7 @@ inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_
inline name const & abst_name(expr_cell * e) { return to_abstraction(e)->get_name(); }
inline expr const & abst_type(expr_cell * e) { return to_abstraction(e)->get_type(); }
inline expr const & abst_body(expr_cell * e) { return to_abstraction(e)->get_body(); }
inline unsigned ty_num_vars(expr_cell * e) { return to_type(e)->size(); }
inline uvar const & ty_var(expr_cell * e, unsigned idx) { return to_type(e)->get_var(idx); }
inline level const & ty_level(expr_cell * e) { return to_type(e)->get_level(); }
inline mpz const & num_value(expr_cell * e) { return to_numeral(e)->get_num(); }
inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); }
@ -318,10 +297,7 @@ inline expr const * end_args(expr const & e) { return to_app(e)->end
inline name const & abst_name(expr const & e) { return to_abstraction(e)->get_name(); }
inline expr const & abst_type(expr const & e) { return to_abstraction(e)->get_type(); }
inline expr const & abst_body(expr const & e) { return to_abstraction(e)->get_body(); }
inline unsigned ty_num_vars(expr const & e) { return to_type(e)->size(); }
inline uvar const & ty_var(expr const & e, unsigned idx) { return to_type(e)->get_var(idx); }
inline uvar const * begin_ty_vars(expr const & e) { return to_type(e)->get_vars(); }
inline uvar const * end_ty_vars(expr const & e) { return begin_ty_vars(e) + ty_num_vars(e); }
inline level const & ty_level(expr const & e) { return to_type(e)->get_level(); }
inline mpz const & num_value(expr const & e) { return to_numeral(e)->get_num(); }
// =======================================

22
src/kernel/level.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "level.h"
#include "rc.h"
#include "debug.h"
#include "hash.h"
namespace lean {
struct level_cell {
@ -30,11 +31,14 @@ struct level_max : public level_cell {
level m_l2;
level_max(level const & l1, level const & l2):level_cell(level_kind::Max), m_l1(l1), m_l2(l2) {}
};
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 static_cast<level_uvar*>(this); break;
case level_kind::Lift: delete static_cast<level_lift*>(this); break;
case level_kind::Max: delete static_cast<level_max*> (this); break;
case level_kind::UVar: delete to_uvar(this); break;
case level_kind::Lift: delete to_lift(this); break;
case level_kind::Max: delete to_max(this); break;
}
}
level::level(): m_ptr(new level_uvar(name("bot"), 0)) { lean_assert(uvar_name(*this) == name("bot")); }
@ -54,6 +58,14 @@ level::~level() {
if (m_ptr)
m_ptr->dec_ref();
}
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_l1.hash(), to_max(m_ptr)->m_l2.hash());
}
return 0;
}
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; }
@ -80,8 +92,8 @@ bool operator==(level const & l1, level const & l2) {
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: out << lift_of(l) << " + " << lift_offset(l); return out;
case level_kind::Max: out << "max(" << max_level1(l) << ", " << max_level2(l) << ")"; return out;
case level_kind::Lift: out << lift_of(l) << "+" << lift_offset(l); return out;
case level_kind::Max: out << "(max " << max_level1(l) << " " << max_level2(l) << ")"; return out;
}
return out;
}

6
src/kernel/level.h
View file

@ -19,15 +19,21 @@ enum class level_kind { UVar, Lift, Max };
class level {
friend class environment;
level_cell * m_ptr;
/** \brief Private constructor used by the environment to create a new universe variable named \c n with internal id \c u. */
level(name const & n, uvar u);
public:
/** \brief Universe 0 */
level();
/** \brief Lift universe l by k (l + k) */
level(level const & l, unsigned k);
/** \brief New level that is >= max(l1,l2) */
level(level const & l1, level const & l2);
level(level const & l);
level(level&& s);
~level();
unsigned hash() const;
friend level_kind kind (level const & l);
friend name const & uvar_name (level const & l);
friend uvar uvar_idx (level const & l);

9
src/tests/kernel/expr.cpp
View file

@ -304,6 +304,14 @@ void tst13() {
lean_assert(eqp(M(a1), M(a2)));
}
void tst14() {
expr t0 = type(level());
expr t1 = type(level()+1);
lean_assert(ty_level(t1) == level()+1);
lean_assert(t0 != t1);
std::cout << t0 << " " << t1 << "\n";
}
int main() {
continue_on_violation(true);
std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
@ -322,6 +330,7 @@ int main() {
tst11();
tst12();
tst13();
tst14();
std::cout << "done" << "\n";
return has_violations() ? 1 : 0;
}