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

Rename eqp --> is_eqp. The name is too similar to heterogeneous equality constructor eq.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-04 09:41:49 -07:00
parent 3f789ce2b7
commit f0ccb2a03e
5 changed files with 19 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/abstract.cpp
View file

@ -31,7 +31,7 @@ expr abstract_p(expr const & e, unsigned n, expr const * s) {
unsigned i = n; unsigned i = n;
while (i > 0) { while (i > 0) {
--i; --i;
if (eqp(s[i], e)) if (is_eqp(s[i], e))
return var(offset + n - i - 1); return var(offset + n - i - 1);
} }
return e; return e;

2
src/kernel/expr.cpp
View file

@ -137,7 +137,7 @@ class eq_fn {
expr_cell_pair_set m_eq_visited; expr_cell_pair_set m_eq_visited;
bool apply(expr const & a, expr const & b) { bool apply(expr const & a, expr const & b) {
if (eqp(a, b)) return true; if (is_eqp(a, b)) return true;
if (a.hash() != b.hash()) return false; if (a.hash() != b.hash()) return false;
if (a.kind() != b.kind()) return false; if (a.kind() != b.kind()) return false;
if (is_var(a)) return var_idx(a) == var_idx(b); if (is_var(a)) return var_idx(a) == var_idx(b);

14
src/kernel/expr.h
View file

@ -104,7 +104,7 @@ public:
friend expr type(level const & l); friend expr type(level const & l);
friend expr let(name const & n, expr const & v, expr const & e); friend expr let(name const & n, expr const & v, expr const & e);
friend bool eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; } friend bool is_eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
// Overloaded operator() can be used to create applications // Overloaded operator() can be used to create applications
expr operator()(expr const & a1) const; expr operator()(expr const & a1) const;
@ -358,7 +358,7 @@ typedef std::pair<expr_cell*, unsigned> expr_cell_offset;
/** \brief Functional object for hashing kernel expressions. */ /** \brief Functional object for hashing kernel expressions. */
struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); } }; struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); } };
/** \brief Functional object for testing pointer equality between kernel expressions. */ /** \brief Functional object for testing pointer equality between kernel expressions. */
struct expr_eqp { bool operator()(expr const & e1, expr const & e2) const { return eqp(e1, e2); } }; struct expr_eqp { bool operator()(expr const & e1, expr const & e2) const { return is_eqp(e1, e2); } };
/** \brief Functional object for hashing kernel expression cells. */ /** \brief Functional object for hashing kernel expression cells. */
struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } }; struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } };
/** \brief Functional object for testing pointer equality between kernel cell expressions. */ /** \brief Functional object for testing pointer equality between kernel cell expressions. */
@ -366,7 +366,7 @@ struct expr_cell_eqp { bool operator()(expr_cell * e1, expr_cell * e2) const { r
/** \brief Functional object for hashing a pair (n,k) where n is a kernel expressions, and k is an offset. */ /** \brief Functional object for hashing a pair (n,k) where n is a kernel expressions, and k is an offset. */
struct expr_offset_hash { unsigned operator()(expr_offset const & p) const { return hash(p.first.hash(), p.second); } }; struct expr_offset_hash { unsigned operator()(expr_offset const & p) const { return hash(p.first.hash(), p.second); } };
/** \brief Functional object for comparing pairs (expression, offset). */ /** \brief Functional object for comparing pairs (expression, offset). */
struct expr_offset_eqp { unsigned operator()(expr_offset const & p1, expr_offset const & p2) const { return eqp(p1.first, p2.first) && p1.second == p2.second; } }; struct expr_offset_eqp { unsigned operator()(expr_offset const & p1, expr_offset const & p2) const { return is_eqp(p1.first, p2.first) && p1.second == p2.second; } };
/** \brief Functional object for hashing a pair (n,k) where n is a kernel cell expressions, and k is an offset. */ /** \brief Functional object for hashing a pair (n,k) where n is a kernel cell expressions, and k is an offset. */
struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) const { return hash(p.first->hash(), p.second); } }; struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) const { return hash(p.first->hash(), p.second); } };
/** \brief Functional object for comparing pairs (expression cell, offset). */ /** \brief Functional object for comparing pairs (expression cell, offset). */
@ -408,7 +408,7 @@ template<typename F> expr update_app(expr const & e, F f) {
bool modified = false; bool modified = false;
for (expr const & a : args(e)) { for (expr const & a : args(e)) {
new_args.push_back(f(a)); new_args.push_back(f(a));
if (!eqp(a, new_args.back())) if (!is_eqp(a, new_args.back()))
modified = true; modified = true;
} }
if (modified) if (modified)
@ -423,7 +423,7 @@ template<typename F> expr update_abst(expr const & e, F f) {
expr const & old_t = abst_domain(e); expr const & old_t = abst_domain(e);
expr const & old_b = abst_body(e); expr const & old_b = abst_body(e);
std::pair<expr, expr> p = f(old_t, old_b); std::pair<expr, expr> p = f(old_t, old_b);
if (!eqp(p.first, old_t) || !eqp(p.second, old_b)) { if (!is_eqp(p.first, old_t) || !is_eqp(p.second, old_b)) {
name const & n = abst_name(e); name const & n = abst_name(e);
return is_pi(e) ? pi(n, p.first, p.second) : lambda(n, p.first, p.second); return is_pi(e) ? pi(n, p.first, p.second) : lambda(n, p.first, p.second);
} }
@ -438,7 +438,7 @@ template<typename F> expr update_let(expr const & e, F f) {
expr const & old_v = let_value(e); expr const & old_v = let_value(e);
expr const & old_b = let_body(e); expr const & old_b = let_body(e);
std::pair<expr, expr> p = f(old_v, old_b); std::pair<expr, expr> p = f(old_v, old_b);
if (!eqp(p.first, old_v) || !eqp(p.second, old_b)) if (!is_eqp(p.first, old_v) || !is_eqp(p.second, old_b))
return let(let_name(e), p.first, p.second); return let(let_name(e), p.first, p.second);
else else
return e; return e;
@ -450,7 +450,7 @@ template<typename F> expr update_eq(expr const & e, F f) {
expr const & old_l = eq_lhs(e); expr const & old_l = eq_lhs(e);
expr const & old_r = eq_rhs(e); expr const & old_r = eq_rhs(e);
std::pair<expr, expr> p = f(old_l, old_r); std::pair<expr, expr> p = f(old_l, old_r);
if (!eqp(p.first, old_l) || !eqp(p.second, old_r)) if (!is_eqp(p.first, old_l) || !is_eqp(p.second, old_r))
return eq(p.first, p.second); return eq(p.first, p.second);
else else
return e; return e;

2
src/kernel/replace.h
View file

@ -37,7 +37,7 @@ class replace_fn {
} }
expr r = m_f(e, offset); expr r = m_f(e, offset);
if (eqp(e, r)) { if (is_eqp(e, r)) {
switch (e.kind()) { switch (e.kind()) {
case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var: case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var:
break; break;

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

@ -25,9 +25,9 @@ void tst1() {
expr ty = type(level()); expr ty = type(level());
std::cout << fa << "\n"; std::cout << fa << "\n";
std::cout << fa(a) << "\n"; std::cout << fa(a) << "\n";
lean_assert(eqp(arg(fa, 0), f)); lean_assert(is_eqp(arg(fa, 0), f));
lean_assert(eqp(arg(fa, 1), a)); lean_assert(is_eqp(arg(fa, 1), a));
lean_assert(!eqp(fa, f(a))); lean_assert(!is_eqp(fa, f(a)));
lean_assert(app(fa, a) == f(a, a)); lean_assert(app(fa, a) == f(a, a));
std::cout << fa(fa, fa) << "\n"; std::cout << fa(fa, fa) << "\n";
std::cout << lambda("x", ty, var(0)) << "\n"; std::cout << lambda("x", ty, var(0)) << "\n";
@ -243,9 +243,9 @@ void tst7() {
expr v = var(0); expr v = var(0);
expr a1 = max_sharing(f(v,v)); expr a1 = max_sharing(f(v,v));
expr a2 = max_sharing(f(v,v)); expr a2 = max_sharing(f(v,v));
lean_assert(!eqp(a1, a2)); lean_assert(!is_eqp(a1, a2));
expr b = max_sharing(f(a1, a2)); expr b = max_sharing(f(a1, a2));
lean_assert(eqp(arg(b, 1), arg(b, 2))); lean_assert(is_eqp(arg(b, 1), arg(b, 2)));
} }
void tst8() { void tst8() {
@ -339,7 +339,7 @@ void tst12() {
expr F = pi("y", t, lambda("x", t, f(f(f(x,a),constant("10")),x))); expr F = pi("y", t, lambda("x", t, f(f(f(x,a),constant("10")),x)));
expr G = deep_copy(F); expr G = deep_copy(F);
lean_assert(F == G); lean_assert(F == G);
lean_assert(!eqp(F, G)); lean_assert(!is_eqp(F, G));
lean_assert(count(F) == count(G)); lean_assert(count(F) == count(G));
} }
@ -348,11 +348,11 @@ void tst13() {
expr v = var(0); expr v = var(0);
expr a1 = max_sharing(f(v,v)); expr a1 = max_sharing(f(v,v));
expr a2 = max_sharing(f(v,v)); expr a2 = max_sharing(f(v,v));
lean_assert(!eqp(a1, a2)); lean_assert(!is_eqp(a1, a2));
lean_assert(a1 == a2); lean_assert(a1 == a2);
max_sharing_fn M; max_sharing_fn M;
lean_assert(eqp(M(f(v,v)), M(f(v,v)))); lean_assert(is_eqp(M(f(v,v)), M(f(v,v))));
lean_assert(eqp(M(a1), M(a2))); lean_assert(is_eqp(M(a1), M(a2)));
} }
void tst14() { void tst14() {