chore: remove abstract_context_cache
This commit is contained in:
Leonardo de Moura
parent
95acb5cf3a
commit
7d8c079d71
9 changed files with 12 additions and 480 deletions
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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<constant_info> context_cacheless::get_decl(type_context_old & ctx, transparency_mode m, name const & n) {
|
||||
if (optional<constant_info> info = ctx.env().find(n)) {
|
||||
if (info->has_value() && is_transparent(ctx, m, *info)) {
|
||||
return info;
|
||||
}
|
||||
}
|
||||
return none_constant_info();
|
||||
}
|
||||
|
||||
optional<projection_info> 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;
|
||||
}
|
||||
}
|
||||
|
|
@ -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<optional<expr>> m_inst_args; // "mask" of implicit instance arguments
|
||||
list<expr> 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<constant_info> get_decl(type_context_old &, transparency_mode, name const &) = 0;
|
||||
virtual optional<projection_info> 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<expr> 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<expr> 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<constant_info> get_decl(type_context_old &, transparency_mode, name const &) override;
|
||||
virtual optional<projection_info> 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<expr> 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<expr> 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();
|
||||
}
|
||||
|
|
@ -9,7 +9,6 @@ Author: Leonardo de Moura
|
|||
#include <string>
|
||||
#include <lean/sstream.h>
|
||||
#include "util/name_hash_map.h"
|
||||
#include "library/abstract_type_context.h"
|
||||
#include "library/annotation.h"
|
||||
#include "library/pos_info_provider.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include <string>
|
||||
#include "kernel/environment.h"
|
||||
#include "library/abstract_type_context.h"
|
||||
#include "library/exception.h"
|
||||
#include "library/io_state.h"
|
||||
#include "library/ext_exception.h"
|
||||
|
|
|
|||
|
|
@ -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<local_decl> 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() {
|
||||
|
|
|
|||
|
|
@ -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<scope_data> 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<bool(name const & e)> 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<projection_info> is_projection(expr const & e);
|
||||
optional<expr> reduce_projection_core(optional<projection_info> 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:
|
||||
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue