feat(library/blast/grinder): add grinder actions

src/library/blast/actions/recursor_action.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "library/blast/hypothesis.h"
 namespace lean {
 namespace blast {
+action_result recursor_action(hypothesis_idx hidx, name const & R);
 action_result recursor_preprocess_action(hypothesis_idx hidx);
 action_result recursor_action();
 

src/library/blast/backward/backward_action.cpp

@@ -114,7 +114,7 @@ public:
     }
 };
 
-action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branches, char const * action_name) {
+action_result backward_action_core(list<gexpr> const & lemmas, bool prop_only_branches, char const * action_name, bool cut) {
     state  s = curr_state();
     auto it  = lemmas;
     while (!empty(it)) {
@@ -122,7 +122,7 @@ action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branche
         it              = tail(it);
         if (!failed(r)) {
             // create choice point
-            if (!empty(it))
+            if (!cut && !empty(it))
                 push_choice_point(choice_point(new backward_choice_point_cell(s, it, prop_only_branches)));
             trace_action(action_name);
             return r;
@@ -133,7 +133,11 @@ action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branche
 }
 
 action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branches) {
-    return backward_action(lemmas, prop_only_branches, "backward");
+    return backward_action_core(lemmas, prop_only_branches, "backward", false);
+}
+
+action_result backward_cut_action(list<gexpr> const & lemmas, bool prop_only_branches) {
+    return backward_action_core(lemmas, prop_only_branches, "backward", true);
 }
 
 action_result constructor_action(bool prop_only_branches) {
@@ -146,6 +150,6 @@ action_result constructor_action(bool prop_only_branches) {
     buffer<gexpr> lemmas;
     for (name c_name : c_names)
         lemmas.push_back(gexpr(c_name));
-    return backward_action(to_list(lemmas), prop_only_branches, "constructor");
+    return backward_action_core(to_list(lemmas), prop_only_branches, "constructor", false);
 }
 }}

src/library/blast/backward/backward_action.h

@@ -11,5 +11,8 @@ Author: Leonardo de Moura
 namespace lean {
 namespace blast {
 action_result backward_action(list<gexpr> const & lemmas, bool prop_only_branches = true);
+/** Similar to previous action, but does not generate a choice point.
+    It commits to the first lemma that unifies with the target */
+action_result backward_cut_action(list<gexpr> const & lemmas, bool prop_only_branches = true);
 action_result constructor_action(bool prop_only_branches = true);
 }}

src/library/blast/grinder/CMakeLists.txt

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

src/library/blast/grinder/grinder_actions.cpp

@@ -0,0 +1,65 @@
+/*
+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/blast.h"
+#include "library/blast/actions/recursor_action.h"
+#include "library/blast/backward/backward_action.h"
+#include "library/blast/grinder/intro_elim_lemmas.h"
+
+namespace lean {
+namespace blast {
+static unsigned g_ext_id = 0;
+
+struct grinder_branch_extension : public branch_extension {
+    head_map<gexpr> m_intro_lemmas;
+    name_map<name>  m_elim_lemmas;
+
+    grinder_branch_extension() {}
+    grinder_branch_extension(grinder_branch_extension const &) {}
+    virtual ~grinder_branch_extension() {}
+    virtual branch_extension * clone() override { return new grinder_branch_extension(*this); }
+    virtual void initialized() override {
+        m_intro_lemmas = mk_intro_lemma_index();
+        m_elim_lemmas  = mk_elim_lemma_index();
+    }
+};
+
+void initialize_grinder_actions() {
+    g_ext_id = register_branch_extension(new grinder_branch_extension());
+}
+
+void finalize_grinder_actions() {}
+
+static grinder_branch_extension & get_ext() {
+    return static_cast<grinder_branch_extension&>(curr_state().get_extension(g_ext_id));
+}
+
+action_result grinder_elim_action(hypothesis_idx hidx) {
+    grinder_branch_extension & ext = get_ext();
+    state & s                      = curr_state();
+    hypothesis const & h           = s.get_hypothesis_decl(hidx);
+    expr const & f                 = get_app_fn(h.get_type());
+    if (!is_constant(f))
+        return action_result::failed();
+    auto R = ext.m_elim_lemmas.find(const_name(f));
+    if (!R)
+        return action_result::failed();
+    return recursor_action(hidx, *R);
+}
+
+action_result grinder_intro_action() {
+    grinder_branch_extension & ext = get_ext();
+    state & s                      = curr_state();
+    expr const & target            = s.get_target();
+    expr const & f                 = get_app_fn(target);
+    if (!is_constant(f))
+        return action_result::failed();
+    list<gexpr> const * lemmas = ext.m_intro_lemmas.find(head_index(f));
+    if (!lemmas)
+        return action_result::failed();
+    return backward_cut_action(*lemmas);
+}
+}}

src/library/blast/grinder/grinder_actions.h

@@ -0,0 +1,17 @@
+/*
+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 "library/blast/action_result.h"
+#include "library/blast/hypothesis.h"
+
+namespace lean {
+namespace blast {
+action_result grinder_elim_action(hypothesis_idx hidx);
+action_result grinder_intro_action();
+void initialize_grinder_actions();
+void finalize_grinder_actions();
+}}

src/library/blast/grinder/init_module.cpp

@@ -6,14 +6,17 @@ Author: Leonardo de Moura
 */
 #include "library/blast/grinder/init_module.h"
 #include "library/blast/grinder/intro_elim_lemmas.h"
+#include "library/blast/grinder/grinder_actions.h"
 
 namespace lean {
 namespace blast {
 void initialize_grinder_module() {
     initialize_intro_elim_lemmas();
+    initialize_grinder_actions();
 }
 
 void finalize_grinder_module() {
+    finalize_grinder_actions();
     finalize_intro_elim_lemmas();
 }
 }}

src/library/blast/grinder/intro_elim_lemmas.cpp

@@ -11,6 +11,8 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "library/user_recursors.h"
 #include "library/tmp_type_context.h"
+#include "library/blast/blast.h"
+#include "library/blast/grinder/intro_elim_lemmas.h"
 
 namespace lean {
 static name * g_class_name = nullptr;
@@ -119,4 +121,39 @@ void finalize_intro_elim_lemmas() {
     delete g_key;
     delete g_class_name;
 }
+
+namespace blast {
+head_map<gexpr> mk_intro_lemma_index() {
+    head_map<gexpr> r;
+    buffer<name> lemmas;
+    blast_tmp_type_context ctx;
+    get_intro_lemmas(env(), lemmas);
+    unsigned i = lemmas.size();
+    while (i > 0) {
+        --i;
+        ctx->clear();
+        optional<name> target = get_intro_target(*ctx, lemmas[i]);
+        if (!target) {
+            // TODO(Leo): generate event
+        } else {
+            r.insert(head_index(*target), gexpr(lemmas[i]));
         }
+    }
+    return r;
+}
+
+name_map<name> mk_elim_lemma_index() {
+    name_map<name> r;
+    buffer<name> lemmas;
+    get_elim_lemmas(env(), lemmas);
+    for (name const & lemma : lemmas) {
+        try {
+            recursor_info info = get_recursor_info(env(), lemma);
+            r.insert(info.get_type_name(), lemma);
+        } catch (exception &) {
+            // TODO(Leo): generate event
+        }
+    }
+    return r;
+}
+}}

src/library/blast/grinder/intro_elim_lemmas.h

@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/environment.h"
 #include "library/io_state.h"
+#include "library/head_map.h"
+#include "library/blast/gexpr.h"
 
 #ifndef LEAN_ELIM_DEFAULT_PRIORITY
 #define LEAN_ELIM_DEFAULT_PRIORITY 1000
@@ -25,4 +27,9 @@ 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();
-}
+namespace blast {
+/* The following indices are based on blast current set of opaque/reducible constants. They
+   must be rebuilt whenever a key is "unfolded by blast */
+head_map<gexpr> mk_intro_lemma_index();
+name_map<name>  mk_elim_lemma_index();
+}}