From 0e4f97792e1b5fd9bba798a9a2008cdf747b40ce Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Oct 2015 18:14:34 -0700
Subject: [PATCH] feat(library/blast): add blast::scope_debug auxiliary class
 for testing blast related procedures

---
 src/library/blast/blast.cpp | 38 ++++++++++++++++++++++++++++++++-----
 src/library/blast/blast.h   | 21 +++++++++++++++++---
 2 files changed, 51 insertions(+), 8 deletions(-)

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 94e80920c..7e8f09334 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/normalize.h"
 #include "library/class.h"
+#include "library/util.h"
 #include "library/type_inference.h"
 #include "library/projection.h"
 #include "library/tactic/goal.h"
@@ -26,7 +27,7 @@ namespace blast {
 static name * g_prefix = nullptr;
 
 class blastenv {
-    friend class scope;
+    friend class scope_assignment;
     environment                m_env;
     io_state                   m_ios;
     name_generator             m_ngen;
@@ -365,10 +366,14 @@ public:
         m_ti(*this) {
     }
 
-    optional<expr> operator()(goal const & g) {
+    void init_state(goal const & g) {
         m_curr_state = to_state(g);
 
         // TODO(Leo): set local context for type class resolution at ti
+    }
+
+    optional<expr> operator()(goal const & g) {
+        init_state(g);
 
         // TODO(Leo): blast main loop
         display("Blast tactic initial state\n");
@@ -478,6 +483,10 @@ void display_curr_state() {
     display("\n");
 }
 
+void display_expr(expr const & e) {
+    ios().get_diagnostic_channel() << e << "\n";
+}
+
 void display(char const * msg) {
     ios().get_diagnostic_channel() << msg;
 }
@@ -486,21 +495,40 @@ void display(sstream const & msg) {
     ios().get_diagnostic_channel() << msg.str();
 }
 
-scope::scope():m_keep(false) {
+scope_assignment::scope_assignment():m_keep(false) {
     lean_assert(g_blastenv);
     g_blastenv->m_ti.push();
 }
 
-scope::~scope() {
+scope_assignment::~scope_assignment() {
     if (m_keep)
         g_blastenv->m_ti.commit();
     else
         g_blastenv->m_ti.pop();
 }
 
-void scope::commit() {
+void scope_assignment::commit() {
     m_keep = true;
 }
+
+struct scope_debug::imp {
+    scope_hash_consing m_scope1;
+    blastenv           m_benv;
+    scope_blastenv     m_scope2;
+    imp(environment const & env, io_state const & ios):
+        m_benv(env, ios, list<name>(), list<name>()),
+        m_scope2(m_benv) {
+        expr aux_mvar = mk_metavar("dummy_mvar", mk_true());
+        goal aux_g(aux_mvar, mlocal_type(aux_mvar));
+        m_benv.init_state(aux_g);
+    }
+};
+
+scope_debug::scope_debug(environment const & env, io_state const & ios):
+    m_imp(new imp(env, ios)) {
+}
+
+scope_debug::~scope_debug() {}
 }
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g) {
diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h
index 9e3a889c4..4989d176d 100644
--- a/src/library/blast/blast.h
+++ b/src/library/blast/blast.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <memory>
 #include "kernel/environment.h"
 #include "library/io_state.h"
 #include "library/blast/state.h"
@@ -48,19 +49,33 @@ optional<expr> mk_class_instance(expr const & e);
 
 /** \brief Display the current state of the blast tactic in the diagnostic channel. */
 void display_curr_state();
+/** \brief Display the given expression in the diagnostic channel. */
+void display_expr(expr const & e);
 /** \brief Display message in the blast tactic diagnostic channel. */
 void display(char const * msg);
 void display(sstream const & msg);
 /**
     \brief Create a local scope for saving the assignment and
     metavariable declarations at curr_state() */
-class scope {
+class scope_assignment {
     bool m_keep;
 public:
-    scope();
-    ~scope();
+    scope_assignment();
+    ~scope_assignment();
     void commit();
 };
+
+/** \brief Auxiliary object for setting thread local storage associated with blast tactic.
+
+    This is for debugging purposes only. It allow us to debug/test procedures that can
+    only be invoked from blast. */
+class scope_debug {
+    struct imp;
+    std::unique_ptr<imp> m_imp;
+public:
+    scope_debug(environment const & env, io_state const & ios);
+    ~scope_debug();
+};
 }
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g);