From 9d486a4e88537e29bc677d1309dd2e5d28753180 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 Aug 2015 17:43:02 -0700 Subject: [PATCH] feat(tests/shared): add test for the hierarchical name C API --- src/CMakeLists.txt | 4 +-- src/api/lean_name.h | 2 ++ src/api/name.cpp | 4 +++ src/api/string.cpp | 1 + src/tests/shared/CMakeLists.txt | 6 +++++ src/tests/shared/name.c | 44 +++++++++++++++++++++++++++++++++ 6 files changed, 59 insertions(+), 2 deletions(-) create mode 100644 src/tests/shared/name.c diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9268fe249b..d12b47d4d6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,5 +1,5 @@ cmake_minimum_required(VERSION 2.8.7) -project(LEAN CXX) +project(LEAN CXX C) set(LEAN_VERSION_MAJOR 0) set(LEAN_VERSION_MINOR 2) set(LEAN_VERSION_PATCH 0) @@ -364,7 +364,7 @@ if (${CMAKE_SYSTEM_NAME} MATCHES "Windows") set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all") endif() add_subdirectory(api) -add_library(leanshared SHARED shared/init.cpp ${LEAN_OBJS} $) +add_library(leanshared SHARED shared/init.cpp $ ${LEAN_OBJS}) target_link_libraries(leanshared ${EXTRA_LIBS}) add_subdirectory(shell) diff --git a/src/api/lean_name.h b/src/api/lean_name.h index aac1b2050e..13c9dc4a83 100644 --- a/src/api/lean_name.h +++ b/src/api/lean_name.h @@ -29,6 +29,8 @@ lean_bool lean_is_anonymous_name(lean_name n); lean_bool lean_is_str_name(lean_name n); /** \brief Return lean_true iff \c n is a name of the form pre.i where \c i is an unsigned integer. */ lean_bool lean_is_idx_name(lean_name n); +/** \brief Return true iff the two given hierarchical names are equal */ +lean_bool lean_name_eq(lean_name n1, lean_name n2); /** \brief Return the prefix of the given name. \pre !lean_is_anonymous_name(n) */ diff --git a/src/api/name.cpp b/src/api/name.cpp index 4dd3ea0528..75c661088a 100644 --- a/src/api/name.cpp +++ b/src/api/name.cpp @@ -49,6 +49,10 @@ lean_bool lean_is_idx_name(lean_name n) { return n && to_name_ref(n).is_numeral(); } +lean_bool lean_name_eq(lean_name n1, lean_name n2) { + return n1 && n2 && to_name_ref(n1) == to_name_ref(n2); +} + lean_bool lean_get_name_prefix(lean_name n, lean_name * r, lean_exception * ex) { LEAN_TRY; check_nonnull(n); diff --git a/src/api/string.cpp b/src/api/string.cpp index ce7293ba3f..7ab4209468 100644 --- a/src/api/string.cpp +++ b/src/api/string.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "api/lean_string.h" #include "api/string.h" namespace lean { diff --git a/src/tests/shared/CMakeLists.txt b/src/tests/shared/CMakeLists.txt index b0d9bf4ec2..86462a61e8 100644 --- a/src/tests/shared/CMakeLists.txt +++ b/src/tests/shared/CMakeLists.txt @@ -3,3 +3,9 @@ target_link_libraries(shared_test ${EXTRA_LIBS} leanshared) add_test(NAME shared_test WORKING_DIRECTORY "${LEAN_BINARY_DIR}" COMMAND "${CMAKE_CURRENT_BINARY_DIR}/shared_test") + +add_executable(c_name_test name.c) +target_link_libraries(c_name_test ${EXTRA_LIBS} leanshared) +add_test(NAME c_name_test + WORKING_DIRECTORY "${LEAN_BINARY_DIR}" + COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_name_test") diff --git a/src/tests/shared/name.c b/src/tests/shared/name.c new file mode 100644 index 0000000000..a184874c36 --- /dev/null +++ b/src/tests/shared/name.c @@ -0,0 +1,44 @@ +#include +#include +#include "api/lean.h" + +void check(int v) { + if (!v) { + printf("test failed\n"); + exit(1); + } +} + +int main() { + printf("Started name test\n"); + lean_exception ex; + lean_name a, n1, n2, n3, n4; + char const * s1; + char const * s2; + unsigned idx; + check(lean_mk_anonymous_name(&a, &ex)); + check(lean_is_anonymous_name(a)); + check(lean_mk_str_name(a, "foo", &n1, &ex)); + check(lean_mk_str_name(n1, "bla", &n2, &ex)); + check(lean_name_to_string(n2, &s1, &ex)); + printf("Lean name: %s\n", s1); + check(lean_is_str_name(n2)); + check(!lean_is_anonymous_name(n2)); + check(!lean_is_idx_name(n2)); + check(lean_mk_idx_name(n2, 1, &n3, &ex)); + check(lean_name_to_string(n3, &s2, &ex)); + printf("Lean name: %s\n", s2); + check(lean_is_idx_name(n3)); + check(lean_get_name_prefix(n3, &n4, &ex)); + check(lean_name_eq(n2, n4)); + check(lean_get_name_idx(n3, &idx, &ex)); + check(idx == 1); + lean_del_name(a); + lean_del_name(n1); + lean_del_name(n2); + lean_del_name(n3); + lean_del_name(n4); + lean_del_string(s1); + lean_del_string(s2); + return 0; +}