michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

chore(tests/library): enable old tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-22 12:05:49 -07:00
parent ad43d9177b
commit 3b78af0db5
5 changed files with 19 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -246,7 +246,7 @@ add_subdirectory(tests/util)
add_subdirectory(tests/util/numerics) add_subdirectory(tests/util/numerics)
add_subdirectory(tests/util/interval) add_subdirectory(tests/util/interval)
add_subdirectory(tests/kernel) add_subdirectory(tests/kernel)
# add_subdirectory(tests/library) add_subdirectory(tests/library)
# add_subdirectory(tests/library/rewriter) # add_subdirectory(tests/library/rewriter)
# add_subdirectory(tests/library/tactic) # add_subdirectory(tests/library/tactic)
# add_subdirectory(tests/library/elaborator) # add_subdirectory(tests/library/elaborator)

20
src/tests/library/CMakeLists.txt
View file

@ -1,6 +1,6 @@
add_executable(formatter formatter.cpp) # add_executable(formatter formatter.cpp)
target_link_libraries(formatter ${EXTRA_LIBS}) # target_link_libraries(formatter ${EXTRA_LIBS})
add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter) # add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter)
add_executable(max_sharing max_sharing.cpp) add_executable(max_sharing max_sharing.cpp)
target_link_libraries(max_sharing ${EXTRA_LIBS}) target_link_libraries(max_sharing ${EXTRA_LIBS})
add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing) 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) add_executable(deep_copy deep_copy.cpp)
target_link_libraries(deep_copy ${EXTRA_LIBS}) target_link_libraries(deep_copy ${EXTRA_LIBS})
add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy) add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
add_executable(arith_tst arith.cpp) # add_executable(arith_tst arith.cpp)
target_link_libraries(arith_tst ${EXTRA_LIBS}) # target_link_libraries(arith_tst ${EXTRA_LIBS})
add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst) # add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
set_tests_properties(arith_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") # set_tests_properties(arith_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
add_executable(update_expr update_expr.cpp) # add_executable(update_expr update_expr.cpp)
target_link_libraries(update_expr ${EXTRA_LIBS}) # target_link_libraries(update_expr ${EXTRA_LIBS})
add_test(update_expr ${CMAKE_CURRENT_BINARY_DIR}/update_expr) # add_test(update_expr ${CMAKE_CURRENT_BINARY_DIR}/update_expr)

7
src/tests/library/deep_copy.cpp
View file

@ -14,11 +14,10 @@ static void tst1() {
expr f = Const("f"); expr f = Const("f");
expr a = Const("a"); expr a = Const("a");
expr x = Var(0); expr x = Var(0);
expr t = Type(); expr t = Type;
expr z = Const("z"); expr z = Const("z");
local_context lctx{mk_lift(0, 1), mk_inst(0, a)}; expr m = mk_metavar("a", Type);
expr m = mk_metavar("a", lctx); 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 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 G = deep_copy(F); expr G = deep_copy(F);
lean_assert(F == G); lean_assert(F == G);
lean_assert(!is_eqp(F, G)); lean_assert(!is_eqp(F, G));

41
src/tests/library/expr_lt.cpp
View file

@ -6,11 +6,7 @@ Author: Leonardo de Moura
*/ */
#include "util/test.h" #include "util/test.h"
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "kernel/kernel.h"
#include "library/expr_lt.h" #include "library/expr_lt.h"
#include "library/arith/nat.h"
#include "library/arith/int.h"
#include "library/arith/real.h"
using namespace lean; using namespace lean;
static void lt(expr const & e1, expr const & e2, bool expected) { 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() { 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(0), false);
lt(Var(0), Var(1), true); 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("b"), true);
lt(Const("a"), Const("a"), false); lt(Const("a"), Const("a"), false);
lt(Var(1), Const("a"), true); 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("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(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(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() { int main() {

19
src/tests/library/max_sharing.cpp
View file

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#include "util/test.h" #include "util/test.h"
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "kernel/max_sharing.h" #include "kernel/max_sharing.h"
#include "library/printer.h"
using namespace lean; using namespace lean;
static void tst1() { static void tst1() {
@ -21,24 +20,16 @@ static void tst1() {
expr N = Const("N"); expr N = Const("N");
expr F1, F2; expr F1, F2;
F1 = f(Fun({x, N}, f(x, x)), Fun({y, N}, f(y, y))); 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); F2 = max_fn(F1);
std::cout << F2 << "\n"; 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(); max_fn.clear();
local_context lctx{mk_lift(1, 1), mk_inst(0, a1)}; F1 = f(Let(x, Type, f(a1), f(x, x)), Let(y, Type, f(a1), f(y, y)));
expr m1 = mk_metavar("m1", lctx); lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1)));
expr m2 = mk_metavar("m1", lctx);
F1 = f(m1, m2);
lean_assert(!is_eqp(arg(F1, 1), arg(F1, 2)));
F2 = max_fn(F1); F2 = max_fn(F1);
std::cout << F2 << "\n"; 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)));
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)));
} }
int main() { int main() {