From aa9080e9e7c34a99d027af322e575ea63bbc30b4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Nov 2019 13:32:52 -0800 Subject: [PATCH] feat: do not specialize functions inside functions marked with `@[specialize]` --- src/library/compiler/specialize.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index 515836dfa5..f661339392 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -1020,8 +1020,12 @@ pair specialize(environment env, comp_decls const & ds, comp_decls r; for (comp_decl const & d : ds) { comp_decls new_ds; - std::tie(env, new_ds) = specialize_core(env, d, cfg); - r = append(r, new_ds); + if (has_specialize_attribute(env, d.fst())) { + 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); }