From f0ccb2a03e579552f44d53b5e991060a19faeaa9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 4 Aug 2013 09:41:49 -0700 Subject: [PATCH] Rename eqp --> is_eqp. The name is too similar to heterogeneous equality constructor eq. Signed-off-by: Leonardo de Moura --- src/kernel/abstract.cpp | 2 +- src/kernel/expr.cpp | 2 +- src/kernel/expr.h | 14 +++++++------- src/kernel/replace.h | 2 +- src/tests/kernel/expr.cpp | 18 +++++++++--------- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index 5a309eac74..53b040696a 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -31,7 +31,7 @@ expr abstract_p(expr const & e, unsigned n, expr const * s) { unsigned i = n; while (i > 0) { --i; - if (eqp(s[i], e)) + if (is_eqp(s[i], e)) return var(offset + n - i - 1); } return e; diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 7e2060dbc3..56baf239d1 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -137,7 +137,7 @@ class eq_fn { expr_cell_pair_set m_eq_visited; 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.kind() != b.kind()) return false; if (is_var(a)) return var_idx(a) == var_idx(b); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 654dd5a272..e5a7a38205 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -104,7 +104,7 @@ public: friend expr type(level const & l); 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 expr operator()(expr const & a1) const; @@ -358,7 +358,7 @@ typedef std::pair expr_cell_offset; /** \brief Functional object for hashing kernel expressions. */ struct expr_hash { unsigned operator()(expr const & e) const { return e.hash(); } }; /** \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. */ struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } }; /** \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. */ 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). */ -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. */ 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). */ @@ -408,7 +408,7 @@ template expr update_app(expr const & e, F f) { bool modified = false; for (expr const & a : args(e)) { new_args.push_back(f(a)); - if (!eqp(a, new_args.back())) + if (!is_eqp(a, new_args.back())) modified = true; } if (modified) @@ -423,7 +423,7 @@ template expr update_abst(expr const & e, F f) { expr const & old_t = abst_domain(e); expr const & old_b = abst_body(e); std::pair 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); return is_pi(e) ? pi(n, p.first, p.second) : lambda(n, p.first, p.second); } @@ -438,7 +438,7 @@ template expr update_let(expr const & e, F f) { expr const & old_v = let_value(e); expr const & old_b = let_body(e); std::pair 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); else return e; @@ -450,7 +450,7 @@ template expr update_eq(expr const & e, F f) { expr const & old_l = eq_lhs(e); expr const & old_r = eq_rhs(e); std::pair 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); else return e; diff --git a/src/kernel/replace.h b/src/kernel/replace.h index e05cd8e7a8..951d6e045d 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -37,7 +37,7 @@ class replace_fn { } expr r = m_f(e, offset); - if (eqp(e, r)) { + if (is_eqp(e, r)) { switch (e.kind()) { case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var: break; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index b872b5a44b..bf2e251350 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -25,9 +25,9 @@ void tst1() { expr ty = type(level()); std::cout << fa << "\n"; std::cout << fa(a) << "\n"; - lean_assert(eqp(arg(fa, 0), f)); - lean_assert(eqp(arg(fa, 1), a)); - lean_assert(!eqp(fa, f(a))); + lean_assert(is_eqp(arg(fa, 0), f)); + lean_assert(is_eqp(arg(fa, 1), a)); + lean_assert(!is_eqp(fa, f(a))); lean_assert(app(fa, a) == f(a, a)); std::cout << fa(fa, fa) << "\n"; std::cout << lambda("x", ty, var(0)) << "\n"; @@ -243,9 +243,9 @@ void tst7() { expr v = var(0); expr a1 = 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)); - lean_assert(eqp(arg(b, 1), arg(b, 2))); + lean_assert(is_eqp(arg(b, 1), arg(b, 2))); } 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 G = deep_copy(F); lean_assert(F == G); - lean_assert(!eqp(F, G)); + lean_assert(!is_eqp(F, G)); lean_assert(count(F) == count(G)); } @@ -348,11 +348,11 @@ void tst13() { expr v = var(0); expr a1 = 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); max_sharing_fn M; - lean_assert(eqp(M(f(v,v)), M(f(v,v)))); - lean_assert(eqp(M(a1), M(a2))); + lean_assert(is_eqp(M(f(v,v)), M(f(v,v)))); + lean_assert(is_eqp(M(a1), M(a2))); } void tst14() {