refactor(library): move backward lemmas to tactic

src/CMakeLists.txt

@@ -335,6 +335,8 @@ add_subdirectory(library/tactic/defeq_simplifier)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:defeq_simplifier>)
 add_subdirectory(library/tactic/simplifier)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:simplifier>)
+add_subdirectory(library/tactic/backward)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:backward>)
 add_subdirectory(library/definitional)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
 # add_subdirectory(library/blast)

src/library/blast/backward/CMakeLists.txt

@@ -1 +0,0 @@
-add_library(backward OBJECT init_module.cpp backward_action.cpp backward_lemmas.cpp backward_strategy.cpp)

src/library/tactic/backward/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(backward OBJECT init_module.cpp backward_lemmas.cpp)

src/library/tactic/backward/backward_lemmas.cpp

@@ -11,10 +11,9 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/scoped_ext.h"
 #include "library/user_recursors.h"
-#include "library/old_tmp_type_context.h"
+#include "library/type_context.h"
 #include "library/attribute_manager.h"
-#include "library/blast/blast.h"
-#include "library/blast/backward/backward_lemmas.h"
+#include "library/tactic/backward/backward_lemmas.h"
 
 namespace lean {
 static name * g_class_name = nullptr;
@@ -57,10 +56,11 @@ struct backward_config {
 
 typedef scoped_ext<backward_config> backward_ext;
 
-static optional<head_index> get_backward_target(old_tmp_type_context & ctx, expr type) {
+static optional<head_index> get_backward_target(type_context & ctx, expr type) {
+    type_context::tmp_locals locals(ctx);
     while (is_pi(type)) {
-        expr local = ctx.mk_tmp_local(binding_domain(type));
-        type = ctx.whnf(instantiate(binding_body(type), local));
+        expr local  = locals.push_local_from_binding(type);
+        type = ctx.try_to_pi(instantiate(binding_body(type), local));
     }
     expr fn = get_app_fn(type);
     if (is_constant(fn) || is_local(fn))
@@ -69,18 +69,15 @@ static optional<head_index> get_backward_target(old_tmp_type_context & ctx, expr
         return optional<head_index>();
 }
 
-static optional<head_index> get_backward_target(old_tmp_type_context & ctx, name const & c) {
+static optional<head_index> get_backward_target(type_context & ctx, name const & c) {
     declaration const & d = ctx.env().get(c);
-    buffer<level> us;
-    unsigned num_us = d.get_num_univ_params();
-    for (unsigned i = 0; i < num_us; i++)
-        us.push_back(ctx.mk_uvar());
-    expr type = ctx.try_to_pi(instantiate_type_univ_params(d, to_list(us)));
+    list<level> us = param_names_to_levels(d.get_univ_params());
+    expr type      = ctx.try_to_pi(instantiate_type_univ_params(d, us));
     return get_backward_target(ctx, type);
 }
 
 environment add_backward_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent) {
-    old_tmp_type_context ctx(env, ios.get_options());
+    aux_type_context ctx(env, ios.get_options());
     auto index = get_backward_target(ctx, c);
     if (!index || index->kind() != expr_kind::Constant)
         throw exception(sstream() << "invalid [intro] attribute for '" << c << "', head symbol of resulting type must be a constant");
@@ -99,6 +96,7 @@ void initialize_backward_lemmas() {
     g_class_name = new name("backward");
     g_key        = new std::string("BWD");
     backward_ext::initialize();
+    register_trace_class(name{"tactic", "back_chaining"});
     register_prio_attribute("intro", "introduction rule for backward chaining",
                             add_backward_lemma,
                             is_backward_lemma,
@@ -116,30 +114,26 @@ void finalize_backward_lemmas() {
     delete g_class_name;
 }
 
-namespace blast {
 unsigned backward_lemma_prio_fn::operator()(backward_lemma const & r) const {
     if (r.is_universe_polymorphic()) {
         name const & n = r.to_name();
-        auto const & s = backward_ext::get_state(env());
-        if (auto prio = s.get_prio(n))
+        if (auto prio = m_prios.get_prio(n))
             return *prio;
     }
     return LEAN_DEFAULT_PRIORITY;
 }
 
-void backward_lemma_index::init() {
-    m_index.clear();
+backward_lemma_index::backward_lemma_index(type_context & ctx):
+    m_index(backward_lemma_prio_fn(backward_ext::get_state(ctx.env()))) {
     buffer<name> lemmas;
-    blast_old_tmp_type_context ctx;
-    auto const & s = backward_ext::get_state(env());
+    auto const & s = backward_ext::get_state(ctx.env());
     s.to_buffer(lemmas);
     unsigned i = lemmas.size();
     while (i > 0) {
         --i;
-        ctx->clear();
-        optional<head_index> target = get_backward_target(*ctx, lemmas[i]);
+        optional<head_index> target = get_backward_target(ctx, lemmas[i]);
         if (!target || target->kind() != expr_kind::Constant) {
-            lean_trace(name({"blast", "event"}),
+            lean_trace(name({"tactic", "back_chaining"}),
                        tout() << "discarding [intro] lemma '" << lemmas[i] << "', failed to find target type\n";);
         } else {
             m_index.insert(*target, backward_lemma(lemmas[i]));
@@ -147,18 +141,16 @@ void backward_lemma_index::init() {
     }
 }
 
-void backward_lemma_index::insert(expr const & href) {
-    blast_old_tmp_type_context ctx;
-    expr href_type = ctx->infer(href);
-    if (optional<head_index> target = get_backward_target(*ctx, href_type)) {
+void backward_lemma_index::insert(type_context & ctx, expr const & href) {
+    expr href_type = ctx.infer(href);
+    if (optional<head_index> target = get_backward_target(ctx, href_type)) {
         m_index.insert(*target, backward_lemma(gexpr(href)));
     }
 }
 
-void backward_lemma_index::erase(expr const & href) {
-    blast_old_tmp_type_context ctx;
-    expr href_type = ctx->infer(href);
-    if (optional<head_index> target = get_backward_target(*ctx, href_type)) {
+void backward_lemma_index::erase(type_context & ctx, expr const & href) {
+    expr href_type = ctx.infer(href);
+    if (optional<head_index> target = get_backward_target(ctx, href_type)) {
         m_index.erase(*target, backward_lemma(gexpr(href)));
     }
 }
@@ -169,4 +161,4 @@ list<backward_lemma> backward_lemma_index::find(head_index const & h) const {
     else
         return list<backward_lemma>();
 }
-}}
+}

src/library/tactic/backward/backward_lemmas.h

@@ -5,10 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "util/priority_queue.h"
 #include "kernel/environment.h"
 #include "library/io_state.h"
 #include "library/head_map.h"
-#include "library/blast/gexpr.h"
+#include "library/type_context.h"
+#include "library/tactic/gexpr.h"
 
 namespace lean {
 environment add_backward_lemma(environment const & env, io_state const & ios, name const & c, unsigned prio, name const & ns, bool persistent);
@@ -16,17 +18,20 @@ bool is_backward_lemma(environment const & env, name const & n);
 void get_backward_lemmas(environment const & env, buffer<name> & r);
 void initialize_backward_lemmas();
 void finalize_backward_lemmas();
-namespace blast {
+
 typedef gexpr backward_lemma;
-struct backward_lemma_prio_fn { unsigned operator()(backward_lemma const & r) const; };
-/* The following indices are based on blast current set of opaque/reducible constants. They
-   must be rebuilt whenever a key is "unfolded by blast */
+struct backward_lemma_prio_fn {
+    priority_queue<name, name_quick_cmp> m_prios;
+    backward_lemma_prio_fn(priority_queue<name, name_quick_cmp> const & prios):m_prios(prios) {}
+    unsigned operator()(backward_lemma const & r) const;
+};
+
 class backward_lemma_index {
     head_map_prio<backward_lemma, backward_lemma_prio_fn> m_index;
 public:
-    void init();
-    void insert(expr const & href);
-    void erase(expr const & href);
+    backward_lemma_index(type_context & ctx);
+    void insert(type_context & ctx, expr const & href);
+    void erase(type_context & ctx, expr const & href);
     list<backward_lemma> find(head_index const & h) const;
 };
-}}
+}

src/library/tactic/backward/init_module.cpp

@@ -3,21 +3,15 @@ Copyright (c) 2015 Daniel Selsam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Daniel Selsam
 */
-#include "library/blast/backward/init_module.h"
-#include "library/blast/backward/backward_lemmas.h"
-#include "library/blast/backward/backward_strategy.h"
+#include "library/tactic/backward/init_module.h"
+#include "library/tactic/backward/backward_lemmas.h"
 
 namespace lean {
-namespace blast {
-
 void initialize_backward_module() {
     initialize_backward_lemmas();
-    initialize_backward_strategy();
 }
 
 void finalize_backward_module() {
-    finalize_backward_strategy();
     finalize_backward_lemmas();
 }
 }
-}

src/library/tactic/backward/init_module.h

@@ -4,10 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Daniel Selsam
 */
 #pragma once
-
 namespace lean {
-namespace blast {
 void initialize_backward_module();
 void finalize_backward_module();
 }
-}

src/library/tactic/init_module.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/tactic/elaborate.h"
 #include "library/tactic/defeq_simplifier/init_module.h"
 #include "library/tactic/simplifier/init_module.h"
+#include "library/tactic/backward/init_module.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -44,12 +45,14 @@ void initialize_tactic_module() {
     initialize_induction_tactic();
     initialize_defeq_simplifier_module();
     initialize_simplifier_module();
+    initialize_backward_module();
     initialize_elaborate();
 }
 void finalize_tactic_module() {
     finalize_elaborate();
-    finalize_defeq_simplifier_module();
+    finalize_backward_module();
     finalize_simplifier_module();
+    finalize_defeq_simplifier_module();
     finalize_induction_tactic();
     finalize_ac_tactics();
     finalize_match_tactic();