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

feat(library/blast): add is_hi_lemma

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-25 17:52:59 -08:00
parent d395a54165
commit 996a660de8
2 changed files with 23 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/library/blast/forward/pattern.cpp
View file

@ -141,6 +141,7 @@ struct hi_entry {
struct hi_state {
name_set m_no_patterns;
name_set m_lemma_names;
hi_lemmas m_lemmas;
};
@ -154,6 +155,16 @@ deserializer & operator>>(deserializer & d, multi_pattern & mp) {
return d;
}
static optional<name> get_hi_lemma_name(expr const & H) {
if (is_lambda(H))
return get_hi_lemma_name(binding_body(H));
expr const & f = get_app_fn(H);
if (is_constant(f))
return optional<name>(const_name(f));
else
return optional<name>();
}
struct hi_config {
typedef hi_entry entry;
typedef hi_state state;
@ -162,6 +173,8 @@ struct hi_config {
if (e.m_no_pattern) {
s.m_no_patterns.insert(*e.m_no_pattern);
} else {
if (auto n = get_hi_lemma_name(e.m_lemma.m_proof))
s.m_lemma_names.insert(*n);
for (multi_pattern const & mp : e.m_lemma.m_multi_patterns) {
for (expr const & p : mp) {
lean_assert(is_app(p));
@ -326,7 +339,9 @@ hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, fun_info_manager & fm, expr co
unsigned priority) {
// TODO(Leo):
std::cout << H << "\n";
return hi_lemma();
hi_lemma r;
r.m_proof = H; // fix
return r;
}
hi_lemma mk_hi_lemma(tmp_type_context & ctx, fun_info_manager & fm, expr const & H) {
@ -346,6 +361,10 @@ environment add_hi_lemma(environment const & env, name const & c, unsigned prior
persistent);
}
bool is_hi_lemma(environment const & env, name const & c) {
return hi_ext::get_state(env).m_lemma_names.contains(c);
}
/** pattern_le */
struct pattern_le_fn {
tmp_type_context & m_ctx;

3
src/library/blast/forward/pattern.h
View file

@ -54,6 +54,9 @@ typedef rb_multi_map<name, hi_lemma, name_quick_cmp> hi_lemmas;
/** \brief Add the given theorem as a heuristic instantiation lemma in the current environment. */
environment add_hi_lemma(environment const & env, name const & c, unsigned priority, bool persistent);
/** \brief Return true iff \c c was added as a heuristic instantiation lemma */
bool is_hi_lemma(environment const & env, name const & c);
/** \brief Retrieve the active set of heuristic instantiation lemmas. */
hi_lemmas get_hi_lemma_index(environment const & env);