From c5921fca6d124ed26d4c435f65676f8762084e11 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Sep 2015 16:22:24 -0700
Subject: [PATCH] refactor(library/blast): remove dead code

We don't need context anymore. The "context" is the blast goal object.
---
 src/library/blast/CMakeLists.txt |  2 +-
 src/library/blast/context.cpp    | 93 --------------------------------
 src/library/blast/context.h      | 39 --------------
 3 files changed, 1 insertion(+), 133 deletions(-)
 delete mode 100644 src/library/blast/context.cpp
 delete mode 100644 src/library/blast/context.h

diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt
index 9d27f1134..dbeb4b3a0 100644
--- a/src/library/blast/CMakeLists.txt
+++ b/src/library/blast/CMakeLists.txt
@@ -1 +1 @@
-add_library(blast OBJECT state.cpp context.cpp expr.cpp)
+add_library(blast OBJECT state.cpp expr.cpp)
diff --git a/src/library/blast/context.cpp b/src/library/blast/context.cpp
deleted file mode 100644
index e3cfa2580..000000000
--- a/src/library/blast/context.cpp
+++ /dev/null
@@ -1,93 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "library/kernel_serializer.h"
-#include "library/blast/context.h"
-
-namespace lean {
-LEAN_THREAD_PTR(context, g_context);
-static name * g_ref_value = nullptr;
-static std::string * g_ref_value_opcode = nullptr;
-
-class ref_definition_cell : public macro_definition_cell {
-    name m_name;
-    void check_macro(expr const & m) const {
-        lean_assert(is_macro(m));
-        if (macro_num_args(m) != 0)
-            throw exception("invalid ref expression");
-    }
-public:
-    ref_definition_cell(name const & n):m_name(n) {}
-    name get_ref_name() const { return m_name; }
-
-    virtual name get_name() const { return *g_ref_value; }
-
-    virtual pair<expr, constraint_seq> check_type(expr const & m, extension_context &, bool) const {
-        lean_assert(g_context);
-        check_macro(m);
-        return mk_pair(g_context->get_type(m_name), constraint_seq());
-    }
-
-    virtual optional<expr> expand(expr const & m, extension_context &) const {
-        lean_assert(g_context);
-        check_macro(m);
-        return g_context->get_value(m_name);
-    }
-
-    virtual void write(serializer & s) const {
-        s.write_string(*g_ref_value_opcode);
-        s << m_name;
-    }
-
-    virtual bool operator==(macro_definition_cell const & other) const {
-        return
-            dynamic_cast<ref_definition_cell const *>(&other) != nullptr &&
-            m_name == static_cast<ref_definition_cell const&>(other).m_name;
-    }
-
-    virtual unsigned hash() const { return m_name.hash(); }
-};
-
-expr mk_ref(name const & n) {
-    return mk_macro(macro_definition(new ref_definition_cell(n)), 0, nullptr);
-}
-
-bool is_ref(expr const & e) {
-    return is_macro(e) && dynamic_cast<ref_definition_cell const *>(macro_def(e).raw());
-}
-
-name get_ref_name(expr const & e) {
-    lean_assert(is_ref(e));
-    return static_cast<ref_definition_cell const *>(macro_def(e).raw())->get_ref_name();
-}
-
-scope_context::scope_context(context & ctx) {
-    m_old_context = g_context;
-    g_context     = &ctx;
-}
-
-scope_context::~scope_context() {
-    g_context     = m_old_context;
-}
-
-void initialize_context() {
-    g_ref_value        = new name("refv");
-    g_ref_value_opcode = new std::string("RefV");
-    register_macro_deserializer(*g_ref_value_opcode,
-                                [](deserializer & d, unsigned num, expr const *) {
-                                    if (num != 0) throw corrupted_stream_exception();
-                                    name n;
-                                    d >> n;
-                                    return mk_ref(n);
-                                });
-}
-
-void finalize_context() {
-    delete g_ref_value;
-    delete g_ref_value_opcode;
-}
-}
diff --git a/src/library/blast/context.h b/src/library/blast/context.h
deleted file mode 100644
index 91e1894a2..000000000
--- a/src/library/blast/context.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-/** \brief Abstract context-like object */
-class context {
-public:
-    virtual ~context() {}
-    virtual expr get_type(name const & n) const = 0;
-    virtual optional<expr> get_value(name const & n) const = 0;
-};
-
-/** \brief Create a reference to an object defined in a context.
-    This is an auxiliary expression only used during elaboration (e.g., tactics and blast).
-    The type (and optionally value) must be stored in a context-like object (see #context).
- */
-expr mk_ref(name const & n);
-/** \brief Return true iff \c e is an expression created using #mk_ref */
-bool is_ref(expr const & e);
-/** \brief Return the name of an expression created using #mk_ref */
-name get_ref_name(expr const & e);
-
-/** \brief Set the current context like object. It is setting thread local storage. */
-class scope_context {
-    context * m_old_context;
-public:
-    scope_context(context & ctx);
-    ~scope_context();
-};
-
-void initialize_context();
-void finalize_context();
-}