test(tests/shared): add some tests for lean_expr C API

src/api/expr.cpp

@@ -338,8 +338,12 @@ lean_bool lean_list_expr_is_cons(lean_list_expr l) {
     return l && !is_nil(to_list_expr_ref(l));
 }
 
-lean_bool lean_list_expr_eq(lean_list_expr l1, lean_list_expr l2) {
-    return l1 && l2 && to_list_expr_ref(l1) == to_list_expr_ref(l2);
+lean_bool lean_list_expr_eq(lean_list_expr l1, lean_list_expr l2, lean_bool * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l1);
+    check_nonnull(l2);
+    *b = to_list_expr_ref(l1) == to_list_expr_ref(l2);
+    LEAN_CATCH;
 }
 
 lean_bool lean_list_expr_head(lean_list_expr l, lean_expr * r, lean_exception * ex) {

src/api/lean_expr.h

@@ -144,8 +144,8 @@ lean_bool lean_list_expr_mk_cons(lean_expr h, lean_list_expr t, lean_list_expr *
 void lean_list_expr_del(lean_list_expr l);
 /** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */
 lean_bool lean_list_expr_is_cons(lean_list_expr l);
-/** \brief Return true iff the two given lists are equal */
-lean_bool lean_list_expr_eq(lean_list_expr n1, lean_list_expr n2);
+/** \brief Return true in \c b iff the two given lists are equal */
+lean_bool lean_list_expr_eq(lean_list_expr n1, lean_list_expr n2, lean_bool * b, lean_exception * ex);
 /** \brief Store in \c r the head of the given list
     \pre lean_list_expr_is_cons(l) */
 lean_bool lean_list_expr_head(lean_list_expr l, lean_expr * r, lean_exception * ex);

src/api/lean_univ.h

@@ -100,8 +100,8 @@ lean_bool lean_list_univ_mk_cons(lean_univ h, lean_list_univ t, lean_list_univ *
 void lean_list_univ_del(lean_list_univ l);
 /** \brief Return true iff the list is a "cons" (i.e., it is not the nil list) */
 lean_bool lean_list_univ_is_cons(lean_list_univ l);
-/** \brief Return true iff the two given lists are equal */
-lean_bool lean_list_univ_eq(lean_list_univ n1, lean_list_univ n2);
+/** \brief Store true in \c b iff the two given lists are equal */
+lean_bool lean_list_univ_eq(lean_list_univ n1, lean_list_univ n2, lean_bool * b, lean_exception * ex);
 /** \brief Store in \c r the head of the given list
     \pre lean_list_univ_is_cons(l) */
 lean_bool lean_list_univ_head(lean_list_univ l, lean_univ * r, lean_exception * ex);

src/api/univ.cpp

@@ -201,8 +201,12 @@ lean_bool lean_list_univ_is_cons(lean_list_univ l) {
     return l && !is_nil(to_list_level_ref(l));
 }
 
-lean_bool lean_list_univ_eq(lean_list_univ l1, lean_list_univ l2) {
-    return l1 && l2 && to_list_level_ref(l1) == to_list_level_ref(l2);
+lean_bool lean_list_univ_eq(lean_list_univ l1, lean_list_univ l2, lean_bool * b, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(l1);
+    check_nonnull(l2);
+    *b = to_list_level_ref(l1) == to_list_level_ref(l2);
+    LEAN_CATCH;
 }
 
 lean_bool lean_list_univ_head(lean_list_univ l, lean_univ * r, lean_exception * ex) {

src/tests/shared/CMakeLists.txt

@@ -21,3 +21,9 @@ target_link_libraries(c_univ_test ${EXTRA_LIBS} leanshared)
 add_test(UNIV c_univ_test
          WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
          COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_univ_test")
+
+add_executable(c_expr_test expr.c)
+target_link_libraries(c_expr_test ${EXTRA_LIBS} leanshared)
+add_test(EXPR c_expr_test
+         WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
+         COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_expr_test")

src/tests/shared/expr.c

@@ -0,0 +1,86 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <stdlib.h>
+#include <stdio.h>
+#include "api/lean.h"
+
+void check_core(int v, unsigned l) {
+    if (!v) {
+        printf("Test failed at line %d\n", l);
+        exit(1);
+    }
+}
+
+#define check(v) check_core(v, __LINE__)
+
+void test_var() {
+    lean_exception ex;
+    lean_expr e1, e2, e3;
+    lean_bool b; unsigned i;
+    check(lean_expr_mk_var(0, &e1, &ex));
+    check(lean_expr_mk_var(1, &e2, &ex));
+    check(lean_expr_mk_var(0, &e3, &ex));
+    check(lean_expr_eq(e1, e3, &b, &ex) && b);
+    check(lean_expr_eq(e1, e2, &b, &ex) && !b);
+    check(lean_expr_get_var_idx(e1, &i, &ex) && i == 0);
+    check(lean_expr_get_var_idx(e2, &i, &ex) && i == 1);
+    check(lean_expr_get_kind(e1) == LEAN_EXPR_VAR);
+    check(lean_expr_get_kind(e2) == LEAN_EXPR_VAR);
+    lean_expr_del(e1);
+    lean_expr_del(e2);
+    lean_expr_del(e3);
+}
+
+void test_const() {
+    lean_exception ex;
+    lean_name n1, n2, n3, n4;
+    lean_univ u1;
+    lean_list_univ l1, l2, l3, l4;
+    lean_expr e1, e2, e3;
+    lean_bool b;
+    char const * s;
+    check(lean_name_mk_anonymous(&n1, &ex));
+    check(lean_name_mk_str(n1, "id", &n2, &ex));
+    check(lean_name_mk_str(n1, "func", &n3, &ex));
+    check(lean_univ_mk_zero(&u1, &ex));
+    check(lean_list_univ_mk_nil(&l1, &ex));
+    check(lean_list_univ_mk_cons(u1, l1, &l2, &ex));
+    check(lean_list_univ_mk_cons(u1, l2, &l3, &ex));
+    check(lean_expr_mk_const(n2, l2, &e1, &ex));
+    check(lean_expr_mk_const(n2, l3, &e2, &ex));
+    check(lean_expr_mk_const(n3, l3, &e3, &ex));
+    check(lean_expr_eq(e1, e1, &b, &ex) && b);
+    check(lean_expr_eq(e1, e2, &b, &ex) && !b);
+    check(lean_expr_get_const_name(e2, &n4, &ex));
+    check(lean_name_eq(n2, n4));
+    check(lean_expr_get_const_univs(e3, &l4, &ex));
+    check(lean_list_univ_eq(l3, l4, &b, &ex) && b);
+    check(lean_expr_get_kind(e1) == LEAN_EXPR_CONST);
+    check(lean_expr_get_kind(e2) == LEAN_EXPR_CONST);
+    check(lean_expr_get_kind(e3) == LEAN_EXPR_CONST);
+    check(lean_expr_to_string(e3, &s, &ex));
+    printf("expr: %s\n", s);
+    lean_name_del(n1);
+    lean_name_del(n2);
+    lean_name_del(n3);
+    lean_name_del(n4);
+    lean_univ_del(u1);
+    lean_list_univ_del(l1);
+    lean_list_univ_del(l2);
+    lean_list_univ_del(l3);
+    lean_list_univ_del(l4);
+    lean_expr_del(e1);
+    lean_expr_del(e2);
+    lean_expr_del(e3);
+    lean_string_del(s);
+}
+
+int main() {
+    test_var();
+    test_const();
+    return 0;
+}