diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 20f7296c2f..088e3de5e7 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -584,10 +584,10 @@ static environment unify_cmd(parser & p) { e1 = convert_metavars(mctx, e1); e2 = convert_metavars(mctx, e2); tout() << e1 << " =?= " << e2 << "\n"; - type_context ctx(env, p.get_options(), mctx, lctx, transparency_mode::Semireducible); - bool success = ctx.is_def_eq(e1, e2); + aux_type_context ctx(env, p.get_options(), mctx, lctx, transparency_mode::Semireducible); + bool success = ctx->is_def_eq(e1, e2); if (success) - tout() << ctx.instantiate_mvars(e1) << " =?= " << ctx.instantiate_mvars(e2) << "\n"; + tout() << ctx->instantiate_mvars(e1) << " =?= " << ctx->instantiate_mvars(e2) << "\n"; flycheck_information info(p.ios()); if (info.enabled()) { p.display_information_pos(p.cmd_pos()); @@ -680,7 +680,7 @@ static environment elab_cmd(parser & p) { expr new_e; level_param_names ls; std::tie(new_e, ls) = p.elaborate(e); metavar_context mctx; - type_context ctx(p.env(), p.get_options(), mctx, p.get_local_context()); + aux_type_context ctx(p.env(), p.get_options(), mctx, p.get_local_context()); auto out = regular(p.env(), p.ios(), ctx); out << ">> " << e << "\n"; out << ">> " << new_e << "\n"; diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index 8f7254ebd8..f9910e2303 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -1971,8 +1971,8 @@ void old_elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name throw_elaborator_exception("tactic failed, result contains meta-variables", r); } metavar_decl main_decl = *mctx.get_metavar_decl(new_ts->main()); - type_context aux_ctx(env(), opts, mctx, main_decl.get_context()); - r = aux_ctx.mk_lambda(new_locals, r); + aux_type_context aux_ctx(env(), opts, mctx, main_decl.get_context()); + r = aux_ctx->mk_lambda(new_locals, r); subst.assign(mvar, r); } } diff --git a/src/library/compiler/compiler_step_visitor.cpp b/src/library/compiler/compiler_step_visitor.cpp index 1d3608dd76..aefa05b0de 100644 --- a/src/library/compiler/compiler_step_visitor.cpp +++ b/src/library/compiler/compiler_step_visitor.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura namespace lean { compiler_step_visitor::compiler_step_visitor(environment const & env): m_env(env), - m_ctx(m_env, options(), m_mctx, m_lctx, transparency_mode::All) { + m_ctx(env, transparency_mode::All) { } compiler_step_visitor::~compiler_step_visitor() { diff --git a/src/library/compiler/compiler_step_visitor.h b/src/library/compiler/compiler_step_visitor.h index 63ee2300f9..940458e4b3 100644 --- a/src/library/compiler/compiler_step_visitor.h +++ b/src/library/compiler/compiler_step_visitor.h @@ -13,10 +13,8 @@ namespace lean { Types are ignored during compilation steps. */ class compiler_step_visitor : public replace_visitor { protected: - environment m_env; - local_context m_lctx; - metavar_context m_mctx; - type_context m_ctx; + environment m_env; + aux_type_context m_ctx; expr visit_lambda_let(expr const & e); protected: diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp index b77440e1f8..49694c4a8f 100644 --- a/src/library/compiler/elim_recursors.cpp +++ b/src/library/compiler/elim_recursors.cpp @@ -41,7 +41,7 @@ protected: typedef rb_map idx2decls; void collect_locals(expr const & e, idx2decls & r) { - local_context const & lctx = m_ctx.lctx(); + local_context const & lctx = ctx().lctx(); for_each(e, [&](expr const & e, unsigned) { if (is_local_decl_ref(e)) { local_decl d = *lctx.get_local_decl(e); @@ -109,7 +109,7 @@ protected: buffer abst_locals; aux = abstract_locals(aux, abst_locals); /* Create expr (rec_fn) for representing recursive calls. */ - expr aux_decl_type = m_ctx.infer(aux); + expr aux_decl_type = ctx().infer(aux); name aux_decl_name = mk_fresh_name(m_env, m_prefix, "_rec", m_idx); expr rec_fn = mk_rec_fn_macro(aux_decl_name, aux_decl_type); /* Create new locals for aux. @@ -132,23 +132,23 @@ protected: These parameters are fixed in recursive calls. */ rec_fn = mk_app(rec_fn, aux_decl_params); /* Create locals for indices and major premise */ - expr aux_body_type = m_ctx.infer(aux_body); + expr aux_body_type = ctx().infer(aux_body); buffer indices; for (unsigned i = 0; i < nindices; i++) { - aux_body_type = m_ctx.whnf(aux_body_type); + aux_body_type = ctx().whnf(aux_body_type); lean_assert(is_pi(aux_body_type)); expr index = locals.push_local_from_binding(aux_body_type); indices.push_back(index); aux_body_type = instantiate(binding_body(aux_body_type), index); } - aux_body_type = m_ctx.whnf(aux_body_type); + aux_body_type = ctx().whnf(aux_body_type); lean_assert(is_pi(aux_body_type)); expr major = locals.push_local_from_binding(aux_body_type); /* Make sure result is eta-expanded */ buffer extra_args; /* to make sure result is eta-expanded */ aux_body_type = instantiate(binding_body(aux_body_type), major); while (true) { - aux_body_type = m_ctx.whnf(aux_body_type); + aux_body_type = ctx().whnf(aux_body_type); if (!is_pi(aux_body_type)) break; expr new_arg = locals.push_local_from_binding(aux_body_type); @@ -182,11 +182,11 @@ protected: minor = instantiate(binding_body(minor), minor_local); /* Check if minor_local is recursive data */ type_context::tmp_locals aux_locals(m_ctx); - expr minor_local_type = m_ctx.whnf(ctx().infer(minor_local)); + expr minor_local_type = ctx().whnf(ctx().infer(minor_local)); // tout() << ">>> minor_local_type: " << minor_local_type << "\n"; while (is_pi(minor_local_type)) { expr aux_local = aux_locals.push_local_from_binding(minor_local_type); - minor_local_type = m_ctx.whnf(instantiate(binding_body(minor_local_type), aux_local)); + minor_local_type = ctx().whnf(instantiate(binding_body(minor_local_type), aux_local)); } if (is_constant(get_app_fn(minor_local_type), I_name)) { /* Recursive data, we must update minor_recs */ diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 4881b70807..2039ecd95a 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -43,7 +43,7 @@ class lambda_lifting_fn : public compiler_step_visitor { typedef rb_map idx2decls; void collect_locals(expr const & e, idx2decls & r) { - local_context const & lctx = m_ctx.lctx(); + local_context const & lctx = ctx().lctx(); for_each(e, [&](expr const & e, unsigned) { if (is_local_decl_ref(e)) { local_decl d = *lctx.get_local_decl(e); diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 2da2900fb6..d8c57458b0 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -88,7 +88,7 @@ format tactic_state::pp_goal(formatter_factory const & fmtf, expr const & g) con metavar_decl decl = *mctx().get_metavar_decl(g); local_context const & lctx = decl.get_context(); metavar_context mctx_tmp = mctx(); - type_context ctx(env(), get_options(), mctx_tmp, lctx, transparency_mode::All); + aux_type_context ctx(env(), get_options(), mctx_tmp, lctx, transparency_mode::All); formatter fmt = fmtf(env(), get_options(), ctx); format r = lctx.pp(fmt); unsigned indent = get_pp_indent(get_options()); @@ -236,7 +236,7 @@ vm_obj tactic_format_result(vm_obj const & o) { metavar_context mctx = s.mctx(); expr r = mctx.instantiate_mvars(s.main()); metavar_decl main_decl = *mctx.get_metavar_decl(s.main()); - type_context ctx(s.env(), s.get_options(), mctx, main_decl.get_context(), transparency_mode::All); + aux_type_context ctx(s.env(), s.get_options(), mctx, main_decl.get_context(), transparency_mode::All); formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); formatter fmt = fmtf(s.env(), s.get_options(), ctx); return mk_tactic_success(to_obj(fmt(r)), s); diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index d20052e26d..017ba82d42 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -184,29 +184,21 @@ void type_context::init_core(transparency_mode m) { m_is_def_eq_depth = 0; m_tmp_uassignment = nullptr; m_tmp_eassignment = nullptr; - m_cache->m_init_local_context = m_lctx; - if (!m_cache->m_frozen_mode) { + m_cache.m_init_local_context = m_lctx; + if (!m_cache.m_frozen_mode) { /* default type class resolution mode */ - m_cache->m_local_instances_initialized = false; + m_cache.m_local_instances_initialized = false; } m_unfold_pred = nullptr; } type_context::type_context(metavar_context & mctx, local_context const & lctx, type_context_cache & cache, transparency_mode m): - m_mctx(mctx), m_lctx(lctx), m_cache(&cache), m_cache_owner(false) { - init_core(m); -} - -type_context::type_context(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx, - transparency_mode m): - m_mctx(mctx), m_lctx(lctx), m_cache(new type_context_cache(env, opts)), m_cache_owner(true) { + m_mctx(mctx), m_lctx(lctx), m_cache(cache) { init_core(m); } type_context::~type_context() { - if (m_cache_owner) - delete m_cache; } expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) { @@ -387,7 +379,7 @@ expr type_context::mk_pi(std::initializer_list const & locals, expr const -------------------- */ optional type_context::is_transparent(transparency_mode m, name const & n) { - return m_cache->is_transparent(m, n); + return m_cache.is_transparent(m, n); } optional type_context::is_transparent(name const & n) { @@ -431,7 +423,7 @@ optional type_context::reduce_projection(expr const & e) { expr const & f = get_app_fn(e); if (!is_constant(f)) return none_expr(); - projection_info const * info = m_cache->m_proj_info.find(const_name(f)); + projection_info const * info = m_cache.m_proj_info.find(const_name(f)); if (!info) return none_expr(); buffer args; @@ -471,7 +463,7 @@ bool type_context::should_unfold_macro(expr const & e) { return m_transparency_mode == transparency_mode::All || m_in_is_def_eq || - m_cache->should_unfold_macro(e); + m_cache.should_unfold_macro(e); } optional type_context::expand_macro(expr const & e) { @@ -628,7 +620,7 @@ expr type_context::infer_core(expr const & e) { lean_assert(!is_var(e)); lean_assert(closed(e)); - auto & cache = m_cache->m_infer_cache; + auto & cache = m_cache.m_infer_cache; auto it = cache.find(e); if (it != cache.end()) return it->second; @@ -2087,17 +2079,17 @@ optional type_context::is_class(expr const & type) { bool type_context::compatible_local_instances(bool frozen_only) { unsigned i = 0; bool failed = false; - m_cache->m_init_local_context.for_each([&](local_decl const & decl) { + m_cache.m_init_local_context.for_each([&](local_decl const & decl) { if (failed) return; - if (frozen_only && !m_cache->m_init_local_context.is_frozen(decl.get_name())) + if (frozen_only && !m_cache.m_init_local_context.is_frozen(decl.get_name())) return; if (auto cname = is_class(decl.get_type())) { - if (i == m_cache->m_local_instances.size()) { + if (i == m_cache.m_local_instances.size()) { /* initial local context has more local instances than the ones cached at found m_local_instances */ failed = true; return; } - if (decl.get_name() != mlocal_name(m_cache->m_local_instances[i].second)) { + if (decl.get_name() != mlocal_name(m_cache.m_local_instances[i].second)) { /* local instance in initial local constext is not compatible with the one cached at m_local_instances */ failed = true; return; @@ -2105,35 +2097,35 @@ bool type_context::compatible_local_instances(bool frozen_only) { i++; } }); - return i == m_cache->m_local_instances.size(); + return i == m_cache.m_local_instances.size(); } void type_context::set_local_instances() { - m_cache->m_instance_cache.clear(); - m_cache->m_subsingleton_cache.clear(); - m_cache->m_local_instances.clear(); - m_cache->m_init_local_context.for_each([&](local_decl const & decl) { + m_cache.m_instance_cache.clear(); + m_cache.m_subsingleton_cache.clear(); + m_cache.m_local_instances.clear(); + m_cache.m_init_local_context.for_each([&](local_decl const & decl) { if (auto cls_name = is_class(decl.get_type())) { - m_cache->m_local_instances.emplace_back(*cls_name, decl.mk_ref()); + m_cache.m_local_instances.emplace_back(*cls_name, decl.mk_ref()); } }); } void type_context::init_local_instances() { - if (m_cache->m_frozen_mode) { - lean_assert(m_cache->m_local_instances_initialized); + if (m_cache.m_frozen_mode) { + lean_assert(m_cache.m_local_instances_initialized); /* Check if the local instances are really compatible. See comment at type_context_cache. */ lean_cond_assert("type_context", compatible_local_instances(true)); - } else if (!m_cache->m_local_instances_initialized) { + } else if (!m_cache.m_local_instances_initialized) { /* default type class resolution mode */ bool frozen_only = false; if (!compatible_local_instances(frozen_only)) { set_local_instances(); } - m_cache->m_local_instances_initialized = true; + m_cache.m_local_instances_initialized = true; } - lean_assert(m_cache->m_local_instances_initialized); + lean_assert(m_cache.m_local_instances_initialized); } [[ noreturn ]] static void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); } @@ -2196,12 +2188,12 @@ struct instance_synthesizer { auto out = tout(); if (!m_displayed_trace_header && m_choices.size() == 1) { out << tclass("class_instances"); - if (m_ctx.m_cache->m_pip) { - if (auto fname = m_ctx.m_cache->m_pip->get_file_name()) { + if (m_ctx.m_cache.m_pip) { + if (auto fname = m_ctx.m_cache.m_pip->get_file_name()) { out << fname << ":"; } - if (m_ctx.m_cache->m_ci_pos) - out << m_ctx.m_cache->m_ci_pos->first << ":" << m_ctx.m_cache->m_ci_pos->second << ":"; + if (m_ctx.m_cache.m_ci_pos) + out << m_ctx.m_cache.m_ci_pos->first << ":" << m_ctx.m_cache.m_ci_pos->second << ":"; } out << " class-instance resolution trace" << endl; m_displayed_trace_header = true; @@ -2274,7 +2266,7 @@ struct instance_synthesizer { list get_local_instances(name const & cname) { buffer selected; - for (pair const & p : m_ctx.m_cache->m_local_instances) { + for (pair const & p : m_ctx.m_cache.m_local_instances) { if (p.first == cname) selected.push_back(p.second); } @@ -2283,7 +2275,7 @@ struct instance_synthesizer { bool mk_choice_point(expr const & mvar) { lean_assert(is_metavar(mvar)); - if (m_choices.size() > m_ctx.m_cache->m_ci_max_depth) { + if (m_choices.size() > m_ctx.m_cache.m_ci_max_depth) { throw_class_exception("maximum class-instance resolution depth has been reached " "(the limit can be increased by setting option 'class.instance_max_depth') " "(the class-instance resolution trace can be visualized " @@ -2306,7 +2298,7 @@ struct instance_synthesizer { if (!cname) return false; r.m_local_instances = get_local_instances(*cname); - if (m_ctx.m_cache->m_ci_trans_instances && toplevel_choice) { + if (m_ctx.m_cache.m_ci_trans_instances && toplevel_choice) { // we only use transitive instances in the top-level r.m_trans_instances = get_class_derived_trans_instances(env(), *cname); } @@ -2418,7 +2410,7 @@ struct instance_synthesizer { } void cache_result(expr const & type, optional const & inst) { - m_ctx.m_cache->m_instance_cache.insert(mk_pair(type, inst)); + m_ctx.m_cache.m_instance_cache.insert(mk_pair(type, inst)); } optional ensure_no_meta(optional r) { @@ -2437,8 +2429,8 @@ struct instance_synthesizer { optional mk_class_instance_core(expr const & type) { /* We do not cache results when multiple instances have to be generated. */ - auto it = m_ctx.m_cache->m_instance_cache.find(type); - if (it != m_ctx.m_cache->m_instance_cache.end()) { + auto it = m_ctx.m_cache.m_instance_cache.find(type); + if (it != m_ctx.m_cache.m_instance_cache.end()) { /* instance/failure is already cached */ lean_trace("class_instances", if (it->second) @@ -2478,12 +2470,12 @@ optional type_context::mk_class_instance(expr const & type) { } optional type_context::mk_subsingleton_instance(expr const & type) { - auto it = m_cache->m_subsingleton_cache.find(type); - if (it != m_cache->m_subsingleton_cache.end()) + auto it = m_cache.m_subsingleton_cache.find(type); + if (it != m_cache.m_subsingleton_cache.end()) return it->second; expr Type = whnf(infer(type)); if (!is_sort(Type)) { - m_cache->m_subsingleton_cache.insert(mk_pair(type, none_expr())); + m_cache.m_subsingleton_cache.insert(mk_pair(type, none_expr())); return none_expr(); } level lvl = sort_level(Type); @@ -2493,7 +2485,7 @@ optional type_context::mk_subsingleton_instance(expr const & type) { else subsingleton = whnf(mk_app(mk_constant(get_is_trunc_is_prop_name(), {lvl}), type)); auto r = mk_class_instance(subsingleton); - m_cache->m_subsingleton_cache.insert(mk_pair(type, r)); + m_cache.m_subsingleton_cache.insert(mk_pair(type, r)); return r; } diff --git a/src/library/type_context.h b/src/library/type_context.h index dce0473977..5b97bd3e5b 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include "util/flet.h" #include "kernel/environment.h" #include "kernel/abstract_type_context.h" #include "kernel/expr_maps.h" @@ -145,8 +146,7 @@ class type_context : public abstract_type_context { metavar_context & m_mctx; local_context m_lctx; - cache * m_cache; - bool m_cache_owner; + cache & m_cache; /* We only cache results when m_used_assignment is false */ bool m_used_assignment; transparency_mode m_transparency_mode; @@ -179,13 +179,10 @@ class type_context : public abstract_type_context { public: type_context(metavar_context & mctx, local_context const & lctx, type_context_cache & cache, transparency_mode m = transparency_mode::Reducible); - /* Constructor for creating a type_context with a temporary type_context_cache object. */ - type_context(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx, - transparency_mode m = transparency_mode::Reducible); virtual ~type_context(); - virtual environment const & env() const override { return m_cache->m_env; } - options const & get_options() const { return m_cache->m_options; } + virtual environment const & env() const override { return m_cache.m_env; } + options const & get_options() const { return m_cache.m_options; } local_context const & lctx() const { return m_lctx; } bool is_def_eq(level const & l1, level const & l2); @@ -243,6 +240,12 @@ public: transparency_mode mode() const { return m_transparency_mode; } unsigned mode_idx() const { return static_cast(mode()); } + struct transparency_scope : public flet { + transparency_scope(type_context & ctx, transparency_mode m): + flet(ctx.m_transparency_mode, m) { + } + }; + /* -------------------------- Temporary assignment mode. It is used when performing type class resolution and matching. @@ -460,21 +463,32 @@ public: /** Auxiliary object for automating the creation of temporary type_context objects */ class aux_type_context { - metavar_context m_mctx; - type_context m_ctx; + type_context_cache m_cache; + metavar_context m_mctx; + type_context m_ctx; public: + aux_type_context(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx, + transparency_mode m = transparency_mode::Reducible): + m_cache(env, opts), + m_mctx(mctx), + m_ctx(m_mctx, lctx, m_cache, m) {} + aux_type_context(environment const & env, options const & opts, local_context const & lctx, transparency_mode m = transparency_mode::Reducible): - m_ctx(env, opts, m_mctx, lctx, m) {} + m_cache(env, opts), + m_ctx(m_mctx, lctx, m_cache, m) {} + aux_type_context(environment const & env, options const & opts, transparency_mode m = transparency_mode::Reducible): - m_ctx(env, opts, m_mctx, local_context(), m) {} + m_cache(env, opts), + m_ctx(m_mctx, local_context(), m_cache, m) {} + aux_type_context(environment const & env, transparency_mode m = transparency_mode::Reducible): - m_ctx(env, options(), m_mctx, local_context(), m) {} + m_cache(env, options()), + m_ctx(m_mctx, local_context(), m_cache, m) {} type_context & get() { return m_ctx; } operator type_context&() { return m_ctx; } - operator type_context() { return m_ctx; } type_context * operator->() { return &m_ctx; } };