diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp index 34d4d65e8..cb7dedc8a 100644 --- a/src/kernel/context.cpp +++ b/src/kernel/context.cpp @@ -19,4 +19,11 @@ std::pair const & lookup(context const & c, unsigned i) { } throw exception("unknown free variable"); } +optional> find(context const & c, unsigned i) { + try { + return optional>(lookup(c, i)); + } catch (exception &) { + return optional>(); + } +} } diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index 4c4bcc26d..ca094ec61 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -15,12 +15,12 @@ add_test(diff_cnstrs ${CMAKE_CURRENT_BINARY_DIR}/diff_cnstrs) # 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(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) @@ -29,9 +29,9 @@ add_test(diff_cnstrs ${CMAKE_CURRENT_BINARY_DIR}/diff_cnstrs) # target_link_libraries(environment ${EXTRA_LIBS}) # add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment) # set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") -# add_executable(occurs occurs.cpp) -# target_link_libraries(occurs ${EXTRA_LIBS}) -# add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) +add_executable(occurs occurs.cpp) +target_link_libraries(occurs ${EXTRA_LIBS}) +add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs) # add_executable(metavar metavar.cpp) # target_link_libraries(metavar ${EXTRA_LIBS}) # add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar) diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp index e851928e1..710744d87 100644 --- a/src/tests/kernel/free_vars.cpp +++ b/src/tests/kernel/free_vars.cpp @@ -7,8 +7,6 @@ Author: Leonardo de Moura #include "util/test.h" #include "kernel/free_vars.h" #include "kernel/abstract.h" -#include "kernel/metavar.h" -#include "kernel/kernel.h" using namespace lean; static void tst1() { @@ -39,7 +37,7 @@ static void tst2() { expr B = Const("Bool"); expr t = Fun({x, B}, Fun({y, B}, x)); lean_assert(closed(t)); - lean_assert(!closed(abst_body(t))); + lean_assert(!closed(binder_body(t))); } static void tst3() { @@ -55,105 +53,14 @@ static void tst3() { bool flag = true; while (is_lambda(r)) { flag = flag && closed(r); - r = abst_body(r); + r = binder_body(r); } } -static void tst4() { - metavar_env menv; - auto fn = [&](expr const & e) { return free_var_range(e, menv); }; - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr x = Const("x"); - expr m1 = menv->mk_metavar(); - lean_assert(fn(m1) == 0); - lean_assert(fn(Var(0)) == 1); - lean_assert(fn(Var(0)(Var(2), Var(1))) == 3); - lean_assert(fn(Type()) == 0); - lean_assert(fn(Bool) == 0); - lean_assert(fn(Fun({x, Type()}, Var(0))) == 0); - lean_assert(fn(Fun({x, Var(0)}, Var(0))) == 1); - lean_assert(fn(Fun({x, Var(0)}, Var(2))) == 2); - lean_assert(fn(Pi({x, Type()}, Var(0))) == 0); - lean_assert(fn(Pi({x, Var(0)}, Var(0))) == 1); - lean_assert(fn(Pi({x, Var(0)}, Var(2))) == 2); - context ctx; - ctx = extend(ctx, name("x"), Bool); - ctx = extend(ctx, name("y"), Bool); - expr m2 = menv->mk_metavar(ctx); - lean_assert_eq(fn(m2), 2); - lean_assert_eq(fn(add_lift(m2, 3, 5)), 2); - lean_assert_eq(fn(add_lift(m2, 2, 5)), 2); - lean_assert_eq(fn(add_lift(m2, 1, 5)), 7); - lean_assert_eq(fn(add_inst(m2, 3, Var(10))), 2); - lean_assert_eq(fn(add_inst(m2, 1, Var(10))), 11); - // Here is the explanation for the following assertion. - // If m2 is assigned to #1, that m2[1:f(#2)] becomes f(#2), - // and then lift:2:2 transforms it to f(#4) - lean_assert_eq(fn(add_lift(add_inst(m2, 1, f(Var(2))), 2, 2)), 5); - ctx = extend(ctx, name("w"), Bool); - ctx = extend(ctx, name("z"), Bool); - expr m3 = menv->mk_metavar(ctx); - lean_assert_eq(fn(m3), 4); - lean_assert_eq(fn(add_lift(add_inst(m3, 1, f(Var(0))), 1, 1)), 4); - lean_assert_eq(fn(add_lift(add_inst(m3, 1, f(Var(3))), 1, 1)), 5); - lean_assert_eq(fn(mk_let("x", Var(0), Var(1))), 1); - lean_assert_eq(fn(mk_let("x", Var(1), Var(1))), 2); - lean_assert_eq(fn(mk_let("x", Var(2), Var(1), Var(1))), 3); - lean_assert_eq(fn(mk_let("x", Var(2), Var(1), Var(4))), 4); -} - -static void tst5() { - metavar_env menv; - expr m1 = menv->mk_metavar(); - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr t = Const("t"); - expr x = Const("x"); - lean_assert(has_free_var(mk_lambda("x", t, f(Var(1))), 0, menv)); - lean_assert(!has_free_var(mk_lambda("x", t, f(Var(0))), 1, menv)); - lean_assert(!has_free_var(m1, 0, menv)); - lean_assert(!has_free_var(m1, 1, menv)); - context ctx({{"x", Bool}, {"y", Bool}}); - expr m2 = menv->mk_metavar(ctx); - lean_assert(has_free_var(m2, 0, menv)); - lean_assert(has_free_var(m2, 1, menv)); - lean_assert(!has_free_var(m2, 2, menv)); - lean_assert(has_free_var(Fun({x, Bool}, m2), 0, menv)); - lean_assert(!has_free_var(Fun({x, Bool}, m2), 1, menv)); - lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 3), 0, Var(0))), 0, menv)); - lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 1), 0, Var(0))), 0, menv)); - lean_assert(!has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 1), 0, Var(0))), 1, menv)); - lean_assert(has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 1, 3, menv)); - lean_assert(!has_free_var(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 2, 5, menv)); - lean_assert_eq(lower_free_vars(Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0))), 5, 3, menv), - Fun({x, Bool}, add_inst(add_lift(m2, 1, 2), 0, Var(0)))); - lean_assert_eq(lower_free_vars(Fun({x, Bool}, Var(6)(add_inst(add_lift(m2, 1, 2), 0, Var(0)))), 5, 3, menv), - Fun({x, Bool}, Var(3)(add_inst(add_lift(m2, 1, 2), 0, Var(0))))); -} - -static void tst6() { - metavar_env menv; - expr f = Const("f"); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(context({{"x", Bool}, {"y", Bool}})); - lean_assert(lift_free_vars(m1, 0, 1, menv) == m1); - lean_assert(lift_free_vars(m2, 0, 1, menv) != m2); - lean_assert(lift_free_vars(m2, 0, 1, menv) == add_lift(m2, 0, 1)); - lean_assert(lift_free_vars(m1, 0, 1) == add_lift(m1, 0, 1)); - lean_assert(lift_free_vars(f(m1), 0, 1, menv) == f(m1)); - lean_assert(lift_free_vars(f(m2), 0, 1, menv) == f(add_lift(m2, 0, 1))); -} - int main() { save_stack_info(); tst1(); tst2(); tst3(); - tst4(); - tst5(); - tst6(); return has_violations() ? 1 : 0; } diff --git a/src/tests/kernel/instantiate.cpp b/src/tests/kernel/instantiate.cpp index aec6212ff..a42e9d635 100644 --- a/src/tests/kernel/instantiate.cpp +++ b/src/tests/kernel/instantiate.cpp @@ -21,10 +21,10 @@ static void tst1() { expr N = Const("N"); expr F1 = Fun({x, N}, x)(f, a); lean_assert(is_head_beta(F1)); - lean_assert(head_beta_reduce(F1) == f(a)); + 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)); - lean_assert(head_beta_reduce(F2) == f(a, b, c)); + 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)); lean_assert(head_beta_reduce(F3) == f(Fun({y, N}, y)(a), a)); diff --git a/src/tests/kernel/occurs.cpp b/src/tests/kernel/occurs.cpp index deb579e97..a6927f8e1 100644 --- a/src/tests/kernel/occurs.cpp +++ b/src/tests/kernel/occurs.cpp @@ -7,56 +7,23 @@ Author: Leonardo de Moura #include "util/test.h" #include "kernel/occurs.h" #include "kernel/abstract.h" -#include "library/printer.h" using namespace lean; static void tst1() { expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); - expr T = Type(); + expr T = Type; lean_assert(occurs(f, f)); lean_assert(!occurs(a, f)); lean_assert(occurs(a, f(a))); lean_assert(occurs("a", f(a))); lean_assert(!occurs("b", f)); lean_assert(!occurs(a, Fun({a, T}, f(a)))); - context c; - c = extend(c, name("x"), T); - lean_assert(!occurs(f, c)); - lean_assert(occurs(f, c, {a, f(a)})); - lean_assert(occurs(f(a), c, {a, f(a)})); - lean_assert(!occurs(f(b), c, {a, f(a)})); - lean_assert(occurs("f", c, {a, f(a)})); - lean_assert(!occurs(b, c, {a, f(a)})); - c = extend(c, name("y"), T, f(a)); - lean_assert(!occurs("x", c)); - lean_assert(occurs(f, c)); - lean_assert(occurs("f", c)); - c = extend(c, name("z"), T, f(Const("x"))); - lean_assert(occurs("x", c)); - lean_assert(occurs("a", c)); - lean_assert(occurs(f(Const("x")), c)); - lean_assert(!occurs(f(b), c)); -} - -static void tst2() { - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - context c; - c = extend(c, "a", Type()); - std::cout << c; - lean_assert(c.size() == 1); - lean_assert(lookup(c, 0).get_name() == "a"); - auto p = lookup_ext(c, 0); - lean_assert(p.first.get_name() == "a"); - lean_assert(p.second.size() == 0); } int main() { save_stack_info(); tst1(); - tst2(); return has_violations() ? 1 : 0; } diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index 012127929..f9712a525 100644 --- a/src/tests/kernel/replace.cpp +++ b/src/tests/kernel/replace.cpp @@ -11,8 +11,6 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/expr_maps.h" #include "kernel/replace_fn.h" -#include "library/printer.h" -#include "library/deep_copy.h" using namespace lean; expr mk_big(expr f, unsigned depth, unsigned val) { @@ -32,15 +30,15 @@ static void tst1() { } static void tst2() { - expr r = mk_lambda("x", Type(), mk_app({Var(0), Var(1), Var(2)})); + expr r = mk_lambda("x", Type, mk_app({Var(0), Var(1), Var(2)})); std::cout << instantiate_with_closed(r, Const("a")) << std::endl; - lean_assert(instantiate_with_closed(r, Const("a")) == mk_lambda("x", Type(), mk_app({Var(0), Const("a"), Var(1)}))); + lean_assert(instantiate_with_closed(r, Const("a")) == mk_lambda("x", Type, mk_app({Var(0), Const("a"), Var(1)}))); lean_assert(instantiate_with_closed(instantiate_with_closed(r, Const("a")), Const("b")) == - mk_lambda("x", Type(), mk_app({Var(0), Const("a"), Const("b")}))); - std::cout << instantiate_with_closed(abst_body(r), Const("a")) << std::endl; - lean_assert(instantiate_with_closed(abst_body(r), Const("a")) == mk_app({Const("a"), Var(0), Var(1)})); + mk_lambda("x", Type, mk_app({Var(0), Const("a"), Const("b")}))); + std::cout << instantiate_with_closed(binder_body(r), Const("a")) << std::endl; + lean_assert(instantiate_with_closed(binder_body(r), Const("a")) == mk_app({Const("a"), Var(0), Var(1)})); std::cout << instantiate(r, Var(10)) << std::endl; - lean_assert(instantiate(r, Var(10)) == mk_lambda("x", Type(), mk_app({Var(0), Var(11), Var(1)}))); + lean_assert(instantiate(r, Var(10)) == mk_lambda("x", Type, mk_app({Var(0), Var(11), Var(1)}))); std::cout << mk_pi("_", Var(3), Var(4)) << std::endl; std::cout << instantiate(mk_pi("_", Var(3), Var(4)), Var(0)) << std::endl; lean_assert(instantiate(mk_pi("_", Var(3), Var(4)), Var(0)) == mk_pi("_", Var(2), Var(3))); @@ -58,6 +56,16 @@ public: } }; +static expr arg(expr n, unsigned i) { + buffer args; + while (is_app(n)) { + args.push_back(app_arg(n)); + n = app_fn(n); + } + args.push_back(n); + return args[args.size() - i - 1]; +} + static void tst3() { expr f = Const("f"); expr x = Const("x"); @@ -79,9 +87,9 @@ static void tst3() { return x; } }; - replace_fn replacer(proc, tracer(trace)); + replace_fn replacer(proc, tracer(trace)); expr t = Fun({{x, A}, {y, A}}, f(x, f(f(f(x, x), f(y, d)), f(d, d)))); - expr b = abst_body(t); + expr b = binder_body(t); expr r = replacer(b); std::cout << r << "\n"; lean_assert(r == Fun({y, A}, f(c, f(f(f(c, c), f(y, d)), f(d, d))))); @@ -89,14 +97,14 @@ static void tst3() { std::cout << p.first << " --> " << p.second << "\n"; } lean_assert(trace[c] == Var(1)); - std::cout << arg(arg(abst_body(r), 2), 2) << "\n"; - lean_assert(arg(arg(abst_body(r), 2), 2) == f(d, d)); - lean_assert(trace.find(arg(arg(abst_body(r), 2), 2)) == trace.end()); - lean_assert(trace.find(abst_body(r)) != trace.end()); - lean_assert(trace.find(arg(abst_body(r), 2)) != trace.end()); - lean_assert(trace.find(arg(arg(abst_body(r), 2), 1)) != trace.end()); - lean_assert(trace.find(arg(arg(arg(abst_body(r), 2), 1), 1)) != trace.end()); - lean_assert(trace.find(arg(arg(arg(abst_body(r), 2), 1), 2)) == trace.end()); + std::cout << arg(arg(binder_body(r), 2), 2) << "\n"; + lean_assert(arg(arg(binder_body(r), 2), 2) == f(d, d)); + lean_assert(trace.find(arg(arg(binder_body(r), 2), 2)) == trace.end()); + lean_assert(trace.find(binder_body(r)) != trace.end()); + lean_assert(trace.find(arg(binder_body(r), 2)) != trace.end()); + lean_assert(trace.find(arg(arg(binder_body(r), 2), 1)) != trace.end()); + lean_assert(trace.find(arg(arg(arg(binder_body(r), 2), 1), 1)) != trace.end()); + lean_assert(trace.find(arg(arg(arg(binder_body(r), 2), 1), 2)) == trace.end()); } int main() {