From ffdb43da0227eaae371588198366f359166e6c3d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Jul 2014 22:56:38 +0100 Subject: [PATCH] perf(kernel/type_checker): improve infer_pi performance Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 2853c4bf4..8902f31c5 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -253,14 +253,26 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) { return r; } -expr type_checker::infer_pi(expr const & e, bool infer_only) { - expr t1 = ensure_sort_core(infer_type_core(binding_domain(e), infer_only), binding_domain(e)); - auto b = open_binding_body(e); - expr t2 = ensure_sort_core(infer_type_core(b.first, infer_only), binding_body(e)); - if (m_env.impredicative()) - return mk_sort(mk_imax(sort_level(t1), sort_level(t2))); - else - return mk_sort(mk_max(sort_level(t1), sort_level(t2))); +expr type_checker::infer_pi(expr const & _e, bool infer_only) { + buffer ls; + buffer us; + expr e = _e; + while (is_pi(e)) { + expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); + expr t1 = ensure_sort_core(infer_type_core(d, infer_only), d); + us.push_back(sort_level(t1)); + expr l = mk_local(m_gen.next(), binding_name(e), d, binding_info(e)); + ls.push_back(l); + e = binding_body(e); + } + e = instantiate_rev(e, ls.size(), ls.data()); + level r = sort_level(ensure_sort_core(infer_type_core(e, infer_only), e)); + unsigned i = ls.size(); + while (i > 0) { + --i; + r = m_env.impredicative() ? mk_imax(us[i], r) : mk_max(us[i], r); + } + return mk_sort(r); } expr type_checker::infer_app(expr const & e, bool infer_only) {