From f873def910fa1a8e7f2b99baae21db6eb3aa1a95 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Mar 2018 12:17:09 -0800 Subject: [PATCH] refactor(library/type_context): move unification_hints to cache object --- src/library/abstract_context_cache.cpp | 4 ++++ src/library/abstract_context_cache.h | 3 +++ src/library/context_cache.cpp | 7 +++++++ src/library/context_cache.h | 3 +++ src/library/persistent_context_cache.cpp | 4 ++++ src/library/persistent_context_cache.h | 1 + src/library/type_context.cpp | 7 ++----- src/library/type_context.h | 1 - 8 files changed, 24 insertions(+), 6 deletions(-) diff --git a/src/library/abstract_context_cache.cpp b/src/library/abstract_context_cache.cpp index d65f1d894c..9fb29e32e8 100644 --- a/src/library/abstract_context_cache.cpp +++ b/src/library/abstract_context_cache.cpp @@ -109,6 +109,10 @@ bool context_cacheless::get_aux_recursor(type_context & ctx, name const & n) { return ::lean::is_aux_recursor(ctx.env(), n); } +void context_cacheless::get_unification_hints(type_context & ctx, name const & f1, name const & f2, buffer & hints) { + return ::lean::get_unification_hints(ctx.env(), f1, f2, hints); +} + void initialize_abstract_context_cache() { g_class_instance_max_depth = new name{"class", "instance_max_depth"}; register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH, diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h index 6cf690a903..1ad788c003 100644 --- a/src/library/abstract_context_cache.h +++ b/src/library/abstract_context_cache.h @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/projection.h" #include "library/fun_info.h" #include "library/local_instances.h" +#include "library/unification_hint.h" namespace lean { #define LEAN_NUM_TRANSPARENCY_MODES 5 @@ -181,6 +182,7 @@ public: virtual optional get_decl(type_context &, transparency_mode, name const &) = 0; virtual projection_info const * get_proj_info(type_context &, name const &) = 0; virtual bool get_aux_recursor(type_context &, name const &) = 0; + virtual void get_unification_hints(type_context &, name const & f1, name const & f2, buffer & hints) = 0; /* Cache support for type_context module */ @@ -296,6 +298,7 @@ public: virtual optional get_decl(type_context &, transparency_mode, name const &) override; virtual projection_info const * get_proj_info(type_context &, name const &) override; virtual bool get_aux_recursor(type_context &, name const &) override; + virtual void get_unification_hints(type_context &, name const & f1, name const & f2, buffer & hints) override; /* Cache support for type_context module */ diff --git a/src/library/context_cache.cpp b/src/library/context_cache.cpp index 4173b740fc..7fc89fcba9 100644 --- a/src/library/context_cache.cpp +++ b/src/library/context_cache.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/context_cache.h" +#include "library/type_context.h" namespace lean { context_cache::context_cache(): @@ -43,6 +44,12 @@ bool context_cache::get_aux_recursor(type_context & ctx, name const & n) { return r; } +void context_cache::get_unification_hints(type_context & ctx, name const & f1, name const & f2, buffer & hints) { + if (!m_uhints) + m_uhints = ::lean::get_unification_hints(ctx.env()); + ::lean::get_unification_hints(*m_uhints, f1, f2, hints); +} + template optional find_at(C const & c, expr const & e) { auto it = c.find(e); diff --git a/src/library/context_cache.h b/src/library/context_cache.h index b9ce2dd89b..2369ef59d0 100644 --- a/src/library/context_cache.h +++ b/src/library/context_cache.h @@ -87,6 +87,8 @@ class context_cache : public context_cacheless { cache manager. */ instance_cache m_instance_cache; subsingleton_cache m_subsingleton_cache; + + optional m_uhints; public: context_cache(); context_cache(options const & o); @@ -100,6 +102,7 @@ public: virtual optional get_decl(type_context &, transparency_mode, name const &) override; virtual projection_info const * get_proj_info(type_context &, name const &) override; virtual bool get_aux_recursor(type_context &, name const &) override; + virtual void get_unification_hints(type_context &, name const & f1, name const & f2, buffer & hints) override; /* Cache support for type_context module */ diff --git a/src/library/persistent_context_cache.cpp b/src/library/persistent_context_cache.cpp index bad1dff7fa..b05ed38e23 100644 --- a/src/library/persistent_context_cache.cpp +++ b/src/library/persistent_context_cache.cpp @@ -63,6 +63,10 @@ bool persistent_context_cache::get_aux_recursor(type_context & ctx, name const & return m_cache_ptr->get_aux_recursor(ctx, n); } +void persistent_context_cache::get_unification_hints(type_context & ctx, name const & f1, name const & f2, buffer & hints) { + return m_cache_ptr->get_unification_hints(ctx, f1, f2, hints); +} + optional persistent_context_cache::get_infer(expr const & e) { return m_cache_ptr->get_infer(e); } diff --git a/src/library/persistent_context_cache.h b/src/library/persistent_context_cache.h index bd6d2053cc..e6018bd639 100644 --- a/src/library/persistent_context_cache.h +++ b/src/library/persistent_context_cache.h @@ -46,6 +46,7 @@ public: virtual optional get_decl(type_context &, transparency_mode, name const &) override; virtual projection_info const * get_proj_info(type_context &, name const &) override; virtual bool get_aux_recursor(type_context &, name const &) override; + virtual void get_unification_hints(type_context &, name const & f1, name const & f2, buffer & hints) override; /* Cache support for type_context module */ diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index a91b9e7e21..c9eb30eaa9 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -134,7 +134,6 @@ void type_context::init_core(transparency_mode m) { init_local_instances(); flush_instance_cache(); } - m_uhints = get_unification_hints(env()); } type_context::type_context(environment const & env, options const & o, metavar_context const & mctx, @@ -164,8 +163,7 @@ type_context::type_context(type_context && src): m_transparency_mode(src.m_transparency_mode), m_approximate(src.m_approximate), m_zeta(src.m_zeta), - m_smart_unfolding(src.m_smart_unfolding), - m_uhints(src.m_uhints) { + 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); @@ -184,7 +182,6 @@ type_context::~type_context() { void type_context::set_env(environment const & env) { m_env = env; - m_uhints = get_unification_hints(env); } void type_context::update_local_instances(expr const & new_local, expr const & new_type) { @@ -3295,7 +3292,7 @@ bool type_context::try_unification_hints(expr const & e1, expr const & e2) { expr e2_fn = get_app_fn(e2); if (is_constant(e1_fn) && is_constant(e2_fn)) { buffer hints; - get_unification_hints(m_uhints, const_name(e1_fn), const_name(e2_fn), hints); + m_cache->get_unification_hints(*this, const_name(e1_fn), const_name(e2_fn), hints); for (unification_hint const & hint : hints) { lean_trace(name({"type_context", "unification_hint"}), scope_trace_env scope(env(), *this); diff --git a/src/library/type_context.h b/src/library/type_context.h index 20d1f55b8d..479d4b22b7 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -524,7 +524,6 @@ private: that cannot be solved precisely are ignored. This step is approximate, and it is useful to skip it until we have additional information. */ bool m_full_postponed{true}; - unification_hints m_uhints; std::function const * m_transparency_pred{nullptr}; // NOLINT