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

Simplify expr accessor names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-23 11:47:36 -07:00
parent 2c3fc09e3c
commit 54a02b4fc7
5 changed files with 87 additions and 88 deletions

70
src/kernel/expr.cpp
View file

@ -43,34 +43,34 @@ expr_app::~expr_app() {
for (unsigned i = 0; i < m_num_args; i++)
(m_args+i)->~expr();
}
expr app(unsigned num_args, expr const * args) {
lean_assert(num_args > 1);
unsigned _num_args;
unsigned _num_args0 = 0;
expr const & arg0 = args[0];
expr app(unsigned n, expr const * as) {
lean_assert(n > 1);
unsigned new_n;
unsigned n0 = 0;
expr const & arg0 = as[0];
// Remark: we represet ((app a b) c) as (app a b c)
if (is_app(arg0)) {
_num_args0 = get_num_args(arg0);
_num_args = num_args + _num_args0 - 1;
n0 = num_args(arg0);
new_n = n + n0 - 1;
}
else {
_num_args = num_args;
new_n = n;
}
char * mem = new char[sizeof(expr_app) + _num_args*sizeof(expr)];
expr r(new (mem) expr_app(_num_args));
char * mem = new char[sizeof(expr_app) + new_n*sizeof(expr)];
expr r(new (mem) expr_app(new_n));
expr * m_args = to_app(r)->m_args;
unsigned i = 0;
unsigned j = 0;
if (_num_args != num_args) {
for (; i < _num_args0; i++)
new (m_args+i) expr(get_arg(arg0, i));
if (new_n != n) {
for (; i < n0; i++)
new (m_args+i) expr(arg(arg0, i));
j++;
}
for (; i < _num_args; ++i, ++j) {
lean_assert(j < num_args);
new (m_args+i) expr(args[j]);
for (; i < new_n; ++i, ++j) {
lean_assert(j < n);
new (m_args+i) expr(as[j]);
}
to_app(r)->m_hash = hash_args(_num_args, m_args);
to_app(r)->m_hash = hash_args(new_n, m_args);
return r;
}
@ -125,7 +125,7 @@ public:
if (eqp(a, b)) return true;
if (a.hash() != b.hash()) return false;
if (a.kind() != b.kind()) return false;
if (is_var(a)) return get_var_idx(a) == get_var_idx(b);
if (is_var(a)) return var_idx(a) == var_idx(b);
if (is_prop(a)) return true;
if (is_shared(a) && is_shared(b)) {
auto p = std::make_pair(a.raw(), b.raw());
@ -135,31 +135,31 @@ public:
}
switch (a.kind()) {
case expr_kind::Var: lean_unreachable(); return true;
case expr_kind::Constant: return get_const_name(a) == get_const_name(b);
case expr_kind::Constant: return const_name(a) == const_name(b);
case expr_kind::App:
if (get_num_args(a) != get_num_args(b))
if (num_args(a) != num_args(b))
return false;
for (unsigned i = 0; i < get_num_args(a); i++)
if (!apply(get_arg(a, i), get_arg(b, i)))
for (unsigned i = 0; i < num_args(a); i++)
if (!apply(arg(a, i), arg(b, i)))
return false;
return true;
case expr_kind::Lambda:
case expr_kind::Pi:
// Lambda and Pi
// Remark: we ignore get_abs_name because we want alpha-equivalence
return apply(get_abs_type(a), get_abs_type(b)) && apply(get_abs_expr(a), get_abs_expr(b));
return apply(abst_type(a), abst_type(b)) && apply(abst_expr(a), abst_expr(b));
case expr_kind::Prop: lean_unreachable(); return true;
case expr_kind::Type:
if (get_ty_num_vars(a) != get_ty_num_vars(b))
if (ty_num_vars(a) != ty_num_vars(b))
return false;
for (unsigned i = 0; i < get_ty_num_vars(a); i++) {
uvar v1 = get_ty_var(a, i);
uvar v2 = get_ty_var(b, i);
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::Numeral: return get_numeral(a) == get_numeral(b);
case expr_kind::Numeral: return num_value(a) == num_value(b);
}
lean_unreachable();
return false;
@ -174,21 +174,21 @@ bool operator==(expr const & a, expr const & b) {
// Low-level pretty printer
std::ostream & operator<<(std::ostream & out, expr const & a) {
switch (a.kind()) {
case expr_kind::Var: out << "#" << get_var_idx(a); break;
case expr_kind::Constant: out << get_const_name(a); break;
case expr_kind::Var: out << "#" << var_idx(a); break;
case expr_kind::Constant: out << const_name(a); break;
case expr_kind::App:
out << "(";
for (unsigned i = 0; i < get_num_args(a); i++) {
for (unsigned i = 0; i < num_args(a); i++) {
if (i > 0) out << " ";
out << get_arg(a, i);
out << arg(a, i);
}
out << ")";
break;
case expr_kind::Lambda: out << "(fun (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")"; break;
case expr_kind::Pi: out << "(pi (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")"; break;
case expr_kind::Lambda: out << "(fun (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_expr(a) << ")"; break;
case expr_kind::Pi: out << "(pi (" << abst_name(a) << " : " << abst_type(a) << ") " << abst_expr(a) << ")"; break;
case expr_kind::Prop: out << "Prop"; break;
case expr_kind::Type: out << "Type"; break;
case expr_kind::Numeral: out << get_numeral(a); break;
case expr_kind::Numeral: out << num_value(a); break;
}
return out;
}

64
src/kernel/expr.h
View file

@ -279,35 +279,35 @@ inline expr_numeral * to_numeral(expr const & e) { return to_numeral(e.r
// =======================================
// Accessors
inline unsigned get_rc(expr_cell * e) { return e->get_rc(); }
inline bool is_shared(expr_cell * e) { return get_rc(e) > 1; }
inline unsigned get_var_idx(expr_cell * e) { return to_var(e)->get_vidx(); }
inline name const & get_const_name(expr_cell * e) { return to_constant(e)->get_name(); }
inline unsigned get_const_pos(expr_cell * e) { return to_constant(e)->get_pos(); }
inline unsigned get_num_args(expr_cell * e) { return to_app(e)->get_num_args(); }
inline expr const & get_arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline name const & get_abs_name(expr_cell * e) { return to_abstraction(e)->get_name(); }
inline expr const & get_abs_type(expr_cell * e) { return to_abstraction(e)->get_type(); }
inline expr const & get_abs_expr(expr_cell * e) { return to_abstraction(e)->get_expr(); }
inline unsigned get_ty_num_vars(expr_cell * e) { return to_type(e)->size(); }
inline uvar const & get_ty_var(expr_cell * e, unsigned idx) { return to_type(e)->get_var(idx); }
inline mpz const & get_numeral(expr_cell * e) { return to_numeral(e)->get_num(); }
inline unsigned get_rc(expr_cell * e) { return e->get_rc(); }
inline bool is_shared(expr_cell * e) { return get_rc(e) > 1; }
inline unsigned var_idx(expr_cell * e) { return to_var(e)->get_vidx(); }
inline name const & const_name(expr_cell * e) { return to_constant(e)->get_name(); }
inline unsigned const_pos(expr_cell * e) { return to_constant(e)->get_pos(); }
inline unsigned num_args(expr_cell * e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr_cell * e, unsigned idx) { return to_app(e)->get_arg(idx); }
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_expr(expr_cell * e) { return to_abstraction(e)->get_expr(); }
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 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(); }
inline bool is_shared(expr const & e) { return get_rc(e) > 1; }
inline unsigned get_var_idx(expr const & e) { return to_var(e)->get_vidx(); }
inline name const & get_const_name(expr const & e) { return to_constant(e)->get_name(); }
inline unsigned get_const_pos(expr const & e) { return to_constant(e)->get_pos(); }
inline unsigned get_num_args(expr const & e) { return to_app(e)->get_num_args(); }
inline expr const & get_arg(expr const & e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline expr const * begin_args(expr const & e) { return to_app(e)->begin_args(); }
inline expr const * end_args(expr const & e) { return to_app(e)->end_args(); }
inline name const & get_abs_name(expr const & e) { return to_abstraction(e)->get_name(); }
inline expr const & get_abs_type(expr const & e) { return to_abstraction(e)->get_type(); }
inline expr const & get_abs_expr(expr const & e) { return to_abstraction(e)->get_expr(); }
inline unsigned get_ty_num_vars(expr const & e) { return to_type(e)->size(); }
inline uvar const & get_ty_var(expr const & e, unsigned idx) { return to_type(e)->get_var(idx); }
inline mpz const & get_numeral(expr const & e) { return to_numeral(e)->get_num(); }
inline unsigned get_rc(expr const & e) { return e.raw()->get_rc(); }
inline bool is_shared(expr const & e) { return get_rc(e) > 1; }
inline unsigned var_idx(expr const & e) { return to_var(e)->get_vidx(); }
inline name const & const_name(expr const & e) { return to_constant(e)->get_name(); }
inline unsigned const_pos(expr const & e) { return to_constant(e)->get_pos(); }
inline unsigned num_args(expr const & e) { return to_app(e)->get_num_args(); }
inline expr const & arg(expr const & e, unsigned idx) { return to_app(e)->get_arg(idx); }
inline expr const * begin_args(expr const & e) { return to_app(e)->begin_args(); }
inline expr const * end_args(expr const & e) { return to_app(e)->end_args(); }
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_expr(expr const & e) { return to_abstraction(e)->get_expr(); }
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 mpz const & num_value(expr const & e) { return to_numeral(e)->get_num(); }
// =======================================
// =======================================
@ -344,11 +344,11 @@ std::ostream & operator<<(std::ostream & out, expr const & a);
... do something with argument
}
*/
struct app_args {
struct args {
expr const & m_app;
app_args(expr const & a):m_app(a) { lean_assert(is_app(a)); }
expr const * begin() const { return &get_arg(m_app, 0); }
expr const * end() const { return begin() + get_num_args(m_app); }
args(expr const & a):m_app(a) { lean_assert(is_app(a)); }
expr const * begin() const { return &arg(m_app, 0); }
expr const * end() const { return begin() + num_args(m_app); }
};
// =======================================

4
src/kernel/free_vars.cpp
View file

@ -19,7 +19,7 @@ public:
case expr_kind::Constant: case expr_kind::Prop: case expr_kind::Type: case expr_kind::Numeral:
return false;
case expr_kind::Var:
return get_var_idx(e) >= offset;
return var_idx(e) >= offset;
case expr_kind::App: case expr_kind::Lambda: case expr_kind::Pi:
break;
}
@ -45,7 +45,7 @@ public:
break;
case expr_kind::Lambda:
case expr_kind::Pi:
result = apply(get_abs_type(e), offset) || apply(get_abs_expr(e), offset + 1);
result = apply(abst_type(e), offset) || apply(abst_expr(e), offset + 1);
break;
}

8
src/kernel/max_sharing.cpp
View file

@ -40,7 +40,7 @@ public:
case expr_kind::App: {
std::vector<expr> new_args;
bool modified = false;
for (expr const & old_arg : app_args(a)) {
for (expr const & old_arg : args(a)) {
new_args.push_back(apply(old_arg));
if (!eqp(old_arg, new_args.back()))
modified = true;
@ -57,12 +57,12 @@ public:
}
case expr_kind::Lambda:
case expr_kind::Pi: {
expr const & old_t = get_abs_type(a);
expr const & old_e = get_abs_expr(a);
expr const & old_t = abst_type(a);
expr const & old_e = abst_expr(a);
expr t = apply(old_t);
expr e = apply(old_e);
if (!eqp(t, old_t) || !eqp(e, old_e)) {
name const & n = get_abs_name(a);
name const & n = abst_name(a);
expr r = is_pi(a) ? pi(n, t, e) : lambda(n, t, e);
cache(r);
return r;

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

@ -20,8 +20,8 @@ void tst1() {
expr fa = app(f, a);
std::cout << fa << "\n";
std::cout << app(fa, a) << "\n";
lean_assert(eqp(get_arg(fa, 0), f));
lean_assert(eqp(get_arg(fa, 1), a));
lean_assert(eqp(arg(fa, 0), f));
lean_assert(eqp(arg(fa, 1), a));
lean_assert(!eqp(fa, app(f, a)));
lean_assert(app(fa, a) == app(f, a, a));
std::cout << app(fa, fa, fa) << "\n";
@ -46,12 +46,12 @@ unsigned depth1(expr const & e) {
return 1;
case expr_kind::App: {
unsigned m = 0;
for (expr const & a : app_args(e))
for (expr const & a : args(e))
m = std::max(m, depth1(a));
return m + 1;
}
case expr_kind::Lambda: case expr_kind::Pi:
return std::max(depth1(get_abs_type(e)), depth1(get_abs_expr(e))) + 1;
return std::max(depth1(abst_type(e)), depth1(abst_expr(e))) + 1;
}
return 0;
}
@ -67,7 +67,7 @@ unsigned depth2(expr const & e) {
[](unsigned m, expr const & arg){ return std::max(depth2(arg), m); })
+ 1;
case expr_kind::Lambda: case expr_kind::Pi:
return std::max(depth2(get_abs_type(e)), depth2(get_abs_expr(e))) + 1;
return std::max(depth2(abst_type(e)), depth2(abst_expr(e))) + 1;
}
return 0;
}
@ -87,14 +87,14 @@ unsigned depth3(expr const & e) {
m = std::max(c, m);
break;
case expr_kind::App: {
unsigned num = get_num_args(e);
unsigned num = num_args(e);
for (unsigned i = 0; i < num; i++)
todo.push_back(std::make_pair(&get_arg(e, i), c));
todo.push_back(std::make_pair(&arg(e, i), c));
break;
}
case expr_kind::Lambda: case expr_kind::Pi:
todo.push_back(std::make_pair(&get_abs_type(e), c));
todo.push_back(std::make_pair(&get_abs_expr(e), c));
todo.push_back(std::make_pair(&abst_type(e), c));
todo.push_back(std::make_pair(&abst_expr(e), c));
break;
}
}
@ -150,7 +150,7 @@ unsigned count_core(expr const & a, expr_set & s) {
return std::accumulate(begin_args(a), end_args(a), 1,
[&](unsigned sum, expr const & arg){ return sum + count_core(arg, s); });
case expr_kind::Lambda: case expr_kind::Pi:
return count_core(get_abs_type(a), s) + count_core(get_abs_expr(a), s) + 1;
return count_core(abst_type(a), s) + count_core(abst_expr(a), s) + 1;
}
return 0;
}
@ -195,7 +195,7 @@ void tst7() {
expr a2 = max_sharing(app(f, v, v));
lean_assert(!eqp(a1, a2));
expr b = max_sharing(app(f, a1, a2));
lean_assert(eqp(get_arg(b, 1), get_arg(b, 2)));
lean_assert(eqp(arg(b, 1), arg(b, 2)));
}
void tst8() {
@ -249,10 +249,6 @@ int main() {
continue_on_violation(true);
std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
tst8();
tst9();
tst10();
return 0;
tst1();
tst2();
tst3();
@ -260,6 +256,9 @@ int main() {
tst5();
tst6();
tst7();
tst8();
tst9();
tst10();
std::cout << "done" << "\n";
return has_violations() ? 1 : 0;
}