From 5f5e4fe7fb9310f7b2fdc75780b5d019862c32ae Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Dec 2015 17:07:09 -0800 Subject: [PATCH] feat(library/blast/grinder): add intro/elim lemmas --- src/CMakeLists.txt | 2 + src/library/blast/forward/forward_lemma_set.h | 4 +- src/library/blast/forward/pattern.cpp | 4 +- src/library/blast/grinder/CMakeLists.txt | 1 + src/library/blast/grinder/init_module.cpp | 19 ++++ src/library/blast/grinder/init_module.h | 14 +++ .../blast/grinder/intro_elim_lemmas.cpp | 100 ++++++++++++++++++ src/library/blast/grinder/intro_elim_lemmas.h | 28 +++++ src/library/blast/init_module.cpp | 3 + 9 files changed, 171 insertions(+), 4 deletions(-) create mode 100644 src/library/blast/grinder/CMakeLists.txt create mode 100644 src/library/blast/grinder/init_module.cpp create mode 100644 src/library/blast/grinder/init_module.h create mode 100644 src/library/blast/grinder/intro_elim_lemmas.cpp create mode 100644 src/library/blast/grinder/intro_elim_lemmas.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 46d4bbb07..a2b11b0c5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -357,6 +357,8 @@ add_subdirectory(library/blast/actions) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/blast/strategies) set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(library/blast/grinder) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/blast/simplifier) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/error_handling) diff --git a/src/library/blast/forward/forward_lemma_set.h b/src/library/blast/forward/forward_lemma_set.h index 98e45efb1..202010296 100644 --- a/src/library/blast/forward/forward_lemma_set.h +++ b/src/library/blast/forward/forward_lemma_set.h @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include "util/rb_tree.h" #include "kernel/expr.h" -#ifndef LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY -#define LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY 1000 +#ifndef LEAN_FORWARD_DEFAULT_PRIORITY +#define LEAN_FORWARD_DEFAULT_PRIORITY 1000 #endif namespace lean { diff --git a/src/library/blast/forward/pattern.cpp b/src/library/blast/forward/pattern.cpp index 9704bb51d..6ab003836 100644 --- a/src/library/blast/forward/pattern.cpp +++ b/src/library/blast/forward/pattern.cpp @@ -619,7 +619,7 @@ hi_lemma mk_hi_lemma_core(tmp_type_context & ctx, expr const & H, unsigned num_u hi_lemma mk_hi_lemma(expr const & H) { blast_tmp_type_context ctx; unsigned max_steps = get_config().m_pattern_max_steps; - return mk_hi_lemma_core(*ctx, H, 0, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY, max_steps); + return mk_hi_lemma_core(*ctx, H, 0, LEAN_FORWARD_DEFAULT_PRIORITY, max_steps); } hi_lemma mk_hi_lemma(name const & c, unsigned priority) { @@ -638,7 +638,7 @@ hi_lemma mk_hi_lemma(name const & c, unsigned priority) { list mk_multipatterns(environment const & env, io_state const & ios, name const & c) { blast::scope_debug scope(env, ios); // we regenerate the patterns to make sure they reflect the current set of reducible constants - auto lemma = blast::mk_hi_lemma(c, LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY); + auto lemma = blast::mk_hi_lemma(c, LEAN_FORWARD_DEFAULT_PRIORITY); return lemma.m_multi_patterns; } diff --git a/src/library/blast/grinder/CMakeLists.txt b/src/library/blast/grinder/CMakeLists.txt new file mode 100644 index 000000000..9ba50b59b --- /dev/null +++ b/src/library/blast/grinder/CMakeLists.txt @@ -0,0 +1 @@ +add_library(blast_grinder OBJECT init_module.cpp intro_elim_lemmas.cpp) diff --git a/src/library/blast/grinder/init_module.cpp b/src/library/blast/grinder/init_module.cpp new file mode 100644 index 000000000..c4b4c6bf7 --- /dev/null +++ b/src/library/blast/grinder/init_module.cpp @@ -0,0 +1,19 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/blast/grinder/init_module.h" +#include "library/blast/grinder/intro_elim_lemmas.h" + +namespace lean { +namespace blast { +void initialize_grinder_module() { + initialize_intro_elim_lemmas(); +} + +void finalize_grinder_module() { + finalize_intro_elim_lemmas(); +} +}} diff --git a/src/library/blast/grinder/init_module.h b/src/library/blast/grinder/init_module.h new file mode 100644 index 000000000..19f50169f --- /dev/null +++ b/src/library/blast/grinder/init_module.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +namespace blast { +void initialize_grinder_module(); +void finalize_grinder_module(); +} +} diff --git a/src/library/blast/grinder/intro_elim_lemmas.cpp b/src/library/blast/grinder/intro_elim_lemmas.cpp new file mode 100644 index 000000000..98149745c --- /dev/null +++ b/src/library/blast/grinder/intro_elim_lemmas.cpp @@ -0,0 +1,100 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "util/priority_queue.h" +#include "kernel/instantiate.h" +#include "library/scoped_ext.h" +#include "library/user_recursors.h" +#include "library/type_context.h" + +namespace lean { +static name * g_class_name = nullptr; +static std::string * g_key = nullptr; + +struct intro_elim_state { + priority_queue m_elim_lemmas; + priority_queue m_intro_lemmas; +}; + +typedef std::tuple intro_elim_entry; + +struct intro_elim_config { + typedef intro_elim_entry entry; + typedef intro_elim_state state; + + static void add_entry(environment const &, io_state const &, state & s, entry const & e) { + bool is_elim; unsigned prio; name n; + std::tie(is_elim, prio, n) = e; + if (is_elim) { + s.m_elim_lemmas.insert(n, prio); + } else { + s.m_intro_lemmas.insert(n, prio); + } + } + static name const & get_class_name() { + return *g_class_name; + } + static std::string const & get_serialization_key() { + return *g_key; + } + static void write_entry(serializer & s, entry const & e) { + bool is_elim; unsigned prio; name n; + std::tie(is_elim, prio, n) = e; + s << is_elim << prio << n; + } + static entry read_entry(deserializer & d) { + bool is_elim; unsigned prio; name n; + d >> is_elim >> prio >> n; + return entry(is_elim, prio, n); + } + static optional get_fingerprint(entry const & e) { + bool is_elim; unsigned prio; name n; + std::tie(is_elim, prio, n) = e; + return some(hash(hash(n.hash(), prio), is_elim ? 17u : 31u)); + } +}; + +typedef scoped_ext intro_elim_ext; + +environment add_elim_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) { + // TODO(Leo): VALIDATE + return intro_elim_ext::add_entry(env, ios, intro_elim_entry(true, prio, c), ns, persistent); +} + +environment add_intro_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) { + // TODO(Leo): VALIDATE + return intro_elim_ext::add_entry(env, ios, intro_elim_entry(false, prio, c), ns, persistent); +} + +bool is_elim_lemma(environment const & env, name const & c) { + return intro_elim_ext::get_state(env).m_elim_lemmas.contains(c); +} + +bool is_intro_lemma(environment const & env, name const & c) { + return intro_elim_ext::get_state(env).m_intro_lemmas.contains(c); +} + +void get_elim_lemmas(environment const & env, buffer & r) { + return intro_elim_ext::get_state(env).m_elim_lemmas.to_buffer(r); +} + +void get_intro_lemmas(environment const & env, buffer & r) { + return intro_elim_ext::get_state(env).m_intro_lemmas.to_buffer(r); +} + +void initialize_intro_elim_lemmas() { + g_class_name = new name("grinder"); + g_key = new std::string("grinder"); + intro_elim_ext::initialize(); +} + +void finalize_intro_elim_lemmas() { + intro_elim_ext::finalize(); + delete g_key; + delete g_class_name; +} +} diff --git a/src/library/blast/grinder/intro_elim_lemmas.h b/src/library/blast/grinder/intro_elim_lemmas.h new file mode 100644 index 000000000..7dd7b05dc --- /dev/null +++ b/src/library/blast/grinder/intro_elim_lemmas.h @@ -0,0 +1,28 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" +#include "library/io_state.h" + +#ifndef LEAN_ELIM_DEFAULT_PRIORITY +#define LEAN_ELIM_DEFAULT_PRIORITY 1000 +#endif + +#ifndef LEAN_INTRO_DEFAULT_PRIORITY +#define LEAN_INTRO_DEFAULT_PRIORITY 1000 +#endif + +namespace lean { +environment add_elim_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent); +environment add_intro_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent); +bool is_elim_lemma(environment const & env, name const & c); +bool is_intro_lemma(environment const & env, name const & c); +void get_elim_lemmas(environment const & env, buffer & r); +void get_intro_lemmas(environment const & env, buffer & r); +void initialize_intro_elim_lemmas(); +void finalize_intro_elim_lemmas(); +} diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp index 87ea22136..4466873b0 100644 --- a/src/library/blast/init_module.cpp +++ b/src/library/blast/init_module.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/blast/forward/init_module.h" #include "library/blast/unit/init_module.h" #include "library/blast/actions/init_module.h" +#include "library/blast/grinder/init_module.h" namespace lean { void initialize_blast_module() { @@ -27,8 +28,10 @@ void initialize_blast_module() { initialize_blast_tactic(); blast::initialize_actions_module(); blast::initialize_congruence_closure(); + blast::initialize_grinder_module(); } void finalize_blast_module() { + blast::finalize_grinder_module(); blast::finalize_congruence_closure(); blast::finalize_actions_module(); finalize_blast_tactic();