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

chore(library/abstract_context_cache): remove unnecessary argument

Browse source
This commit is contained in:
Leonardo de Moura 2018-03-05 14:40:47 -08:00
parent a5ace58fb3
commit eddc64d154
3 changed files with 130 additions and 130 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

104
src/library/abstract_context_cache.h
View file

@ -213,48 +213,48 @@ public:
/* Cache support for fun_info module */
virtual optional<fun_info> get_fun_info(type_context_old &, expr const &) = 0;
virtual void set_fun_info(type_context_old &, expr const &, fun_info const &) = 0;
virtual optional<fun_info> get_fun_info(expr const &) = 0;
virtual void set_fun_info(expr const &, fun_info const &) = 0;
virtual optional<fun_info> get_fun_info_nargs(type_context_old &, expr const &, unsigned) = 0;
virtual void set_fun_info_nargs(type_context_old &, expr const &, unsigned, fun_info const &) = 0;
virtual optional<fun_info> get_fun_info_nargs(expr const &, unsigned) = 0;
virtual void set_fun_info_nargs(expr const &, unsigned, fun_info const &) = 0;
virtual optional<unsigned> get_specialization_prefix_size(type_context_old &, expr const &, unsigned) = 0;
virtual void set_specialization_prefix_size(type_context_old &, expr const &, unsigned, unsigned) = 0;
virtual optional<unsigned> get_specialization_prefix_size(expr const &, unsigned) = 0;
virtual void set_specialization_prefix_size(expr const &, unsigned, unsigned) = 0;
virtual optional<ss_param_infos> get_subsingleton_info(type_context_old &, expr const &) = 0;
virtual void set_subsingleton_info(type_context_old &, expr const &, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> get_subsingleton_info(expr const &) = 0;
virtual void set_subsingleton_info(expr const &, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) = 0;
virtual void set_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> get_subsingleton_info_nargs(expr const &, unsigned) = 0;
virtual void set_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) = 0;
virtual void set_specialization_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) = 0;
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(expr const &, unsigned) = 0;
virtual void set_specialization_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) = 0;
/* Cache support for congr_lemma module */
virtual optional<congr_lemma> get_simp_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
virtual void set_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_simp_congr_lemma(expr const &, unsigned) = 0;
virtual void set_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
virtual void set_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_specialized_simp_congr_lemma(expr const &, unsigned) = 0;
virtual void set_specialized_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
virtual void set_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_congr_lemma(expr const &, unsigned) = 0;
virtual void set_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_specialized_congr_lemma(type_context_old &, expr const &, unsigned) = 0;
virtual void set_specialized_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_specialized_congr_lemma(expr const &, unsigned) = 0;
virtual void set_specialized_congr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_hcongr_lemma(type_context_old &, expr const &, unsigned) = 0;
virtual void set_hcongr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) = 0;
virtual optional<congr_lemma> get_hcongr_lemma(expr const &, unsigned) = 0;
virtual void set_hcongr_lemma(expr const &, unsigned, congr_lemma const &) = 0;
/* Cache support for app_builder */
virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, unsigned) = 0;
virtual void set_app_builder_info(type_context_old &, expr const &, unsigned, app_builder_info const &) = 0;
virtual optional<app_builder_info> get_app_builder_info(expr const &, unsigned) = 0;
virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) = 0;
virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, list<bool> const &) = 0;
virtual void set_app_builder_info(type_context_old &, expr const &, list<bool> const &, app_builder_info const &) = 0;
virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) = 0;
virtual void set_app_builder_info(expr const &, list<bool> const &, app_builder_info const &) = 0;
};
/* Dummy implementation of the abstract_context_cache interface that does not do cache anything but configuration options. */
@ -324,48 +324,48 @@ public:
/* Cache support for fun_info module */
virtual optional<fun_info> get_fun_info(type_context_old &, expr const &) override { return optional<fun_info>(); }
virtual void set_fun_info(type_context_old &, expr const &, fun_info const &) override {}
virtual optional<fun_info> get_fun_info(expr const &) override { return optional<fun_info>(); }
virtual void set_fun_info(expr const &, fun_info const &) override {}
virtual optional<fun_info> get_fun_info_nargs(type_context_old &, expr const &, unsigned) override { return optional<fun_info>(); }
virtual void set_fun_info_nargs(type_context_old &, expr const &, unsigned, fun_info const &) override {}
virtual optional<fun_info> get_fun_info_nargs(expr const &, unsigned) override { return optional<fun_info>(); }
virtual void set_fun_info_nargs(expr const &, unsigned, fun_info const &) override {}
virtual optional<unsigned> get_specialization_prefix_size(type_context_old &, expr const &, unsigned) override { return optional<unsigned>(); }
virtual void set_specialization_prefix_size(type_context_old &, expr const &, unsigned, unsigned) override {}
virtual optional<unsigned> get_specialization_prefix_size(expr const &, unsigned) override { return optional<unsigned>(); }
virtual void set_specialization_prefix_size(expr const &, unsigned, unsigned) override {}
virtual optional<ss_param_infos> get_subsingleton_info(type_context_old &, expr const &) override { return optional<ss_param_infos>(); }
virtual void set_subsingleton_info(type_context_old &, expr const &, ss_param_infos const &) override {}
virtual optional<ss_param_infos> get_subsingleton_info(expr const &) override { return optional<ss_param_infos>(); }
virtual void set_subsingleton_info(expr const &, ss_param_infos const &) override {}
virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override { return optional<ss_param_infos>(); }
virtual void set_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override {}
virtual optional<ss_param_infos> get_subsingleton_info_nargs(expr const &, unsigned) override { return optional<ss_param_infos>(); }
virtual void set_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override {}
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override { return optional<ss_param_infos>(); }
virtual void set_specialization_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override {}
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(expr const &, unsigned) override { return optional<ss_param_infos>(); }
virtual void set_specialization_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override {}
/* Cache support for congr_lemma module */
virtual optional<congr_lemma> get_simp_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_simp_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_specialized_simp_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_specialized_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_specialized_congr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_specialized_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_specialized_congr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_specialized_congr_lemma(expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_hcongr_lemma(type_context_old &, expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_hcongr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override {}
virtual optional<congr_lemma> get_hcongr_lemma(expr const &, unsigned) override { return optional<congr_lemma>(); }
virtual void set_hcongr_lemma(expr const &, unsigned, congr_lemma const &) override {}
/* Cache support for app_builder */
virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, unsigned) override { return optional<app_builder_info>(); }
virtual void set_app_builder_info(type_context_old &, expr const &, unsigned, app_builder_info const &) override {}
virtual optional<app_builder_info> get_app_builder_info(expr const &, unsigned) override { return optional<app_builder_info>(); }
virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) override {}
virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, list<bool> const &) override { return optional<app_builder_info>(); }
virtual void set_app_builder_info(type_context_old &, expr const &, list<bool> const &, app_builder_info const &) override {}
virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) override { return optional<app_builder_info>(); }
virtual void set_app_builder_info(expr const &, list<bool> const &, app_builder_info const &) override {}
};
void initialize_abstract_context_cache();

104
src/library/persistent_context_cache.cpp
View file

@ -131,109 +131,109 @@ optional<local_instances> persistent_context_cache::get_frozen_local_instances()
return m_cache_ptr->get_frozen_local_instances();
}
optional<fun_info> persistent_context_cache::get_fun_info(type_context_old & ctx, expr const & e) {
return m_cache_ptr->get_fun_info(ctx, e);
optional<fun_info> persistent_context_cache::get_fun_info(expr const & e) {
return m_cache_ptr->get_fun_info(e);
}
void persistent_context_cache::set_fun_info(type_context_old & ctx, expr const & e, fun_info const & r) {
return m_cache_ptr->set_fun_info(ctx, e, r);
void persistent_context_cache::set_fun_info(expr const & e, fun_info const & r) {
return m_cache_ptr->set_fun_info(e, r);
}
optional<fun_info> persistent_context_cache::get_fun_info_nargs(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_fun_info_nargs(ctx, e, k);
optional<fun_info> persistent_context_cache::get_fun_info_nargs(expr const & e, unsigned k) {
return m_cache_ptr->get_fun_info_nargs(e, k);
}
void persistent_context_cache::set_fun_info_nargs(type_context_old & ctx, expr const & e, unsigned k, fun_info const & r) {
return m_cache_ptr->set_fun_info_nargs(ctx, e, k, r);
void persistent_context_cache::set_fun_info_nargs(expr const & e, unsigned k, fun_info const & r) {
return m_cache_ptr->set_fun_info_nargs(e, k, r);
}
optional<unsigned> persistent_context_cache::get_specialization_prefix_size(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_specialization_prefix_size(ctx, e, k);
optional<unsigned> persistent_context_cache::get_specialization_prefix_size(expr const & e, unsigned k) {
return m_cache_ptr->get_specialization_prefix_size(e, k);
}
void persistent_context_cache::set_specialization_prefix_size(type_context_old & ctx, expr const & e, unsigned k, unsigned r) {
return m_cache_ptr->set_specialization_prefix_size(ctx, e, k, r);
void persistent_context_cache::set_specialization_prefix_size(expr const & e, unsigned k, unsigned r) {
return m_cache_ptr->set_specialization_prefix_size(e, k, r);
}
optional<ss_param_infos> persistent_context_cache::get_subsingleton_info(type_context_old & ctx, expr const & e) {
return m_cache_ptr->get_subsingleton_info(ctx, e);
optional<ss_param_infos> persistent_context_cache::get_subsingleton_info(expr const & e) {
return m_cache_ptr->get_subsingleton_info(e);
}
void persistent_context_cache::set_subsingleton_info(type_context_old & ctx, expr const & e, ss_param_infos const & r) {
return m_cache_ptr->set_subsingleton_info(ctx, e, r);
void persistent_context_cache::set_subsingleton_info(expr const & e, ss_param_infos const & r) {
return m_cache_ptr->set_subsingleton_info(e, r);
}
optional<ss_param_infos> persistent_context_cache::get_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_subsingleton_info_nargs(ctx, e, k);
optional<ss_param_infos> persistent_context_cache::get_subsingleton_info_nargs(expr const & e, unsigned k) {
return m_cache_ptr->get_subsingleton_info_nargs(e, k);
}
void persistent_context_cache::set_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k, ss_param_infos const & r) {
return m_cache_ptr->set_subsingleton_info_nargs(ctx, e, k, r);
void persistent_context_cache::set_subsingleton_info_nargs(expr const & e, unsigned k, ss_param_infos const & r) {
return m_cache_ptr->set_subsingleton_info_nargs(e, k, r);
}
optional<ss_param_infos> persistent_context_cache::get_specialized_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_specialized_subsingleton_info_nargs(ctx, e, k);
optional<ss_param_infos> persistent_context_cache::get_specialized_subsingleton_info_nargs(expr const & e, unsigned k) {
return m_cache_ptr->get_specialized_subsingleton_info_nargs(e, k);
}
void persistent_context_cache::set_specialization_subsingleton_info_nargs(type_context_old & ctx, expr const & e, unsigned k, ss_param_infos const & r) {
return m_cache_ptr->set_specialization_subsingleton_info_nargs(ctx, e, k, r);
void persistent_context_cache::set_specialization_subsingleton_info_nargs(expr const & e, unsigned k, ss_param_infos const & r) {
return m_cache_ptr->set_specialization_subsingleton_info_nargs(e, k, r);
}
optional<congr_lemma> persistent_context_cache::get_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_simp_congr_lemma(ctx, e, k);
optional<congr_lemma> persistent_context_cache::get_simp_congr_lemma(expr const & e, unsigned k) {
return m_cache_ptr->get_simp_congr_lemma(e, k);
}
void persistent_context_cache::set_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_simp_congr_lemma(ctx, e, k, r);
void persistent_context_cache::set_simp_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_simp_congr_lemma(e, k, r);
}
optional<congr_lemma> persistent_context_cache::get_specialized_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_specialized_simp_congr_lemma(ctx, e, k);
optional<congr_lemma> persistent_context_cache::get_specialized_simp_congr_lemma(expr const & e, unsigned k) {
return m_cache_ptr->get_specialized_simp_congr_lemma(e, k);
}
void persistent_context_cache::set_specialized_simp_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_specialized_simp_congr_lemma(ctx, e, k, r);
void persistent_context_cache::set_specialized_simp_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_specialized_simp_congr_lemma(e, k, r);
}
optional<congr_lemma> persistent_context_cache::get_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_congr_lemma(ctx, e, k);
optional<congr_lemma> persistent_context_cache::get_congr_lemma(expr const & e, unsigned k) {
return m_cache_ptr->get_congr_lemma(e, k);
}
void persistent_context_cache::set_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_congr_lemma(ctx, e, k, r);
void persistent_context_cache::set_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_congr_lemma(e, k, r);
}
optional<congr_lemma> persistent_context_cache::get_specialized_congr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_specialized_congr_lemma(ctx, e, k);
optional<congr_lemma> persistent_context_cache::get_specialized_congr_lemma(expr const & e, unsigned k) {
return m_cache_ptr->get_specialized_congr_lemma(e, k);
}
void persistent_context_cache::set_specialized_congr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_specialized_congr_lemma(ctx, e, k, r);
void persistent_context_cache::set_specialized_congr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_specialized_congr_lemma(e, k, r);
}
optional<congr_lemma> persistent_context_cache::get_hcongr_lemma(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_hcongr_lemma(ctx, e, k);
optional<congr_lemma> persistent_context_cache::get_hcongr_lemma(expr const & e, unsigned k) {
return m_cache_ptr->get_hcongr_lemma(e, k);
}
void persistent_context_cache::set_hcongr_lemma(type_context_old & ctx, expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_hcongr_lemma(ctx, e, k, r);
void persistent_context_cache::set_hcongr_lemma(expr const & e, unsigned k, congr_lemma const & r) {
return m_cache_ptr->set_hcongr_lemma(e, k, r);
}
optional<app_builder_info> persistent_context_cache::get_app_builder_info(type_context_old & ctx, expr const & e, unsigned k) {
return m_cache_ptr->get_app_builder_info(ctx, e, k);
optional<app_builder_info> persistent_context_cache::get_app_builder_info(expr const & e, unsigned k) {
return m_cache_ptr->get_app_builder_info(e, k);
}
void persistent_context_cache::set_app_builder_info(type_context_old & ctx, expr const & e, unsigned k, app_builder_info const & r) {
return m_cache_ptr->set_app_builder_info(ctx, e, k, r);
void persistent_context_cache::set_app_builder_info(expr const & e, unsigned k, app_builder_info const & r) {
return m_cache_ptr->set_app_builder_info(e, k, r);
}
optional<app_builder_info> persistent_context_cache::get_app_builder_info(type_context_old & ctx, expr const & e, list<bool> const & m) {
return m_cache_ptr->get_app_builder_info(ctx, e, m);
optional<app_builder_info> persistent_context_cache::get_app_builder_info(expr const & e, list<bool> const & m) {
return m_cache_ptr->get_app_builder_info(e, m);
}
void persistent_context_cache::set_app_builder_info(type_context_old & ctx, expr const & e, list<bool> const & m, app_builder_info const & r) {
return m_cache_ptr->set_app_builder_info(ctx, e, m, r);
void persistent_context_cache::set_app_builder_info(expr const & e, list<bool> const & m, app_builder_info const & r) {
return m_cache_ptr->set_app_builder_info(e, m, r);
}
void initialize_persistent_context_cache() {

52
src/library/persistent_context_cache.h
View file

@ -77,47 +77,47 @@ public:
/* Cache support for fun_info module */
virtual optional<fun_info> get_fun_info(type_context_old &, expr const &) override;
virtual void set_fun_info(type_context_old &, expr const &, fun_info const &) override;
virtual optional<fun_info> get_fun_info(expr const &) override;
virtual void set_fun_info(expr const &, fun_info const &) override;
virtual optional<fun_info> get_fun_info_nargs(type_context_old &, expr const &, unsigned) override;
virtual void set_fun_info_nargs(type_context_old &, expr const &, unsigned, fun_info const &) override;
virtual optional<fun_info> get_fun_info_nargs(expr const &, unsigned) override;
virtual void set_fun_info_nargs(expr const &, unsigned, fun_info const &) override;
virtual optional<unsigned> get_specialization_prefix_size(type_context_old &, expr const &, unsigned) override;
virtual void set_specialization_prefix_size(type_context_old &, expr const &, unsigned, unsigned) override;
virtual optional<unsigned> get_specialization_prefix_size(expr const &, unsigned) override;
virtual void set_specialization_prefix_size(expr const &, unsigned, unsigned) override;
virtual optional<ss_param_infos> get_subsingleton_info(type_context_old &, expr const &) override;
virtual void set_subsingleton_info(type_context_old &, expr const &, ss_param_infos const &) override;
virtual optional<ss_param_infos> get_subsingleton_info(expr const &) override;
virtual void set_subsingleton_info(expr const &, ss_param_infos const &) override;
virtual optional<ss_param_infos> get_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override;
virtual void set_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override;
virtual optional<ss_param_infos> get_subsingleton_info_nargs(expr const &, unsigned) override;
virtual void set_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override;
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(type_context_old &, expr const &, unsigned) override;
virtual void set_specialization_subsingleton_info_nargs(type_context_old &, expr const &, unsigned, ss_param_infos const &) override;
virtual optional<ss_param_infos> get_specialized_subsingleton_info_nargs(expr const &, unsigned) override;
virtual void set_specialization_subsingleton_info_nargs(expr const &, unsigned, ss_param_infos const &) override;
/* Cache support for congr_lemma module */
virtual optional<congr_lemma> get_simp_congr_lemma(type_context_old &, expr const &, unsigned) override;
virtual void set_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_simp_congr_lemma(expr const &, unsigned) override;
virtual void set_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned) override;
virtual void set_specialized_simp_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_specialized_simp_congr_lemma(expr const &, unsigned) override;
virtual void set_specialized_simp_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_congr_lemma(type_context_old &, expr const &, unsigned) override;
virtual void set_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_congr_lemma(expr const &, unsigned) override;
virtual void set_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_specialized_congr_lemma(type_context_old &, expr const &, unsigned) override;
virtual void set_specialized_congr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_specialized_congr_lemma(expr const &, unsigned) override;
virtual void set_specialized_congr_lemma(expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_hcongr_lemma(type_context_old &, expr const &, unsigned) override;
virtual void set_hcongr_lemma(type_context_old &, expr const &, unsigned, congr_lemma const &) override;
virtual optional<congr_lemma> get_hcongr_lemma(expr const &, unsigned) override;
virtual void set_hcongr_lemma(expr const &, unsigned, congr_lemma const &) override;
/* Cache support for app_builder */
virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, unsigned) override;
virtual void set_app_builder_info(type_context_old &, expr const &, unsigned, app_builder_info const &) override;
virtual optional<app_builder_info> get_app_builder_info(expr const &, unsigned) override;
virtual void set_app_builder_info(expr const &, unsigned, app_builder_info const &) override;
virtual optional<app_builder_info> get_app_builder_info(type_context_old &, expr const &, list<bool> const &) override;
virtual void set_app_builder_info(type_context_old &, expr const &, list<bool> const &, app_builder_info const &) override;
virtual optional<app_builder_info> get_app_builder_info(expr const &, list<bool> const &) override;
virtual void set_app_builder_info(expr const &, list<bool> const &, app_builder_info const &) override;
};
}