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

feat: do not specialize functions inside functions marked with @[specialize]

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-13 13:32:52 -08:00
parent 53b1128491
commit aa9080e9e7
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/specialize.cpp
View file

@ -1020,8 +1020,12 @@ pair<environment, comp_decls> specialize(environment env, comp_decls const & ds,
comp_decls r; comp_decls r;
for (comp_decl const & d : ds) { for (comp_decl const & d : ds) {
comp_decls new_ds; comp_decls new_ds;
std::tie(env, new_ds) = specialize_core(env, d, cfg); if (has_specialize_attribute(env, d.fst())) {
r = append(r, new_ds); r = append(r, comp_decls(d));
} else {
std::tie(env, new_ds) = specialize_core(env, d, cfg);
r = append(r, new_ds);
}
} }
return mk_pair(env, r); return mk_pair(env, r);
} }