diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index e2ad2c063..f4fdcf38a 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -4,6 +4,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp normalize.cpp shared_environment.cpp module.cpp coercion.cpp private.cpp placeholder.cpp aliases.cpp scope.cpp level_names.cpp update_declaration.cpp) -# fo_unify.cpp hop_match.cpp) +# hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index b8e290730..cfde1f1bb 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -7,30 +7,18 @@ add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr) add_executable(max_sharing max_sharing.cpp) target_link_libraries(max_sharing ${EXTRA_LIBS}) add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing) -# add_executable(threads threads.cpp) -# target_link_libraries(threads ${EXTRA_LIBS}) -# add_test(threads ${CMAKE_CURRENT_BINARY_DIR}/threads) -# set_tests_properties(threads PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") add_executable(free_vars free_vars.cpp) target_link_libraries(free_vars ${EXTRA_LIBS}) add_test(free_vars ${CMAKE_CURRENT_BINARY_DIR}/free_vars) add_executable(replace replace.cpp) target_link_libraries(replace ${EXTRA_LIBS}) add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace) -# add_executable(type_checker type_checker.cpp) -# target_link_libraries(type_checker ${EXTRA_LIBS}) -# add_test(type_checker ${CMAKE_CURRENT_BINARY_DIR}/type_checker) -# set_tests_properties(type_checker PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") add_executable(environment environment.cpp) target_link_libraries(environment ${EXTRA_LIBS}) add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment) add_executable(metavar metavar.cpp) target_link_libraries(metavar ${EXTRA_LIBS}) add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) -# set_tests_properties(metavar PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") add_executable(instantiate instantiate.cpp) target_link_libraries(instantiate ${EXTRA_LIBS}) add_test(instantiate ${CMAKE_CURRENT_BINARY_DIR}/instantiate) -# add_executable(universe_constraints universe_constraints.cpp) -# target_link_libraries(universe_constraints ${EXTRA_LIBS}) -# add_test(universe_constraints ${CMAKE_CURRENT_BINARY_DIR}/universe_constraints) diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp deleted file mode 100644 index 072d7770f..000000000 --- a/src/tests/kernel/threads.cpp +++ /dev/null @@ -1,72 +0,0 @@ -/* -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 -#include "util/thread.h" -#include "util/test.h" -#include "kernel/expr.h" -#include "kernel/free_vars.h" -#include "kernel/abstract.h" -#include "kernel/normalizer.h" -#include "kernel/max_sharing.h" -#include "library/io_state_stream.h" -#include "library/deep_copy.h" -#include "library/arith/arith.h" -#include "frontends/lean/frontend.h" -#include "frontends/lua/register_modules.h" -using namespace lean; - -expr norm(expr const & e, environment & env) { - env->add_var("a", Int); - env->add_var("b", Int); - env->add_var("f", Int >> (Int >> Int)); - env->add_var("h", Int >> (Int >> Int)); - return normalize(e, env); -} - -static void mk(expr const & a) { - environment env; init_test_frontend(env); - expr b = Const("b"); - for (unsigned i = 0; i < 100; i++) { - expr h = Const("h"); - h = h(a); - for (unsigned j = 0; j < 100; j++) - h = mk_app(h, b); - h = max_sharing(h); - lean_assert(closed(h)); - environment env2 = env->mk_child(); - h = norm(h, env2); - h = abstract(h, a); - lean_assert(!closed(h)); - h = deep_copy(h); - } -} - -static void tst1() { - expr a = Const("a"); - expr f = Const("f"); - a = f(a, a); - std::vector ts; - - #if defined(LEAN_MULTI_THREAD) - for (unsigned i = 0; i < 8; i++) { - ts.push_back(thread([&](){ save_stack_info(); mk(a); })); - } - for (unsigned i = 0; i < 8; i++) { - ts[i].join(); - std::cout << "finished " << i << "\n"; - } - #else - mk(a); - #endif -} - -int main() { - save_stack_info(); - register_modules(); - tst1(); - return 0; -} diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp deleted file mode 100644 index 86d9a65af..000000000 --- a/src/tests/kernel/type_checker.cpp +++ /dev/null @@ -1,528 +0,0 @@ -/* -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 -#include -#include "util/thread.h" -#include "util/test.h" -#include "util/trace.h" -#include "util/exception.h" -#include "util/interrupt.h" -#include "util/timeit.h" -#include "kernel/type_checker.h" -#include "kernel/environment.h" -#include "kernel/abstract.h" -#include "kernel/kernel.h" -#include "kernel/normalizer.h" -#include "kernel/kernel_exception.h" -#include "kernel/type_checker_justification.h" -#include "kernel/io_state.h" -#include "library/printer.h" -#include "library/io_state_stream.h" -#include "library/arith/arith.h" -#include "frontends/lean/frontend.h" -#include "frontends/lua/register_modules.h" -using namespace lean; - -expr c(char const * n) { return mk_constant(n); } - -static void tst1() { - environment env; - expr t0 = Type(); - std::cout << type_check(t0, env) << "\n"; - lean_assert(type_check(t0, env) == Type(level()+1)); - expr f = mk_pi("_", t0, t0); - std::cout << type_check(f, env) << "\n"; - lean_assert(type_check(f, env) == Type(level()+1)); - level u = env->add_uvar_cnstr("u", level() + 1); - level v = env->add_uvar_cnstr("v", level() + 1); - expr g = mk_pi("_", Type(u), Type(v)); - std::cout << type_check(g, env) << "\n"; - lean_assert(type_check(g, env) == Type(max(u+1, v+1))); - std::cout << type_check(Type(u), env) << "\n"; - lean_assert(type_check(Type(u), env) == Type(u+1)); - std::cout << type_check(mk_lambda("x", Type(u), Var(0)), env) << "\n"; - lean_assert(type_check(mk_lambda("x", Type(u), Var(0)), env) == mk_pi("_", Type(u), Type(u))); - std::cout << type_check(mk_lambda("Nat", Type(), mk_lambda("n", Var(0), Var(0))), env) << "\n"; - expr nat = c("nat"); - expr T = Fun("nat", Type(), - Fun("+", mk_arrow(nat, mk_arrow(nat, nat)), - Fun("m", nat, mk_app({c("+"), c("m"), c("m")})))); - std::cout << T << "\n"; - std::cout << type_check(T, env) << "\n"; - std::cout << Pi("nat", Type(), mk_arrow(mk_arrow(nat, mk_arrow(nat, nat)), mk_arrow(nat, nat))) << "\n"; - lean_assert(type_check(T, env) == Pi("nat", Type(), mk_arrow(mk_arrow(nat, mk_arrow(nat, nat)), mk_arrow(nat, nat)))); -} - -static void tst2() { - try{ - environment env; - level l1 = env->add_uvar_cnstr("l1", level() + 1); - expr t0 = Type(); - expr t1 = Type(l1); - expr F = - Fun("Nat", t0, - Fun("Vec", mk_arrow(c("Nat"), t0), - Fun("n", c("Nat"), - Fun("len", mk_arrow(mk_app({c("Vec"), c("n")}), c("Nat")), - Fun("v", mk_app({c("Vec"), c("n")}), - mk_app({c("len"), c("v")})))))); - std::cout << F << "\n"; - std::cout << type_check(F, env) << "\n"; - } - catch (exception & ex) { - std::cout << "Error: " << ex.what() << "\n"; - } -} - -static void tst3() { - environment env; - init_test_frontend(env); - expr f = Fun("a", Bool, mk_eq(Bool, Const("a"), True)); - std::cout << type_check(f, env) << "\n"; - lean_assert(type_check(f, env) == mk_arrow(Bool, Bool)); - expr t = mk_let("a", none_expr(), True, Var(0)); - std::cout << type_check(t, env) << "\n"; -} - -static void tst4() { - environment env; - init_test_frontend(env); - expr a = mk_eq(Int, iVal(1), iVal(2)); - expr pr = mk_lambda("x", a, Var(0)); - std::cout << type_check(pr, env) << "\n"; -} - -static void tst5() { - environment env; - init_test_frontend(env); - env->add_var("P", Bool); - expr P = Const("P"); - expr H = Const("H"); - unsigned n = 4000; - expr prop = P; - expr pr = H; - for (unsigned i = 1; i < n; i++) { - pr = mk_and_intro_th(P, prop, H, pr); - prop = And(P, prop); - } -} - -static void tst6() { - environment env; - init_test_frontend(env); - expr A = Const("A"); - expr f = Const("f"); - expr x = Const("x"); - expr t = Fun({A, Type()}, Fun({f, mk_arrow(Int, A)}, Fun({x, Int}, f(x, x)))); - try { - type_check(t, env); - lean_unreachable(); - } catch (exception & ex) { - std::cout << "Error: " << ex.what() << "\n"; - } -} - -static void tst7() { - environment env; - init_test_frontend(env); - expr A = Const(name{"foo", "bla", "bla", "foo"}); - expr f = Const("f"); - expr x = Const("x"); - expr t = Fun({A, Type()}, Fun({f, mk_arrow(Int, mk_arrow(A, mk_arrow(A, mk_arrow(A, mk_arrow(A, mk_arrow(A, A))))))}, Fun({x, Int}, f(x, x)))); - try { - type_check(t, env); - lean_unreachable(); - } catch (exception & ex) { - std::cout << "Error: " << ex.what() << "\n"; - } -} - -static void tst8() { - environment env; - init_test_frontend(env); - env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); - env->add_var("x", Int); - expr P = Const("P"); - context c; - c = extend(c, "P", mk_arrow(Bool, Bool)); - c = extend(c, "P", mk_arrow(Int, Int)); - c = extend(c, "H", Var(1)(True)); - c = extend(c, "x", Bool); - expr t = P(Const("x"), Var(0)); - try { - type_check(t, env, c); - lean_unreachable(); - } catch (exception & ex) { - std::cout << "Error: " << ex.what() << "\n"; - } -} - -static void tst9() { - environment env; - init_test_frontend(env); - env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); - env->add_var("x", Int); - expr P = Const("P"); - context c; - c = extend(c, "P", mk_arrow(Bool, Bool)); - c = extend(c, "P", Bool, Var(0)(True)); - c = extend(c, "H", Var(1)(True)); - c = extend(c, "x", Bool); - expr t = P(Const("x"), Var(0)); - try { - type_check(t, env, c); - lean_unreachable(); - } catch (exception & ex) { - std::cout << "Error: " << ex.what() << "\n"; - } -} - -static void tst10() { - environment env; - init_test_frontend(env); - env->add_var("f", mk_arrow(Int, Int)); - env->add_var("b", Int); - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr t1 = Let({{a, f(b)}, {a, f(a)}}, f(a)); - expr t2 = f(f(f(b))); - std::cout << t1 << " --> " << normalize(t1, env) << "\n"; - expr prop = mk_eq(Int, t1, t2); - expr proof = mk_refl_th(Int, t1); - env->add_theorem("simp_eq", prop, proof); - std::cout << env->get_object("simp_eq").get_name() << "\n"; -} - -static void tst11() { - environment env; - init_test_frontend(env); - env->add_var("f", Int >> (Int >> Int)); - env->add_var("a", Int); - unsigned n = 1000; - expr f = Const("f"); - expr a = Const("a"); - expr t1 = f(a, a); - expr b = Const("a"); - expr t2 = f(a, a); - expr t3 = f(b, b); - for (unsigned i = 0; i < n; i++) { - t1 = f(t1, t1); - t2 = mk_let("x", none_expr(), t2, f(Var(0), Var(0))); - t3 = f(t3, t3); - } - lean_assert(t1 != t2); - env->add_theorem("eqs1", mk_eq(Int, t1, t2), mk_refl_th(Int, t1)); - env->add_theorem("eqs2", mk_eq(Int, t1, t3), mk_refl_th(Int, t1)); -} - -static expr mk_big(unsigned depth) { - if (depth == 0) - return Const("a"); - else - return Const("f")(mk_big(depth - 1), mk_big(depth - 1)); -} - -static void tst12() { -#if defined(LEAN_MULTI_THREAD) - expr t = mk_big(18); - environment env; - init_test_frontend(env); - env->add_var("f", Int >> (Int >> Int)); - env->add_var("a", Int); - type_checker checker(env); - chrono::milliseconds dura(100); - interruptible_thread thread([&]() { - try { - std::cout << checker.check(t) << "\n"; - // Remark: if the following code is reached, we - // should decrease dura. - lean_unreachable(); - } catch (interrupted & it) { - std::cout << "interrupted\n"; - } - }); - this_thread::sleep_for(dura); - thread.request_interrupt(); - thread.join(); -#endif -} - -static void tst13() { - environment env; - init_test_frontend(env); - env->add_var("f", Type() >> Type()); - expr f = Const("f"); - std::cout << type_check(f(Bool), env) << "\n"; - std::cout << type_check(f(mk_eq(Bool, True, False)), env) << "\n"; -} - -static void tst14() { - environment env; - init_test_frontend(env); - expr f = Const("f"); - expr a = Const("a"); - env->add_var("f", Int >> Int); - env->add_var("a", Real); - expr F = f(a); - type_checker checker(env); - formatter fmt = mk_simple_formatter(); - io_state st(options(), fmt); - try { - std::cout << checker.check(F) << "\n"; - } catch (kernel_exception & ex) { - regular(st) << ex << "\n"; - } -} - -static void tst15() { - environment env; - init_test_frontend(env); - context ctx1, ctx2; - expr A = Const("A"); - expr vec1 = Const("vec1"); - expr vec2 = Const("vec2"); - env->add_var("vec1", Int >> (Type() >> Type())); - env->add_var("vec2", Real >> (Type() >> Type())); - ctx1 = extend(ctx1, "x", Int, iVal(1)); - ctx1 = extend(ctx1, "f", Pi({A, Int}, vec1(A, Int))); - ctx2 = extend(ctx2, "x", Real, rVal(2)); - ctx2 = extend(ctx2, "f", Pi({A, Real}, vec2(A, Real))); - expr F = Var(0)(Var(1)); - expr F_copy = F; - type_checker checker(env); - std::cout << checker.check(F, ctx1) << "\n"; - lean_assert_eq(checker.check(F, ctx1), vec1(Var(1), Int)); - lean_assert_eq(checker.check(F, ctx2), vec2(Var(1), Real)); - // Disable for now - // lean_assert(is_eqp(checker.check(F, ctx2), checker.check(F, ctx2))); - // lean_assert(is_eqp(checker.check(F, ctx1), checker.check(F, ctx1))); - expr r = checker.check(F, ctx1); - checker.clear(); - lean_assert(!is_eqp(r, checker.check(F, ctx1))); - r = checker.check(F, ctx1); - // lean_assert(is_eqp(r, checker.check(F, ctx1))); -} - -static void check_justification_msg(justification const & t, char const * expected) { - formatter fmt = mk_simple_formatter(); - options opts; - opts = opts.update({"pp", "indent"}, 2); - format r = t.pp(fmt, opts); - std::cout << r << "\n"; - std::ostringstream strm; - strm << r; - lean_assert_eq(strm.str(), std::string(expected)); -} - -static void tst16() { - std::cout << "Testing type checker justification objects\n"; - context ctx; - expr f = Const("f"); - expr a = Const("a"); - expr x = Var(0); - ctx = extend(ctx, "x", Const("N")); - check_justification_msg(mk_function_expected_justification(ctx, f(a, x)), "Function expected at\n f a x#0"); - check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x#1"); - check_justification_msg(mk_type_expected_justification(ctx, Pi({a, Const("N")}, Var(1)(a))), "Type expected at\n Pi a : N, (x#1 a#0)"); - check_justification_msg(mk_app_type_match_justification(ctx, f(a, x), 1), "Type of argument 1 must be convertible to the expected type in the application of\n f\nwith arguments:\n a\n x#0"); - check_justification_msg(mk_max_type_justification(ctx, Pi({a, Const("N")}, Var(1))), "Type expected at\n N -> x#1"); - check_justification_msg(mk_def_type_match_justification(ctx, "foo", f(a, x)), "Type of definition 'foo' must be convertible to expected type."); -} - -static void f1(type_checker & tc, expr const & F) { - metavar_env menv; - expr m1 = menv->mk_metavar(context(), some_expr(Bool >> Int)); - expr r = tc.check(F, context(), menv); - lean_assert_eq(r, Int); -} - -static void f2(type_checker & tc, expr const & F) { - metavar_env menv; - expr m1 = menv->mk_metavar(context(), some_expr(Bool >> Bool)); - expr r = tc.check(F, context(), menv); - lean_assert_eq(r, Bool); -} - -static void tst17() { - environment env; - init_test_frontend(env); - type_checker tc(env); - expr A = Const("A"); - expr F; - { - metavar_env menv; - expr m1 = menv->mk_metavar(); - F = m1(True); - } - expr F2 = F; - f1(tc, F); - f2(tc, F); -} - -static std::ostream & operator<<(std::ostream & out, buffer const & uc) { - formatter fmt = mk_simple_formatter(); - for (auto c : uc) { - out << c.pp(fmt, options(), nullptr, true) << "\n"; - } - return out; -} - -static void tst18() { - environment env; - init_test_frontend(env); - type_inferer type_of(env); - expr f = Const("f"); - expr g = Const("g"); - expr a = Const("a"); - expr b = Const("b"); - expr A = Const("A"); - env->add_var("f", Int >> (Int >> Int)); - lean_assert(type_of(f(a, a)) == Int); - lean_assert(type_of(f(a)) == Int >> Int); - lean_assert(is_bool(type_of(And(a, f(a))))); - lean_assert(type_of(Fun({a, Int}, mk_Int_add(a, iVal(1)))) == Int >> Int); - lean_assert(type_of(Let({a, iVal(10)}, mk_Int_add(a, b))) == Int); - lean_assert(type_of(Type()) == Type(level() + 1)); - lean_assert(type_of(Bool) == Type()); - lean_assert(type_of(Pi({a, Type()}, Type(level() + 2))) == Type(level() + 3)); - lean_assert(type_of(Pi({a, Type(level()+4)}, Type(level() + 2))) == Type(level() + 5)); - lean_assert(type_of(Pi({a, Int}, Bool)) == Type()); - env->add_var("g", Pi({A, Type()}, A >> A)); - lean_assert(type_of(g(Int, a)) == Int); - lean_assert(type_of(g(Fun({a, Type()}, a)(Int), a)) == Fun({a, Type()}, a)(Int)); -} - -static expr mk_big(unsigned val, unsigned depth) { - if (depth == 0) - return iVal(val); - else - return mk_Int_add(mk_big(val*2, depth-1), mk_big(val*2 + 1, depth-1)); -} - -static void tst19() { - environment env; - init_test_frontend(env); - type_inferer type_of(env); - type_checker type_of_slow(env); - expr t = mk_big(0, 10); - { - timeit timer(std::cout, "light checker 10000 calls"); - for (unsigned i = 0; i < 10000; i++) { - type_of(t); - type_of.clear(); - } - } - { - timeit timer(std::cout, "type checker 300 calls"); - for (unsigned i = 0; i < 300; i++) { - type_of_slow.check(t); - type_of_slow.clear(); - } - } -} - -static void tst20() { - environment env; - init_test_frontend(env); - context ctx1, ctx2; - expr A = Const("A"); - expr vec1 = Const("vec1"); - expr vec2 = Const("vec2"); - env->add_var("vec1", Int >> (Type() >> Type())); - env->add_var("vec2", Real >> (Type() >> Type())); - ctx1 = extend(ctx1, "x", Int, iVal(1)); - ctx1 = extend(ctx1, "f", Pi({A, Int}, vec1(A, Int))); - ctx2 = extend(ctx2, "x", Real, rVal(2)); - ctx2 = extend(ctx2, "f", Pi({A, Real}, vec2(A, Real))); - expr F = Var(0)(Var(1)); - expr F_copy = F; - type_inferer infer(env); - std::cout << infer(F, ctx1) << "\n"; - lean_assert_eq(infer(F, ctx1), vec1(Var(1), Int)); - lean_assert_eq(infer(F, ctx2), vec2(Var(1), Real)); - lean_assert(is_eqp(infer(F, ctx2), infer(F, ctx2))); - lean_assert(is_eqp(infer(F, ctx1), infer(F, ctx1))); - expr r = infer(F, ctx1); - infer.clear(); - lean_assert(!is_eqp(r, infer(F, ctx1))); - r = infer(F, ctx1); - lean_assert(is_eqp(r, infer(F, ctx1))); -} - -static void tst21() { - environment env; - init_test_frontend(env); - metavar_env menv; - buffer uc; - type_inferer inferer(env); - expr list = Const("list"); - expr nil = Const("nil"); - expr cons = Const("cons"); - expr A = Const("A"); - env->add_var("list", Type() >> Type()); - env->add_var("nil", Pi({A, Type()}, list(A))); - env->add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); - env->add_var("a", Int); - env->add_var("b", Int); - env->add_var("n", Nat); - env->add_var("m", Nat); - expr a = Const("a"); - expr b = Const("b"); - expr n = Const("n"); - expr m = Const("m"); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr A1 = menv->mk_metavar(); - expr A2 = menv->mk_metavar(); - expr A3 = menv->mk_metavar(); - expr A4 = menv->mk_metavar(); - expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4)))); - std::cout << F << "\n"; - std::cout << inferer(F, context(), menv, uc) << "\n"; - std::cout << uc << "\n"; -} - -static void tst22() { - environment env; - init_test_frontend(env); - expr a = mk_arrow(Nat, Bool); - expr b = mk_arrow(Nat, Nat); - type_checker tc(env); - lean_assert(!tc.is_convertible(a, b)); - lean_assert(!tc.is_convertible(b, a)); -} - -int main() { - save_stack_info(); - register_modules(); - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - tst6(); - tst7(); - tst8(); - tst9(); - tst10(); - tst11(); - tst12(); - tst13(); - tst14(); - tst15(); - tst16(); - tst17(); - tst18(); - tst19(); - return has_violations() ? 1 : 0; - tst20(); - tst21(); - tst22(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/kernel/universe_constraints.cpp b/src/tests/kernel/universe_constraints.cpp deleted file mode 100644 index d7bb9399f..000000000 --- a/src/tests/kernel/universe_constraints.cpp +++ /dev/null @@ -1,47 +0,0 @@ -/* -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/universe_constraints.h" -using namespace lean; - -static void tst1() { - universe_constraints uc; - name a("a"), b("b"), c("c"), d("d"); - uc.add_var(a); uc.add_var(b); uc.add_var(c); uc.add_var(d); - lean_assert(*(uc.get_distance(a, a)) == 0); - lean_assert(!uc.get_distance(a, b)); - uc.add_constraint(a, b, 1); - lean_assert(uc.is_consistent(a, b, 1)); - lean_assert(*(uc.get_distance(a, b)) == 1); - uc.add_constraint(a, c, 1); - lean_assert(uc.is_consistent(b, c, 1)); - lean_assert(*(uc.get_distance(a, c)) == 1); - lean_assert(uc.is_implied(a, c, 1)); - lean_assert(!uc.is_implied(a, c, 2)); - lean_assert(uc.is_implied(a, c, 0)); - lean_assert(!uc.is_implied(b, c, 0)); - lean_assert(!uc.is_implied(a, d, 3)); - lean_assert(uc.is_consistent(a, d, 2)); - lean_assert(uc.is_consistent(c, d, 1)); - uc.add_constraint(c, d, 1); - lean_assert(*(uc.get_distance(a, d)) == 2); - lean_assert(uc.is_implied(a, d, 2)); - lean_assert(!uc.is_implied(a, d, 3)); - uc.add_constraint(b, d, 2); - lean_assert(*(uc.get_distance(a, d)) == 3); - lean_assert(uc.is_implied(a, d, 3)); - lean_assert(!uc.is_consistent(d, a, 0)); - lean_assert(!uc.is_consistent(d, a, -2)); - lean_assert(uc.is_consistent(d, a, -3)); -} - -int main() { - save_stack_info(); - tst1(); - return has_violations() ? 1 : 0; -} - diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 51b9b168d..337534ff5 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,6 +1,3 @@ -# add_executable(formatter formatter.cpp) -# target_link_libraries(formatter ${EXTRA_LIBS}) -# add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter) add_executable(expr_lt expr_lt.cpp) target_link_libraries(expr_lt ${EXTRA_LIBS}) add_test(expr_lt ${CMAKE_CURRENT_BINARY_DIR}/expr_lt) @@ -10,10 +7,3 @@ add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy) add_executable(occurs occurs.cpp) target_link_libraries(occurs ${EXTRA_LIBS}) add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) -# 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/formatter.cpp b/src/tests/library/formatter.cpp deleted file mode 100644 index 8775deb37..000000000 --- a/src/tests/library/formatter.cpp +++ /dev/null @@ -1,46 +0,0 @@ -/* -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 -#include -#include "util/test.h" -#include "kernel/environment.h" -#include "kernel/abstract.h" -#include "kernel/formatter.h" -#include "kernel/kernel.h" -#include "library/printer.h" -using namespace lean; - -static void check(format const & f, char const * expected) { - std::ostringstream strm; - strm << f; - std::cout << strm.str() << "\n"; - lean_assert_eq(strm.str(), expected); -} - -static void tst1() { - environment env; - env->add_var("N", Type()); - formatter fmt = mk_simple_formatter(); - check(fmt(env), "variable N : Type\n"); - expr f = Const("f"); - expr a = Const("a"); - expr x = Const("x"); - expr y = Const("y"); - expr N = Const("N"); - check(fmt(env->get_object("N")), "variable N : Type"); - context ctx; - ctx = extend(ctx, "x", f(a)); - ctx = extend(ctx, "y", f(Var(0), N >> N)); - check(fmt(ctx, f(Var(0), Var(2))), "f y#0 #2"); - check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x#0 (N -> N)] |- f y#0 #2"); -} - -int main() { - save_stack_info(); - tst1(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/library/update_expr.cpp b/src/tests/library/update_expr.cpp deleted file mode 100644 index 339b0f74e..000000000 --- a/src/tests/library/update_expr.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/* -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 "kernel/update_expr.h" -using namespace lean; - -static void tst1() { - expr a = Const("a"); - expr b = Const("b"); -} - -static void tst2() { - expr a = Const("a"); - expr N = Const("N"); - expr t1 = Fun(a, N, a); - expr b = Const("b"); - expr t2 = update_abstraction(t1, N, abst_body(t1)); - lean_assert(is_eqp(t1, t2)); - t2 = update_abstraction(t1, N, a); - lean_assert(!is_eqp(t1, t2)); - lean_assert(abst_body(t2) == a); - t1 = Pi(a, N, a); - t2 = update_abstraction(t1, N, abst_body(t1)); - lean_assert(is_eqp(t1, t2)); -} - -void tst3() { - expr a = Const("a"); - expr b = Const("b"); - expr f = Const("f"); - expr t1 = Let(a, b, f(a)); - expr t2 = update_let(t1, none_expr(), b, let_body(t1)); - lean_assert(is_eqp(t1, t2)); - t2 = update_let(t1, none_expr(), a, let_body(t1)); - lean_assert(!is_eqp(t1, t2)); - lean_assert(t2 == Let(a, a, f(a))); -} - -int main() { - save_stack_info(); - tst1(); - tst2(); - tst3(); - return has_violations() ? 1 : 0; -}