From c83b72e9b6642145bc22befc18d37b0f43cdabe6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 22 Aug 2015 13:35:35 -0700 Subject: [PATCH] test(tests/shared/env): add tests for lean_env API --- src/api/decl.cpp | 2 +- src/api/env.cpp | 4 +- src/api/lean.h | 1 + src/api/lean_decl.h | 2 +- src/api/lean_env.h | 9 +- src/tests/shared/CMakeLists.txt | 6 + src/tests/shared/env.c | 215 ++++++++++++++++++++++++++++++++ 7 files changed, 233 insertions(+), 6 deletions(-) create mode 100644 src/tests/shared/env.c diff --git a/src/api/decl.cpp b/src/api/decl.cpp index bd35e431ec..23b677eeff 100644 --- a/src/api/decl.cpp +++ b/src/api/decl.cpp @@ -69,7 +69,7 @@ lean_bool lean_decl_mk_thm(lean_env e, lean_name n, lean_list_name p, lean_expr LEAN_CATCH; } -void lean_decl_decl(lean_decl d) { +void lean_decl_del(lean_decl d) { delete to_decl(d); } diff --git a/src/api/env.cpp b/src/api/env.cpp index 3a2c498306..1af48f5319 100644 --- a/src/api/env.cpp +++ b/src/api/env.cpp @@ -96,7 +96,7 @@ lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exceptio LEAN_TRY; check_nonnull(e); to_env_ref(e).for_each_declaration([&](declaration const & d) { - f(of_decl(const_cast(&d))); + f(of_decl(new declaration(d))); }); return lean_true; LEAN_CATCH; @@ -106,7 +106,7 @@ lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exceptio LEAN_TRY; check_nonnull(e); to_env_ref(e).for_each_universe([&](name const & u) { - f(of_name(const_cast(&u))); + f(of_name(new name(u))); }); return lean_true; LEAN_CATCH; diff --git a/src/api/lean.h b/src/api/lean.h index ed6f589e45..c2800075dd 100644 --- a/src/api/lean.h +++ b/src/api/lean.h @@ -16,5 +16,6 @@ Author: Leonardo de Moura #include "lean_univ.h" // NOLINT #include "lean_expr.h" // NOLINT #include "lean_decl.h" // NOLINT +#include "lean_env.h" // NOLINT #endif diff --git a/src/api/lean_decl.h b/src/api/lean_decl.h index 6fabb02fc8..fbd5237501 100644 --- a/src/api/lean_decl.h +++ b/src/api/lean_decl.h @@ -58,7 +58,7 @@ lean_bool lean_decl_mk_thm(lean_name n, lean_list_name p, lean_expr t, lean_expr lean_bool lean_decl_mk_thm_with(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_decl * r, lean_exception * ex); /** \brief Delete/dispose the given declaration. */ -void lean_decl_decl(lean_decl d); +void lean_decl_del(lean_decl d); /** \brief Return the kind of the given declaration. \remark Return LEAN_DECL_CONST if d is null. */ lean_decl_kind lean_decl_get_kind(lean_decl d); diff --git a/src/api/lean_env.h b/src/api/lean_env.h index c1ffe18cc9..1f641ce07d 100644 --- a/src/api/lean_env.h +++ b/src/api/lean_env.h @@ -27,6 +27,9 @@ lean_bool lean_env_mk_std(unsigned t, lean_env * r, lean_exception * ex); /** \brief Create a HoTT environment (i.e., proof relevant, no Prop) with trust level \c t. */ lean_bool lean_env_mk_hott(unsigned t, lean_env * r, lean_exception * ex); +/** Trust all macros implemented in Lean, and do no retype-check imported modules */ +#define LEAN_TRUST_HIGH 100000 + /** \brief Add a new global universe with name \c u. */ lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex); /** \brief Create a new environment by adding the given certified declaration \c d to the environment \c e. */ @@ -61,9 +64,11 @@ lean_bool lean_env_is_descendant(lean_env e1, lean_env e2); is not pointer equal to the result. */ lean_bool lean_env_forget(lean_env e, lean_env * r, lean_exception * ex); -/** \brief Execute \c f for each declaration in \c env. */ +/** \brief Execute \c f for each declaration in \c env. + \remark Every declaration passed to \c f must be disposed using \c lean_decl_del. */ lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exception * ex); -/** \brief Execute \c f for each global universe in \c env. */ +/** \brief Execute \c f for each global universe in \c env. + \remark Every name passed to \c f must be disposed using \c lean_nam_del. */ lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex); /*@}*/ /*@}*/ diff --git a/src/tests/shared/CMakeLists.txt b/src/tests/shared/CMakeLists.txt index 7a4d4f272c..81ec10935b 100644 --- a/src/tests/shared/CMakeLists.txt +++ b/src/tests/shared/CMakeLists.txt @@ -27,3 +27,9 @@ 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") + +add_executable(c_env_test env.c) +target_link_libraries(c_env_test ${EXTRA_LIBS} leanshared) +add_test(ENV c_env_test + WORKING_DIRECTORY "${LEAN_BINARY_DIR}" + COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_env_test") diff --git a/src/tests/shared/env.c b/src/tests/shared/env.c new file mode 100644 index 0000000000..2993a99a9c --- /dev/null +++ b/src/tests/shared/env.c @@ -0,0 +1,215 @@ +/* +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 +#include +#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__) + +lean_name mk_name(char const * n) { + lean_exception ex; + lean_name a, r; + check(lean_name_mk_anonymous(&a, &ex)); + check(lean_name_mk_str(a, n, &r, &ex)); + lean_name_del(a); + return r; +} + +lean_univ mk_uparam(char const * n) { + lean_exception ex; + lean_univ r; + lean_name _n = mk_name(n); + check(lean_univ_mk_param(_n, &r, &ex)); + lean_name_del(_n); + return r; +} + +lean_list_name mk_unary_name_list(lean_name u) { + lean_exception ex; + lean_list_name n, r; + check(lean_list_name_mk_nil(&n, &ex)); + check(lean_list_name_mk_cons(u, n, &r, &ex)); + lean_list_name_del(n); + return r; +} + +lean_env mk_env() { + lean_exception ex; + lean_env r; + check(lean_env_mk_std(LEAN_TRUST_HIGH, &r, &ex)); + return r; +} + +lean_expr mk_constant(char const * n, lean_list_univ us) { + lean_exception ex; + lean_name _n = mk_name(n); + lean_expr r; + check(lean_expr_mk_const(_n, us, &r, &ex)); + lean_name_del(_n); + return r; +} + +lean_expr mk_var(unsigned i) { + lean_exception ex; + lean_expr r; + check(lean_expr_mk_var(i, &r, &ex)); + return r; +} + +lean_expr mk_sort(lean_univ u) { + lean_exception ex; + lean_expr r; + check(lean_expr_mk_sort(u, &r, &ex)); + return r; +} + +lean_expr mk_pi(char const * n, lean_expr d, lean_expr c) { + lean_exception ex; + lean_name name = mk_name(n); + lean_expr r; + check(lean_expr_mk_pi(name, d, c, LEAN_BINDER_DEFAULT, &r, &ex)); + lean_name_del(name); + return r; +} + +lean_expr mk_lambda(char const * n, lean_expr d, lean_expr c) { + lean_exception ex; + lean_name name = mk_name(n); + lean_expr r; + check(lean_expr_mk_lambda(name, d, c, LEAN_BINDER_DEFAULT, &r, &ex)); + lean_name_del(name); + return r; +} + +lean_decl mk_def(char const * n, lean_list_name p, lean_expr t, lean_expr v) { + lean_exception ex; + lean_name name = mk_name(n); + lean_decl r; + check(lean_decl_mk_def(name, p, t, v, 0, lean_true, &r, &ex)); + lean_name_del(name); + return r; +} + +void print_univ_and_del(lean_name n) { + lean_exception ex; + char const * s; + check(lean_name_to_string(n, &s, &ex)); + printf("universe: %s\n", s); + lean_string_del(s); + lean_name_del(n); +} + +void print_expr(lean_expr e) { + lean_exception ex; + char const * s; + check(lean_expr_to_string(e, &s, &ex)); + printf("%s\n", s); + lean_string_del(s); +} + +void print_decl_and_del(lean_decl d) { + lean_exception ex; + lean_name n; + lean_expr t; + char const * s; + check(lean_decl_get_name(d, &n, &ex)); + check(lean_name_to_string(n, &s, &ex)); + printf("declaration name: %s\n", s); + check(lean_decl_get_type(d, &t, &ex)); + printf(" type: "); + print_expr(t); + if (lean_decl_get_kind(d) == LEAN_DECL_DEF || lean_decl_get_kind(d) == LEAN_DECL_THM) { + lean_expr v; + check(lean_decl_get_value(d, &v, &ex)); + printf(" value: "); + print_expr(v); + lean_expr_del(v); + } + lean_expr_del(t); + lean_name_del(n); + lean_string_del(s); + lean_decl_del(d); +} + +void test_add_univ() { + lean_exception ex; + lean_name u = mk_name("u"); + lean_name v = mk_name("v"); + lean_env env = mk_env(); + lean_env new_env; + check(lean_env_add_univ(env, u, &new_env, &ex)); + check(lean_env_contains_univ(new_env, u)); + check(!lean_env_contains_univ(new_env, v)); + check(lean_env_for_each_univ(new_env, print_univ_and_del, &ex)); + lean_name_del(u); + lean_name_del(v); + lean_env_del(env); + lean_env_del(new_env); +} + +void test_id() { + lean_exception ex; + lean_univ l = mk_uparam("l"); + lean_env env = mk_env(); + lean_expr v0 = mk_var(0); + lean_expr v1 = mk_var(1); + lean_expr AA = mk_pi("a", v0, v1); + lean_expr Type = mk_sort(l); + lean_expr id_type = mk_pi("A", Type, AA); + lean_expr f = mk_lambda("a", v0, v0); + lean_expr id_val = mk_lambda("A", Type, f); + lean_name l_name = mk_name("l"); + lean_list_name id_ps = mk_unary_name_list(l_name); + lean_decl id_def = mk_def("id", id_ps, id_type, id_val); + lean_name id_name = mk_name("id"); + lean_cert_decl id_cert_def; + lean_env new_env; + + printf("id type: "); + print_expr(id_type); + printf("id value: "); + print_expr(id_val); + printf("-------\n"); + + /* type check definition */ + check(lean_decl_check(env, id_def, &id_cert_def, &ex)); + /* add certified definition to environment */ + check(lean_env_add(env, id_cert_def, &new_env, &ex)); + + check(!lean_env_contains_decl(env, id_name)); + check(lean_env_contains_decl(new_env, id_name)); + check(lean_env_for_each_decl(new_env, print_decl_and_del, &ex)); + + lean_univ_del(l); + lean_env_del(env); + lean_expr_del(v0); + lean_expr_del(v1); + lean_expr_del(Type); + lean_expr_del(AA); + lean_expr_del(id_type); + lean_expr_del(f); + lean_expr_del(id_val); + lean_decl_del(id_def); + lean_list_name_del(id_ps); + lean_name_del(l_name); + lean_cert_decl_del(id_cert_def); + lean_env_del(new_env); + lean_name_del(id_name); +} + +int main() { + test_add_univ(); + test_id(); + return 0; +}