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

refactor(kernel/converter): remove mk_default_converter procedures

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-07 19:03:58 -08:00
parent a47615009f
commit a11d1efb42
2 changed files with 0 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/kernel/converter.cpp
View file

@ -103,25 +103,6 @@ name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); }
pair<expr, constraint_seq> converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,
bool memoize, extra_opaque_pred const & pred) {
return std::unique_ptr<converter>(new default_converter(env, mod_idx, memoize, pred));
}
std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,
bool memoize) {
return mk_default_converter(env, mod_idx, memoize, g_always_false);
}
std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize,
extra_opaque_pred const & pred) {
if (unfold_opaque_main)
return mk_default_converter(env, optional<module_idx>(0), memoize, pred);
else
return mk_default_converter(env, optional<module_idx>(), memoize, pred);
}
std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize) {
return mk_default_converter(env, unfold_opaque_main, memoize, g_always_false);
}
void initialize_converter() {
g_opt_main_module_idx = new optional<module_idx>(g_main_module_idx);
g_no_delayed_jst = new no_delayed_justification();

8
src/kernel/converter.h
View file

@ -26,14 +26,6 @@ public:
};
std::unique_ptr<converter> mk_dummy_converter();
std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx = optional<module_idx>(),
bool memoize = true);
std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx,
bool memoize, extra_opaque_pred const & pred);
std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main,
bool memoize = true);
std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main,
bool memoize, extra_opaque_pred const & pred);
bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx);
optional<declaration> is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx);