diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index d95bb40750..f39f0d2850 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -467,7 +467,7 @@ static void print_unification_hints(parser & p) { static void print_rfl_lemmas(parser & p) { type_checker tc(p.env()); auto out = regular(p.env(), p.ios(), tc); - out << pp_rfl_lemmas(*get_rfl_lemmas(p.env()), out.get_formatter()); + out << pp_rfl_lemmas(get_rfl_lemmas(p.env()), out.get_formatter()); } static void print_simp_rules(parser & p) { diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index c2e7c43e1c..e2dd3c1ca6 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -302,8 +302,8 @@ static environment add_equation_lemma(environment const & env, options const & o if (use_dsimp) { try { type_context ctx(env, opts, mctx, lctx, transparency_mode::None); - rfl_lemmas_ptr lemmas = get_rfl_lemmas(env, g_eqn_sanitizer_token); - new_type = defeq_simplify(ctx, *lemmas, type); + rfl_lemmas lemmas = get_rfl_lemmas(env, g_eqn_sanitizer_token); + new_type = defeq_simplify(ctx, lemmas, type); } catch (defeq_simplifier_exception & ex) { throw nested_exception("equation compiler failed to simplify type of automatically generated lemma using " "defeq simplifier " diff --git a/src/library/rfl_lemmas.cpp b/src/library/rfl_lemmas.cpp index 58ec2d5991..d0cffb182e 100644 --- a/src/library/rfl_lemmas.cpp +++ b/src/library/rfl_lemmas.cpp @@ -54,7 +54,7 @@ static void on_add_rfl_lemma(environment const & env, name const & decl_name, bo } static void add_lemma_core(tmp_type_context & ctx, name const & decl_name, unsigned priority, - rfl_lemmas_ptr & result) { + rfl_lemmas & result) { environment const & env = ctx.env(); declaration const & d = env.get(decl_name); lean_assert(d.is_definition()); @@ -76,15 +76,15 @@ static void add_lemma_core(tmp_type_context & ctx, name const & decl_name, unsig expr lhs, rhs; lean_verify(is_eq(type, lhs, rhs)); rfl_lemma lemma(decl_name, to_list(umetas), to_list(emetas), to_list(instances), lhs, rhs, priority); - result->insert(lhs, lemma); + result.insert(lhs, lemma); } -static rfl_lemmas_ptr get_rfl_lemmas_from_attribute(type_context & ctx, name const & attr_name) { +static rfl_lemmas get_rfl_lemmas_from_attribute(type_context & ctx, name const & attr_name) { environment const & env = ctx.env(); auto const & attr = get_attribute(env, attr_name); buffer lemmas; attr.get_instances(env, lemmas); - rfl_lemmas_ptr result = std::make_shared(); + rfl_lemmas result; unsigned i = lemmas.size(); while (i > 0) { i--; @@ -96,7 +96,7 @@ static rfl_lemmas_ptr get_rfl_lemmas_from_attribute(type_context & ctx, name con return result; } -static rfl_lemmas_ptr get_rfl_lemmas_from_attribute(environment const & env, name const & attr_name) { +static rfl_lemmas get_rfl_lemmas_from_attribute(environment const & env, name const & attr_name) { type_context ctx(env); return get_rfl_lemmas_from_attribute(ctx, attr_name); } @@ -114,10 +114,10 @@ rfl_lemmas_token register_defeq_simp_attribute(name const & attr_name) { class rfl_lemmas_cache { struct entry { - environment m_env; - name m_attr_name; - unsigned m_attr_fingerprint; - rfl_lemmas_ptr m_lemmas; + environment m_env; + name m_attr_name; + unsigned m_attr_fingerprint; + optional m_lemmas; entry(environment const & env, name const & attr_name): m_env(env), m_attr_name(attr_name), m_attr_fingerprint(0) {} }; @@ -129,20 +129,20 @@ public: } } - rfl_lemmas_ptr mk_lemmas(environment const & env, entry & C) { + rfl_lemmas mk_lemmas(environment const & env, entry & C) { lean_trace("rfl_lemmas_cache", tout() << "make reflexivity lemmas [" << C.m_attr_name << "]\n";); C.m_env = env; C.m_lemmas = get_rfl_lemmas_from_attribute(env, C.m_attr_name); C.m_attr_fingerprint = get_attribute_fingerprint(env, C.m_attr_name); - return C.m_lemmas; + return *C.m_lemmas; } - rfl_lemmas_ptr lemmas_of(entry const & C) { + rfl_lemmas lemmas_of(entry const & C) { lean_trace("rfl_lemmas_cache", tout() << "reusing cached reflexivity lemmas [" << C.m_attr_name << "]\n";); - return C.m_lemmas; + return *C.m_lemmas; } - rfl_lemmas_ptr get(environment const & env, rfl_lemmas_token token) { + rfl_lemmas get(environment const & env, rfl_lemmas_token token) { lean_assert(token < g_rfl_lemmas_attributes->size()); if (token >= m_entries.size()) expand(env, token+1); lean_assert(token < m_entries.size()); @@ -163,11 +163,11 @@ public: MK_THREAD_LOCAL_GET_DEF(rfl_lemmas_cache, get_cache); -rfl_lemmas_ptr get_rfl_lemmas(environment const & env) { +rfl_lemmas get_rfl_lemmas(environment const & env) { return get_cache().get(env, g_default_token); } -rfl_lemmas_ptr get_rfl_lemmas(environment const & env, rfl_lemmas_token token) { +rfl_lemmas get_rfl_lemmas(environment const & env, rfl_lemmas_token token) { return get_cache().get(env, token); } diff --git a/src/library/rfl_lemmas.h b/src/library/rfl_lemmas.h index ae1c8708bf..980be46ce0 100644 --- a/src/library/rfl_lemmas.h +++ b/src/library/rfl_lemmas.h @@ -53,9 +53,8 @@ typedef unsigned rfl_lemmas_token; It returns an internal "token" for retrieving the lemmas */ rfl_lemmas_token register_defeq_simp_attribute(name const & attr_name); -typedef std::shared_ptr rfl_lemmas_ptr; -rfl_lemmas_ptr get_rfl_lemmas(environment const & env); -rfl_lemmas_ptr get_rfl_lemmas(environment const & env, rfl_lemmas_token token); +rfl_lemmas get_rfl_lemmas(environment const & env); +rfl_lemmas get_rfl_lemmas(environment const & env, rfl_lemmas_token token); format pp_rfl_lemmas(rfl_lemmas const & lemmas, formatter const & fmt); diff --git a/src/library/tactic/defeq_simplifier.cpp b/src/library/tactic/defeq_simplifier.cpp index a3dd683711..f6e05f8055 100644 --- a/src/library/tactic/defeq_simplifier.cpp +++ b/src/library/tactic/defeq_simplifier.cpp @@ -301,15 +301,15 @@ vm_obj tactic_defeq_simp(vm_obj const & m, vm_obj const & e, vm_obj const & s0) type_context ctx = mk_type_context_for(s0, m); tactic_state const & s = to_tactic_state(s0); LEAN_TACTIC_TRY; - rfl_lemmas_ptr lemmas = get_rfl_lemmas(s.env()); - expr new_e = defeq_simplify(ctx, *lemmas, to_expr(e)); + rfl_lemmas lemmas = get_rfl_lemmas(s.env()); + expr new_e = defeq_simplify(ctx, lemmas, to_expr(e)); return mk_tactic_success(to_obj(new_e), s); LEAN_TACTIC_CATCH(s); } expr defeq_simplify(type_context & ctx, expr const & e) { - rfl_lemmas_ptr lemmas = get_rfl_lemmas(ctx.env()); - return defeq_simplify(ctx, *lemmas, e); + rfl_lemmas lemmas = get_rfl_lemmas(ctx.env()); + return defeq_simplify(ctx, lemmas, e); } /* Setup and teardown */