feat(library/blast/grinder): add intro/elim lemmas

src/CMakeLists.txt

@@ -357,6 +357,8 @@ add_subdirectory(library/blast/actions)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_actions>)
 add_subdirectory(library/blast/strategies)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_strategies>)
+add_subdirectory(library/blast/grinder)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast_grinder>)
 add_subdirectory(library/blast/simplifier)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
 add_subdirectory(library/error_handling)

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
+#ifndef LEAN_FORWARD_DEFAULT_PRIORITY
-#define LEAN_FORWARD_LEMMA_DEFAULT_PRIORITY 1000
+#define LEAN_FORWARD_DEFAULT_PRIORITY 1000
 #endif
 
 namespace lean {

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<multi_pattern> 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;
 }
 

src/library/blast/grinder/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(blast_grinder OBJECT init_module.cpp intro_elim_lemmas.cpp)

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();
+}
+}}

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();
+}
+}

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 <string>
+#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<name, name_quick_cmp> m_elim_lemmas;
+    priority_queue<name, name_quick_cmp> m_intro_lemmas;
+};
+
+typedef std::tuple<bool, unsigned, name> 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<unsigned> 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_config> 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<name> & r) {
+    return intro_elim_ext::get_state(env).m_elim_lemmas.to_buffer(r);
+}
+
+void get_intro_lemmas(environment const & env, buffer<name> & 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;
+}
+}

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<name> & r);
+void get_intro_lemmas(environment const & env, buffer<name> & r);
+void initialize_intro_elim_lemmas();
+void finalize_intro_elim_lemmas();
+}

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();