From 373e979a2a4e4f9bcebc6fee5a0d7c3e8650533e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Sep 2018 12:23:43 -0700 Subject: [PATCH] chore(library): remove dead code --- src/library/CMakeLists.txt | 3 +- src/library/elab_context.cpp | 24 -------------- src/library/elab_context.h | 61 ------------------------------------ 3 files changed, 1 insertion(+), 87 deletions(-) delete mode 100644 src/library/elab_context.cpp delete mode 100644 src/library/elab_context.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 2c5160764e..aaabfea095 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -16,6 +16,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp eval_helper.cpp messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp check.cpp parray.cpp process.cpp pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp - context_cache.cpp elab_context.cpp - scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp pos_info_provider.cpp + context_cache.cpp scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp pos_info_provider.cpp derive_attribute.cpp) diff --git a/src/library/elab_context.cpp b/src/library/elab_context.cpp deleted file mode 100644 index e0584b8f47..0000000000 --- a/src/library/elab_context.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/* -Copyright (c) 2018 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/elab_context.h" - -namespace lean { -elab_context::elab_context(environment const & env, metavar_context const & mctx, name_generator const & ngen, abstract_context_cache * cache): - m_env(env), - m_mctx(mctx), - m_ngen(ngen), - m_cache(cache) { -} - -elab_context::elab_context(environment const & env, metavar_context const & mctx, name_generator const & ngen, options const & opts): - m_env(env), - m_mctx(mctx), - m_ngen(ngen), - m_dummy_cache(opts), - m_cache(&m_dummy_cache) { -} -} diff --git a/src/library/elab_context.h b/src/library/elab_context.h deleted file mode 100644 index 9fd1710c37..0000000000 --- a/src/library/elab_context.h +++ /dev/null @@ -1,61 +0,0 @@ -/* -Copyright (c) 2018 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/name_generator.h" -#include "kernel/environment.h" -#include "library/abstract_context_cache.h" -#include "library/metavar_context.h" - -namespace lean { -/* - The elaboration context contains the main data used to elaborate a Lean expression. - This context is shared between different \c type_context objects. - A \c type_context object is used to infer types; solve unification/matching constraints; - perform type class resolution; and reduce terms. Each \c type_context object may - use a different \c local_context (i.e., hypotheses). - - When we create a \c type_context object we just need to provide this \c elab_context - object and a \c local_context. - - In the tactic framework, we define a subclass called \c tactic_context. - It contains additional information such as the set of goals. The \c tactic_context - is the preferred way to write tactics in C++. - - In the past, the \c type_context object would contain the information stored here. - This decision created several problems when we needed to create multiple \c type_context - objects with different local contexts and/or for solving different unification/matching - constraints. The main benefits of the new design are: - - Multiple \c type_context objects may share the same \c elab_context. - - Faster \c type_context creation. - - It allows us to provide a clean Lean API for using type_context objects directly. -*/ -class elab_context { -protected: - environment m_env; - metavar_context m_mctx; - name_generator m_ngen; - context_cacheless m_dummy_cache; - abstract_context_cache * m_cache; - - friend class type_context; // TODO(Leo): delete after we have a cleaner API here - friend class type_context_old; // TODO(Leo): delete after refactoring -public: - elab_context(environment const & env, metavar_context const & mctx, name_generator const & ngen, abstract_context_cache * cache); - elab_context(environment const & env, metavar_context const & mctx, name_generator const & ngen, options const & opts); - elab_context(elab_context const &) = delete; - elab_context(elab_context &&) = delete; - ~elab_context() {} - - elab_context const & operator=(elab_context const &) = delete; - elab_context const & operator=(elab_context &&) = delete; - - environment const & env() const { return m_env; } - metavar_context & mctx() { return m_mctx; } - abstract_context_cache & cache() { return *m_cache; } - name next_name() { return m_ngen.next(); } -}; -}