feat(library/blast): add helper functions to access blast tactic thread local state/context

src/library/blast/blast.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/blast/expr.h"
 #include "library/blast/state.h"
 #include "library/blast/blast.h"
+#include "library/blast/blast_context.h"
 #include "library/blast/blast_exception.h"
 
 namespace lean {
@@ -37,7 +38,8 @@ class context {
     io_state       m_ios;
     name_set       m_lemma_hints;
     name_set       m_unfold_hints;
-    name_map<expr> m_mvar2mref; // map goal metavariables to blast mref's
+    name_map<expr> m_mvar2mref;    // map goal metavariables to blast mref's
+    state          m_curr_state;   // current state
 
     class to_blast_expr_fn : public replace_visitor {
         type_checker                 m_tc;
@@ -208,15 +210,59 @@ public:
     }
 
     optional<expr> operator()(goal const & g) {
-        state s = to_state(g);
+        m_curr_state = to_state(g);
+        // TODO(Leo): blast main loop
         return none_expr();
     }
+
+    environment const & get_env() const { return m_env; }
+
+    io_state const & get_ios() const { return m_ios; }
+
+    state const & get_curr_state() const { return m_curr_state; }
 };
+
+LEAN_THREAD_PTR(context, g_context);
+struct scope_context {
+    context * m_prev_context;
+public:
+    scope_context(context & c):m_prev_context(g_context) { g_context = &c; }
+    ~scope_context() { g_context = m_prev_context; }
+};
+
+environment const & env() {
+    lean_assert(g_context);
+    return g_context->get_env();
+}
+
+io_state const & ios() {
+    lean_assert(g_context);
+    return g_context->get_ios();
+}
+
+state const & curr_state() {
+    lean_assert(g_context);
+    return g_context->get_curr_state();
+}
+
+void display_curr_state() {
+    curr_state().display(env(), ios());
+    display("\n");
+}
+
+void display(char const * msg) {
+    ios().get_diagnostic_channel() << msg;
+}
+
+void display(sstream const & msg) {
+    ios().get_diagnostic_channel() << msg.str();
+}
 }
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g) {
-    blast::scope_hash_consing scope;
+    blast::scope_hash_consing scope1;
     blast::context c(env, ios, ls, ds);
+    blast::scope_context scope2(c);
     return c(g);
 }
 void initialize_blast() {}

src/library/blast/blast_context.h

@@ -0,0 +1,29 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+
+API for accessing the thread local context used by the blast tactic.
+These procedures can only be invoked while the blast tactic is being executed.
+
+Remark: the API is implemented in the file blast.cpp
+*/
+#pragma once
+#include "util/sstream.h"
+#include "library/blast/state.h"
+
+namespace lean {
+namespace blast {
+/** \brief Return the thread local environment being used by the blast tactic. */
+environment const & env();
+/** \brief Return the thread local io_state being used by the blast tactic. */
+io_state const & ios();
+/** \brief Return the thread local current state begin processed by the blast tactic. */
+state const & curr_state();
+/** \brief Display the current state of the blast tactic in the diagnostic channel. */
+void display_curr_state();
+/** \brief Display message in the blast tactic diagnostic channel. */
+void display(char const * msg);
+void display(sstream const & msg);
+}}

src/library/blast/state.cpp

@@ -79,7 +79,7 @@ goal state::to_goal(branch const & b) const {
         hypothesis const * h = b.get(hidx);
         lean_assert(h);
         // after we add support for let-decls in goals, we must convert back h->get_value() if it is available
-        expr new_h = lean::mk_local(h->get_name(), name(H, hidx), convert(h->get_type()), binder_info());
+        expr new_h = lean::mk_local(name(H, hidx), h->get_name(), convert(h->get_type()), binder_info());
         hidx2local.insert(hidx, new_h);
         hyps.push_back(new_h);
     }
@@ -94,6 +94,11 @@ goal state::to_goal() const {
     return to_goal(m_main);
 }
 
+void state::display(environment const & env, io_state const & ios) const {
+    formatter fmt = ios.get_formatter_factory()(env, ios.get_options());
+    ios.get_diagnostic_channel() << mk_pair(to_goal().pp(fmt), ios.get_options());
+}
+
 #ifdef LEAN_DEBUG
 bool state::check_deps(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const {
     for_each(e, [&](expr const & n, unsigned) {

src/library/blast/state.h

@@ -75,6 +75,8 @@ public:
         to invoke the tactic framework from the blast tactic. */
     goal to_goal() const;
 
+    void display(environment const & env, io_state const & ios) const;
+
     #ifdef LEAN_DEBUG
     bool check_invariant() const;
     #endif