diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index beee50f7d..281d6dd55 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -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;
}
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index a0400eb58..b9229514c 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -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); }
};
// =======================================
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index c497c22ff..f191ef3dc 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -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;
}
diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp
index 32ca88cd3..6aee9179b 100644
--- a/src/kernel/max_sharing.cpp
+++ b/src/kernel/max_sharing.cpp
@@ -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;
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 635bd9c03..d7e3cdd96 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -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;
}