test(library): add tests for improving coverage

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

src/tests/library/CMakeLists.txt

@@ -16,3 +16,9 @@ add_test(expr_lt ${CMAKE_CURRENT_BINARY_DIR}/expr_lt)
 add_executable(deep_copy deep_copy.cpp)
 target_link_libraries(deep_copy ${EXTRA_LIBS})
 add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
+add_executable(reduce reduce.cpp)
+target_link_libraries(reduce ${EXTRA_LIBS})
+add_test(reduce ${CMAKE_CURRENT_BINARY_DIR}/reduce)
+add_executable(arith_tst arith.cpp)
+target_link_libraries(arith_tst ${EXTRA_LIBS})
+add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)

src/tests/library/arith.cpp

@@ -0,0 +1,49 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "kernel/builtin.h"
+#include "kernel/normalizer.h"
+#include "library/arith/arith.h"
+using namespace lean;
+
+static void tst1() {
+    environment env;
+    normalizer  norm(env);
+    import_basic(env);
+    import_arith(env);
+    env.add_var("n", Nat);
+    expr n = Const("n");
+    lean_assert_eq(mk_nat_type(), Nat);
+    lean_assert_eq(norm(nMul(nVal(2), nVal(3))), nVal(6));
+    lean_assert_eq(norm(nLe(nVal(2), nVal(3))), True);
+    lean_assert_eq(norm(nLe(nVal(5), nVal(3))), False);
+    lean_assert_eq(norm(nLe(nVal(2), nVal(3))), True);
+    lean_assert_eq(norm(nLe(n, nVal(3))), nLe(n, nVal(3)));
+    env.add_var("x", Real);
+    expr x = Const("x");
+    lean_assert_eq(mk_real_type(), Real);
+    lean_assert_eq(norm(rMul(rVal(2), rVal(3))), rVal(6));
+    lean_assert_eq(norm(rDiv(rVal(2), rVal(0))), rVal(0));
+    lean_assert_eq(norm(rLe(rVal(2),  rVal(3))), True);
+    lean_assert_eq(norm(rLe(rVal(5),  rVal(3))), False);
+    lean_assert_eq(norm(rLe(rVal(2),  rVal(3))), True);
+    lean_assert_eq(norm(rLe(x, rVal(3))), rLe(x, rVal(3)));
+    env.add_var("i", Int);
+    expr i = Const("i");
+    lean_assert_eq(norm(i2r(i)), i2r(i));
+    lean_assert_eq(norm(i2r(iVal(2))), rVal(2));
+    lean_assert_eq(mk_int_type(), Int);
+    lean_assert_eq(norm(n2i(n)), n2i(n));
+    lean_assert_eq(norm(n2i(nVal(2))), iVal(2));
+    lean_assert_eq(norm(iDiv(iVal(2), iVal(0))), iVal(0));
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}
+

src/tests/library/formatter.cpp

@@ -39,6 +39,8 @@ static void tst1() {
     check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y = x]");
     check(fmt(ctx, f(Var(0), Var(2))), "f z x");
     check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y = x] |- f z x");
+    fmt.set_interrupt(true);
+    fmt.set_interrupt(false);
 }
 
 int main() {

src/tests/library/reduce.cpp

@@ -0,0 +1,60 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "kernel/abstract.h"
+#include "library/reduce.h"
+using namespace lean;
+
+static void tst1() {
+    expr f = Const("f");
+    expr h = Const("h");
+    expr x = Const("x");
+    expr y = Const("y");
+    expr a = Const("a");
+    expr b = Const("b");
+    expr c = Const("c");
+    expr d = Const("d");
+    expr N = Const("N");
+    expr F1 = Fun({x, N}, x)(f, a);
+    lean_assert(is_head_beta(F1));
+    std::cout << F1 << " --> " << head_beta_reduce(F1) << "\n";
+    lean_assert_eq(head_beta_reduce(F1), f(a));
+    expr F2 = Fun({{h, N >> (N >> (N >> N))}, {y, N}}, h(y))(f, a, b, c);
+    lean_assert(is_head_beta(F2));
+    std::cout << F2 << " --> " << head_beta_reduce(F2) << "\n";
+    lean_assert_eq(head_beta_reduce(F2), f(a, b, c));
+    expr F3 = Fun({x, N}, f(Fun({y, N}, y)(x), x))(a);
+    lean_assert(is_head_beta(F3));
+    std::cout << F3 << " --> " << head_beta_reduce(F3) << "\n";
+    lean_assert_eq(head_beta_reduce(F3), f(Fun({y, N}, y)(a), a));
+    std::cout << F3 << " --> " << beta_reduce(F3) << "\n";
+    lean_assert_eq(beta_reduce(F3), f(a, a));
+}
+
+static void tst2() {
+    environment env;
+    expr x = Const("x");
+    expr a = Const("a");
+    expr f = Const("f");
+    expr N = Const("N");
+    expr F1 = Let({x, a}, f(x));
+    lean_assert_eq(head_beta_reduce(F1), F1);
+    lean_assert_eq(head_reduce(F1, env), f(a));
+    context ctx;
+    ctx = extend(ctx, "x", N, f(a));
+    ctx = extend(ctx, "y", N, f(Var(0)));
+    std::cout << head_reduce(Var(0), env, ctx) << "\n";
+    lean_assert_eq(head_reduce(Var(0), env, ctx), f(Var(1)));
+}
+
+int main() {
+    tst1();
+    tst2();
+    return has_violations() ? 1 : 0;
+}
+
+