feat(tests/shared): add test for the hierarchical name C API

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} $<TARGET_OBJECTS:api>)
+add_library(leanshared SHARED shared/init.cpp $<TARGET_OBJECTS:api> ${LEAN_OBJS})
 target_link_libraries(leanshared ${EXTRA_LIBS})
 
 add_subdirectory(shell)

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 <tt>pre.i</tt> 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)
 */

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

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 <string.h>
+#include "api/lean_string.h"
 #include "api/string.h"
 
 namespace lean {

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

src/tests/shared/name.c

@@ -0,0 +1,44 @@
+#include <stdlib.h>
+#include <stdio.h>
+#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;
+}