From 751cdd7c4240323da71b02847eb06d069a450abe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 29 Sep 2018 17:13:18 -0700 Subject: [PATCH] feat(kernel/type_checker): avoid unnecessary lambdas --- src/kernel/type_checker.cpp | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 423b9600f5..9c19510083 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -806,15 +806,26 @@ bool type_checker::is_def_eq(expr const & t, expr const & s) { } expr type_checker::eta_expand(expr const & e) { - buffer args; + buffer fvars; flet save_lctx(m_lctx, m_lctx); - expr e_type = whnf(infer(e)); - while (is_pi(e_type)) { - expr arg = m_lctx.mk_local_decl(m_st->m_ngen, binding_name(e_type), binding_domain(e_type), binding_info(e_type)); - args.push_back(arg); - e_type = whnf(instantiate(binding_body(e_type), arg)); + expr it = e; + while (is_lambda(it)) { + expr d = instantiate_rev(binding_domain(it), fvars.size(), fvars.data()); + fvars.push_back(m_lctx.mk_local_decl(m_st->m_ngen, binding_name(it), d, binding_info(it))); + it = binding_body(it); } - return m_lctx.mk_lambda(args, mk_app(e, args)); + it = instantiate_rev(it, fvars.size(), fvars.data()); + expr it_type = whnf(infer(it)); + if (!is_pi(it_type)) return e; + buffer args; + while (is_pi(it_type)) { + expr arg = m_lctx.mk_local_decl(m_st->m_ngen, binding_name(it_type), binding_domain(it_type), binding_info(it_type)); + args.push_back(arg); + fvars.push_back(arg); + it_type = whnf(instantiate(binding_body(it_type), arg)); + } + expr r = mk_app(it, args); + return m_lctx.mk_lambda(fvars, r); } type_checker::type_checker(environment const & env, local_ctx const & lctx, bool non_meta_only):