From 29db6accb8830439a7dfc22af60e398c853dc97a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jan 2014 14:34:21 -0800 Subject: [PATCH] test(tests/lean): new tests for exercising the environment object Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 2 +- src/kernel/environment.cpp | 19 ++++------------ src/kernel/environment.h | 3 --- tests/lean/env_errors.lean | 29 ++++++++++++++++++++++++ tests/lean/env_errors.lean.expected.out | 12 ++++++++++ tests/lean/fake1.olean | 1 + tests/lean/fake2.olean | Bin 0 -> 1476 bytes tests/lean/univ2.lean | 7 ++++++ tests/lean/univ2.lean.expected.out | 5 ++++ 9 files changed, 59 insertions(+), 19 deletions(-) create mode 100644 tests/lean/env_errors.lean create mode 100644 tests/lean/env_errors.lean.expected.out create mode 100644 tests/lean/fake1.olean create mode 100644 tests/lean/fake2.olean create mode 100644 tests/lean/univ2.lean create mode 100644 tests/lean/univ2.lean.expected.out diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index e85263ae3..c267759c0 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -34,7 +34,7 @@ function(add_theory_core FILE ARG EXTRA_DEPS) add_custom_target("${BASENAME}_builtin" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} ${EXTRA_DEPS}) add_dependencies(builtin ${BASENAME}_builtin) install(FILES ${CMAKE_CURRENT_BINARY_DIR}/${FNAME} DESTINATION library) - add_test("${BASENAME}_builtin_test" ${SHELL_DIR}/lean ${ARG} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}) + add_test("${BASENAME}_builtin_test" ${SHELL_DIR}/lean -o ${CMAKE_CURRENT_BINARY_DIR}/${FNAME}_test ${ARG} ${CMAKE_CURRENT_SOURCE_DIR}/${FILE}) endfunction() # When cross compiling, we cannot execute lean during the build. diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index be98b8439..f460b8537 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -386,7 +386,7 @@ void environment_cell::init_uvars() { */ void environment_cell::check_no_cached_type(expr const & e) { if (find(e, [](expr const & a) { return is_constant(a) && const_type(a); })) - throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers"); + throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers"); // LCOV_EXCL_LINE } /** @@ -411,7 +411,7 @@ void environment_cell::check_new_definition(name const & n, expr const & t, expr /** \brief Add a new builtin value to this environment */ void environment_cell::add_builtin(expr const & v) { if (!is_value(v)) - throw invalid_builtin_value_declaration(env(), v); + throw invalid_builtin_value_declaration(env(), v); // LCOV_EXCL_LINE name const & n = to_value(v).get_name(); check_name(n); name const & u = to_value(v).get_unicode_name(); @@ -427,7 +427,7 @@ void environment_cell::add_builtin(expr const & v) { /** \brief Add a new builtin value set to this environment */ void environment_cell::add_builtin_set(expr const & r) { if (!is_value(r)) - throw invalid_builtin_value_declaration(env(), r); + throw invalid_builtin_value_declaration(env(), r); // LCOV_EXCL_LINE check_name(to_value(r).get_name()); register_named_object(mk_builtin_set(r)); } @@ -531,17 +531,6 @@ expr environment_cell::normalize(expr const & e, context const & ctx, bool unfol return m_type_checker->get_normalizer()(e, ctx, unfold_opaque); } -/** \brief Display universal variable constraints and objects stored in this environment and its parents. */ -void environment_cell::display(std::ostream & out) const { - if (has_parent()) - m_parent->display(out); - for (object const & obj : m_objects) { - if (obj.has_name()) { - out << obj.keyword() << " " << obj.get_name() << "\n"; - } - } -} - bool environment_cell::already_imported(name const & n) const { if (m_imported_modules.find(n) != m_imported_modules.end()) return true; @@ -752,7 +741,7 @@ name_map> & get_available_builtins() { void register_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set) { auto & bs = get_available_builtins(); if (bs.find(n) != bs.end()) - throw exception("invalid builtin object, system already has a builtin object with the given name"); + throw exception("invalid builtin object, system already has a builtin object with the given name"); // LCOV_EXCL_LINE bs[n] = mk_pair(mk, is_builtin_set); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 130c00581..98a2b7c75 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -289,9 +289,6 @@ public: object_iterator end_local_objects() const { return object_iterator(m_this.lock(), get_num_objects(true), true); } // ======================================= - /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ - void display(std::ostream & out) const; - /** \brief Register an environment extension. Every environment object will contain this extension. The funciton mk creates a diff --git a/tests/lean/env_errors.lean b/tests/lean/env_errors.lean new file mode 100644 index 000000000..fd677bee0 --- /dev/null +++ b/tests/lean/env_errors.lean @@ -0,0 +1,29 @@ + +variable x : Nat + +set::opaque x true. + +print "before import" +(* +local env = get_environment() +env:import("tstblafoo.lean") +*) + +print "before load1" +(* +local env = get_environment() +env:load("tstblafoo.lean") +*) + +print "before load2" +(* +local env = get_environment() +env:load("fake1.olean") +*) + +print "before load3" +(* +local env = get_environment() +env:load("fake2.olean") +*) + diff --git a/tests/lean/env_errors.lean.expected.out b/tests/lean/env_errors.lean.expected.out new file mode 100644 index 000000000..4f70b45e3 --- /dev/null +++ b/tests/lean/env_errors.lean.expected.out @@ -0,0 +1,12 @@ + Set: pp::colors + Set: pp::unicode + Assumed: x +Error (line: 4, pos: 0) set_opaque failed, 'x' is not a definition +before import +Error (line: 12, pos: 0) file 'tstblafoo.lean' not found in the LEAN_PATH +before load1 +Error (line: 18, pos: 0) failed to open file 'tstblafoo.lean' +before load2 +Error (line: 24, pos: 0) corrupted binary file +before load3 +Error (line: 30, pos: 0) file 'fake2.olean' does not seem to be a valid object Lean file diff --git a/tests/lean/fake1.olean b/tests/lean/fake1.olean new file mode 100644 index 000000000..b26633f1e --- /dev/null +++ b/tests/lean/fake1.olean @@ -0,0 +1 @@ +This is an invalid .olean file. It is used only for debugging purposes \ No newline at end of file diff --git a/tests/lean/fake2.olean b/tests/lean/fake2.olean new file mode 100644 index 0000000000000000000000000000000000000000..b40df3fe2fba1b103d5fd0b192c7145a1c127476 GIT binary patch literal 1476 zcmZ`(+invv5FImD z{8+vOpYd+ij>2l?ow3i%86S_=ry|OJ(U=El7SVEOi9Q z#8^^!rj{hvf9^>7=wy}UHY=!6C_Axck~#DjqZdCjQ!ql7h^4mF!0Id7#5i}N(v&WZ zRkjQe@|1IbLUc2N&R6*s^aVr5fVLuNnq6-}F@u^J+>XFbinxM{k0c!Q40${8()#u; zSWESknyk=FQ(GzokZ8-q8&ZBYCU>>L-NzuN~((sQOT_Ft%@Zm0Z(bz9 z6sK^wt$JL8#C>#EE#|uk4x%5hsl+qYnmlV{Q_kgCTz1ewWQ}&n|-J{Wms!A3N;flY_?%7*m*1%XB1zH Ibc|p3KZeiF#Q*>R literal 0 HcmV?d00001 diff --git a/tests/lean/univ2.lean b/tests/lean/univ2.lean new file mode 100644 index 000000000..00ea05ce6 --- /dev/null +++ b/tests/lean/univ2.lean @@ -0,0 +1,7 @@ +universe Z >= max U+1 M+1 +print environment 2 +(* +local env = get_environment() +assert(env:get_universe_distance("Z", "U") == 1) +assert(env:get_universe_distance("Z", "M") == 513) +*) diff --git a/tests/lean/univ2.lean.expected.out b/tests/lean/univ2.lean.expected.out new file mode 100644 index 000000000..d7a2c5f98 --- /dev/null +++ b/tests/lean/univ2.lean.expected.out @@ -0,0 +1,5 @@ + Set: pp::colors + Set: pp::unicode +import "kernel" +import "Nat" +universe Z ≥ U+1 ⊔ M+1