From 5cce74d11637a3b3cb3e2dba952e8b1aad3f1ef1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Sep 2013 19:42:02 -0700 Subject: [PATCH] test(library): add tests for improving coverage Signed-off-by: Leonardo de Moura --- src/tests/library/CMakeLists.txt | 6 ++++ src/tests/library/arith.cpp | 49 ++++++++++++++++++++++++++ src/tests/library/formatter.cpp | 2 ++ src/tests/library/reduce.cpp | 60 ++++++++++++++++++++++++++++++++ 4 files changed, 117 insertions(+) create mode 100644 src/tests/library/arith.cpp create mode 100644 src/tests/library/reduce.cpp diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 6cc0f4378..4dc5380ec 100644 --- a/src/tests/library/CMakeLists.txt +++ b/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) diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp new file mode 100644 index 000000000..0eb1eb2d0 --- /dev/null +++ b/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; +} + diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp index 3ac8058fe..9248e6df5 100644 --- a/src/tests/library/formatter.cpp +++ b/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() { diff --git a/src/tests/library/reduce.cpp b/src/tests/library/reduce.cpp new file mode 100644 index 000000000..ea6ebc0f7 --- /dev/null +++ b/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; +} + +