From 23e518001a98088b45ca89bb3bab30e83f89a389 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Dec 2013 17:38:04 -0800 Subject: [PATCH] feat(kernel/normalizer): avoid unnecessary creation of closures for n-ary functions Signed-off-by: Leonardo de Moura --- src/kernel/normalizer.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 16c0a2fba..36b05f533 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -220,18 +220,22 @@ class normalizer::imp { while (true) { if (is_closure(f) && is_lambda(to_closure(f).get_expr())) { // beta reduction - expr const & fv = to_closure(f).get_expr(); + expr fv = to_closure(f).get_expr(); + value_stack new_s = to_closure(f).get_stack(); + while (is_lambda(fv) && i < n) { + new_s = extend(new_s, normalize(arg(a, i), s, k)); + i++; + fv = abst_body(fv); + } { freset reset(m_cache); flet set(m_ctx, to_closure(f).get_context()); - value_stack new_s = extend(to_closure(f).get_stack(), normalize(arg(a, i), s, k)); - f = normalize(abst_body(fv), new_s, k); + f = normalize(fv, new_s, k); } - if (i == n - 1) { + if (i == n) { r = f; break; } - i++; } else { buffer new_args; new_args.push_back(f);