From b72105efff22f041c717af25d2ece08848754924 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Jul 2014 22:39:45 +0100 Subject: [PATCH] perf(kernel/type_checker): improve infer_lambda performance Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 29 +++++++++++++++++++++++------ 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index dfad99901..2853c4bf4 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -227,13 +227,30 @@ expr type_checker::infer_macro(expr const & e, bool infer_only) { return r; } -expr type_checker::infer_lambda(expr const & e, bool infer_only) { - if (!infer_only) { - expr t = infer_type_core(binding_domain(e), infer_only); - ensure_sort_core(t, binding_domain(e)); +expr type_checker::infer_lambda(expr const & _e, bool infer_only) { + buffer es, ds, ls; + expr e = _e; + while (is_lambda(e)) { + es.push_back(e); + expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); + ds.push_back(d); + expr l = mk_local(m_gen.next(), binding_name(e), d, binding_info(e)); + ls.push_back(l); + if (!infer_only) { + expr t = infer_type_core(d, infer_only); + ensure_sort_core(t, d); + } + e = binding_body(e); } - auto b = open_binding_body(e); - return mk_pi(binding_name(e), binding_domain(e), abstract_local(infer_type_core(b.first, infer_only), b.second), binding_info(e)); + expr r = infer_type_core(instantiate_rev(e, ls.size(), ls.data()), infer_only); + r = abstract_locals(r, ls.size(), ls.data()); + unsigned i = es.size(); + while (i > 0) { + --i; + expr d = abstract_locals(ds[i], i, ls.data()); + r = mk_pi(binding_name(es[i]), d, r, binding_info(es[i])); + } + return r; } expr type_checker::infer_pi(expr const & e, bool infer_only) {