max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/llnf): adjust code, now type must match arity

Browse source 
We recently modified the type of closures in LLNF.
This commit fixes a mismatch.
This commit is contained in:
Leonardo de Moura 2019-01-28 15:55:01 -08:00
parent 0e8067e191
commit 61e51ba402
1 changed files with 4 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/compiler/llnf.cpp
View file

@ -1311,20 +1311,17 @@ class explicit_boxing_fn {
expr visit_app_default(expr const & fn, buffer<expr> & 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. */