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

Fix bugs in hierarchical names module. Add unit tests.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-07-21 15:08:14 -07:00
parent ecc8e8f813
commit ecb7316943
4 changed files with 44 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tests/util/CMakeLists.txt
View file

@ -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)

32
src/tests/util/name.cpp Normal file
View file

@ -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;
}

12
src/util/name.cpp
View file

@ -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;

6
src/util/name.h
View file

@ -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; }