diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt
index 3320c14c4..6dd17c393 100644
--- a/src/library/blast/CMakeLists.txt
+++ b/src/library/blast/CMakeLists.txt
@@ -1 +1 @@
-add_library(blast OBJECT state.cpp expr.cpp blast_tactic.cpp init_module.cpp blast.cpp)
+add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp)
diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 4659eae4f..f8efba515 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -4,22 +4,188 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/type_checker.h"
+#include "library/replace_visitor.h"
 #include "library/blast/expr.h"
 #include "library/blast/state.h"
 #include "library/blast/blast.h"
 
 namespace lean {
 namespace blast {
+level to_blast_level(level const & l) {
+    level lhs;
+    switch (l.kind()) {
+    case level_kind::Succ:    return blast::mk_succ(to_blast_level(succ_of(l)));
+    case level_kind::Zero:    return blast::mk_level_zero();
+    case level_kind::Param:   return blast::mk_param_univ(param_id(l));
+    case level_kind::Meta:    return blast::mk_meta_univ(meta_id(l));
+    case level_kind::Global:  return blast::mk_global_univ(global_id(l));
+    case level_kind::Max:
+        lhs = to_blast_level(max_lhs(l));
+        return blast::mk_max(lhs, to_blast_level(max_rhs(l)));
+    case level_kind::IMax:
+        lhs = to_blast_level(imax_lhs(l));
+        return blast::mk_imax(lhs, to_blast_level(imax_rhs(l)));
+    }
+    lean_unreachable();
+}
+
 class context {
     environment m_env;
     io_state    m_ios;
     name_set    m_lemma_hints;
     name_set    m_unfold_hints;
+
+    class to_blast_expr_fn : public replace_visitor {
+        type_checker                 m_tc;
+        state &                      m_state;
+        // We map each metavariable to a metavariable application that contains only pairwise
+        // distinct local constants (that have been converted into lrefs).
+        name_map<pair<expr, expr>> & m_mvar2meta_mref;
+        name_map<expr> &             m_local2lref;
+
+        expr visit_sort(expr const & e) {
+            return blast::mk_sort(to_blast_level(sort_level(e)));
+        }
+
+        virtual expr visit_macro(expr const & e) {
+            buffer<expr> new_args;
+            for (unsigned i = 0; i < macro_num_args(e); i++) {
+                new_args.push_back(visit(macro_arg(e, i)));
+            }
+            return blast::mk_macro(macro_def(e), new_args.size(), new_args.data());
+        }
+
+        virtual expr visit_constant(expr const & e) {
+            levels new_ls = map(const_levels(e), [&](level const & l) { return to_blast_level(l); });
+            return blast::mk_constant(const_name(e), new_ls);
+        }
+
+        virtual expr visit_var(expr const & e) {
+            return blast::mk_var(var_idx(e));
+        }
+
+        void throw_unsupported_metavar_occ(expr const &) {
+            // TODO(Leo): improve error message
+            throw exception("'blast' tactic failed, goal contains a meta-variable application that is not supported");
+        }
+
+        expr mk_mref_app(expr const & mref, unsigned nargs, expr const * args) {
+            lean_assert(is_mref(mref));
+            buffer<expr> new_args;
+            for (unsigned i = 0; i < nargs; i++) {
+                new_args.push_back(visit(args[i]));
+            }
+            return blast::mk_app(mref, new_args.size(), new_args.data());
+        }
+
+        expr visit_meta_app(expr const & e) {
+            lean_assert(is_meta(e));
+            buffer<expr> args;
+            expr const & mvar = get_app_args(e, args);
+            if (pair<expr, expr> const * meta_mref = m_mvar2meta_mref.find(mlocal_name(mvar))) {
+                lean_assert(is_meta(meta_mref->first));
+                lean_assert(is_mref(meta_mref->second));
+                buffer<expr> decl_args;
+                get_app_args(meta_mref->first, decl_args);
+                if (decl_args.size() > args.size())
+                    throw_unsupported_metavar_occ(e);
+                for (unsigned i = 0; i < decl_args.size(); i++) {
+                    lean_assert(is_local(decl_args[i]));
+                    if (!is_local(args[i]) || mlocal_name(args[i]) != mlocal_name(decl_args[i]))
+                        throw_unsupported_metavar_occ(e);
+                }
+                return mk_mref_app(meta_mref->second, args.size() - decl_args.size(), args.data() + decl_args.size());
+            } else {
+                unsigned i = 0;
+                hypothesis_set ctx;
+                // find prefix of pair-wise distinct local constants that have already been processed.
+                for (; i < args.size(); i++) {
+                    if (!is_local(args[i]))
+                        break;
+                    expr const & l = args[i];
+                    if (!std::all_of(args.begin(), args.begin() + i,
+                                     [&](expr const & prev) { return mlocal_name(prev) != mlocal_name(l); }))
+                        break;
+                    if (auto lref = m_local2lref.find(mlocal_name(l))) {
+                        ctx.insert(lref_index(*lref));
+                    } else {
+                        break;
+                    }
+                }
+                unsigned  prefix_sz = i;
+                expr aux  = e;
+                for (; i < args.size(); i++)
+                    aux = app_fn(aux);
+                lean_assert(is_meta(aux));
+                expr type           = visit(m_tc.infer(aux).first);
+                unsigned mref_index = m_state.add_metavar_decl(metavar_decl(ctx, type));
+                expr mref           = blast::mk_mref(mref_index);
+                m_mvar2meta_mref.insert(mlocal_name(mvar), mk_pair(aux, mref));
+                return mk_mref_app(mref, args.size() - prefix_sz, args.data() + prefix_sz);
+            }
+        }
+
+        virtual expr visit_meta(expr const & e) {
+            return visit_meta_app(e);
+        }
+
+        virtual expr visit_local(expr const & e) {
+            if (auto r = m_local2lref.find(mlocal_name(e)))
+                return * r;
+            else
+                throw exception("blast tactic failed, ill-formed input goal");
+        }
+
+        virtual expr visit_app(expr const & e) {
+            if (is_meta(e)) {
+                return visit_meta_app(e);
+            } else {
+                expr f = visit(app_fn(e));
+                return blast::mk_app(f, visit(app_arg(e)));
+            }
+        }
+
+        virtual expr visit_lambda(expr const & e) {
+            expr d = visit(binding_domain(e));
+            return blast::mk_lambda(binding_name(e), d, visit(binding_body(e)), binding_info(e));
+        }
+
+        virtual expr visit_pi(expr const & e) {
+            expr d = visit(binding_domain(e));
+            return blast::mk_pi(binding_name(e), d, visit(binding_body(e)), binding_info(e));
+        }
+
+    public:
+        to_blast_expr_fn(environment const & env, state & s, name_map<pair<expr, expr>> & mvar2meta_mref,
+                         name_map<expr> & local2lref):
+            m_tc(env), m_state(s), m_mvar2meta_mref(mvar2meta_mref), m_local2lref(local2lref) {}
+    };
+
+    state to_state(goal const & g) {
+        state s;
+        branch b;
+        name_map<pair<expr, expr>> mvar2meta_mref;
+        name_map<expr> local2lref;
+        to_blast_expr_fn to_blast_expr(m_env, s, mvar2meta_mref, local2lref);
+        buffer<expr> hs;
+        g.get_hyps(hs);
+        for (expr const & h : hs) {
+            expr new_type = to_blast_expr(mlocal_type(h));
+            // TODO(Leo): create hypothesis using new_type
+        }
+        expr new_target = to_blast_expr(g.get_type());
+        // TODO(Leo): create branch and store in the state.
+        return s;
+    }
+
 public:
     context(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds):
         m_env(env), m_ios(ios), m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)) {
     }
-    optional<expr> operator()(goal const &) {
+
+    optional<expr> operator()(goal const & g) {
+        state s = to_state(g);
         return none_expr();
     }
 };
@@ -30,4 +196,6 @@ optional<expr> blast_goal(environment const & env, io_state const & ios, list<na
     blast::context c(env, ios, ls, ds);
     return c(g);
 }
+void initialize_blast() {}
+void finalize_blast() {}
 }
diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h
index 7f8e9e049..372d5288c 100644
--- a/src/library/blast/blast.h
+++ b/src/library/blast/blast.h
@@ -10,4 +10,6 @@ Author: Leonardo de Moura
 namespace lean {
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g);
+void initialize_blast();
+void finalize_blast();
 }
diff --git a/src/library/blast/branch.h b/src/library/blast/branch.h
index 49c69220b..bf41e6c8e 100644
--- a/src/library/blast/branch.h
+++ b/src/library/blast/branch.h
@@ -21,11 +21,11 @@ class branch {
     expr          m_target;
     metavar_set   m_mvars;
 public:
-    goal():m_next(0) {}
+    branch():m_next(0) {}
     hypothesis const * get(unsigned idx) const { return m_context.find(idx); }
     hypothesis const * get(expr const & e) const {
         lean_assert(is_lref(e));
-        return get(get_lmindex(e));
+        return get(lref_index(e));
     }
 };
 }}
diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp
index 87d03eae3..2955b414b 100644
--- a/src/library/blast/expr.cpp
+++ b/src/library/blast/expr.cpp
@@ -78,7 +78,7 @@ bool is_mref(expr const & e) {
     return is_lmref(e) && !is_lref(e);
 }
 
-unsigned get_lmindex(expr const & e) {
+unsigned lmref_index(expr const & e) {
     lean_assert(is_lmref(e));
     return static_cast<ref_definition_cell const *>(macro_def(e).raw())->get_index();
 }
@@ -254,6 +254,18 @@ expr mk_app(expr const & f, expr const & a) {
     return cache(lean::mk_app(f, a));
 }
 
+expr mk_app(expr const & f, unsigned num_args, expr const * args) {
+    expr r = f;
+    for (unsigned i = 0; i < num_args; i++)
+        r = blast::mk_app(r, args[i]);
+    return r;
+}
+
+expr mk_app(unsigned num_args, expr const * args) {
+    lean_assert(num_args >= 2);
+    return blast::mk_app(blast::mk_app(args[0], args[1]), num_args - 2, args+2);
+}
+
 expr mk_sort(level const & l) {
     lean_assert(is_cached(l));
     return cache(lean::mk_sort(l));
@@ -572,7 +584,7 @@ expr abstract_lrefs(expr const & e, unsigned n, expr const * subst) {
                 unsigned i = n;
                 while (i > 0) {
                     --i;
-                    if (get_lmindex(subst[i]) == get_lmindex(m))
+                    if (lref_index(subst[i]) == lref_index(m))
                         return some_expr(blast::mk_var(offset + n - i - 1));
                 }
                 return none_expr();
diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h
index 7c85cebbd..541985f0d 100644
--- a/src/library/blast/expr.h
+++ b/src/library/blast/expr.h
@@ -47,6 +47,8 @@ expr mk_mref(unsigned idx);
 expr mk_sort(level const & l);
 expr mk_constant(name const & n, levels const & ls);
 expr mk_app(expr const & f, expr const & a);
+expr mk_app(expr const & f, unsigned num_args, expr const * args);
+expr mk_app(unsigned num_args, expr const * args);
 expr mk_binding(expr_kind k, name const & n, expr const & t, expr const & e, binder_info const & bi);
 inline expr mk_pi(name const & n, expr const & t, expr const & e, binder_info const & bi) {
     return blast::mk_binding(expr_kind::Pi, n, t, e, bi);
@@ -71,7 +73,9 @@ bool is_mref(expr const & e);
 bool is_lref(expr const & e);
 /** \brief Return the index of the give lref/mref.
     \pre is_mref(e) || is_lref(e) */
-unsigned get_lmindex(expr const & e);
+unsigned lmref_index(expr const & e);
+inline unsigned mref_index(expr const & e) { return lmref_index(e); }
+inline unsigned lref_index(expr const & e) { return lmref_index(e); }
 
 level update_succ(level const & l, level const & new_arg);
 level update_max(level const & l, level const & new_lhs, level const & new_rhs);
diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h
index 859bd16ac..a5e4138f7 100644
--- a/src/library/blast/hypothesis.h
+++ b/src/library/blast/hypothesis.h
@@ -19,6 +19,7 @@ typedef rb_tree<unsigned, unsigned_cmp> hypothesis_set;
 
 class hypothesis {
     friend class branch;
+    name           m_name; // for pretty printing
     bool           m_active;
     unsigned       m_depth;
     hypothesis_set m_backward_deps;
@@ -27,7 +28,7 @@ class hypothesis {
     optional<expr> m_value;
     optional<expr> m_justification;
 public:
-    hypothesis();
+    hypothesis():m_active(0), m_depth(0) {}
     bool is_active() const { return m_active; }
     unsigned get_depth() const { return m_depth; }
     hypothesis_set const & get_backward_deps() const { return m_backward_deps; }
diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp
index b06050860..f655c089d 100644
--- a/src/library/blast/init_module.cpp
+++ b/src/library/blast/init_module.cpp
@@ -4,13 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "library/blast/blast.h"
 #include "library/blast/blast_tactic.h"
 
 namespace lean {
 void initialize_blast_module() {
+    initialize_blast();
     initialize_blast_tactic();
 }
 void finalize_blast_module() {
+    finalize_blast();
     finalize_blast_tactic();
 }
 }
diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index f904579cc..20f1789fe 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -5,3 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/blast/state.h"
+
+namespace lean {
+namespace blast {
+state::state():m_next_mref_index(0) {}
+unsigned state::add_metavar_decl(metavar_decl const & decl) {
+    unsigned r = m_next_mref_index;
+    m_next_mref_index++;
+    m_metavar_decls.insert(r, decl);
+    return r;
+}
+}}
diff --git a/src/library/blast/state.h b/src/library/blast/state.h
index 07a3c967a..40da27051 100644
--- a/src/library/blast/state.h
+++ b/src/library/blast/state.h
@@ -8,18 +8,29 @@ Author: Leonardo de Moura
 #include "util/rb_map.h"
 #include "kernel/expr.h"
 #include "library/blast/hypothesis.h"
+#include "library/blast/branch.h"
 
 namespace lean {
 namespace blast {
 class metavar_decl {
     hypothesis_set m_context;
     expr           m_type;
+public:
+    metavar_decl() {}
+    metavar_decl(hypothesis_set const & c, expr const & t):m_context(c), m_type(t) {}
 };
 
 class state {
+    friend class context;
+    unsigned m_next_mref_index;
     typedef rb_map<unsigned, metavar_decl, unsigned_cmp> metavar_decls;
     typedef rb_map<unsigned, expr, unsigned_cmp>         assignment;
     metavar_decls m_metavar_decls;
     assignment    m_assignment;
+public:
+    state();
+    unsigned add_metavar_decl(metavar_decl const & decl);
+    metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); }
+    metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); }
 };
 }}