From 7d8c079d71009f736cb5c30a4f107bf726740e70 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Oct 2020 09:35:58 -0700 Subject: [PATCH] chore: remove `abstract_context_cache` --- src/library/CMakeLists.txt | 1 - src/library/abstract_context_cache.cpp | 125 ------------ src/library/abstract_context_cache.h | 254 ------------------------- src/library/annotation.cpp | 1 - src/library/init_module.cpp | 3 - src/library/io_state_stream.h | 1 - src/library/type_context.cpp | 71 +------ src/library/type_context.h | 35 +--- src/library/util.cpp | 1 - 9 files changed, 12 insertions(+), 480 deletions(-) delete mode 100644 src/library/abstract_context_cache.cpp delete mode 100644 src/library/abstract_context_cache.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 1b65db9a93..b1907ad148 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -9,6 +9,5 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp type_context.cpp locals.cpp messages.cpp message_builder.cpp check.cpp profiling.cpp time_task.cpp - abstract_context_cache.cpp scope_pos_info_provider.cpp formatter.cpp json.cpp pos_info_provider.cpp abstract_type_context.cpp aux_match.cpp) diff --git a/src/library/abstract_context_cache.cpp b/src/library/abstract_context_cache.cpp deleted file mode 100644 index 8a6c816296..0000000000 --- a/src/library/abstract_context_cache.cpp +++ /dev/null @@ -1,125 +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 "util/option_declarations.h" -#include "library/abstract_context_cache.h" -#include "library/type_context.h" -#include "library/class.h" -#include "library/reducible.h" -#include "library/aux_recursors.h" - -#ifndef LEAN_DEFAULT_NAT_OFFSET_CNSTR_THRESHOLD -#define LEAN_DEFAULT_NAT_OFFSET_CNSTR_THRESHOLD 1024 -#endif - -#ifndef LEAN_DEFAULT_SMART_UNFOLDING -#define LEAN_DEFAULT_SMART_UNFOLDING true -#endif - -#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH -#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 5000 -#endif - -namespace lean { -static name * g_class_instance_max_depth = nullptr; -static name * g_nat_offset_threshold = nullptr; -static name * g_unfold_lemmas = nullptr; -static name * g_smart_unfolding = nullptr; - -unsigned get_class_instance_max_depth(options const & o) { - return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH); -} - -unsigned get_nat_offset_cnstr_threshold(options const & o) { - return o.get_unsigned(*g_nat_offset_threshold, LEAN_DEFAULT_NAT_OFFSET_CNSTR_THRESHOLD); -} - -bool get_smart_unfolding(options const & o) { - return o.get_bool(*g_smart_unfolding, LEAN_DEFAULT_SMART_UNFOLDING); -} - -context_cacheless::context_cacheless(): - m_nat_offset_cnstr_threshold(LEAN_DEFAULT_NAT_OFFSET_CNSTR_THRESHOLD), - m_smart_unfolding(LEAN_DEFAULT_SMART_UNFOLDING), - m_class_instance_max_depth(LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH) { -} - -context_cacheless::context_cacheless(options const & o): - m_options(o), - m_nat_offset_cnstr_threshold(::lean::get_nat_offset_cnstr_threshold(o)), - m_smart_unfolding(::lean::get_smart_unfolding(o)), - m_class_instance_max_depth(::lean::get_class_instance_max_depth(o)) { -} - -context_cacheless::context_cacheless(abstract_context_cache const & c, bool): - m_options(c.get_options()), - m_nat_offset_cnstr_threshold(c.get_nat_offset_cnstr_threshold()), - m_smart_unfolding(c.get_smart_unfolding()), - m_class_instance_max_depth(c.get_class_instance_max_depth()) { -} - -bool context_cacheless::is_transparent(type_context_old & ctx, transparency_mode m, constant_info const & info) { - name const & n = info.get_name(); - if (get_proj_info(ctx, n)) - return false; - if (m == transparency_mode::All) - return true; - if (m == transparency_mode::Reducible && is_instance(ctx.env(), info.get_name())) - return true; - auto s = get_reducible_status(ctx.env(), info.get_name()); - if (s == reducible_status::Reducible && m == transparency_mode::Reducible) - return true; - if (s != reducible_status::Irreducible && m == transparency_mode::Semireducible) - return true; - return false; -} - -optional context_cacheless::get_decl(type_context_old & ctx, transparency_mode m, name const & n) { - if (optional info = ctx.env().find(n)) { - if (info->has_value() && is_transparent(ctx, m, *info)) { - return info; - } - } - return none_constant_info(); -} - -optional context_cacheless::get_proj_info(type_context_old & ctx, name const & n) { - return get_projection_info(ctx.env(), n); -} - -bool context_cacheless::get_aux_recursor(type_context_old & ctx, name const & n) { - return ::lean::is_aux_recursor(ctx.env(), n); -} - -void initialize_abstract_context_cache() { - g_class_instance_max_depth = new name{"class", "instance_max_depth"}; - mark_persistent(g_class_instance_max_depth->raw()); - register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH, - "(class) max allowed depth in class-instance resolution"); - g_nat_offset_threshold = new name{"unifier", "nat_offset_cnstr_threshold"}; - mark_persistent(g_nat_offset_threshold->raw()); - register_unsigned_option(*g_nat_offset_threshold, LEAN_DEFAULT_NAT_OFFSET_CNSTR_THRESHOLD, - "(unifier) the unifier has special support for offset nat constraints of the form: " - "(t + k_1 =?= s + k_2), (t + k_1 =?= k_2) and (k_1 =?= k_2), " - "where k_1 and k_2 are numerals, t and s are arbitrary terms, and they all have type nat, " - "the offset constraint solver is used if k_1 and k_2 are smaller than the given threshold"); - g_unfold_lemmas = new name{"type_context", "unfold_lemmas"}; - mark_persistent(g_unfold_lemmas->raw()); - register_bool_option(*g_unfold_lemmas, LEAN_DEFAULT_UNFOLD_LEMMAS, - "(type-context) whether to unfold lemmas (e.g., during elaboration)"); - g_smart_unfolding = new name{"type_context", "smart_unfolding"}; - mark_persistent(g_smart_unfolding->raw()); - register_bool_option(*g_smart_unfolding, LEAN_DEFAULT_SMART_UNFOLDING, - "(type-context) enable/disable smart unfolding (e.g., during elaboration)"); -} - -void finalize_abstract_context_cache() { - delete g_class_instance_max_depth; - delete g_nat_offset_threshold; - delete g_smart_unfolding; - delete g_unfold_lemmas; -} -} diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h deleted file mode 100644 index df5394dba0..0000000000 --- a/src/library/abstract_context_cache.h +++ /dev/null @@ -1,254 +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/lbool.h" -#include "kernel/expr.h" -#include "kernel/declaration.h" -#include "library/projection.h" - -namespace lean { -#define LEAN_NUM_TRANSPARENCY_MODES 3 -enum class transparency_mode { All = 0, Semireducible, Reducible }; - -class type_context_old; - -/* Auxiliary information that is cached by the app_builder module in - the context_cache. */ -struct app_builder_info { - unsigned m_num_umeta; - unsigned m_num_emeta; - expr m_app; - list> m_inst_args; // "mask" of implicit instance arguments - list m_expl_args; // metavars for explicit arguments - /* - IMPORTANT: for m_inst_args we store the arguments in reverse order. - For example, the first element in the list indicates whether the last argument - is an instance implicit argument or not. If it is not none, then the element - is the associated metavariable - - m_expl_args are also stored in reverse order - */ -}; - -/* - ==== IMPORTANT ==== - THIS FILE WILL BE DELETED - THIS COMMENT DOES NOT REFLECT THE CURRENT DESIGN - =================== - - We have two main kinds of cache in Lean: environmental and contextual. - The environmental caches only depend on the environment, and are easier to maintain. - We usually store them in thread local storage, and before using them we compare - if the current environment is a descendant of the one in the cache, and we - check for attribute fingerprints. - - This class defines the interface for contextual caches. - A contextual cache depends on the local_context object. - Ideally, the cache should be stored in the local_context object, - but this is not feasible due to performance issues. The local_context object - should support a fast O(1) copy operation. Thus, we implement it using - functional data-structures such as red-black trees. This kind of data-structure - is too inefficient for a cache data structure, and we want to be able to - use hashtables (at least 10x faster than red-black trees). Another - issue is that we want to keep the `local_context` object simple and - without the overhead of many caches. - - We use contextual caches for the operations performed in the following modules: - type_context_old, app_builder, fun_info. - In the type_context_old, we cache inferred types, whnf, type class instances, - to cite a few. - - This class has been added to address problems with the former `type_context_old_cache_manager`. - The `type_context_old_cache_manager` objects were stored in thread local objects. - The correctness of this cache relied on the fact we used to never reuse fresh names in the whole system. - This is not true in the new name_generator refactoring (for addressing issue #1601). - The caches for the modules app_builder, fun_info have the same problem. - - We have implemented a thread local cache reset operation, but it is - not sufficient for fixing this issue since we only reset the cache - before each command and when start a task. - - Here is a scenario that demonstrates the problem. - Suppose we are executing the tactic `t1 <|> t2`. - First, we execute `t1`, and in the process, the type_context_old - cache is populated with new local constants created by `t1`. - Then `t1` fails and we execute `t2`. When, we execute `t2` - on the initial `tactic_state` object. Thus, - `t2` may potentially create new local constants using the names - used by `t1`, but with different types. So, the content - of the cache is invalid. - - Here are possible implementations of this API: - - - An "imperative" implementation using hashtables, and it is useful for modules - that own a type_context_old object (e.g., elaborator). - This implementation is also useful for the new type_context_old API we are going to expose in the `io` monad. - - - In principle, a "functional" implementation using rb_map and rb_tree is possible. - Then, this version could be stored in the tactic_state or local_context objects. - We decided to not use it for performe issues. See comment above. - - - For caching contextual information in the tactic framework, we use the following approach: - * We implement a thread local unique token generator. - * The token can be viewed as a reference to the cache. - * tactic_state stores this token. - * Thread local storage stores the "imperative" implementation and a token of its owner. - * When we create a type_context_old for a tactic_state we check whether the thread local - storage contains the cache for the given tactic_state. If yes, we use it, and obtain - a new token for it since we will perform destructive updates. - Otherwise, we create a new one. - * When we finish using the type_context_old, we update the tactic_state with the new fresh token, - and put the updated cache back into the thread local storage. - - Remark: the thread local storage may store more than one cache. - - Remark: this approach should work well for "sequential" tactic execution. - For `t1 <|> t2`, if `t1` fails, `t2` will potentially start with the empty cache - since the thread local storage contains the cache for `t1`. - We should measure whether this approach is more efficient than the functional one. - With the "abstract interface", we can even have both approaches. - - Remark: we have considered storing the token on the local context, but this is not ideal - because there are many tactics that create more than on subgoal (e.g., `apply`), - and we would have to use an empty cache for each subgoal but the first. - The situation would be analogous to the `t1 <|> t2` scenario described in the previous - remark. Moreover, the different subgoals usually have very similar local contexts - and information cached in one can be reused in the others. - - Remark: recall that in a sequence of tactic_states [s_1, s_2, ...] obtained by executing tactics [t_1, t_2, ...] - - s_1 -t_1-> s_2 -t_2-> s_3 -> ... - - we never reuse names for labeling local declarations, and the cache is reused, since we will store the - cache on the thread local storage after each step, and will retrieve it before the beginning of the following step. - Most cached data (e.g., inferred types) is still valid because we never reuse names in the sequence. - The only exception is cached data related to type class instances and subsigletons (which depends on type class instances). - Here the result depends on the local instances available in the local context. - Recall we have two modes for handling local instances: - - 1) liberal: any local instance can be used. In this mode, the cache for type class instances and subsigletons has to be - flushed in the beginning of each step if the local_context is different from the previous one. Actually, - we do not track the local_context. So, the cache is always flushed in the beginning of each step in the liberal mode. - This is fine because we only use the "liberal" mode when elaborating the header of a declaration. - - 2) frozen: after elaborating the header of a declaration, we freeze the local instances that can be used to - elaborate its body. The freeze step is also useful to speedup the type_context_old initialization - (see comment in the type_context_old class). So, we just check if the frozen local instances are the same - before starting each step. This check is performed in the method `init_local_instances`. - - Here are some benefits of the new approach: - - - The cache will be smaller in many cases. For example, after `t1` fails in `t1 <|> t2`, the cached information - about its new fresh local constants is not useful anymore, but it stays in the current - cache. - - - We don't need to check whether the cache is valid or not when we create a new - type_context_old. - - - It is more efficient when creating temporary type_context_old objects for performing - a single operation. In this kind of scenario, we can use the dummy cache implementation - that doesn't cache anything. - - - It is easy to experiment with new cache data structures. - - - We can easily flush the cache if a primitive tactic performs an operation that invalidates it. - Examples: - * A tactic that allows user to use all local class instances available in the local context. - * A tactic that reverses local instances -*/ -class abstract_context_cache { -public: - abstract_context_cache() {} - abstract_context_cache(abstract_context_cache const &) = delete; - abstract_context_cache(abstract_context_cache &&) = default; - virtual ~abstract_context_cache() {} - - abstract_context_cache & operator=(abstract_context_cache const &) = delete; - abstract_context_cache & operator=(abstract_context_cache &&) = default; - - /* Cached configuration options */ - virtual options const & get_options() const = 0; - virtual unsigned get_nat_offset_cnstr_threshold() const = 0; - virtual unsigned get_smart_unfolding() const = 0; - virtual unsigned get_class_instance_max_depth() const = 0; - - /* Operations for accessing environment data more efficiently. - The default implementation provided by this class does not have any optimization. */ - - virtual optional get_decl(type_context_old &, transparency_mode, name const &) = 0; - virtual optional get_proj_info(type_context_old &, name const &) = 0; - virtual bool get_aux_recursor(type_context_old &, name const &) = 0; - - /* Cache support for type_context_old module */ - - virtual optional get_infer(expr const &) = 0; - virtual void set_infer(expr const &, expr const &) = 0; - - virtual bool get_equiv(transparency_mode, expr const &, expr const &) = 0; - virtual void set_equiv(transparency_mode, expr const &, expr const &) = 0; - - virtual bool get_is_def_eq_failure(transparency_mode, expr const &, expr const &) = 0; - virtual void set_is_def_eq_failure(transparency_mode, expr const &, expr const &) = 0; - - virtual optional get_whnf(transparency_mode, expr const &) = 0; - virtual void set_whnf(transparency_mode, expr const &, expr const &) = 0; - -}; - -/* Dummy implementation of the abstract_context_cache interface that does not do cache anything but configuration options. */ -class context_cacheless : public abstract_context_cache { -protected: - bool is_transparent(type_context_old & ctx, transparency_mode m, constant_info const & info); -private: - options m_options; - unsigned m_nat_offset_cnstr_threshold; - unsigned m_smart_unfolding; - unsigned m_class_instance_max_depth; -public: - context_cacheless(); - context_cacheless(options const &); - /* Faster version of `context_cacheless(c.get_options())`. - The bool parameter is not used. It is here just to make sure we don't confuse - this constructor with the copy constructor. */ - context_cacheless(abstract_context_cache const &, bool); - context_cacheless(context_cacheless const &) = delete; - context_cacheless(context_cacheless &&) = default; - virtual ~context_cacheless() {} - - context_cacheless & operator=(context_cacheless const &) = delete; - context_cacheless & operator=(context_cacheless &&) = default; - - virtual options const & get_options() const override { return m_options; } - virtual unsigned get_nat_offset_cnstr_threshold() const override { return m_nat_offset_cnstr_threshold; } - virtual unsigned get_smart_unfolding() const override { return m_smart_unfolding; } - virtual unsigned get_class_instance_max_depth() const override { return m_class_instance_max_depth; } - - /* Operations for accessing environment data more efficiently. - The default implementation provided by this class does not have any optimization. */ - - virtual optional get_decl(type_context_old &, transparency_mode, name const &) override; - virtual optional get_proj_info(type_context_old &, name const &) override; - virtual bool get_aux_recursor(type_context_old &, name const &) override; - - /* Cache support for type_context_old module */ - - virtual optional get_infer(expr const &) override { return none_expr(); } - virtual void set_infer(expr const &, expr const &) override {} - - virtual bool get_equiv(transparency_mode, expr const &, expr const &) override { return false; } - virtual void set_equiv(transparency_mode, expr const &, expr const &) override {} - - virtual bool get_is_def_eq_failure(transparency_mode, expr const &, expr const &) override { return false; } - virtual void set_is_def_eq_failure(transparency_mode, expr const &, expr const &) override {} - - virtual optional get_whnf(transparency_mode, expr const &) override { return none_expr(); } - virtual void set_whnf(transparency_mode, expr const &, expr const &) override {} -}; - -void initialize_abstract_context_cache(); -void finalize_abstract_context_cache(); -} diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index 047100120c..b514c8f2de 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include #include #include "util/name_hash_map.h" -#include "library/abstract_type_context.h" #include "library/annotation.h" #include "library/pos_info_provider.h" diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index c79685a0e9..78a2548334 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/print.h" #include "library/util.h" #include "library/pp_options.h" -#include "library/abstract_context_cache.h" #include "library/type_context.h" #include "library/local_context.h" #include "library/metavar_context.h" @@ -57,7 +56,6 @@ void initialize_library_module() { initialize_class(); initialize_library_util(); initialize_pp_options(); - initialize_abstract_context_cache(); initialize_type_context(); initialize_check(); initialize_time_task(); @@ -67,7 +65,6 @@ void finalize_library_module() { finalize_time_task(); finalize_check(); finalize_type_context(); - finalize_abstract_context_cache(); finalize_pp_options(); finalize_library_util(); finalize_class(); diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h index db2afc5d84..cb0001bbdb 100644 --- a/src/library/io_state_stream.h +++ b/src/library/io_state_stream.h @@ -7,7 +7,6 @@ Author: Leonardo de Moura #pragma once #include #include "kernel/environment.h" -#include "library/abstract_type_context.h" #include "library/exception.h" #include "library/io_state.h" #include "library/ext_exception.h" diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index ecb651ff0e..75ba55c34f 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -33,17 +33,6 @@ Author: Leonardo de Moura #include "library/time_task.h" namespace lean { -bool is_at_least_semireducible(transparency_mode m) { - return m == transparency_mode::All || m == transparency_mode::Semireducible; -} - -bool is_at_least_instances(transparency_mode m) { - return m == transparency_mode::All || m == transparency_mode::Semireducible; -} - -transparency_mode ensure_semireducible_mode(transparency_mode m) { - return is_at_least_semireducible(m) ? m : transparency_mode::Semireducible; -} /* ===================== type_context_old::tmp_locals @@ -53,70 +42,14 @@ type_context_old::tmp_locals::~tmp_locals() { m_ctx.pop_local(); } -bool type_context_old::tmp_locals::all_let_decls() const { - for (expr const & l : m_locals) { - if (optional d = m_ctx.m_lctx.find_local_decl(l)) { - if (!d->get_value()) - return false; - } else { - lean_unreachable(); - } - } - return true; -} - /* ===================== type_context_old ===================== */ -void type_context_old::cache_failure(expr const & t, expr const & s) { - m_cache->set_is_def_eq_failure(m_transparency_mode, t, s); -} - -bool type_context_old::is_cached_failure(expr const & t, expr const & s) { - if (has_expr_metavar(t) || has_expr_metavar(s)) { - return false; - } else { - return m_cache->get_is_def_eq_failure(m_transparency_mode, t, s); - } -} - -type_context_old::type_context_old(environment const & env, options const & o, metavar_context const & mctx, +type_context_old::type_context_old(environment const & env, options const &, metavar_context const & mctx, local_context const & lctx, transparency_mode): m_env(env), - m_mctx(mctx), m_lctx(lctx), - m_dummy_cache(o), - m_cache(&m_dummy_cache) { -} - -type_context_old::type_context_old(environment const & env, metavar_context const & mctx, - local_context const & lctx, abstract_context_cache & cache, transparency_mode): - m_env(env), - m_mctx(mctx), m_lctx(lctx), - m_cache(&cache) { -} - -type_context_old::type_context_old(type_context_old && src): - m_env(std::move(src.m_env)), - m_mctx(std::move(src.m_mctx)), - m_lctx(std::move(src.m_lctx)), - m_dummy_cache(src.get_options()), - m_cache(src.m_cache == &src.m_dummy_cache ? &m_dummy_cache : src.m_cache), - m_local_instances(src.m_local_instances), - m_transparency_mode(src.m_transparency_mode), - m_unifier_cfg(src.m_unifier_cfg), - m_smart_unfolding(src.m_smart_unfolding) { - lean_assert(!src.m_tmp_data); - lean_assert(!src.m_used_assignment); - lean_assert(!src.m_in_is_def_eq); - lean_assert(src.m_is_def_eq_depth == 0); - lean_assert(src.m_scopes.empty()); - lean_assert(src.m_update_left); - lean_assert(src.m_update_right); - lean_assert(src.m_unfold_depth == 0); - lean_assert(src.m_postponed.empty()); - lean_assert(src.m_full_postponed); - lean_assert(!src.m_transparency_pred); + m_mctx(mctx), m_lctx(lctx) { } type_context_old::~type_context_old() { diff --git a/src/library/type_context.h b/src/library/type_context.h index 8acd00ea09..4d4466e611 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -11,16 +11,17 @@ Author: Leonardo de Moura #include "util/lbool.h" #include "util/fresh_name.h" #include "kernel/environment.h" -#include "library/abstract_type_context.h" #include "library/idx_metavar.h" #include "library/projection.h" #include "library/metavar_context.h" -#include "library/abstract_context_cache.h" +#include "library/abstract_type_context.h" #include "library/exception.h" #include "library/expr_pair.h" #include "library/local_instances.h" namespace lean { +enum class transparency_mode { All = 0, Semireducible, Reducible }; + /* Return `f._sunfold` */ name mk_smart_unfolding_name_for(name const & f); @@ -77,13 +78,9 @@ public: }; private: typedef buffer scopes; - typedef abstract_context_cache cache; - typedef context_cacheless dummy_cache; environment m_env; metavar_context m_mctx; local_context m_lctx; - dummy_cache m_dummy_cache; /* cache used when user does not provide a cache */ - cache * m_cache; local_instances m_local_instances; /* We only cache results when m_used_assignment is false */ bool m_used_assignment{false}; @@ -132,14 +129,12 @@ private: std::function const * m_transparency_pred{nullptr}; // NOLINT - static bool is_equiv_cache_target(expr const & e1, expr const & e2) { - return !has_metavar(e1) && !has_metavar(e2) && (!is_atomic(e1) || !is_atomic(e2)); + static bool is_equiv_cache_target(expr const &, expr const &) { + lean_unreachable(); } - bool is_cached_equiv(expr const & e1, expr const & e2) { - return is_equiv_cache_target(e1, e2) && m_cache->get_equiv(m_transparency_mode, e1, e2); - } - void cache_equiv(expr const & e1, expr const & e2) { - if (is_equiv_cache_target(e1, e2)) m_cache->set_equiv(m_transparency_mode, e1, e2); + bool is_cached_equiv(expr const &, expr const &) { lean_unreachable(); } + void cache_equiv(expr const &, expr const &) { + lean_unreachable(); } void cache_failure(expr const & t, expr const & s); @@ -151,31 +146,23 @@ private: optional is_projection(expr const & e); optional reduce_projection_core(optional const & info, expr const & e); - type_context_old(abstract_context_cache * cache, metavar_context const & mctx, local_context const & lctx, - transparency_mode m); public: - type_context_old(environment const & env, metavar_context const & mctx, local_context const & lctx, - abstract_context_cache & cache, transparency_mode m = transparency_mode::Reducible); type_context_old(environment const & env, options const & o, metavar_context const & mctx, local_context const & lctx, transparency_mode m = transparency_mode::Reducible); type_context_old(environment const & env, options const & o, local_context const & lctx, - transparency_mode m = transparency_mode::Reducible): + transparency_mode m = transparency_mode::Reducible): type_context_old(env, o, metavar_context(), lctx, m) {} explicit type_context_old(environment const & env, transparency_mode m = transparency_mode::Reducible): type_context_old(env, options(), metavar_context(), local_context(), m) {} type_context_old(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible): type_context_old(env, o, metavar_context(), local_context(), m) {} - type_context_old(environment const & env, abstract_context_cache & cache, transparency_mode m = transparency_mode::Reducible): - type_context_old(env, metavar_context(), local_context(), cache, m) {} - type_context_old(type_context_old const &) = delete; - type_context_old(type_context_old &&); virtual ~type_context_old(); type_context_old & operator=(type_context_old const &) = delete; type_context_old & operator=(type_context_old &&) = delete; virtual environment const & env() const override { return m_env; } - options const & get_options() const { return m_cache->get_options(); } + options const & get_options() const { lean_unreachable(); } // TODO(Leo): avoid ::lean::mk_fresh_name virtual name next_name() override { return ::lean::mk_fresh_name(); } @@ -204,8 +191,6 @@ public: /* note: env must be a descendant of m_env */ void set_env(environment const & env); - abstract_context_cache & get_cache() { return *m_cache; } - /* Store the current local instances in the local context. This has the following implications: diff --git a/src/library/util.cpp b/src/library/util.cpp index 79724b5796..17979f2fd4 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/inductive.h" -#include "library/abstract_type_context.h" #include "library/locals.h" #include "library/util.h" #include "library/suffixes.h"