From 5607884787c76e330cc321f35f112cc4a692a27e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Feb 2018 17:54:48 -0800 Subject: [PATCH] feat(library/tactic): use new cache Remark: so far, caching, in the tactic framework, only makes a difference for the `simp` tactic. This is not surprising since the simplifier tries to apply rewriting lemmas over and over again. --- src/frontends/lean/elaborator.cpp | 5 ++- src/library/tactic/dsimplify.cpp | 10 +++-- src/library/tactic/exact_tactic.cpp | 8 ++-- src/library/tactic/generalize_tactic.cpp | 5 ++- src/library/tactic/rewrite_tactic.cpp | 5 ++- src/library/tactic/simp_lemmas.cpp | 57 ++++++++++++++---------- src/library/tactic/subst_tactic.cpp | 2 +- src/library/tactic/tactic_state.cpp | 48 ++++++++++++-------- src/library/tactic/tactic_state.h | 2 + 9 files changed, 86 insertions(+), 56 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 4a8bb34f30..01ef9d7385 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -4276,11 +4276,12 @@ expr resolve_names(environment const & env, local_context const & lctx, expr con static vm_obj tactic_save_type_info(vm_obj const &, vm_obj const & _e, vm_obj const & ref, vm_obj const & _s) { expr const & e = to_expr(_e); - tactic_state const & s = tactic::to_state(_s); + tactic_state s = tactic::to_state(_s); if (!get_global_info_manager() || !get_pos_info_provider()) return tactic::mk_success(s); auto pos = get_pos_info_provider()->get_pos_info(to_expr(ref)); if (!pos) return tactic::mk_success(s); - type_context ctx = mk_type_context_for(s); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); try { expr type = ctx.infer(e); get_global_info_manager()->add_type_info(*pos, type); diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index 6b17f2272b..8f3ba79376 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -426,10 +426,11 @@ public: vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a, vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & _cfg, vm_obj const & _s) { - tactic_state const & s = tactic::to_state(_s); + tactic_state s = tactic::to_state(_s); dsimp_config cfg(_cfg); try { - type_context ctx = mk_type_context_for(s, cfg.m_md); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(cfg.m_md); defeq_can_state dcs = s.dcs(); tactic_dsimplify_fn F(ctx, dcs, a, pre, post, s, cfg); expr new_e = F(to_expr(e)); @@ -445,10 +446,11 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a, } vm_obj simp_lemmas_dsimplify(vm_obj const & lemmas, vm_obj const & u, vm_obj const & e, vm_obj const & _cfg, vm_obj const & _s) { - tactic_state const & s = tactic::to_state(_s); + tactic_state s = tactic::to_state(_s); dsimp_config cfg(_cfg); try { - type_context ctx = mk_type_context_for(s, cfg.m_md); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(cfg.m_md); defeq_can_state dcs = s.dcs(); list to_unfold = to_list_name(u); simp_lemmas_for dlemmas; diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 8eab2ea62f..794d8c915a 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -10,12 +10,12 @@ Author: Leonardo de Moura #include "library/tactic/app_builder_tactics.h" namespace lean { - -vm_obj exact(expr const & e, transparency_mode const & m, tactic_state const & s) { +static vm_obj exact(expr const & e, transparency_mode const & m, tactic_state s) { try { optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); - type_context ctx = mk_type_context_for(s, m); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(m); expr mvar = head(s.goals()); if (is_metavar(e) && mlocal_name(mvar) == mlocal_name(e)) { return tactic::mk_exception("invalid exact tactic, trying to solve goal using itself", s); @@ -37,7 +37,7 @@ vm_obj exact(expr const & e, transparency_mode const & m, tactic_state const & s auto thunk = [=]() { format r("exact tactic failed, failed to assign "); formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); - type_context ctx = mk_type_context_for(s, transparency_mode::All); + type_context ctx = mk_cacheless_type_context_for(s, transparency_mode::All); formatter fmt = fmtf(s.env(), s.get_options(), ctx); unsigned indent = get_pp_indent(s.get_options()); r += nest(indent, line() + fmt(e)); diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/tactic/generalize_tactic.cpp index f2e8879330..1419d8871b 100644 --- a/src/library/tactic/generalize_tactic.cpp +++ b/src/library/tactic/generalize_tactic.cpp @@ -12,10 +12,11 @@ Author: Leonardo de Moura #include "library/tactic/kabstract.h" namespace lean { -vm_obj generalize(transparency_mode m, expr const & e, name const & id, tactic_state const & s) { +static vm_obj generalize(transparency_mode m, expr const & e, name const & id, tactic_state s) { optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); - type_context ctx = mk_type_context_for(s, m); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(m); expr target = ctx.instantiate_mvars(g->get_type()); expr target_abst = kabstract(ctx, target, e); if (closed(target_abst)) diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 477f83e100..222d640cec 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -29,10 +29,11 @@ rewrite_cfg::rewrite_cfg(vm_obj const & cfg):apply_cfg(cfield(cfg, 0)) { m_occs = to_occurrences(cfield(cfg, 2)); } -static vm_obj rewrite_core(expr h, expr e, rewrite_cfg const & cfg, tactic_state const & s) { +static vm_obj rewrite_core(expr h, expr e, rewrite_cfg const & cfg, tactic_state s) { optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); - type_context ctx = mk_type_context_for(s, cfg.m_mode); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(cfg.m_mode); type_context::approximate_scope _(ctx, cfg.m_approx); expr h_type = ctx.infer(h); /* Generate meta-variables for arguments */ diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index 685976a699..7abaa1e322 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -1332,9 +1332,11 @@ vm_obj simp_lemmas_mk_default(vm_obj const & s) { LEAN_TACTIC_CATCH(tactic::to_state(s)); } -vm_obj simp_lemmas_add(vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & s) { +vm_obj simp_lemmas_add(vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & s0) { + tactic_state s = tactic::to_state(s0); LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); expr e = to_expr(lemma); name id; if (is_constant(e)) @@ -1352,24 +1354,28 @@ vm_obj simp_lemmas_add(vm_obj const & lemmas, vm_obj const & lemma, vm_obj const expr e_type = ctx.infer(e); simp_lemmas new_lemmas = add_core(ctx, to_simp_lemmas(lemmas), id, umetas, emetas, e_type, e, LEAN_DEFAULT_PRIORITY); - return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); - LEAN_TACTIC_CATCH(tactic::to_state(s)); + return tactic::mk_success(to_obj(new_lemmas), s); + LEAN_TACTIC_CATCH(s); } -vm_obj simp_lemmas_add_simp(vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { +vm_obj simp_lemmas_add_simp(vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s0) { + tactic_state s = tactic::to_state(s0); LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); simp_lemmas new_lemmas = add(ctx, to_simp_lemmas(lemmas), to_name(lemma_name), LEAN_DEFAULT_PRIORITY); - return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); - LEAN_TACTIC_CATCH(tactic::to_state(s)); + return tactic::mk_success(to_obj(new_lemmas), s); + LEAN_TACTIC_CATCH(s); } -vm_obj simp_lemmas_add_congr(vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { +vm_obj simp_lemmas_add_congr(vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s0) { + tactic_state s = tactic::to_state(s0); LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); simp_lemmas new_lemmas = add_congr(ctx, to_simp_lemmas(lemmas), to_name(lemma_name), LEAN_DEFAULT_PRIORITY); - return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); - LEAN_TACTIC_CATCH(tactic::to_state(s)); + return tactic::mk_success(to_obj(new_lemmas), s); + LEAN_TACTIC_CATCH(s); } vm_obj simp_lemmas_mk() { @@ -1447,8 +1453,8 @@ static simp_result simp_lemma_rewrite_core(type_context & ctx, simp_lemma const return simp_result(new_rhs, pf); } -vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & sls, vm_obj const & prove_fn, - name const & R, expr const & e, tactic_state const & s) { +static vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & sls, vm_obj const & prove_fn, + name const & R, expr const & e, tactic_state s) { LEAN_TACTIC_TRY; simp_lemmas_for const * sr = sls.find(R); if (!sr) return tactic::mk_exception("failed to apply simp_lemmas, no lemmas for the given relation", s); @@ -1456,7 +1462,8 @@ vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & list const * srs = sr->find(e); if (!srs) return tactic::mk_exception("failed to apply simp_lemmas, no simp lemma", s); - type_context ctx = mk_type_context_for(s, m); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(m); for (simp_lemma const & lemma : *srs) { simp_result r = simp_lemma_rewrite_core(ctx, lemma, prove_fn, e, s); @@ -1478,7 +1485,7 @@ vm_obj simp_lemmas_rewrite(vm_obj const & sls, vm_obj const & e, vm_obj const & to_name(R), to_expr(e), tactic::to_state(s)); } -vm_obj simp_lemmas_drewrite_core(transparency_mode const & m, simp_lemmas const & sls, expr const & e, tactic_state const & s) { +static vm_obj simp_lemmas_drewrite_core(transparency_mode const & m, simp_lemmas const & sls, expr const & e, tactic_state s) { LEAN_TACTIC_TRY; simp_lemmas_for const * sr = sls.find(get_eq_name()); if (!sr) return tactic::mk_exception("failed to apply simp_lemmas, no lemmas for 'eq' relation", s); @@ -1486,7 +1493,8 @@ vm_obj simp_lemmas_drewrite_core(transparency_mode const & m, simp_lemmas const list const * srs = sr->find(e); if (!srs) return tactic::mk_exception("failed to apply simp_lemmas, no simp lemma", s); - type_context ctx = mk_type_context_for(s, m); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(m); for (simp_lemma const & lemma : *srs) { if (lemma.is_refl()) { @@ -1503,9 +1511,10 @@ vm_obj simp_lemmas_drewrite(vm_obj const & sls, vm_obj const & e, vm_obj const & return simp_lemmas_drewrite_core(to_transparency_mode(m), to_simp_lemmas(sls), to_expr(e), tactic::to_state(s)); } -static bool is_valid_simp_lemma_cnst(name const & cname, tactic_state const & s) { +static bool is_valid_simp_lemma_cnst(name const & cname, tactic_state s) { try { - type_context ctx = mk_type_context_for(s); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); type_context::tmp_mode_scope scope(ctx); declaration const & d = ctx.env().get(cname); levels ls = mk_tmp_levels_for(ctx, d); @@ -1522,9 +1531,10 @@ vm_obj is_valid_simp_lemma_cnst(vm_obj const & n, vm_obj const & s) { tactic::to_state(s)); } -static bool is_valid_simp_lemma(expr const & e, tactic_state const & s) { +static bool is_valid_simp_lemma(expr const & e, tactic_state s) { try { - type_context ctx = mk_type_context_for(s); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); expr type = ctx.infer(e); return !is_nil(to_ceqvs(ctx, name(), type, e)); } catch (exception &) { @@ -1549,8 +1559,9 @@ environment mark_rfl_lemma(environment const & env, name const & cname) { vm_obj simp_lemmas_pp(vm_obj const & S, vm_obj const & _s) { formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); - tactic_state const & s = tactic::to_state(_s); - type_context ctx = mk_type_context_for(s); + tactic_state s = tactic::to_state(_s); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); formatter fmt = fmtf(s.env(), s.get_options(), ctx); format r = to_simp_lemmas(S).pp(fmt); return tactic::mk_success(to_obj(r), s); diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index b626a13c32..313413412c 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -34,7 +34,7 @@ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, expr const & mvar, expr const & H, bool symm, hsubstitution * subst) { #define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE) -#define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S = mk_tactic_state_for_metavar(env, opts, "subst", mctx, MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp_core() << "\n";) +#define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S = mk_tactic_state_for_metavar(env, opts, "subst", mctx, MVAR); type_context TMP_CTX = mk_cacheless_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp_core() << "\n";) lean_subst_trace_state(mvar, "initial:\n"); lean_assert(mctx.find_metavar_decl(mvar)); diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index b3f70cf060..f045191bd6 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -171,7 +171,7 @@ tactic_state set_context_cache_id(tactic_state const & s, context_cache_id const } format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) const { - type_context ctx = mk_type_context_for(*this, transparency_mode::All); + type_context ctx = mk_cacheless_type_context_for(*this, transparency_mode::All); formatter fmt = fmtf(env(), get_options(), ctx); return fmt(e); } @@ -374,6 +374,10 @@ type_context mk_type_context_for(vm_obj const & s, vm_obj const & m) { return mk_type_context_for(tactic::to_state(s), to_transparency_mode(m)); } +type_context mk_cacheless_type_context_for(tactic_state const & s, transparency_mode m) { + return mk_type_context_for(s, m); +} + static void check_closed(char const * tac_name, expr const & e) { if (!closed(e)) throw exception(sstream() << "tactic '" << tac_name << "' failed, " @@ -382,8 +386,9 @@ static void check_closed(char const * tac_name, expr const & e) { } vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = tactic::to_state(s0); - type_context ctx = mk_type_context_for(s); + tactic_state s = tactic::to_state(s0); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); try { check_closed("infer_type", to_expr(e)); return tactic::mk_success(to_obj(ctx.infer(to_expr(e))), s); @@ -393,8 +398,9 @@ vm_obj tactic_infer_type(vm_obj const & e, vm_obj const & s0) { } vm_obj tactic_whnf(vm_obj const & e, vm_obj const & t, vm_obj const & unfold_ginductive, vm_obj const & s0) { - tactic_state const & s = tactic::to_state(s0); - type_context ctx = mk_type_context_for(s, to_transparency_mode(t)); + tactic_state s = tactic::to_state(s0); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(to_transparency_mode(t)); try { check_closed("whnf", to_expr(e)); if (to_bool(unfold_ginductive)) { @@ -408,8 +414,9 @@ vm_obj tactic_whnf(vm_obj const & e, vm_obj const & t, vm_obj const & unfold_gin } vm_obj tactic_head_eta_expand(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = tactic::to_state(s0); - type_context ctx = mk_type_context_for(s); + tactic_state s = tactic::to_state(s0); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); try { check_closed("head_eta_expand", to_expr(e)); return tactic::mk_success(to_obj(ctx.eta_expand(to_expr(e))), s); @@ -468,8 +475,9 @@ vm_obj tactic_zeta(vm_obj const & e0, vm_obj const & s0) { } vm_obj tactic_is_class(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = tactic::to_state(s0); - type_context ctx = mk_type_context_for(s); + tactic_state s = tactic::to_state(s0); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); try { check_closed("is_class", to_expr(e)); return tactic::mk_success(mk_vm_bool(static_cast(ctx.is_class(to_expr(e)))), s); @@ -479,8 +487,9 @@ vm_obj tactic_is_class(vm_obj const & e, vm_obj const & s0) { } vm_obj tactic_mk_instance(vm_obj const & e, vm_obj const & s0) { - tactic_state const & s = tactic::to_state(s0); - type_context ctx = mk_type_context_for(s); + tactic_state s = tactic::to_state(s0); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(); try { check_closed("mk_instance", to_expr(e)); if (auto r = ctx.mk_class_instance(to_expr(e))) { @@ -504,7 +513,7 @@ static vm_obj mk_unify_exception(char const * header, expr const & e1, expr cons format r(header); unsigned indent = get_pp_indent(s.get_options()); formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); - type_context ctx = mk_type_context_for(s, transparency_mode::All); + type_context ctx = mk_cacheless_type_context_for(s, transparency_mode::All); formatter fmt = fmtf(s.env(), s.get_options(), ctx); expr e1_type = ctx.infer(e1); expr e2_type = ctx.infer(e2); @@ -521,8 +530,9 @@ static vm_obj mk_unify_exception(char const * header, expr const & e1, expr cons } vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & approx, vm_obj const & s0) { - tactic_state const & s = tactic::to_state(s0); - type_context ctx = mk_type_context_for(s, to_transparency_mode(t)); + tactic_state s = tactic::to_state(s0); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(to_transparency_mode(t)); try { check_closed("unify", to_expr(e1)); check_closed("unify", to_expr(e2)); @@ -540,8 +550,9 @@ vm_obj tactic_unify(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_o } vm_obj tactic_is_def_eq(vm_obj const & e1, vm_obj const & e2, vm_obj const & t, vm_obj const & approx, vm_obj const & s0) { - tactic_state const & s = tactic::to_state(s0); - type_context ctx = mk_type_context_for(s, to_transparency_mode(t)); + tactic_state s = tactic::to_state(s0); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(to_transparency_mode(t)); try { check_closed("is_def_eq", to_expr(e1)); check_closed("is_def_eq", to_expr(e2)); @@ -779,7 +790,7 @@ vm_obj tactic_decl_name(vm_obj const & _s) { } format tactic_state::pp() const { - type_context ctx = mk_type_context_for(*this, transparency_mode::Semireducible); + type_context ctx = mk_cacheless_type_context_for(*this, transparency_mode::Semireducible); expr ts_expr = mk_constant("tactic_state"); optional to_fmt_inst = ctx.mk_class_instance(mk_app(mk_constant("has_to_format", {mk_level_zero()}), ts_expr)); if (!to_fmt_inst) { @@ -936,7 +947,8 @@ vm_obj tactic_sleep(vm_obj const & msecs, vm_obj const & s0) { vm_obj tactic_type_check(vm_obj const & e, vm_obj const & m, vm_obj const & s0) { tactic_state s = tactic::to_state(s0); try { - type_context ctx = mk_type_context_for(s, to_transparency_mode(m)); + tactic_state_context_cache cache(s); + type_context ctx = cache.mk_type_context(to_transparency_mode(m)); check(ctx, to_expr(e)); return tactic::mk_success(s); } catch (exception & ex) { diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index 269edec9f2..7cb2a290fa 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -196,6 +196,8 @@ type_context mk_type_context_for(environment const & env, options const & o, type_context mk_type_context_for(vm_obj const & s); type_context mk_type_context_for(vm_obj const & s, vm_obj const & m); +type_context mk_cacheless_type_context_for(tactic_state const & s, transparency_mode m = transparency_mode::Semireducible); + #define lean_tactic_trace(N, S, Code) lean_trace(N, { \ type_context _ctx = mk_type_context_for(S); \ scope_trace_env _scope((S).env(), _ctx); \