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

feat(library/reducible): expose 'memoize' flag

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-23 13:09:59 -07:00
parent cadc9b3ff3
commit 8e3ac023bb
2 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/reducible.cpp
View file

@ -116,7 +116,8 @@ bool is_reducible_off(environment const & env, name const & n) {
}
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
bool relax_main_opaque, bool only_main_reducible) {
bool relax_main_opaque, bool only_main_reducible,
bool memoize) {
reducible_state const & s = reducible_ext::get_state(env);
if (only_main_reducible) {
name_set reducible_on = s.m_reducible_on;
@ -127,12 +128,12 @@ std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_gene
(!reducible_on.contains(n));
});
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque,
true, pred)));
memoize, pred)));
} else {
name_set reducible_off = s.m_reducible_off;
extra_opaque_pred pred([=](name const & n) { return reducible_off.contains(n); });
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque,
true, pred)));
memoize, pred)));
}
}
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible) {

3
src/library/reducible.h
View file

@ -35,7 +35,8 @@ bool is_reducible_off(environment const & env, name const & n);
/** \brief Create a type checker that takes the "reducibility" hints into account. */
std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
bool relax_main_opaque = true, bool only_main_reducible = false);
bool relax_main_opaque = true, bool only_main_reducible = false,
bool memoize = true);
std::unique_ptr<type_checker> mk_type_checker(environment const & env, bool relax_main_opaque, bool only_main_reducible = false);
void initialize_reducible();