From 61e51ba402dfce352854d4e34c24080f82d69a74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Jan 2019 15:55:01 -0800 Subject: [PATCH] fix(library/compiler/llnf): adjust code, now type must match arity We recently modified the type of closures in LLNF. This commit fixes a mismatch. --- src/library/compiler/llnf.cpp | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 13a8add619..ccb0193ac8 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -1311,20 +1311,17 @@ class explicit_boxing_fn { expr visit_app_default(expr const & fn, buffer & args, expr const & expected_type) { expr type = get_constant_type(const_name(fn)); for (expr & arg : args) { - lean_assert(is_pi(type)); if (is_fvar(arg)) { - expr arg_expected_type = binding_domain(type); + expr arg_expected_type = is_pi(type) ? binding_domain(type) : mk_enf_object_type(); expr arg_type = get_arg_type(arg); arg = cast_arg_if_needed(arg, arg_type, arg_expected_type); } else { lean_assert(is_enf_neutral(arg)); } - type = binding_body(type); - } - if (is_pi(type)) { - /* Function returns a closure */ - type = mk_enf_object_type(); + if (is_pi(type)) + type = binding_body(type); } + lean_assert(!is_pi(type)); expr r = mk_app(fn, args); return cast_result_if_needed(r, type, expected_type); } @@ -1659,7 +1656,6 @@ class explicit_rc_fn { expr val = get_value_of(x); lean_assert(is_app(val) && is_llnf_proj(app_fn(val))); expr arg = app_arg(val); - /* If arg is */ if (!m_borrowed.contains(fvar_name(arg)) && /* arg is not marked as borrowed */ !live_obj_vars.contains(fvar_name(arg))) { /* arg is not live after projection */ /* We must add decrement. */