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

feat(library/compiler/borrowed_annotation): mark objects as owned when stored in constructors

Browse source 
@kha
This commit is contained in:
Leonardo de Moura 2019-02-23 09:09:47 -08:00
parent 483125f828
commit 313fd69e8c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/borrowed_annotation.cpp
View file

@ -143,7 +143,7 @@ class borrow_inference_fn {
if (is_cases_on_app(m_env, e)) {
for (unsigned i = 1; i < args.size(); i++)
collect(args[i]);
} else if (is_llnf_apply(fn) || is_llnf_closure(fn) || is_llnf_reset(fn)) {
} else if (is_llnf_apply(fn) || is_llnf_closure(fn) || is_llnf_reset(fn) || is_llnf_cnstr(fn) || is_llnf_reuse(fn)) {
mark_owned(args);
} else if (!is_llnf_op(fn)) {
bool tail_call = terminal && (m_decls[m_curr_fidx].fst() == const_name(fn));