From 858971c3a5cd20d9d06498077fbd717ecee38f34 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Aug 2015 15:32:27 -0700
Subject: [PATCH] test(tests/shared): add test for the universe C API

---
 src/tests/shared/CMakeLists.txt |  6 +++
 src/tests/shared/univ.c         | 90 +++++++++++++++++++++++++++++++++
 2 files changed, 96 insertions(+)
 create mode 100644 src/tests/shared/univ.c

diff --git a/src/tests/shared/CMakeLists.txt b/src/tests/shared/CMakeLists.txt
index 19301c43c..8feb1227c 100644
--- a/src/tests/shared/CMakeLists.txt
+++ b/src/tests/shared/CMakeLists.txt
@@ -15,3 +15,9 @@ target_link_libraries(c_options_test ${EXTRA_LIBS} leanshared)
 add_test(OPTIONS c_options_test
          WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
          COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_options_test")
+
+add_executable(c_univ_test univ.c)
+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")
diff --git a/src/tests/shared/univ.c b/src/tests/shared/univ.c
new file mode 100644
index 000000000..8a55c6d62
--- /dev/null
+++ b/src/tests/shared/univ.c
@@ -0,0 +1,90 @@
+/*
+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__)
+
+int main() {
+    lean_exception ex;
+    lean_name a, l, U, pp, pp_unicode, rn;
+    lean_options o1, o2;
+    lean_univ zero, one, p1, g1, m1, u, n, i, ru;
+    char const * s1;
+    lean_bool r;
+
+    check(lean_name_mk_anonymous(&a, &ex));
+    check(lean_name_mk_str(a, "l_1", &l, &ex));
+    check(lean_name_mk_str(a, "U", &U, &ex));
+    check(lean_name_mk_str(a, "pp", &pp, &ex));
+    check(lean_name_mk_str(pp, "unicode", &pp_unicode, &ex));
+
+    check(lean_options_mk_empty(&o1, &ex));
+    check(lean_options_set_bool(o1, pp_unicode, lean_false, &o2, &ex));
+
+    check(lean_univ_mk_zero(&zero, &ex));
+    check(lean_univ_mk_succ(zero, &one, &ex));
+    check(lean_univ_mk_param(l, &p1, &ex));
+    check(lean_univ_mk_global(U, &g1, &ex));
+    check(lean_univ_mk_max(p1, one, &m1, &ex));
+    check(lean_univ_mk_succ(m1, &u, &ex));
+
+    check(lean_univ_normalize(u, &n, &ex));
+    check(lean_univ_to_string(n, &s1, &ex));
+    printf("universe: %s\n", s1);
+
+    check(lean_univ_geq(one, zero, &r, &ex) && r);
+
+    /* replace l_1 with one in u */
+    check(lean_univ_instantiate(u, 1, &l, &one, &i, &ex));
+    lean_string_del(s1);
+    check(lean_univ_to_string_using(i, o2, &s1, &ex));
+    printf("universe: %s\n", s1);
+
+    check(lean_univ_get_kind(zero) == LEAN_UNIV_ZERO);
+    check(lean_univ_get_kind(one) == LEAN_UNIV_SUCC);
+    check(lean_univ_get_kind(n) == LEAN_UNIV_MAX);
+
+    check(lean_univ_get_name(g1, &rn, &ex) && lean_name_eq(rn, U));
+
+    check(lean_univ_get_max_lhs(m1, &ru, &ex) && lean_univ_eq(ru, p1, &r, &ex) && r);
+    lean_univ_del(ru);
+    check(lean_univ_get_max_rhs(m1, &ru, &ex) && lean_univ_eq(ru, one, &r, &ex) && r);
+    lean_univ_del(ru);
+    check(lean_univ_get_pred(one, &ru, &ex) && lean_univ_eq(ru, zero, &r, &ex) && r);
+    lean_univ_del(ru);
+
+    lean_name_del(a);
+    lean_name_del(l);
+    lean_name_del(U);
+    lean_name_del(pp);
+    lean_name_del(pp_unicode);
+    lean_name_del(rn);
+
+    lean_options_del(o1);
+    lean_options_del(o2);
+
+    lean_univ_del(zero);
+    lean_univ_del(one);
+    lean_univ_del(p1);
+    lean_univ_del(g1);
+    lean_univ_del(m1);
+    lean_univ_del(u);
+    lean_univ_del(n);
+    lean_univ_del(i);
+
+    lean_string_del(s1);
+    return 0;
+}