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

fix(library/blast): init_classical_flag

Browse source 
The procedure get_namespaces does not return the set of opened
namespaces. I added a comment there to clarify that.
This commit is contained in:
Leonardo de Moura 2015-12-04 08:13:19 -08:00
parent 0dfac6d07e
commit 83b9769225
4 changed files with 15 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/library/blast/blast.cpp
View file

@ -466,20 +466,24 @@ public:
}
void init_classical_flag() {
for_each(get_namespaces(m_env), [&](name const & ns) {
if (m_classical) return;
if (ns == get_classical_name()) m_classical = true;
});
if (is_standard(env())) {
expr p = m_tmp_ctx->mk_tmp_local(mk_Prop());
expr dec_p = mk_app(mk_constant(get_decidable_name()), p);
if (m_tmp_ctx->mk_class_instance(dec_p)) {
m_classical = true;
}
m_tmp_ctx->clear_cache();
}
}
bool classical() { return m_classical; }
void init_state(goal const & g) {
init_curr_state(g);
init_classical_flag();
save_initial_context();
m_tctx.set_local_instances(m_initial_context);
m_tmp_ctx->set_local_instances(m_initial_context);
init_classical_flag();
}
optional<expr> operator()(goal const & g) {

4
src/library/constants.cpp
View file

@ -23,6 +23,7 @@ name const * g_classical = nullptr;
name const * g_congr = nullptr;
name const * g_congr_arg = nullptr;
name const * g_congr_fun = nullptr;
name const * g_decidable = nullptr;
name const * g_dite = nullptr;
name const * g_div = nullptr;
name const * g_empty = nullptr;
@ -201,6 +202,7 @@ void initialize_constants() {
g_congr = new name{"congr"};
g_congr_arg = new name{"congr_arg"};
g_congr_fun = new name{"congr_fun"};
g_decidable = new name{"decidable"};
g_dite = new name{"dite"};
g_div = new name{"div"};
g_empty = new name{"empty"};
@ -380,6 +382,7 @@ void finalize_constants() {
delete g_congr;
delete g_congr_arg;
delete g_congr_fun;
delete g_decidable;
delete g_dite;
delete g_div;
delete g_empty;
@ -558,6 +561,7 @@ name const & get_classical_name() { return *g_classical; }
name const & get_congr_name() { return *g_congr; }
name const & get_congr_arg_name() { return *g_congr_arg; }
name const & get_congr_fun_name() { return *g_congr_fun; }
name const & get_decidable_name() { return *g_decidable; }
name const & get_dite_name() { return *g_dite; }
name const & get_div_name() { return *g_div; }
name const & get_empty_name() { return *g_empty; }

1
src/library/constants.h
View file

@ -25,6 +25,7 @@ name const & get_classical_name();
name const & get_congr_name();
name const & get_congr_arg_name();
name const & get_congr_fun_name();
name const & get_decidable_name();
name const & get_dite_name();
name const & get_div_name();
name const & get_empty_name();

1
src/library/constants.txt
View file

@ -18,6 +18,7 @@ classical
congr
congr_arg
congr_fun
decidable
dite
div
empty