From 7b15e558a2a3574b15c7e9c4bca3aaa5c42a9e4d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 May 2014 17:49:51 -0700 Subject: [PATCH] refactor(kernel/converter): implement eta in whnf instead of is_def_eq. Without cumulativity, we do not have problems with Eta at whnf anymore. When we had cumulativity, we could not not simply reduce (fun x : A, f x) ==> f This step is correct only if domain(f) was definitionally equal to f. Here is a problematic example for systems with cumulativity Given, f : Type.{2} -> Bool (fun x : Type.{1}, f x) Signed-off-by: Leonardo de Moura --- src/kernel/converter.cpp | 56 ++++++++++++++++++++-------------------- tests/lua/eta.lua | 16 ++++++++++++ 2 files changed, 44 insertions(+), 28 deletions(-) create mode 100644 tests/lua/eta.lua diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 541c71c5b..9fce2639b 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -62,16 +62,36 @@ struct default_converter : public converter { return m_env.norm_ext()(e, xctx); } + /** \brief Try to apply eta-reduction to \c e. */ + expr try_eta(expr const & e) { + lean_assert(is_lambda(e)); + expr const & b = binder_body(e); + if (is_lambda(b)) { + expr new_b = try_eta(b); + if (is_eqp(b, new_b)) { + return e; + } else if (is_app(new_b) && is_var(app_arg(new_b), 0) && !has_free_var(app_fn(new_b), 0)) { + return lower_free_vars(app_fn(new_b), 1); + } else { + return update_binder(e, binder_domain(e), new_b); + } + } else if (is_app(b) && is_var(app_arg(b), 0) && !has_free_var(app_fn(b), 0)) { + return lower_free_vars(app_fn(b), 1); + } else { + return e; + } + } + /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ expr whnf_core(expr const & e, context & c) { check_system("whnf"); // handle easy cases switch (e.kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Pi: case expr_kind::Constant: return e; - case expr_kind::Macro: case expr_kind::Let: case expr_kind::App: + case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::Let: case expr_kind::App: break; } @@ -86,8 +106,11 @@ struct default_converter : public converter { expr r; switch (e.kind()) { case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: + case expr_kind::Pi: case expr_kind::Constant: lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Lambda: + r = (m_env.eta()) ? try_eta(e) : e; + break; case expr_kind::Macro: if (auto m = expand_macro(e, c)) r = whnf_core(*m, c); @@ -261,20 +284,6 @@ struct default_converter : public converter { } } - /** \brief Eta-expand \c s and check if it is definitionally equal to \c t. */ - bool try_eta(expr const & t, expr const & s, context & c, delayed_justification & jst) { - lean_assert(is_lambda(t)); - lean_assert(!is_lambda(s)); - expr t_s = whnf(c.infer_type(s), c); - if (is_pi(t_s)) { - // new_s := lambda x : domain(t_s), s x - expr new_s = mk_lambda(c.mk_fresh_name(), binder_domain(t_s), mk_app(lift_free_vars(s, 1), mk_var(0))); - return is_def_eq(t, new_s, c, jst); - } else { - return false; - } - } - /** \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is def eq to \c s. @@ -419,16 +428,7 @@ struct default_converter : public converter { if (r != l_undef) return r == l_true; } - // At this point, t_n and s_n are in weak head normal form (modulo meta-variables) - - if (m_env.eta()) { - lean_assert(!is_lambda(t_n) || !is_lambda(s_n)); - // Eta-reduction support - if ((is_lambda(t_n) && try_eta(t_n, s_n, c, jst)) || - (is_lambda(s_n) && try_eta(s_n, t_n, c, jst))) - return true; - } - + // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance) if (is_app(t_n) && is_app(s_n)) { expr it1 = t_n; expr it2 = s_n; diff --git a/tests/lua/eta.lua b/tests/lua/eta.lua new file mode 100644 index 000000000..a52d121db --- /dev/null +++ b/tests/lua/eta.lua @@ -0,0 +1,16 @@ +local env = empty_environment() +env = add_decl(env, mk_var_decl("f", mk_arrow(Bool, mk_arrow(Bool, Bool)))) +local f = Const("f") +local x = Const("x") +local y = Const("y") +local z = Const("z") +local tc = type_checker(env) +print(tc:whnf(Fun(x, Bool, f(x)))) +print(tc:whnf(Fun(x, Bool, Fun(y, Bool, f(x, y))))) +print(tc:whnf(Fun(x, Bool, Fun(y, Bool, f(Const("a"), y))))) +print(tc:whnf(Fun(z, Bool, Fun(x, Bool, Fun(y, Bool, f(z, y)))))) +assert(tc:is_def_eq(f, Fun(x, Bool, f(x)))) +assert(tc:is_def_eq(f, Fun(x, Bool, Fun(y, Bool, f(x, y))))) +local a = Const("a") +local A = Const("A") +assert(tc:is_def_eq(Fun(a, A, a)(f), Fun(x, Bool, Fun(y, Bool, f(x, y)))))