diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 12fdb56a7..af7bf3063 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp -for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp -# abstract.cpp instantiate.cpp +for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp +instantiate.cpp # normalizer.cpp context.cpp level.cpp object.cpp environment.cpp # type_checker.cpp kernel.cpp occurs.cpp metavar.cpp # justification.cpp unification_constraint.cpp kernel_exception.cpp diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 561970ce1..83346152f 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -294,10 +294,50 @@ unsigned get_depth(expr const & e) { bool operator==(expr const & a, expr const & b) { return expr_eq_fn()(a, b); } +expr update_app(expr const & e, expr const & new_fn, expr const & new_arg) { + if (!is_eqp(app_fn(e), new_fn) || !is_eqp(app_arg(e), new_arg)) + return mk_app(new_fn, new_arg); + else + return e; +} + +expr update_proj(expr const & e, expr const & new_arg) { + if (!is_eqp(proj_arg(e), new_arg)) + return mk_proj(is_fst(e), new_arg); + else + return e; +} + +expr update_pair(expr const & e, expr const & new_first, expr const & new_second, expr const & new_type) { + if (!is_eqp(pair_first(e), new_first) || !is_eqp(pair_second(e), new_second) || !is_eqp(pair_type(e), new_type)) + return mk_pair(new_first, new_second, new_type); + else + return e; +} + +expr update_binder(expr const & e, expr const & new_domain, expr const & new_body) { + if (!is_eqp(binder_domain(e), new_domain) || !is_eqp(binder_body(e), new_body)) + return mk_binder(e.kind(), binder_name(e), new_domain, new_body); + else + return e; +} + +expr update_let(expr const & e, optional const & new_type, expr const & new_val, expr const & new_body) { + if (!is_eqp(let_type(e), new_type) || !is_eqp(let_value(e), new_val) || !is_eqp(let_body(e), new_body)) + return mk_let(let_name(e), new_type, new_val, new_body); + else + return e; +} + +expr update_mlocal(expr const & e, expr const & new_type) { + if (!is_eqp(mlocal_type(e), new_type)) + return mk_mlocal(is_metavar(e), mlocal_name(e), new_type); + else + return e; +} + #if 0 - - bool is_arrow(expr const & t) { optional r = t.raw()->is_arrow(); if (r) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index d579197dc..d1dbb1c1e 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -122,15 +122,11 @@ public: friend expr mk_var(unsigned idx); friend expr mk_sort(level const & l); friend expr mk_constant(name const & n, levels const & ls); - friend expr mk_metavar(name const & n, expr const & t); - friend expr mk_local(name const & n, expr const & t); + friend expr mk_mlocal(bool is_meta, name const & n, expr const & t); friend expr mk_app(expr const & f, expr const & a); friend expr mk_pair(expr const & f, expr const & s, expr const & t); - friend expr mk_fst(expr const & p); - friend expr mk_snd(expr const & p); - friend expr mk_lambda(name const & n, expr const & t, expr const & e); - friend expr mk_pi(name const & n, expr const & t, expr const & e); - friend expr mk_sigma(name const & n, expr const & t, expr const & e); + friend expr mk_proj(bool fst, expr const & p); + friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e); friend expr mk_let(name const & n, optional const & t, expr const & v, expr const & e); friend expr mk_macro(macro * m); @@ -373,18 +369,21 @@ inline expr mk_constant(name const & n, levels const & ls) { return expr(new exp inline expr mk_constant(name const & n) { return mk_constant(n, levels()); } inline expr Const(name const & n) { return mk_constant(n); } inline expr mk_macro(macro * m) { return expr(new expr_macro(m)); } -inline expr mk_metavar(name const & n, expr const & t) { return expr(new expr_mlocal(true, n, t)); } -inline expr mk_local(name const & n, expr const & t) { return expr(new expr_mlocal(false, n, t)); } +inline expr mk_mlocal(bool is_meta, name const & n, expr const & t) { return expr(new expr_mlocal(is_meta, n, t)); } +inline expr mk_metavar(name const & n, expr const & t) { return mk_mlocal(true, n, t); } +inline expr mk_local(name const & n, expr const & t) { return mk_mlocal(false, n, t); } inline expr mk_pair(expr const & f, expr const & s, expr const & t) { return expr(new expr_dep_pair(f, s, t)); } -inline expr mk_fst(expr const & a) { return expr(new expr_proj(true, a)); } -inline expr mk_snd(expr const & a) { return expr(new expr_proj(false, a)); } +inline expr mk_proj(bool first, expr const & a) { return expr(new expr_proj(first, a)); } +inline expr mk_fst(expr const & a) { return mk_proj(true, a); } +inline expr mk_snd(expr const & a) { return mk_proj(false, a); } inline expr mk_app(expr const & f, expr const & a) { return expr(new expr_app(f, a)); } expr mk_app(unsigned num_args, expr const * args); inline expr mk_app(std::initializer_list const & l) { return mk_app(l.size(), l.begin()); } template expr mk_app(T const & args) { return mk_app(args.size(), args.data()); } -inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Lambda, n, t, e)); } -inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Pi, n, t, e)); } -inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return expr(new expr_binder(expr_kind::Sigma, n, t, e)); } +inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e) { return expr(new expr_binder(k, n, t, e)); } +inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); } +inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); } +inline expr mk_sigma(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Sigma, n, t, e); } inline expr mk_let(name const & n, optional const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); } @@ -556,7 +555,6 @@ struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, e */ expr copy(expr const & e); - // ======================================= // Update expr update_app(expr const & e, expr const & new_fn, expr const & new_arg); diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index ec2d3754e..65eafe0ab 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -8,12 +8,11 @@ Author: Leonardo de Moura #include #include "kernel/free_vars.h" #include "kernel/replace_fn.h" -#include "kernel/metavar.h" #include "kernel/instantiate.h" namespace lean { template -expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst, optional const & menv) { +expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst) { return replace(a, [=](expr const & m, unsigned offset) -> expr { if (is_var(m)) { unsigned vidx = var_idx(m); @@ -22,56 +21,45 @@ expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst if (ClosedSubst) return subst[n - (vidx - s - offset) - 1]; else - return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset, menv); + return lift_free_vars(subst[n - (vidx - s - offset) - 1], offset); } else { return mk_var(vidx - n); } } else { return m; } - } else if (is_metavar(m)) { - expr r = m; - for (unsigned i = 0; i < n; i++) { - expr v = ClosedSubst ? subst[i] : lift_free_vars(subst[i], offset + n - i - 1, menv); - r = add_inst(r, offset + s + n - i - 1, v, menv); - } - return r; } else { return m; } }); } -expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional const & menv) { - lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits::max(), menv); })); - return instantiate_core(a, 0, n, s, menv); -} -expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_ro_menv(menv)); } -expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_ro_menv()); } +expr instantiate_with_closed(expr const & e, unsigned s, unsigned n, expr const * subst) { return instantiate_core(e, s, n, subst); } +expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, 0, n, s); } expr instantiate_with_closed(expr const & e, std::initializer_list const & l) { return instantiate_with_closed(e, l.size(), l.begin()); } -expr instantiate_with_closed(expr const & e, expr const & s, optional const & menv) { return instantiate_with_closed(e, 1, &s, menv); } expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); } -expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate_with_closed(e, s, some_ro_menv(menv)); } - -expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional const & menv) { - return instantiate_core(a, s, n, subst, menv); -} -expr instantiate(expr const & e, unsigned n, expr const * s, optional const & menv) { return instantiate(e, 0, n, s, menv); } -expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate(e, n, s, some_ro_menv(menv)); } -expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, n, s, none_ro_menv()); } +expr instantiate(expr const & e, unsigned s, unsigned n, expr const * subst) { return instantiate_core(e, s, n, subst); } +expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, 0, n, s); } expr instantiate(expr const & e, std::initializer_list const & l) { return instantiate(e, l.size(), l.begin()); } -expr instantiate(expr const & e, unsigned i, expr const & s, optional const & menv) { return instantiate(e, i, 1, &s, menv); } -expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv) { return instantiate(e, i, 1, &s, some_ro_menv(menv)); } -expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s, none_ro_menv()); } -expr instantiate(expr const & e, expr const & s, optional const & menv) { return instantiate(e, 1, &s, menv); } -expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate(e, s, some_ro_menv(menv)); } -expr instantiate(expr const & e, expr const & s) { return instantiate(e, s, none_ro_menv()); } +expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s); } +expr instantiate(expr const & e, expr const & s) { return instantiate(e, 0, s); } bool is_head_beta(expr const & t) { - return is_app(t) && is_lambda(arg(t, 0)); + expr const * it = &t; + while (is_app(*it)) { + expr const & f = app_fn(*it); + if (is_lambda(f)) { + return true; + } else if (is_app(f)) { + it = &f; + } else { + return false; + } + } + return false; } -expr apply_beta(expr f, unsigned num_args, expr const * args, optional const & menv) { +expr apply_beta(expr f, unsigned num_args, expr const * args) { if (!is_lambda(f)) { buffer new_args; new_args.push_back(f); @@ -79,12 +67,12 @@ expr apply_beta(expr f, unsigned num_args, expr const * args, optional const & menv) { +expr head_beta_reduce(expr const & t) { if (!is_head_beta(t)) { return t; } else { - return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1), menv); + buffer args; + expr const * it = &t; + while (true) { + lean_assert(is_app(*it)); + expr f = app_fn(*it); + args.push_back(app_arg(*it)); + if (is_lambda(f)) { + return apply_beta(f, args.size(), args.data()); + } else { + lean_assert(is_app(f)); + it = &f; + } + } } } -expr head_beta_reduce(expr const & t) { return head_beta_reduce(t, none_ro_menv()); } -expr head_beta_reduce(expr const & t, ro_metavar_env const & menv) { return head_beta_reduce(t, some_ro_menv(menv)); } -expr beta_reduce(expr t, optional const & menv) { +expr beta_reduce(expr t) { auto f = [=](expr const & m, unsigned) -> expr { if (is_head_beta(m)) - return head_beta_reduce(m, menv); + return head_beta_reduce(m); else return m; }; while (true) { - expr new_t = replace_fn(f)(t); + expr new_t = replace_fn(f)(t); if (new_t == t) return new_t; else t = new_t; } } -expr beta_reduce(expr t, ro_metavar_env const & menv) { return beta_reduce(t, some_ro_menv(menv)); } -expr beta_reduce(expr t) { return beta_reduce(t, none_ro_menv()); } } diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h index c9952f539..af5903f7f 100644 --- a/src/kernel/instantiate.h +++ b/src/kernel/instantiate.h @@ -13,52 +13,21 @@ class ro_metavar_env; \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. \pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables). - - \remark When the parameter menv is not none, this function will minimize the use - of the local entry inst in metavariables occurring in \c e. */ -expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, optional const & menv); -expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv); expr instantiate_with_closed(expr const & e, unsigned n, expr const * s); expr instantiate_with_closed(expr const & e, std::initializer_list const & l); -expr instantiate_with_closed(expr const & e, expr const & s, optional const & menv); -expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv); expr instantiate_with_closed(expr const & e, expr const & s); -/** - \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. - - \remark When the parameter menv is not none, this function will minimize the use - of the local entry inst in metavariables occurring in \c e. -*/ -expr instantiate(expr const & e, unsigned n, expr const * s, optional const & menv); -expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv); +/** \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e. */ expr instantiate(expr const & e, unsigned n, expr const * s); expr instantiate(expr const & e, std::initializer_list const & l); -/** - \brief Replace free variable \c i with \c s in \c e. -*/ -expr instantiate(expr const & e, unsigned i, expr const & s, optional const & menv); -expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv); +/** \brief Replace free variable \c i with \c s in \c e. */ expr instantiate(expr const & e, unsigned i, expr const & s); -/** - \brief Replace free variable \c 0 with \c s in \c e. -*/ -expr instantiate(expr const & e, expr const & s, optional const & menv); -expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv); +/** \brief Replace free variable \c 0 with \c s in \c e. */ expr instantiate(expr const & e, expr const & s); -expr apply_beta(expr f, unsigned num_args, expr const * args, optional const & menv); -expr apply_beta(expr f, unsigned num_args, expr const * args, ro_metavar_env const & menv); expr apply_beta(expr f, unsigned num_args, expr const * args); - bool is_head_beta(expr const & t); - -expr head_beta_reduce(expr const & t, optional const & menv); -expr head_beta_reduce(expr const & t, ro_metavar_env const & menv); expr head_beta_reduce(expr const & t); - -expr beta_reduce(expr t, optional const & menv); -expr beta_reduce(expr t, ro_metavar_env const & menv); expr beta_reduce(expr t); } diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index 846efb4ab..4c4bcc26d 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/src/tests/kernel/CMakeLists.txt @@ -36,9 +36,9 @@ add_test(diff_cnstrs ${CMAKE_CURRENT_BINARY_DIR}/diff_cnstrs) # 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(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/instantiate.cpp b/src/tests/kernel/instantiate.cpp index e9ead88df..aec6212ff 100644 --- a/src/tests/kernel/instantiate.cpp +++ b/src/tests/kernel/instantiate.cpp @@ -7,7 +7,6 @@ Author: Leonardo de Moura #include "util/test.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" -#include "kernel/metavar.h" using namespace lean; static void tst1() { @@ -22,18 +21,14 @@ static void tst1() { expr N = Const("N"); expr F1 = Fun({x, N}, x)(f, a); lean_assert(is_head_beta(F1)); - std::cout << F1 << " --> " << head_beta_reduce(F1) << "\n"; - lean_assert_eq(head_beta_reduce(F1), f(a)); + lean_assert(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)); - std::cout << F2 << " --> " << head_beta_reduce(F2) << "\n"; - lean_assert_eq(head_beta_reduce(F2), f(a, b, c)); + lean_assert(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)); - std::cout << F3 << " --> " << head_beta_reduce(F3) << "\n"; - lean_assert_eq(head_beta_reduce(F3), f(Fun({y, N}, y)(a), a)); - std::cout << F3 << " --> " << beta_reduce(F3) << "\n"; - lean_assert_eq(beta_reduce(F3), f(a, a)); + lean_assert(head_beta_reduce(F3) == f(Fun({y, N}, y)(a), a)); + lean_assert(beta_reduce(F3) == f(a, a)); } static void tst2() { @@ -42,57 +37,12 @@ static void tst2() { expr f = Const("f"); expr N = Const("N"); expr F1 = Let({x, a}, f(x)); - lean_assert_eq(head_beta_reduce(F1), F1); -} - -static void tst3() { - metavar_env menv; - expr f = Const("f"); - expr a = Const("a"); - expr T = Const("T"); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}})); - lean_assert_eq(instantiate(f(m1, Var(0)), 0, a, menv), f(m1, a)); - lean_assert_ne(instantiate(f(m1, Var(0)), 0, a, menv), instantiate(f(m1, Var(0)), 0, a)); - lean_assert_ne(instantiate(f(m2, Var(0)), 0, a, menv), f(m2, a)); - lean_assert_eq(instantiate(f(m2, Var(0)), 0, a, menv), f(add_inst(m2, 0, a), a)); - expr x = Const("x"); - lean_assert_eq(instantiate(Fun({x, T}, f(m1, Var(1), Var(0))), 0, f(Var(0)), menv), - Fun({x, T}, f(m1, f(Var(1)), Var(0)))); - lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(1), Var(0))), 0, f(Var(0)), menv), - Fun({x, T}, f(add_inst(m2, 1, f(Var(1))), f(Var(1)), Var(0)))); - lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 2, f(Var(0)), menv), - Fun({x, T}, f(m2, f(Var(1)), Var(0)))); - lean_assert_eq(instantiate(Fun({x, T}, f(m1, Var(3), Var(0))), 2, f(Var(0)), menv), - Fun({x, T}, f(m1, f(Var(1)), Var(0)))); - lean_assert_eq(instantiate(Fun({x, T}, f(m2, Var(3), Var(0))), 1, f(Var(0)), menv), - Fun({x, T}, f(m2, Var(2), Var(0)))); - expr m3 = menv->mk_metavar(context({{"x", T}, {"y", T}, {"z", T}})); - lean_assert_eq(instantiate(Fun({x, T}, f(m3, Var(3), Var(0))), 1, f(Var(0)), menv), - Fun({x, T}, f(add_inst(m3, 2, f(Var(1))), Var(2), Var(0)))); -} - -static void tst4() { - metavar_env menv; - expr T = Const("T"); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(context({{"x", T}, {"y", T}})); - expr f = Const("f"); - expr g = Const("f"); - expr x = Const("x"); - expr a = Const("a"); - expr F1 = Fun({x, T}, g(x, m1))(a); - expr F2 = Fun({x, T}, g(x, m2))(a); - lean_assert_eq(head_beta_reduce(F1, menv), g(a, m1)); - lean_assert_eq(head_beta_reduce(F1), g(a, add_inst(m1, 0, a))); - lean_assert_eq(head_beta_reduce(F2, menv), g(a, add_inst(m2, 0, a))); + lean_assert(head_beta_reduce(F1) == F1); } int main() { save_stack_info(); tst1(); tst2(); - tst3(); - tst4(); return has_violations() ? 1 : 0; }