max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic): use new cache

Browse source 
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.
This commit is contained in:
Leonardo de Moura 2018-02-20 17:54:48 -08:00
parent 80b88c53cb
commit 5607884787
9 changed files with 86 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/elaborator.cpp
View file

@ -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);

10
src/library/tactic/dsimplify.cpp
View file

@ -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<name> to_unfold = to_list_name(u);
simp_lemmas_for dlemmas;

8
src/library/tactic/exact_tactic.cpp
View file

@ -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<metavar_decl> 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));

5
src/library/tactic/generalize_tactic.cpp
View file

@ -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<metavar_decl> 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))

5
src/library/tactic/rewrite_tactic.cpp
View file

@ -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<metavar_decl> 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 */

57
src/library/tactic/simp_lemmas.cpp
View file

@ -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<simp_lemma> 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<simp_lemma> 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);

2
src/library/tactic/subst_tactic.cpp
View file

@ -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));

48
src/library/tactic/tactic_state.cpp
View file

@ -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<bool>(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<expr> 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) {

2
src/library/tactic/tactic_state.h
View file

@ -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); \