From 1315378ebbba57b166284eec82ca012ab12242c5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Nov 2013 09:13:34 -0800 Subject: [PATCH] test(*): add missing tests Signed-off-by: Leonardo de Moura --- src/kernel/builtin.cpp | 4 ++ src/shell/CMakeLists.txt | 1 + src/tests/kernel/expr.cpp | 129 ++++++++++++++++++----------------- src/tests/util/list.cpp | 8 +++ src/tests/util/name.cpp | 24 +++++++ src/tests/util/splay_map.cpp | 11 +++ src/util/debug.h | 2 + tests/lua/splay1.lua | 7 ++ 8 files changed, 124 insertions(+), 62 deletions(-) create mode 100644 tests/lua/splay1.lua diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index af4d3be39..8d682fb8c 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -85,10 +85,14 @@ public: virtual expr get_type() const { return Bool; } virtual name get_name() const { return m_val ? g_true_name : g_false_name; } virtual name get_unicode_name() const { return m_val ? g_true_u_name : g_false_u_name; } + // LCOV_EXCL_START virtual bool operator==(value const & other) const { + // This method is unreachable because there is only one copy of True and False in the system, + // and they have different hashcodes. bool_value_value const * _other = dynamic_cast(&other); return _other && _other->m_val == m_val; } + // LCOV_EXCL_STOP bool get_val() const { return m_val; } }; expr const True = mk_value(*(new bool_value_value(true))); diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 82d98d830..016a6b96a 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -5,6 +5,7 @@ target_link_libraries(lean ${EXTRA_LIBS}) add_test(example1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean") add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex2.lean") add_test(example3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex3.lean") +add_test(example1_stdin ${CMAKE_CURRENT_BINARY_DIR}/lean < "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean") add_test(NAME leantests WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean" COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean") diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 597917417..c6596115d 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -19,7 +19,7 @@ Author: Leonardo de Moura #include "library/arith/arith.h" using namespace lean; -void tst1() { +static void tst1() { expr a; a = Const("a"); expr f; @@ -40,7 +40,7 @@ void tst1() { std::cout << mk_pi("x", ty, Var(0)) << "\n"; } -expr mk_dag(unsigned depth, bool _closed = false) { +static expr mk_dag(unsigned depth, bool _closed = false) { expr f = Const("f"); expr a = _closed ? Const("a") : Var(0); while (depth > 0) { @@ -50,7 +50,7 @@ expr mk_dag(unsigned depth, bool _closed = false) { return a; } -unsigned depth1(expr const & e) { +static unsigned depth1(expr const & e) { switch (e.kind()) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::MetaVar: @@ -72,7 +72,7 @@ unsigned depth1(expr const & e) { } // This is the fastest depth implementation in this file. -unsigned depth2(expr const & e) { +static unsigned depth2(expr const & e) { switch (e.kind()) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::MetaVar: @@ -92,45 +92,7 @@ unsigned depth2(expr const & e) { return 0; } -// This is the slowest depth implementation in this file. -unsigned depth3(expr const & e) { - static std::vector> todo; - unsigned m = 0; - todo.emplace_back(&e, 0); - while (!todo.empty()) { - auto const & p = todo.back(); - expr const & e = *(p.first); - unsigned c = p.second + 1; - todo.pop_back(); - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: - case expr_kind::Value: case expr_kind::MetaVar: - m = std::max(c, m); - break; - case expr_kind::App: { - unsigned num = num_args(e); - for (unsigned i = 0; i < num; i++) - todo.emplace_back(&arg(e, i), c); - break; - } - case expr_kind::Eq: - todo.emplace_back(&eq_lhs(e), c); - todo.emplace_back(&eq_rhs(e), c); - break; - case expr_kind::Lambda: case expr_kind::Pi: - todo.emplace_back(&abst_domain(e), c); - todo.emplace_back(&abst_body(e), c); - break; - case expr_kind::Let: - todo.emplace_back(&let_value(e), c); - todo.emplace_back(&let_body(e), c); - break; - } - } - return m; -} - -void tst2() { +static void tst2() { expr r1 = mk_dag(20); expr r2 = mk_dag(20); lean_assert(r1 == r2); @@ -138,21 +100,21 @@ void tst2() { lean_assert(depth2(r1) == 21); } -expr mk_big(expr f, unsigned depth, unsigned val) { +static expr mk_big(expr f, unsigned depth, unsigned val) { if (depth == 1) return Const(name(name("foo"), val)); else return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1)); } -void tst3() { +static void tst3() { expr f = Const("f"); expr r1 = mk_big(f, 20, 0); expr r2 = mk_big(f, 20, 0); lean_assert(r1 == r2); } -void tst4() { +static void tst4() { expr f = Const("f"); expr a = Var(0); for (unsigned i = 0; i < 10000; i++) { @@ -160,15 +122,14 @@ void tst4() { } } -expr mk_redundant_dag(expr f, unsigned depth) { +static expr mk_redundant_dag(expr f, unsigned depth) { if (depth == 0) return Var(0); else return f(mk_redundant_dag(f, depth - 1), mk_redundant_dag(f, depth - 1)); } - -unsigned count_core(expr const & a, expr_set & s) { +static unsigned count_core(expr const & a, expr_set & s) { if (s.find(a) != s.end()) return 0; s.insert(a); @@ -189,12 +150,12 @@ unsigned count_core(expr const & a, expr_set & s) { return 0; } -unsigned count(expr const & a) { +static unsigned count(expr const & a) { expr_set s; return count_core(a, s); } -void tst5() { +static void tst5() { expr f = Const("f"); { expr r1 = mk_redundant_dag(f, 5); @@ -214,7 +175,7 @@ void tst5() { } } -void tst6() { +static void tst6() { expr f = Const("f"); expr r = mk_redundant_dag(f, 12); for (unsigned i = 0; i < 1000; i++) { @@ -226,7 +187,7 @@ void tst6() { } } -void tst7() { +static void tst7() { expr f = Const("f"); expr v = Var(0); expr a1 = max_sharing(f(v, v)); @@ -236,7 +197,7 @@ void tst7() { lean_assert(is_eqp(arg(b, 1), arg(b, 2))); } -void tst8() { +static void tst8() { expr f = Const("f"); expr x = Var(0); expr a = Const("a"); @@ -268,14 +229,14 @@ void tst8() { lean_assert(closed(mk_lambda("z", p, r))); } -void tst9() { +static void tst9() { expr r = mk_dag(20, true); lean_assert(closed(r)); r = mk_dag(20, false); lean_assert(!closed(r)); } -void tst10() { +static void tst10() { expr f = Const("f"); expr r = mk_big(f, 16, 0); for (unsigned i = 0; i < 1000; i++) { @@ -288,11 +249,11 @@ void tst10() { \pre s and t must be closed expressions (i.e., no free variables) */ -inline expr substitute(expr const & e, expr const & s, expr const & t) { +static expr substitute(expr const & e, expr const & s, expr const & t) { return instantiate(abstract(e, s), t); } -void tst11() { +static void tst11() { expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); @@ -315,7 +276,7 @@ void tst11() { lean_assert(substitute(f(f(f(a))), f(a), b) == f(f(b))); } -void tst12() { +static void tst12() { expr f = Const("f"); expr v = Var(0); expr a1 = max_sharing(f(v, v)); @@ -327,7 +288,7 @@ void tst12() { lean_assert(is_eqp(M(a1), M(a2))); } -void tst13() { +static void tst13() { expr t0 = Type(); expr t1 = Type(level()+1); lean_assert(ty_level(t1) == level()+1); @@ -335,7 +296,7 @@ void tst13() { std::cout << t0 << " " << t1 << "\n"; } -void tst14() { +static void tst14() { expr t = Eq(Const("a"), Const("b")); std::cout << t << "\n"; expr l = mk_let("a", expr(), Const("b"), Var(0)); @@ -343,7 +304,7 @@ void tst14() { lean_assert(closed(l)); } -void tst15() { +static void tst15() { expr f = Const("f"); expr x = Var(0); expr a = Const("a"); @@ -372,6 +333,47 @@ void tst15() { lean_assert(has_metavar(Eq(a, f(m)))); } +static void check_copy(expr const & e) { + expr c = copy(e); + lean_assert(!is_eqp(e, c)); + lean_assert(e == c); +} + +static void tst16() { + expr f = Const("f"); + expr a = Const("a"); + check_copy(iVal(10)); + check_copy(f(a)); + check_copy(Eq(f(a), a)); + check_copy(mk_metavar("M")); + check_copy(mk_lambda("x", a, Var(0))); + check_copy(mk_pi("x", a, Var(0))); + check_copy(mk_let("x", expr(), a, Var(0))); +} + +static void tst17() { + lean_assert(is_true(True)); + lean_assert(is_false(False)); + lean_assert(!is_true(Const("a"))); + lean_assert(!is_false(Const("a"))); +} + +static void tst18() { + expr f = Const("f"); + expr a = Const("a"); + lean_assert_eq(mk_bin_rop(f, a, 0, nullptr), a); + expr b = Const("b"); + lean_assert_eq(mk_bin_rop(f, a, 1, &b), b); + expr a1 = Const("a1"); expr a2 = Const("a2"); expr a3 = Const("a3"); + expr ar[] = { a1, a2, a3 }; + lean_assert_eq(mk_bin_rop(f, a, 3, ar), f(a1, f(a2, a3))); + lean_assert_eq(mk_bin_rop(f, a, {a1, a2, a3}), f(a1, f(a2, a3))); + lean_assert_eq(mk_bin_lop(f, a, 0, nullptr), a); + lean_assert_eq(mk_bin_lop(f, a, 1, &b), b); + lean_assert_eq(mk_bin_lop(f, a, 3, ar), f(f(a1, a2), a3)); + lean_assert_eq(mk_bin_lop(f, a, {a1, a2, a3}), f(f(a1, a2), a3)); +} + int main() { std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n"; @@ -391,6 +393,9 @@ int main() { tst13(); tst14(); tst15(); + tst16(); + tst17(); + tst18(); std::cout << "done" << "\n"; return has_violations() ? 1 : 0; } diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp index 92133cdf9..34e3a32b2 100644 --- a/src/tests/util/list.cpp +++ b/src/tests/util/list.cpp @@ -86,6 +86,13 @@ static void tst7() { lean_assert(l2 == l3); } +static void tst8() { + list l1{1, 2, 3}; + unsigned c = 0; + for_each(l1, [&](int ){ c = c + 1; }); + lean_assert(c == length(l1)); +} + int main() { tst1(); tst2(); @@ -94,5 +101,6 @@ int main() { tst5(); tst6(); tst7(); + tst8(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp index e487aeba6..1032cfa9b 100644 --- a/src/tests/util/name.cpp +++ b/src/tests/util/name.cpp @@ -124,6 +124,28 @@ static void tst9() { lean_assert(n1 == a1); } +static void tst10() { + name_generator g1("a"); + name_generator g2("b"); + name a0 = g1.next(); + name b0 = g2.next(); + lean_assert_eq(a0, name(name("a"), 0u)); + lean_assert_eq(b0, name(name("b"), 0u)); + swap(g1, g2); + name a1 = g2.next(); + name b1 = g1.next(); + lean_assert_eq(a1, name(name("a"), 1u)); + lean_assert_eq(b1, name(name("b"), 1u)); +} + +static void tst11() { + name n1("a"); + name n2("b"); + swap(n1, n2); + lean_assert(n1 == name("b")); + lean_assert(n2 == name("a")); +} + int main() { tst1(); tst2(); @@ -134,5 +156,7 @@ int main() { tst7(); tst8(); tst9(); + tst10(); + tst11(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/splay_map.cpp b/src/tests/util/splay_map.cpp index 401b7e0b2..9d8ffb63c 100644 --- a/src/tests/util/splay_map.cpp +++ b/src/tests/util/splay_map.cpp @@ -43,8 +43,19 @@ static void tst1() { lean_assert(out.str() == "t1 t2 "); } +static void tst2() { + int2name m1, m2; + m1[10] = name("t1"); + lean_assert(m1.size() == 1); + lean_assert(m2.size() == 0); + swap(m1, m2); + lean_assert(m2.size() == 1); + lean_assert(m1.size() == 0); +} + int main() { tst0(); tst1(); + tst2(); return has_violations() ? 1 : 0; } diff --git a/src/util/debug.h b/src/util/debug.h index 881976d41..d8eeff670 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -99,6 +99,7 @@ void disable_debug(char const * tag); bool is_debug_enabled(char const * tag); void invoke_debugger(); bool has_violations(); +// LCOV_EXCL_START /** \brief Exception used to sign that unreachable code was reached */ class unreachable_reached : public exception { public: @@ -113,4 +114,5 @@ template void display_var(char const * name, T const & value) { << std::boolalpha << value << std::noboolalpha << std::endl; } } +// LCOV_EXCL_STOP } diff --git a/tests/lua/splay1.lua b/tests/lua/splay1.lua new file mode 100644 index 000000000..dec224203 --- /dev/null +++ b/tests/lua/splay1.lua @@ -0,0 +1,7 @@ +local s = splay_map() +assert(s:empty()) +assert(#s == 0) +s:insert(10, 1) +assert(not s:empty()) +assert(#s == 1) +assert(s:find(10) == 1)