From ecb7316943b4056239f06bc832e31ea04a70c2a8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 21 Jul 2013 15:08:14 -0700 Subject: [PATCH] Fix bugs in hierarchical names module. Add unit tests. Signed-off-by: Leonardo de Moura --- src/tests/util/CMakeLists.txt | 3 +++ src/tests/util/name.cpp | 32 ++++++++++++++++++++++++++++++++ src/util/name.cpp | 12 ++++++------ src/util/name.h | 6 +++--- 4 files changed, 44 insertions(+), 9 deletions(-) create mode 100644 src/tests/util/name.cpp diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 203f770d3b..2d788ecd60 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -1,3 +1,6 @@ add_executable(interrupt interrupt.cpp) target_link_libraries(interrupt ${EXTRA_LIBS}) add_test(interrupt ${CMAKE_CURRENT_BINARY_DIR}/interrupt) +add_executable(name name.cpp) +target_link_libraries(name ${EXTRA_LIBS}) +add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name) diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp new file mode 100644 index 0000000000..fb6c3a2299 --- /dev/null +++ b/src/tests/util/name.cpp @@ -0,0 +1,32 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "name.h" +#include "test.h" +using namespace lean; + +static void tst1() { + name n("foo"); + lean_assert(n == name("foo")); + lean_assert(n != name(1)); + lean_assert(name(n, 1) != name(n, 2)); + lean_assert(name(n, 1) == name(n, 1)); + lean_assert(name(name(n, 1), 2) != name(name(n, 1), 1)); + lean_assert(name(name(n, 1), 1) == name(name(n, 1), 1)); + lean_assert(name(name(n, 2), 1) != name(name(n, 1), 1)); + lean_assert(name(name(n, "bla"), 1) == name(name(n, "bla"), 1)); + lean_assert(name(name(n, "foo"), 1) != name(name(n, "bla"), 1)); + lean_assert(name(name(name("f"), "bla"), 1) != name(name(n, "bla"), 1)); + lean_assert(n != name()); + lean_assert(name().get_kind() == name::kind::ANONYMOUS); + lean_assert(name(name(), "foo") == name("foo")); +} + +int main() { + continue_on_violation(true); + tst1(); + return has_violations() ? 1 : 0; +} diff --git a/src/util/name.cpp b/src/util/name.cpp index 2c51ca8b1b..4f201ca590 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -138,9 +138,9 @@ char const * name::get_string() const { return m_imp->m_str; } -bool name::operator==(name const & other) const { - imp * i1 = m_imp; - imp * i2 = other.m_imp; +bool operator==(name const & a, name const & b) { + name::imp * i1 = a.m_imp; + name::imp * i2 = b.m_imp; while (true) { if (i1 == i2) return true; @@ -150,12 +150,12 @@ bool name::operator==(name const & other) const { lean_assert(i2 != nullptr); if (i1->m_is_string != i2->m_is_string) return false; - if (m_imp->m_is_string) { - if (strcmp(get_string(), other.get_string()) != 0) + if (i1->m_is_string) { + if (strcmp(i1->m_str, i2->m_str) != 0) return false; } else { - if (get_numeral() != other.get_numeral()) + if (i1->m_k != i2->m_k) return false; } i1 = i1->m_prefix; diff --git a/src/util/name.h b/src/util/name.h index 1791b7ae24..e565c16439 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -15,11 +15,11 @@ constexpr char const * default_name_separator = "::"; \brief Hierarchical names. */ class name { - enum class kind { ANONYMOUS, STRING, NUMERAL }; struct imp; imp * m_imp; name(imp * p); public: + enum class kind { ANONYMOUS, STRING, NUMERAL }; name(); explicit name(char const * name); explicit name(unsigned k); @@ -30,8 +30,8 @@ public: ~name(); name & operator=(name const & other); name & operator=(name && other); - bool operator==(name const & other) const; - bool operator!=(name const & other) const { return !operator==(other); } + friend bool operator==(name const & a, name const & b); + friend bool operator!=(name const & a, name const & b) { return !(a == b); } kind get_kind() const; bool is_anonymous() const { return get_kind() == kind::ANONYMOUS; } bool is_string() const { return get_kind() == kind::STRING; }