michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(kernel): move extra_opaque_converter to kernel, and rename it to hint_converter

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-30 12:50:47 -07:00
parent e635d9be9f
commit 772ed111e5
2 changed files with 11 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/kernel/converter.h
View file

@ -28,6 +28,15 @@ public:
pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
};
/** \brief Converter that allows us to specify constants that should be considered opaque */
template<typename Converter>
class hint_converter : public Converter {
name_predicate m_pred;
public:
hint_converter(environment const & env, name_predicate const & p):Converter(env), m_pred(p) {}
virtual bool is_opaque(declaration const & d) const { return m_pred(d.get_name()) || Converter::is_opaque(d); }
};
std::unique_ptr<converter> mk_dummy_converter();
void initialize_converter();

16
src/library/util.cpp
View file

@ -870,25 +870,13 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const &
});
}
template<typename Converter>
class extra_opaque_converter : public Converter {
name_predicate m_pred;
public:
extra_opaque_converter(environment const & env, name_predicate const & p):Converter(env), m_pred(p) {}
virtual bool is_opaque(declaration const & d) const {
if (m_pred(d.get_name()))
return true;
return Converter::is_opaque(d);
}
};
type_checker_ptr mk_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) {
return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new extra_opaque_converter<projection_converter>(env, pred))));
std::unique_ptr<converter>(new hint_converter<projection_converter>(env, pred))));
}
type_checker_ptr mk_simple_type_checker(environment const & env, name_generator && ngen, name_predicate const & pred) {
return std::unique_ptr<type_checker>(new type_checker(env, std::move(ngen),
std::unique_ptr<converter>(new extra_opaque_converter<default_converter>(env, pred))));
std::unique_ptr<converter>(new hint_converter<default_converter>(env, pred))));
}
}