From 3b78af0db53c439d63910c791915d5068745aeea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Apr 2014 12:05:49 -0700 Subject: [PATCH] chore(tests/library): enable old tests Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 2 +- src/tests/library/CMakeLists.txt | 20 +++++++-------- src/tests/library/deep_copy.cpp | 7 +++--- src/tests/library/expr_lt.cpp | 41 ------------------------------- src/tests/library/max_sharing.cpp | 19 ++++---------- 5 files changed, 19 insertions(+), 70 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 879442430..9894d2dae 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -246,7 +246,7 @@ add_subdirectory(tests/util) add_subdirectory(tests/util/numerics) add_subdirectory(tests/util/interval) add_subdirectory(tests/kernel) -# add_subdirectory(tests/library) +add_subdirectory(tests/library) # add_subdirectory(tests/library/rewriter) # add_subdirectory(tests/library/tactic) # add_subdirectory(tests/library/elaborator) diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 7ea6d37ee..962d336e3 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,6 +1,6 @@ -add_executable(formatter formatter.cpp) -target_link_libraries(formatter ${EXTRA_LIBS}) -add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter) +# add_executable(formatter formatter.cpp) +# target_link_libraries(formatter ${EXTRA_LIBS}) +# add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter) add_executable(max_sharing max_sharing.cpp) target_link_libraries(max_sharing ${EXTRA_LIBS}) add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing) @@ -10,10 +10,10 @@ 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(arith_tst arith.cpp) -target_link_libraries(arith_tst ${EXTRA_LIBS}) -add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst) -set_tests_properties(arith_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") -add_executable(update_expr update_expr.cpp) -target_link_libraries(update_expr ${EXTRA_LIBS}) -add_test(update_expr ${CMAKE_CURRENT_BINARY_DIR}/update_expr) +# add_executable(arith_tst arith.cpp) +# target_link_libraries(arith_tst ${EXTRA_LIBS}) +# add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst) +# set_tests_properties(arith_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") +# add_executable(update_expr update_expr.cpp) +# target_link_libraries(update_expr ${EXTRA_LIBS}) +# add_test(update_expr ${CMAKE_CURRENT_BINARY_DIR}/update_expr) diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp index 1d554c020..8889121ac 100644 --- a/src/tests/library/deep_copy.cpp +++ b/src/tests/library/deep_copy.cpp @@ -14,11 +14,10 @@ static void tst1() { expr f = Const("f"); expr a = Const("a"); expr x = Var(0); - expr t = Type(); + expr t = Type; expr z = Const("z"); - local_context lctx{mk_lift(0, 1), mk_inst(0, a)}; - expr m = mk_metavar("a", lctx); - expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), f(x, m))))); + expr m = mk_metavar("a", Type); + expr F = mk_let("z", mk_Bool(), Type, mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), f(x, m))))); expr G = deep_copy(F); lean_assert(F == G); lean_assert(!is_eqp(F, G)); diff --git a/src/tests/library/expr_lt.cpp b/src/tests/library/expr_lt.cpp index 85923941e..ed16125dc 100644 --- a/src/tests/library/expr_lt.cpp +++ b/src/tests/library/expr_lt.cpp @@ -6,11 +6,7 @@ Author: Leonardo de Moura */ #include "util/test.h" #include "kernel/abstract.h" -#include "kernel/kernel.h" #include "library/expr_lt.h" -#include "library/arith/nat.h" -#include "library/arith/int.h" -#include "library/arith/real.h" using namespace lean; static void lt(expr const & e1, expr const & e2, bool expected) { @@ -19,17 +15,8 @@ static void lt(expr const & e1, expr const & e2, bool expected) { } static void tst1() { - lt(iVal(1), iVal(1), false); - lt(iVal(1), iVal(2), true); - lt(rVal(1), rVal(1), false); - lt(rVal(1), rVal(2), true); - lt(nVal(1), nVal(1), false); - lt(nVal(1), nVal(2), true); lt(Var(0), Var(0), false); lt(Var(0), Var(1), true); - lt(False, True, true); - lt(False, False, false); - lt(Bool, Int, true); lt(Const("a"), Const("b"), true); lt(Const("a"), Const("a"), false); lt(Var(1), Const("a"), true); @@ -42,34 +29,6 @@ static void tst1() { lt(Const("g")(Var(0), Const("a")), Const("f")(Var(0), Const("a")), false); lt(Const("f")(Var(1), Const("a")), Const("f")(Var(0), Const("a")), false); lt(Const("f")(Var(0), Const("b")), Const("f")(Var(0), Const("a")), false); - lt(Type(level()), Type(level()+1), true); - lt(Type(level("u")), Type(level("z")), true); - lt(Type(level("u") + 1), Type(level("u") + 2), true); - lt(Type(level("u") + 1), Type(level("u") + 1), false); - lt(Type(max({level("u"), level("v")})), Type(max({level("u"), level("z")})), true); - lt(Type(max({level("u"), level("v")})), Type(max({level("u"), level("v")})), false); - lt(mk_lambda("x", Int, Var(0)), mk_lambda("y", Real, Var(0)), true); - lt(mk_lambda("x", Int, Var(0)), mk_lambda("y", Real, Var(10)), true); - lt(mk_lambda("x", Bool, Var(100)), mk_lambda("y", Real, Var(10)), true); - lt(mk_lambda("x", Int, Var(0)), mk_lambda("y", Int, Var(0)), false); - lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Real, rVal(10), Var(0)), true); - lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Int, iVal(20), Var(0)), true); - lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Int, iVal(10), Var(1)), true); - lt(mk_let("x", Int, iVal(10), Var(0)), mk_let("y", Int, iVal(10), Var(0)), false); - lt(mk_pi("x", Int, Int), mk_pi("y", Real, Bool), true); - lt(mk_pi("x", Int, Int), mk_pi("y", Int, Real), true); - lt(mk_pi("x", Int, Int), mk_pi("y", Int, Int), false); - local_context lctx1{mk_lift(0, 1), mk_inst(0, Const("a"))}; - local_context lctx2{mk_lift(0, 1), mk_inst(0, Const("b"))}; - local_context lctx3{mk_lift(3, 1), mk_inst(0, Const("a"))}; - local_context lctx4{mk_lift(0, 1), mk_inst(0, Const("a")), mk_inst(0, Const("b"))}; - local_context lctx5{mk_inst(0, Const("a")), mk_inst(0, Const("a"))}; - lt(mk_metavar("a", lctx1), mk_metavar("b", lctx1), true); - lt(mk_metavar("a", lctx1), mk_metavar("a", lctx2), true); - lt(mk_metavar("a", lctx1), mk_metavar("a", lctx3), true); - lt(mk_metavar("a", lctx1), mk_metavar("a", lctx4), true); - lt(mk_metavar("a", lctx1), mk_metavar("a", lctx5), true); - lt(mk_metavar("a", lctx1), mk_metavar("a", lctx1), false); } int main() { diff --git a/src/tests/library/max_sharing.cpp b/src/tests/library/max_sharing.cpp index eb0ff6936..f0bf94f86 100644 --- a/src/tests/library/max_sharing.cpp +++ b/src/tests/library/max_sharing.cpp @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include "util/test.h" #include "kernel/abstract.h" #include "kernel/max_sharing.h" -#include "library/printer.h" using namespace lean; static void tst1() { @@ -21,24 +20,16 @@ static void tst1() { expr N = Const("N"); expr F1, F2; F1 = f(Fun({x, N}, f(x, x)), Fun({y, N}, f(y, y))); - lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2))); + lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1))); F2 = max_fn(F1); std::cout << F2 << "\n"; - lean_assert(is_eqp(arg(F2, 1), arg(F2, 2))); + lean_assert(is_eqp(app_arg(app_fn(F2)), app_arg(F2))); max_fn.clear(); - local_context lctx{mk_lift(1, 1), mk_inst(0, a1)}; - expr m1 = mk_metavar("m1", lctx); - expr m2 = mk_metavar("m1", lctx); - F1 = f(m1, m2); - lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2))); + F1 = f(Let(x, Type, f(a1), f(x, x)), Let(y, Type, f(a1), f(y, y))); + lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1))); F2 = max_fn(F1); std::cout << F2 << "\n"; - lean_assert(is_eqp(arg(F2, 1), arg(F2, 2))); - F1 = f(Let({x, f(a1)}, f(x, x)), Let({y, f(a1)}, f(y, y))); - lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2))); - F2 = max_fn(F1); - std::cout << F2 << "\n"; - lean_assert(is_eqp(arg(F2, 1), arg(F2, 2))); + lean_assert(is_eqp(app_arg(app_fn(F2)), app_arg(F2))); } int main() {