/* Copyright (c) 2013 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura Soonho Kong */ #include #include #include #include "util/test.h" #include "kernel/expr.h" #include "kernel/expr_sets.h" #include "kernel/free_vars.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "library/max_sharing.h" #include "library/deep_copy.h" #include "library/kernel_serializer.h" using namespace lean; static void check_serializer(expr const & e) { std::ostringstream out; serializer s(out); s << e << e; std::cout << "OUT size: " << out.str().size() << "\n"; std::istringstream in(out.str()); deserializer d(in); expr n1, n2; d >> n1 >> n2; lean_assert(e == n1); lean_assert(e == n2); lean_assert(is_eqp(n1, n2)); } static void tst1() { expr a; a = Const("a"); expr f; f = Var(0); expr fa = f(a); expr ty = Type; std::cout << fa << "\n"; std::cout << fa(a) << "\n"; lean_assert(is_eqp(app_fn(fa), f)); lean_assert(is_eqp(app_arg(fa), a)); { scoped_expr_caching set(false); lean_assert(!is_eqp(fa, f(a))); } lean_assert(fa(a) == f(a, a)); std::cout << fa(fa, fa) << "\n"; std::cout << mk_lambda("x", ty, Var(0)) << "\n"; lean_assert(f(a)(a) == f(a, a)); lean_assert(f(a(a)) != f(a, a)); lean_assert(mk_lambda("x", ty, Var(0)) == mk_lambda("y", ty, Var(0))); std::cout << mk_pi("x", ty, Var(0)) << "\n"; } static expr mk_dag(unsigned depth, bool _closed = false) { expr f = Const("f"); expr a = _closed ? Const("a") : Var(0); while (depth > 0) { depth--; a = f(a, a); } return a; } static void tst2() { expr r1 = mk_dag(20); expr r2 = mk_dag(20); lean_assert(r1 == r2); std::cout << get_depth(r1) << "\n"; lean_assert_eq(get_depth(r1), 41); } static expr mk_big(expr f, unsigned depth, unsigned val) { if (depth == 1) return Const(name(name("foo"), val)); else return f(mk_big(f, depth - 1, val << 1), mk_big(f, depth - 1, (val << 1) + 1)); } static void tst3() { expr f = Const("f"); expr r1 = mk_big(f, 16, 0); expr r2 = mk_big(f, 16, 0); lean_assert(r1 == r2); check_serializer(r1); } static void tst4() { expr f = Const("f"); expr a = Var(0); for (unsigned i = 0; i < 10000; i++) { a = f(a); } } static expr mk_redundant_dag(expr f, unsigned depth) { if (depth == 0) return Var(0); else return f(mk_redundant_dag(f, depth - 1), mk_redundant_dag(f, depth - 1)); } static unsigned count_core(expr const & a, expr_set & s) { if (s.find(a) != s.end()) return 0; s.insert(a); switch (a.kind()) { case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: case expr_kind::Macro: case expr_kind::Meta: case expr_kind::Local: return 1; case expr_kind::App: return count_core(app_fn(a), s) + count_core(app_arg(a), s) + 1; case expr_kind::Lambda: case expr_kind::Pi: return count_core(binding_domain(a), s) + count_core(binding_body(a), s) + 1; } return 0; } static unsigned count(expr const & a) { expr_set s; return count_core(a, s); } static void tst5() { expr f = Const("f"); { expr r1 = mk_redundant_dag(f, 5); expr r2 = max_sharing(r1); std::cout << "count(r1): " << count(r1) << "\n"; std::cout << "count(r2): " << count(r2) << "\n"; std::cout << "r1 = " << std::endl; std::cout << r1 << std::endl; std::cout << "r2 = " << std::endl; std::cout << r2 << std::endl; lean_assert(r1 == r2); } { expr r1 = mk_redundant_dag(f, 16); expr r2 = max_sharing(r1); lean_assert(r1 == r2); } } static void tst6() { expr f = Const("f"); expr r = mk_redundant_dag(f, 12); max_sharing_fn s; for (unsigned i = 0; i < 1000; i++) { r = s(r); } r = mk_big(f, 16, 0); for (unsigned i = 0; i < 1000000; i++) { r = s(r); } } static void tst7() { scoped_expr_caching set(false); expr f = Const("f"); expr v = Var(0); expr a1 = max_sharing(f(v, v)); expr a2 = max_sharing(f(v, v)); lean_assert(!is_eqp(a1, a2)); expr b = max_sharing(f(a1, a2)); lean_assert(is_eqp(app_arg(app_fn(b)), app_arg(b))); } static void tst8() { expr f = Const("f"); expr x = Var(0); expr a = Const("a"); expr n = Const("n"); expr p = Type; expr y = Var(1); lean_assert(closed(a)); lean_assert(!closed(x)); lean_assert(closed(f)); lean_assert(!closed(f(x))); lean_assert(closed(mk_lambda("x", p, x))); lean_assert(!closed(mk_lambda("x", x, x))); lean_assert(!closed(mk_lambda("x", p, y))); lean_assert(closed(f(f(f(a))))); lean_assert(closed(mk_lambda("x", p, f(f(f(a)))))); lean_assert(closed(mk_pi("x", p, x))); lean_assert(!closed(mk_pi("x", x, x))); lean_assert(!closed(mk_pi("x", p, y))); lean_assert(closed(mk_pi("x", p, f(f(f(a)))))); lean_assert(closed(mk_lambda("y", p, mk_lambda("x", p, y)))); lean_assert(closed(mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)})))); expr r = mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(0)})); lean_assert(closed(r)); lean_assert(closed(r)); r = mk_lambda("y", p, mk_app({mk_lambda("x", p, y), Var(1)})); lean_assert(!closed(r)); r = mk_lambda("y", p, mk_app({mk_lambda("x", p, Var(0)), Var(1)})); lean_assert(!closed(r)); lean_assert(closed(mk_lambda("z", p, r))); } static void tst9() { expr r = mk_dag(20, true); lean_assert(closed(r)); r = mk_dag(20, false); lean_assert(!closed(r)); } static void tst10() { expr f = Const("f"); expr r = mk_big(f, 16, 0); for (unsigned i = 0; i < 1000; i++) { lean_assert(closed(r)); } } /** \brief Substitute s with t in e. \pre s and t must be closed expressions (i.e., no free variables) */ static expr substitute(expr const & e, expr const & s, expr const & t) { check_serializer(e); return instantiate(abstract(e, s), t); } static void tst11() { expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); expr x = Var(0); expr y = Var(1); expr t = Type; std::cout << instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) << "\n"; lean_assert(instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) == mk_lambda("x", t, f(f(f(a), b), f(x, f(a))))); std::cout << abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) << "\n"; lean_assert(abstract(mk_lambda("x", t, f(a, mk_lambda("y", t, f(b, a)))), Const("a")) == mk_lambda("x", t, f(Var(1), mk_lambda("y", t, f(b, Var(2)))))); lean_assert(substitute(f(f(f(a))), f(a), b) == f(f(b))); } static void tst12() { scoped_expr_caching set(false); expr f = Const("f"); expr v = Var(0); expr a1 = max_sharing(f(v, v)); expr a2 = max_sharing(f(v, v)); lean_assert(!is_eqp(a1, a2)); lean_assert(a1 == a2); max_sharing_fn M; lean_assert(is_eqp(M(f(v, v)), M(f(v, v)))); lean_assert(is_eqp(M(a1), M(a2))); } static void tst13() { expr t0 = Type; expr t1 = mk_sort(mk_succ(mk_succ(level()))); check_serializer(t0); check_serializer(t1); lean_assert(sort_level(t1) == mk_succ(mk_succ(level()))); lean_assert(t0 != t1); std::cout << t0 << " " << t1 << "\n"; } static void tst14() { expr l = Const("b"); check_serializer(l); std::cout << l << "\n"; lean_assert(closed(l)); } static void tst15() { expr f = Const("f"); expr x = Var(0); expr a = Local("a", Type); expr m = mk_metavar("m", Prop); check_serializer(m); lean_assert(has_metavar(m)); lean_assert(has_metavar(f(m))); lean_assert(!has_metavar(f(a))); lean_assert(!has_metavar(f(x))); lean_assert(!has_metavar(Pi(a, a))); lean_assert(!has_metavar(Type)); lean_assert(!has_metavar(Fun(a, a))); lean_assert(has_metavar(Pi(a, m))); expr a1 = Local("a", m); lean_assert(has_metavar(Pi(a1, a1))); lean_assert(has_metavar(Fun(a, m))); lean_assert(has_metavar(Fun(a1, a))); lean_assert(has_metavar(f(a, a, m))); lean_assert(has_metavar(f(a, m, a, a))); lean_assert(!has_metavar(f(a, a, a, a))); } static void check_copy(expr const & e) { scoped_expr_caching set(false); expr c = copy(e); lean_assert(!is_eqp(e, c)); lean_assert(e == c); check_serializer(e); } static void tst16() { expr f = Const("f"); expr a = Const("a"); check_copy(f(a)); check_copy(mk_metavar("M", Prop)); check_copy(mk_lambda("x", a, Var(0))); check_copy(mk_pi("x", a, Var(0))); } static void tst17() { expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); expr c = Const("c"); buffer args; args.push_back(f); for (unsigned i = 0; i < 200; i++) { args.push_back(a); args.push_back(b); } args.push_back(c); expr t = mk_app(args); check_serializer(t); } static void tst18() { expr f = Const("f"); expr x = Var(0); expr l = mk_local("m", Prop); expr m = mk_metavar("m", Prop); expr a0 = Const("a"); expr a = Local("a", Type); expr a1 = Local("a", m); expr a2 = Local("a", l); check_serializer(l); lean_assert(!has_local(m)); lean_assert(has_local(l)); lean_assert(!has_local(f(m))); lean_assert(has_local(f(l))); lean_assert(!has_local(f(a0))); lean_assert(!has_local(f(x))); lean_assert(!has_local(Pi(a, a))); lean_assert(!has_local(Pi(a1, a1))); lean_assert(!has_local(Type)); lean_assert(!has_local(Pi(a, a))); lean_assert(has_local(Pi(a, l))); lean_assert(!has_metavar(Pi(a, l))); lean_assert(has_local(Pi(a2, a2))); lean_assert(has_local(Fun(a, l))); lean_assert(has_local(Fun(a2, a2))); lean_assert(has_local(f(a, a, l))); lean_assert(has_local(f(a, l, a, a))); lean_assert(!has_local(f(a0, a0, a0, a0))); } int main() { save_stack_info(); lean_assert(sizeof(expr) == sizeof(optional)); tst1(); tst2(); tst3(); tst4(); tst5(); tst6(); tst7(); tst8(); tst9(); tst10(); tst11(); tst12(); tst13(); tst14(); tst15(); tst16(); tst17(); tst18(); std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n"; std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n"; std::cout << "sizeof(expr_var): " << sizeof(expr_var) << "\n"; std::cout << "sizeof(expr_const): " << sizeof(expr_const) << "\n"; std::cout << "sizeof(optional): " << sizeof(optional) << "\n"; std::cout << "sizeof(optional): " << sizeof(optional) << "\n"; std::cout << "sizeof(std::function): " << sizeof(std::function const &)>) << "\n"; std::cout << "done" << "\n"; return has_violations() ? 1 : 0; }