From 98b79373cc9a2549a4e6d9f29092b243feb84843 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Nov 2015 15:52:38 -0800
Subject: [PATCH] feat(library/blast/blast): add blast::internalize

---
 src/library/blast/blast.cpp | 14 ++++++++++++++
 src/library/blast/blast.h   |  7 +++++++
 2 files changed, 21 insertions(+)

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index a097410d9..806ddf730 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -447,6 +447,15 @@ public:
         ctx->clear();
         m_tmp_ctx_pool.push_back(ctx);
     }
+
+    /** \brief Convert an external expression into a blast expression
+        It converts meta-variables to blast meta-variables, and ensures the expressions
+        are maximally shared.
+        \remark This procedure should only be used for debugging purposes. */
+    expr internalize(expr const & e) {
+        name_map<expr> local2href;
+        return to_blast_expr_fn(m_env, m_curr_state, m_uvar2uref, m_mvar2meta_mref, local2href)(e);
+    }
 };
 
 LEAN_THREAD_PTR(blastenv, g_blastenv);
@@ -626,6 +635,11 @@ blast_tmp_type_context::blast_tmp_type_context() {
 blast_tmp_type_context::~blast_tmp_type_context() {
     g_blastenv->recycle_tmp_type_context(m_ctx);
 }
+
+expr internalize(expr const & e) {
+    lean_assert(g_blastenv);
+    return g_blastenv->internalize(e);
+}
 }
 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 ff9bf4819..805f96f1e 100644
--- a/src/library/blast/blast.h
+++ b/src/library/blast/blast.h
@@ -94,6 +94,13 @@ public:
     tmp_type_context const & operator*() const { return *m_ctx; }
     tmp_type_context & operator*() { return *m_ctx; }
 };
+
+/**
+    \brief Convert an external expression into a blast expression
+    It converts meta-variables to blast meta-variables, and ensures the expressions
+    are maximally shared.
+    \remark This procedure should only be used for **debugging purposes**. */
+expr internalize(expr const & e);
 }
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g);