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

feat: support [nospecialize] on typeclasses

Browse source
This commit is contained in:
Sebastian Ullrich 2021-12-22 13:54:21 +01:00 • committed by Leonardo de Moura
parent b4385bd259
commit 45e8d9af43
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -180,7 +180,12 @@ environment update_spec_info(environment const & env, comp_decls const & ds) {
expr fvar = lctx.mk_local_decl(ngen, binding_name(code), type);
fvars.push_back(fvar);
if (is_inst_implicit(binding_info(code))) {
info.second.push_back(spec_arg_kind::FixedInst);
expr const & fn = get_app_fn(type);
if (is_const(fn) && has_nospecialize_attribute(env, const_name(fn))) {
info.second.push_back(spec_arg_kind::FixedNeutral);
} else {
info.second.push_back(spec_arg_kind::FixedInst);
}
} else {
type_checker tc(env, lctx);
type = tc.whnf(type);