refactor(tests/kernel): move tests to new kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
565dbe1700
commit
73c8bf4436
6 changed files with 47 additions and 158 deletions
|
|
@ -19,4 +19,11 @@ std::pair<name, expr> const & lookup(context const & c, unsigned i) {
|
|||
}
|
||||
throw exception("unknown free variable");
|
||||
}
|
||||
optional<std::pair<name, expr>> find(context const & c, unsigned i) {
|
||||
try {
|
||||
return optional<std::pair<name, expr>>(lookup(c, i));
|
||||
} catch (exception &) {
|
||||
return optional<std::pair<name, expr>>();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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));
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<decltype(proc), tracer> 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() {
|
||||
|
|
|
|||
Loading…
Reference in a new issue