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

refactor(library/blast/expr): remove unnecessary complexity

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-09 12:27:33 -08:00
parent 623d677215
commit d952a1d299
3 changed files with 8 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -756,10 +756,11 @@ void scope_assignment::commit() {
}
struct scope_debug::imp {
scope_hash_consing m_scope1;
blastenv m_benv;
scope_blastenv m_scope2;
scoped_expr_caching m_scope1;
blastenv m_benv;
scope_blastenv m_scope2;
imp(environment const & env, io_state const & ios):
m_scope1(true),
m_benv(env, ios, list<name>(), list<name>()),
m_scope2(m_benv) {
expr aux_mvar = mk_metavar("dummy_mvar", mk_true());
@ -847,7 +848,7 @@ expr internalize(expr const & e) {
}
optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
goal const & g) {
blast::scope_hash_consing scope1;
scoped_expr_caching scope1(true);
blast::blastenv b(env, ios, ls, ds);
blast::scope_blastenv scope2(b);
return b(g);

49
src/library/blast/expr.cpp
View file

@ -13,34 +13,11 @@ Author: Leonardo de Moura
#include "kernel/instantiate_univ_cache.h"
#include "library/blast/expr.h"
#ifndef LEAN_BLAST_INST_UNIV_CACHE_SIZE
#define LEAN_BLAST_INST_UNIV_CACHE_SIZE 1023
#endif
namespace lean {
namespace blast {
static name * g_prefix = nullptr;
static expr * g_dummy_type = nullptr; // dummy type for href/mref
typedef typename std::vector<expr> expr_array;
LEAN_THREAD_PTR(expr_array, g_mref_array);
LEAN_THREAD_PTR(expr_array, g_href_array);
scope_hash_consing::scope_hash_consing():
scoped_expr_caching(true) {
lean_assert(g_mref_array == nullptr);
lean_assert(g_href_array == nullptr);
g_mref_array = new expr_array();
g_href_array = new expr_array();
}
scope_hash_consing::~scope_hash_consing() {
delete g_mref_array;
delete g_href_array;
g_mref_array = nullptr;
g_href_array = nullptr;
}
level mk_uref(unsigned idx) {
return lean::mk_meta_univ(name(*g_prefix, idx));
}
@ -54,38 +31,16 @@ unsigned uref_index(level const & l) {
return meta_id(l).get_numeral();
}
static expr mk_href_core(unsigned idx) {
return lean::mk_local(name(*g_prefix, idx), *g_dummy_type);
}
expr mk_href(unsigned idx) {
lean_assert(g_href_array);
while (g_href_array->size() <= idx) {
unsigned j = g_href_array->size();
expr new_ref = mk_href_core(j);
g_href_array->push_back(new_ref);
}
lean_assert(idx < g_href_array->size());
return (*g_href_array)[idx];
return lean::mk_local(name(*g_prefix, idx), *g_dummy_type);
}
bool is_href(expr const & e) {
return lean::is_local(e) && mlocal_type(e) == *g_dummy_type;
}
static expr mk_mref_core(unsigned idx) {
return mk_metavar(name(*g_prefix, idx), *g_dummy_type);
}
expr mk_mref(unsigned idx) {
lean_assert(g_mref_array);
while (g_mref_array->size() <= idx) {
unsigned j = g_mref_array->size();
expr new_ref = mk_mref_core(j);
g_mref_array->push_back(new_ref);
}
lean_assert(idx < g_mref_array->size());
return (*g_mref_array)[idx];
return mk_metavar(name(*g_prefix, idx), *g_dummy_type);
}
bool is_mref(expr const & e) {

20
src/library/blast/expr.h
View file

@ -10,22 +10,6 @@ Author: Leonardo de Moura
namespace lean {
namespace blast {
// API for creating maximally shared terms used by the blast tactic.
// The API assumes there is a single blast tactic using theses terms.
// The expression hash-consing tables are thread local and implemented
// in the kernel
// Remark: All procedures assume the children levels and expressions are maximally shared.
// That is, it assumes they have been created using the APIs provided by this module.
// Auxiliary object for resetting the the thread local hash-consing tables.
// It also uses an assertion to make sure it is not being used in a recursion.
class scope_hash_consing : public scoped_expr_caching {
public:
scope_hash_consing();
~scope_hash_consing();
};
level mk_uref(unsigned idx);
bool is_uref(level const & l);
@ -45,9 +29,7 @@ bool has_href(expr const & e);
/** \brief Return true iff \c e contain mref's */
bool has_mref(expr const & e);
inline bool is_local_non_href(expr const & e) {
return is_local(e) && !is_href(e);
}
inline bool is_local_non_href(expr const & e) { return is_local(e) && !is_href(e); }
void initialize_expr();
void finalize_expr();