test(*): add missing tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<bool_value_value const*>(&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)));

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")

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<std::pair<expr const *, unsigned>> 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;
 }

src/tests/util/list.cpp

@@ -86,6 +86,13 @@ static void tst7() {
     lean_assert(l2 == l3);
 }
 
+static void tst8() {
+    list<int> 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;
 }

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;
 }

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;
 }

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<typename T> void display_var(char const * name, T const & value) {
               << std::boolalpha << value << std::noboolalpha
               << std::endl; }
 }
+// LCOV_EXCL_STOP
 }

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)