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

refactor(library/tactic): move defeq_canonizer::state to tactic_state

Browse source 
It was being stored in the environment before. This was very hackish,
and it was producing a series of unnecessary environment updates, and
thread local caches invalidations.

The new test tests/lean/run/heap.lean is 5x-6x faster after this commit.
This commit is contained in:
Leonardo de Moura 2017-01-07 10:14:57 -08:00
parent da945e34de
commit 94f16d1e44
19 changed files with 233 additions and 198 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/smt2/parser.cpp
View file

@ -478,7 +478,7 @@ private:
metavar_context mctx;
expr goal_mvar = mctx.mk_metavar_decl(lctx(), mk_constant(get_false_name()));
vm_obj s = to_obj(tactic_state(env(), ios().get_options(), mctx, list<expr>(goal_mvar), goal_mvar));
vm_obj s = to_obj(mk_tactic_state_for_metavar(env(), ios().get_options(), mctx, goal_mvar));
vm_state state(env(), ios().get_options());
scope_vm_state scope(state);

39
src/library/defeq_canonizer.cpp
View file

@ -11,36 +11,11 @@ Author: Leonardo de Moura
#include "library/defeq_canonizer.h"
namespace lean {
struct defeq_canonizer_ext : public environment_extension {
defeq_canonizer::state m_state;
defeq_canonizer_ext() {}
defeq_canonizer_ext(defeq_canonizer::state const & s):m_state(s) {}
};
void initialize_defeq_canonizer() {}
void finalize_defeq_canonizer() {}
struct defeq_canonizer_ext_reg {
unsigned m_ext_id;
defeq_canonizer_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<defeq_canonizer_ext>()); }
};
static defeq_canonizer_ext_reg * g_ext = nullptr;
static defeq_canonizer_ext const & get_extension(environment const & env) {
return static_cast<defeq_canonizer_ext const &>(env.get_extension(g_ext->m_ext_id));
}
static environment update(environment const & env, defeq_canonizer_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<defeq_canonizer_ext>(ext));
}
void initialize_defeq_canonizer() {
g_ext = new defeq_canonizer_ext_reg();
}
void finalize_defeq_canonizer() {
delete g_ext;
}
defeq_canonizer::defeq_canonizer(type_context & ctx):
m_ctx(ctx),
m_state(get_extension(ctx.env()).m_state) {
defeq_canonizer::defeq_canonizer(type_context & ctx, state & s):
m_ctx(ctx), m_state(s) {
}
optional<name> defeq_canonizer::get_head_symbol(expr type) {
@ -135,10 +110,4 @@ expr defeq_canonizer::canonize(expr const & e) {
m_updated = nullptr;
return canonize_core(e);
}
environment defeq_canonizer::update_state(environment const & env) const {
lean_assert(env.is_descendant(m_ctx.env()));
defeq_canonizer_ext ext(m_state);
return update(env, ext);
}
}

17
src/library/defeq_canonizer.h
View file

@ -32,14 +32,14 @@ public:
struct state {
/* Canonical mapping I -> J (i.e., J is the canonical expression for I).
Invariant: locals_subset(J, I) */
rb_expr_map<expr> m_C;
rb_expr_map<expr> m_C;
/* Mapping from head symbol N to list of expressions es s.t.
for each e in es, head_symbol(e) = N. */
name_map<list<expr>> m_M;
name_map<list<expr>> m_M;
};
private:
type_context & m_ctx;
state m_state;
state & m_state;
bool * m_updated{nullptr};
optional<name> get_head_symbol(expr type);
@ -51,16 +51,19 @@ private:
expr canonize_core(expr const & e);
public:
defeq_canonizer(type_context & ctx);
defeq_canonizer(type_context & ctx, state & s);
expr canonize(expr const & e, bool & updated);
expr canonize(expr const & e);
/* Update the defeq_canonizer::state in the given environment with the state in this
defeq_canonizer object. */
environment update_state(environment const & env) const;
state const & get_state() const { return m_state; }
void set_state(state const & s) { m_state = s; }
};
inline bool is_eqp(defeq_canonizer::state const & s1, defeq_canonizer::state const & s2) {
return is_eqp(s1.m_C, s2.m_C) && is_eqp(s1.m_M, s2.m_M);
}
void initialize_defeq_canonizer();
void finalize_defeq_canonizer();
}

3
src/library/inductive_compiler/nested.cpp
View file

@ -1266,7 +1266,8 @@ class add_nested_inductive_decl_fn {
bool canonize_instances = false;
bool canonize_proofs = false;
bool use_axioms = false;
simplify_fn simplifier(tctx, all_lemmas, max_steps, contextual, lift_eq,
defeq_can_state dcs;
simplify_fn simplifier(tctx, dcs, all_lemmas, max_steps, contextual, lift_eq,
canonize_instances, canonize_proofs, use_axioms);
auto thm_pr = simplifier.prove_by_simp(get_eq_name(), thm);
if (!thm_pr) {

4
src/library/tactic/cases_tactic.cpp
View file

@ -56,7 +56,7 @@ struct cases_tactic_fn {
/* throw exception that stores the intermediate state */
[[ noreturn ]] void throw_exception(expr const & mvar, char const * msg) {
throw cases_tactic_exception(tactic_state(m_env, m_opts, m_mctx, to_list(mvar), mvar), msg);
throw cases_tactic_exception(mk_tactic_state_for_metavar(m_env, m_opts, m_mctx, mvar), msg);
}
#define lean_cases_trace(MVAR, CODE) lean_trace(name({"tactic", "cases"}), type_context TMP_CTX = mk_type_context_for(MVAR); scope_trace_env _scope1(m_env, TMP_CTX); CODE)
@ -232,7 +232,7 @@ struct cases_tactic_fn {
}
format pp_goal(expr const & mvar) {
tactic_state tmp(m_env, m_opts, m_mctx, to_list(mvar), mvar);
tactic_state tmp = mk_tactic_state_for_metavar(m_env, m_opts, m_mctx, mvar);
return tmp.pp_goal(mvar);
}

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

@ -176,8 +176,8 @@ expr dsimplify_core_fn::visit(expr const & e) {
return curr_e;
}
dsimplify_core_fn::dsimplify_core_fn(type_context & ctx, unsigned max_steps, bool visit_instances):
m_ctx(ctx), m_defeq_canonizer(ctx), m_num_steps(0), m_need_restart(false),
dsimplify_core_fn::dsimplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, bool visit_instances):
m_ctx(ctx), m_defeq_canonizer(ctx, dcs), m_num_steps(0), m_need_restart(false),
m_max_steps(max_steps), m_visit_instances(visit_instances) {}
expr dsimplify_core_fn::operator()(expr e) {
@ -242,9 +242,9 @@ optional<pair<expr, bool>> dsimplify_fn::post(expr const & e) {
return optional<pair<expr, bool>>(curr_e, true);
}
dsimplify_fn::dsimplify_fn(type_context & ctx, unsigned max_steps, bool visit_instances, simp_lemmas_for const & lemmas,
dsimplify_fn::dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, bool visit_instances, simp_lemmas_for const & lemmas,
bool use_eta):
dsimplify_core_fn(ctx, max_steps, visit_instances),
dsimplify_core_fn(ctx, dcs, max_steps, visit_instances),
m_simp_lemmas(lemmas),
m_use_eta(use_eta) {
}
@ -256,11 +256,12 @@ class tactic_dsimplify_fn : public dsimplify_core_fn {
tactic_state m_s;
optional<pair<expr, bool>> invoke_fn(vm_obj const & fn, expr const & e) {
m_s = set_mctx_lctx(m_s, m_ctx.mctx(), m_ctx.lctx());
m_s = set_mctx_lctx_dcs(m_s, m_ctx.mctx(), m_ctx.lctx(), m_defeq_canonizer.get_state());
vm_obj r = invoke(fn, m_a, to_obj(e), to_obj(m_s));
if (optional<tactic_state> new_s = is_tactic_success(r)) {
m_s = *new_s;
m_ctx.set_mctx(m_s.mctx());
m_defeq_canonizer.set_state(m_s.dcs());
vm_obj p = cfield(r, 0);
m_a = cfield(p, 0);
vm_obj p1 = cfield(p, 1);
@ -281,9 +282,9 @@ class tactic_dsimplify_fn : public dsimplify_core_fn {
}
public:
tactic_dsimplify_fn(type_context & ctx, unsigned max_steps, bool visit_instances,
tactic_dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, bool visit_instances,
vm_obj const & a, vm_obj const & pre, vm_obj const & post):
dsimplify_core_fn(ctx, max_steps, visit_instances),
dsimplify_core_fn(ctx, dcs, max_steps, visit_instances),
m_a(a),
m_pre(pre),
m_post(post),
@ -293,42 +294,40 @@ public:
vm_obj const & get_a() const { return m_a; }
};
static tactic_state update_defeq_canonizer_state(tactic_state const & s, dsimplify_core_fn const & f) {
return set_env(s, f.update_defeq_canonizer_state(s.env()));
}
vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a,
vm_obj const & max_steps, vm_obj const & visit_instances,
vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & s) {
vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & _s) {
tactic_state const & s = to_tactic_state(_s);
try {
type_context ctx = mk_type_context_for(to_tactic_state(s));
tactic_dsimplify_fn F(ctx, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
type_context ctx = mk_type_context_for(s);
defeq_can_state dcs = s.dcs();
tactic_dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
to_bool(visit_instances), a, pre, post);
expr new_e = F(to_expr(e));
tactic_state new_s = set_mctx(to_tactic_state(s), F.mctx());
new_s = update_defeq_canonizer_state(new_s, F);
tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
return mk_tactic_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s);
} catch (exception & ex) {
return mk_tactic_exception(ex, to_tactic_state(s));
return mk_tactic_exception(ex, s);
}
}
vm_obj simp_lemmas_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit_instances, vm_obj const & lemmas,
vm_obj const & e, vm_obj const & s) {
vm_obj const & e, vm_obj const & _s) {
tactic_state const & s = to_tactic_state(_s);
try {
type_context ctx = mk_type_context_for(to_tactic_state(s));
type_context ctx = mk_type_context_for(s);
defeq_can_state dcs = s.dcs();
simp_lemmas_for dlemmas;
if (auto * dls = to_simp_lemmas(lemmas).find(get_eq_name()))
dlemmas = *dls;
bool use_eta = true; /* TODO(Leo): expose flag in the Lean API */
dsimplify_fn F(ctx, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
to_bool(visit_instances), dlemmas, use_eta);
expr new_e = F(to_expr(e));
tactic_state new_s = set_mctx(to_tactic_state(s), F.mctx());
new_s = update_defeq_canonizer_state(new_s, F);
tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
return mk_tactic_success(to_obj(new_e), new_s);
} catch (exception & ex) {
return mk_tactic_exception(ex, to_tactic_state(s));
return mk_tactic_exception(ex, s);
}
}

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

@ -32,13 +32,9 @@ protected:
expr visit(expr const & e);
public:
dsimplify_core_fn(type_context & ctx, unsigned max_steps, bool visit_instances);
dsimplify_core_fn(type_context & ctx, defeq_canonizer::state & s, unsigned max_steps, bool visit_instances);
expr operator()(expr e);
metavar_context const & mctx() const;
environment update_defeq_canonizer_state(environment const & env) const {
return m_defeq_canonizer.update_state(env);
}
};
class dsimplify_fn : public dsimplify_core_fn {
@ -48,8 +44,8 @@ class dsimplify_fn : public dsimplify_core_fn {
virtual optional<pair<expr, bool>> pre(expr const & e) override;
virtual optional<pair<expr, bool>> post(expr const & e) override;
public:
dsimplify_fn(type_context & ctx, unsigned max_steps, bool visit_instances, simp_lemmas_for const & lemmas,
bool use_eta);
dsimplify_fn(type_context & ctx, defeq_canonizer::state & s,
unsigned max_steps, bool visit_instances, simp_lemmas_for const & lemmas, bool use_eta);
};
void initialize_dsimplify();

29
src/library/tactic/simplify.cpp
View file

@ -701,10 +701,10 @@ optional<pair<simp_result, bool>> simplify_core_fn::post(expr const &, optional<
return optional<pair<simp_result, bool>>();
}
simplify_core_fn::simplify_core_fn(type_context & ctx, simp_lemmas const & slss,
simplify_core_fn::simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
unsigned max_steps, bool contextual, bool lift_eq,
bool canonize_instances, bool canonize_proofs):
m_ctx(ctx), m_defeq_canonizer(m_ctx), m_slss(slss), m_max_steps(max_steps), m_contextual(contextual),
m_ctx(ctx), m_defeq_canonizer(m_ctx, dcs), m_slss(slss), m_max_steps(max_steps), m_contextual(contextual),
m_lift_eq(lift_eq), m_canonize_instances(canonize_instances), m_canonize_proofs(canonize_proofs) {
}
@ -759,11 +759,11 @@ optional<expr> simplify_core_fn::prove_by_simp(name const & rel, expr const & e)
simplify_ext_core_fn
------------------------------------ */
simplify_ext_core_fn::simplify_ext_core_fn(type_context & ctx, simp_lemmas const & slss,
simplify_ext_core_fn::simplify_ext_core_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss,
unsigned max_steps, bool contextual, bool lift_eq,
bool canonize_instances, bool canonize_proofs,
bool use_axioms):
simplify_core_fn(ctx, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs),
simplify_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs),
m_use_axioms (use_axioms) {
}
@ -951,12 +951,13 @@ class vm_simplify_fn : public simplify_ext_core_fn {
tactic_state m_s;
optional<pair<simp_result, bool>> invoke_fn(vm_obj const & fn, expr const & e, optional<expr> const & parent) {
m_s = set_mctx_lctx(m_s, m_ctx.mctx(), m_ctx.lctx());
m_s = set_mctx_lctx_dcs(m_s, m_ctx.mctx(), m_ctx.lctx(), m_defeq_canonizer.get_state());
vm_obj r = invoke(fn, m_a, to_obj(m_slss), to_obj(m_rel), to_obj(parent), to_obj(e), to_obj(m_s));
/* r : tactic_state (A × expr × option expr × bool) */
if (optional<tactic_state> new_s = is_tactic_success(r)) {
m_s = *new_s;
m_ctx.set_mctx(m_s.mctx());
m_defeq_canonizer.set_state(m_s.dcs());
vm_obj t = cfield(r, 0);
/* t : A × expr × option expr × bool */
m_a = cfield(t, 0);
@ -996,11 +997,11 @@ class vm_simplify_fn : public simplify_ext_core_fn {
}
public:
vm_simplify_fn(type_context & ctx, simp_lemmas const & slss,
vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss,
unsigned max_steps, bool contextual, bool lift_eq,
bool canonize_instances, bool canonize_proofs, bool use_axioms,
vm_obj const & prove, vm_obj const & pre, vm_obj const & post):
simplify_ext_core_fn(ctx, slss, max_steps, contextual, lift_eq,
simplify_ext_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq,
canonize_instances, canonize_proofs, use_axioms),
m_prove(prove), m_pre(pre), m_post(post),
m_s(mk_tactic_state_for(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx(), mk_true())) {}
@ -1012,10 +1013,6 @@ public:
}
};
static tactic_state update_defeq_canonizer_state(tactic_state const & s, simplify_core_fn const & f) {
return set_env(s, f.update_defeq_canonizer_state(s.env()));
}
/*
structure simplify_config :=
(max_steps : nat)
@ -1048,12 +1045,13 @@ vm_obj tactic_simplify_core(vm_obj const & c, vm_obj const & slss, vm_obj const
unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms;
get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms);
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
simplify_fn simp(ctx, to_simp_lemmas(slss), max_steps, contextual, lift_eq,
defeq_can_state dcs = s.dcs();
simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), max_steps, contextual, lift_eq,
canonize_instances, canonize_proofs, use_axioms);
simp_result result = simp(to_name(rel), to_expr(e));
if (result.get_new() != to_expr(e)) {
result = finalize(ctx, to_name(rel), result);
tactic_state new_s = update_defeq_canonizer_state(s, simp);
tactic_state new_s = set_dcs(s, dcs);
return mk_tactic_success(mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof())), new_s);
} else {
return mk_tactic_exception("simplify tactic failed to simplify", s);
@ -1070,13 +1068,14 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas
unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms;
get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms);
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
vm_simplify_fn simp(ctx, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs,
defeq_can_state dcs = s.dcs();
vm_simplify_fn simp(ctx, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs,
use_axioms, prove, pre, post);
pair<vm_obj, simp_result> p = simp(a, r, e);
if (p.second.get_new() != e) {
vm_obj const & a = p.first;
simp_result result = finalize(ctx, r, p.second);
tactic_state new_s = update_defeq_canonizer_state(s, simp);
tactic_state new_s = set_dcs(s, dcs);
return mk_tactic_success(mk_vm_pair(a, mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof()))), new_s);
} else {
return mk_tactic_exception("simplify tactic failed to simplify", s);

12
src/library/tactic/simplify.h
View file

@ -100,7 +100,7 @@ protected:
simp_result simplify(expr const & e);
public:
simplify_core_fn(type_context & ctx, simp_lemmas const & slss,
simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
unsigned max_steps, bool contextual, bool lift_eq,
bool canonize_instances, bool canonize_proofs);
@ -108,10 +108,6 @@ public:
simp_result operator()(name const & rel, expr const & e);
optional<expr> prove_by_simp(name const & rel, expr const & e);
environment update_defeq_canonizer_state(environment const & env) const {
return m_defeq_canonizer.update_state(env);
}
};
/* Extend simplify_core_fn functionality by assuming function
@ -125,7 +121,7 @@ protected:
virtual simp_result visit_pi(expr const & e) override;
virtual simp_result visit_let(expr const & e) override;
public:
simplify_ext_core_fn(type_context & ctx, simp_lemmas const & slss,
simplify_ext_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
unsigned max_steps, bool contextual, bool lift_eq,
bool canonize_instances, bool canonize_proofs, bool use_axioms);
};
@ -138,10 +134,10 @@ protected:
virtual optional<pair<simp_result, bool>> post(expr const & e, optional<expr> const & parent) override;
virtual optional<expr> prove(expr const & e) override;
public:
simplify_fn(type_context & ctx, simp_lemmas const & slss,
simplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
unsigned max_steps, bool contextual, bool lift_eq,
bool canonize_instances, bool canonize_proofs, bool use_axioms):
simplify_ext_core_fn(ctx, slss, max_steps, contextual, lift_eq,
simplify_ext_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq,
canonize_instances, canonize_proofs, use_axioms) {}
};

4
src/library/tactic/smt/congruence_closure.cpp
View file

@ -98,8 +98,8 @@ public:
MK_THREAD_LOCAL_GET_DEF(ext_congr_lemma_cache_manager, get_clcm);
congruence_closure::congruence_closure(type_context & ctx, state & s, cc_propagation_handler * phandler):
m_ctx(ctx), m_defeq_canonizer(ctx), m_state(s), m_cache_ptr(get_clcm().mk(ctx.env())), m_mode(ctx.mode()),
congruence_closure::congruence_closure(type_context & ctx, state & s, defeq_canonizer::state & dcs, cc_propagation_handler * phandler):
m_ctx(ctx), m_defeq_canonizer(ctx, dcs), m_state(s), m_cache_ptr(get_clcm().mk(ctx.env())), m_mode(ctx.mode()),
m_rel_info_getter(mk_relation_info_getter(ctx.env())),
m_symm_info_getter(mk_symm_info_getter(ctx.env())),
m_refl_info_getter(mk_refl_info_getter(ctx.env())),

7
src/library/tactic/smt/congruence_closure.h
View file

@ -256,7 +256,8 @@ private:
friend ext_congr_lemma_cache_ptr const & get_cache_ptr(congruence_closure const & cc);
public:
congruence_closure(type_context & ctx, state & s, cc_propagation_handler * phandler = nullptr);
congruence_closure(type_context & ctx, state & s, defeq_canonizer::state & dcs,
cc_propagation_handler * phandler = nullptr);
~congruence_closure();
environment const & env() const { return m_ctx.env(); }
@ -304,10 +305,6 @@ public:
entry const * get_entry(expr const & e) const { return m_state.m_entries.find(e); }
bool check_invariant() const { return m_state.check_invariant(); }
environment update_defeq_canonizer_state(environment const & env) const {
return m_defeq_canonizer.update_state(env);
}
};
typedef congruence_closure::state cc_state;

15
src/library/tactic/smt/congruence_tactics.cpp
View file

@ -21,10 +21,6 @@ Author: Leonardo de Moura
#include "library/tactic/smt/ematch.h"
namespace lean {
tactic_state update_defeq_canonizer_state(tactic_state const & s, congruence_closure const & cc) {
return set_env(s, cc.update_defeq_canonizer_state(s.env()));
}
struct vm_cc_state : public vm_external {
congruence_closure::state m_val;
vm_cc_state(congruence_closure::state const & v):m_val(v) {}
@ -88,14 +84,15 @@ vm_obj cc_state_mk_using_hs_core(vm_obj const & cfg, vm_obj const & _s) {
try {
local_context lctx = g->get_context();
type_context ctx = mk_type_context_for(s);
defeq_can_state dcs = s.dcs();
congruence_closure::state r = mk_core(cfg);
congruence_closure cc(ctx, r);
congruence_closure cc(ctx, r, dcs);
lctx.for_each([&](local_decl const & d) {
if (ctx.is_prop(d.get_type())) {
cc.add(d.get_type(), d.mk_ref());
}
});
tactic_state new_s = update_defeq_canonizer_state(s, cc);
tactic_state new_s = set_dcs(s, dcs);
return mk_tactic_success(to_obj(r), new_s);
} catch (exception & ex) {
return mk_tactic_exception(ex, s);
@ -161,14 +158,14 @@ vm_obj cc_state_inc_gmt(vm_obj const & ccs) {
try { \
type_context ctx = mk_type_context_for(s); \
congruence_closure::state S = to_cc_state(ccs); \
congruence_closure cc(ctx, S); \
defeq_can_state dcs = s.dcs(); \
congruence_closure cc(ctx, S, dcs); \
CODE \
} catch (exception & ex) { \
return mk_tactic_exception(ex, s); \
}
#define cc_state_updt_proc(CODE) cc_state_proc({ CODE; return mk_tactic_success(to_obj(S), update_defeq_canonizer_state(s, cc)); })
#define cc_state_updt_proc(CODE) cc_state_proc({ CODE; return mk_tactic_success(to_obj(S), set_dcs(s, dcs)); })
vm_obj cc_state_add(vm_obj const & ccs, vm_obj const & H, vm_obj const & _s) {
cc_state_updt_proc({

28
src/library/tactic/smt/ematch.cpp
View file

@ -623,32 +623,36 @@ vm_obj mk_ematch_result(buffer<expr_pair> const & new_inst_buffer, congruence_cl
return mk_vm_pair(new_insts, mk_vm_pair(to_obj(ccs), to_obj(ems)));
}
vm_obj ematch_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _ems, vm_obj const & hlemma, vm_obj const & t, vm_obj const & s) {
vm_obj ematch_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _ems, vm_obj const & hlemma, vm_obj const & t, vm_obj const & _s) {
tactic_state const & s = to_tactic_state(_s);
LEAN_TACTIC_TRY;
type_context ctx = mk_type_context_for(s, md);
ematch_state ems = to_ematch_state(_ems);
type_context ctx = mk_type_context_for(_s, md);
ematch_state ems = to_ematch_state(_ems);
defeq_can_state dcs = s.dcs();
congruence_closure::state ccs = to_cc_state(_ccs);
congruence_closure cc(ctx, ccs);
congruence_closure cc(ctx, ccs, dcs);
buffer<expr_pair> new_inst_buffer;
ematch(ctx, ems, cc, to_hinst_lemma(hlemma), to_expr(t), new_inst_buffer);
vm_obj r = mk_ematch_result(new_inst_buffer, ccs, ems);
tactic_state new_s = update_defeq_canonizer_state(to_tactic_state(s), cc);
tactic_state new_s = set_dcs(s, dcs);
return mk_tactic_success(r, new_s);
LEAN_TACTIC_CATCH(to_tactic_state(s));
LEAN_TACTIC_CATCH(s);
}
vm_obj ematch_all_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _ems, vm_obj const & hlemma, vm_obj const & filter, vm_obj const & s) {
vm_obj ematch_all_core(vm_obj const & md, vm_obj const & _ccs, vm_obj const & _ems, vm_obj const & hlemma, vm_obj const & filter, vm_obj const & _s) {
tactic_state const & s = to_tactic_state(_s);
LEAN_TACTIC_TRY;
type_context ctx = mk_type_context_for(s, md);
ematch_state ems = to_ematch_state(_ems);
type_context ctx = mk_type_context_for(_s, md);
ematch_state ems = to_ematch_state(_ems);
defeq_can_state dcs = s.dcs();
congruence_closure::state ccs = to_cc_state(_ccs);
congruence_closure cc(ctx, ccs);
congruence_closure cc(ctx, ccs, dcs);
buffer<expr_pair> new_inst_buffer;
ematch(ctx, ems, cc, to_hinst_lemma(hlemma), to_bool(filter), new_inst_buffer);
vm_obj r = mk_ematch_result(new_inst_buffer, ccs, ems);
tactic_state new_s = update_defeq_canonizer_state(to_tactic_state(s), cc);
tactic_state new_s = set_dcs(s, dcs);
return mk_tactic_success(r, new_s);
LEAN_TACTIC_CATCH(to_tactic_state(s));
LEAN_TACTIC_CATCH(s);
}
void initialize_ematch() {

109
src/library/tactic/smt/smt_state.cpp
View file

@ -36,10 +36,10 @@ smt_goal::smt_goal(smt_config const & cfg):
m_pre_config(cfg.m_pre_config) {
}
smt::smt(type_context & ctx, smt_goal & g):
smt::smt(type_context & ctx, defeq_can_state & dcs, smt_goal & g):
m_ctx(ctx),
m_goal(g),
m_cc(ctx, m_goal.m_cc_state, this) {
m_cc(ctx, m_goal.m_cc_state, dcs, this) {
}
smt::~smt() {
@ -147,7 +147,7 @@ tactic_state revert_all(tactic_state const & s) {
return revert(hs, s);
}
static dsimplify_fn mk_dsimp(type_context & ctx, smt_pre_config const & cfg) {
static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {
unsigned max_steps = cfg.m_max_steps;
bool visit_instances = false;
/* We use eta reduction to make sure terms such as (fun x, list x) are reduced to list.
@ -170,29 +170,27 @@ static dsimplify_fn mk_dsimp(type_context & ctx, smt_pre_config const & cfg) {
simp_lemmas_for eq_lemmas;
if (auto r = cfg.m_simp_lemmas.find(get_eq_name()))
eq_lemmas = *r;
return dsimplify_fn(ctx, max_steps, visit_instances, eq_lemmas, use_eta);
return dsimplify_fn(ctx, dcs, max_steps, visit_instances, eq_lemmas, use_eta);
}
static simplify_fn mk_simp(type_context & ctx, smt_pre_config const & cfg) {
static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {
unsigned max_steps = cfg.m_max_steps;
bool contextual = false;
bool lift_eq = true;
bool canonize_instances = true;
bool canonize_proofs = false;
bool use_axioms = true;
return simplify_fn(ctx, cfg.m_simp_lemmas, max_steps,
return simplify_fn(ctx, dcs, cfg.m_simp_lemmas, max_steps,
contextual, lift_eq, canonize_instances,
canonize_proofs, use_axioms);
}
static simp_result preprocess(type_context & ctx, smt_pre_config const & cfg, expr const & e) {
static simp_result preprocess(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg, expr const & e) {
type_context::zeta_scope _1(ctx, cfg.m_zeta);
dsimplify_fn dsimp = mk_dsimp(ctx, cfg);
dsimplify_fn dsimp = mk_dsimp(ctx, dcs, cfg);
expr new_e = dsimp(e);
ctx.set_env(dsimp.update_defeq_canonizer_state(ctx.env()));
simplify_fn simp = mk_simp(ctx, cfg);
simplify_fn simp = mk_simp(ctx, dcs, cfg);
simp_result r = simp(get_eq_name(), new_e);
ctx.set_env(simp.update_defeq_canonizer_state(ctx.env()));
return r;
}
@ -201,26 +199,27 @@ static vm_obj preprocess(tactic_state s, smt_pre_config const & cfg) {
optional<metavar_decl> g = s.get_main_goal_decl();
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
expr target = g->get_type();
simp_result r = preprocess(ctx, cfg, target);
defeq_can_state dcs = s.dcs();
simp_result r = preprocess(ctx, dcs, cfg, target);
if (!r.has_proof()) {
s = set_env(s, ctx.env());
return change(r.get_new(), s);
tactic_state new_s = set_dcs(s, dcs);
return change(r.get_new(), new_s);
} else {
expr new_M = ctx.mk_metavar_decl(ctx.lctx(), r.get_new());
expr h = mk_app(ctx, get_eq_mpr_name(), r.get_proof(), new_M);
metavar_context mctx = ctx.mctx();
mctx.assign(head(s.goals()), h);
tactic_state new_s = set_env_mctx_goals(s, ctx.env(), mctx, cons(new_M, tail(s.goals())));
tactic_state new_s = set_mctx_goals_dcs(s, mctx, cons(new_M, tail(s.goals())), dcs);
return mk_tactic_success(new_s);
}
}
expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, smt_goal & s_goal,
bool use_unused_names) {
expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar,
defeq_can_state & dcs, smt_goal & s_goal, bool use_unused_names) {
optional<metavar_decl> decl = mctx.get_metavar_decl(mvar);
lean_assert(decl);
type_context ctx(env, opts, mctx, decl->get_context(), transparency_mode::Semireducible);
smt S(ctx, s_goal);
smt S(ctx, dcs, s_goal);
expr target = decl->get_type();
type_context::tmp_locals locals(ctx);
buffer<expr> new_Hs;
@ -296,8 +295,9 @@ vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) {
metavar_context mctx = s.mctx();
bool use_unused_names = true;
expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), new_goal, use_unused_names);
s = set_mctx_goals(s, mctx, cons(new_M, tail(s.goals())));
defeq_can_state dcs = s.dcs();
expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), dcs, new_goal, use_unused_names);
s = set_mctx_goals_dcs(s, mctx, cons(new_M, tail(s.goals())), dcs);
return mk_tactic_success(mk_vm_cons(to_obj(new_goal), mk_vm_nil()), s);
}
@ -522,7 +522,8 @@ format smt_goal_to_format(smt_goal sg, tactic_state const & ts) {
type_context ctx(ts.env(), opts, mctx_tmp, lctx, transparency_mode::All);
formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
formatter fmt = fmtf(ts.env(), opts, ctx);
smt S(ctx, sg);
defeq_can_state dcs = ts.dcs();
smt S(ctx, dcs, sg);
format r;
if (S.inconsistent()) {
r = format("contradictory goal, use 'smt_tactic.close' to close this goal");
@ -599,10 +600,11 @@ vm_obj smt_tactic_close(vm_obj const & ss, vm_obj const & _ts) {
if (is_nil(ss))
return mk_smt_state_empty_exception(ts);
lean_assert(ts.goals());
expr target = ts.get_main_goal_decl()->get_type();
type_context ctx = mk_type_context_for(ts);
smt_goal g = to_smt_goal(head(ss));
smt S(ctx, g);
expr target = ts.get_main_goal_decl()->get_type();
type_context ctx = mk_type_context_for(ts);
smt_goal g = to_smt_goal(head(ss));
defeq_can_state dcs = ts.dcs();
smt S(ctx, dcs, g);
if (S.inconsistent()) {
if (auto pr = S.get_inconsistency_proof()) {
expr H = mk_false_rec(ctx, target, *pr);
@ -638,11 +640,12 @@ vm_obj smt_tactic_intros_core(vm_obj const & use_unused_names, vm_obj const & ss
ts = to_tactic_state(get_tactic_result_state(r));
metavar_context mctx = ts.mctx();
expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()), new_sgoal,
to_bool(use_unused_names));
defeq_can_state dcs = ts.dcs();
expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()),
dcs, new_sgoal, to_bool(use_unused_names));
tactic_state new_ts = set_mctx_goals(ts, mctx, cons(new_mvar, tail(ts.goals())));
vm_obj new_ss = mk_vm_cons(to_obj(new_sgoal), tail(ss));
tactic_state new_ts = set_mctx_goals_dcs(ts, mctx, cons(new_mvar, tail(ts.goals())), dcs);
vm_obj new_ss = mk_vm_cons(to_obj(new_sgoal), tail(ss));
return mk_smt_tactic_success(new_ss, new_ts);
LEAN_TACTIC_CATCH(ts);
}
@ -656,8 +659,8 @@ vm_obj smt_state_classical(vm_obj const & ss) {
return mk_vm_bool(r);
}
static expr_pair preprocess_forward(type_context & ctx, smt_pre_config const & cfg, expr const & type, expr const & h) {
simp_result r = preprocess(ctx, cfg, type);
static expr_pair preprocess_forward(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg, expr const & type, expr const & h) {
simp_result r = preprocess(ctx, dcs, cfg, type);
if (r.has_proof()) {
expr new_h = mk_eq_mp(ctx, r.get_proof(), h);
return mk_pair(r.get_new(), new_h);
@ -668,8 +671,8 @@ static expr_pair preprocess_forward(type_context & ctx, smt_pre_config const & c
}
}
static expr_pair preprocess_forward(type_context & ctx, smt_goal const & g, expr const & type, expr const & h) {
return preprocess_forward(ctx, g.get_pre_config(), type, h);
static expr_pair preprocess_forward(type_context & ctx, defeq_can_state & dcs, smt_goal const & g, expr const & type, expr const & h) {
return preprocess_forward(ctx, dcs, g.get_pre_config(), type, h);
}
vm_obj smt_tactic_ematch_core(vm_obj const & pred, vm_obj const & ss, vm_obj const & _ts) {
@ -677,10 +680,11 @@ vm_obj smt_tactic_ematch_core(vm_obj const & pred, vm_obj const & ss, vm_obj con
if (is_nil(ss)) return mk_smt_state_empty_exception(ts);
lean_assert(ts.goals());
LEAN_TACTIC_TRY;
expr target = ts.get_main_goal_decl()->get_type();
type_context ctx = mk_type_context_for(ts);
smt_goal g = to_smt_goal(head(ss));
smt S(ctx, g);
expr target = ts.get_main_goal_decl()->get_type();
type_context ctx = mk_type_context_for(ts);
defeq_can_state dcs = ts.dcs();
smt_goal g = to_smt_goal(head(ss));
smt S(ctx, dcs, g);
S.internalize(target);
buffer<expr_pair> new_instances;
S.ematch(new_instances);
@ -691,14 +695,14 @@ vm_obj smt_tactic_ematch_core(vm_obj const & pred, vm_obj const & ss, vm_obj con
expr proof = p.second;
vm_obj keep = invoke(pred, to_obj(type));
if (to_bool(keep)) {
std::tie(type, proof) = preprocess_forward(ctx, g, type, proof);
std::tie(type, proof) = preprocess_forward(ctx, dcs, g, type, proof);
lean_trace(name({"smt", "ematch"}), scope_trace_env _(ctx.env(), ctx);
tout() << "new instance\n" << type << "\n";);
S.add(type, proof);
}
}
vm_obj new_ss = mk_vm_cons(to_obj(g), tail(ss));
tactic_state new_ts = set_env_mctx(ts, ctx.env(), ctx.mctx());
tactic_state new_ts = set_mctx_dcs(ts, ctx.mctx(), dcs);
return mk_smt_tactic_success(new_ss, new_ts);
LEAN_TACTIC_CATCH(ts);
}
@ -750,9 +754,10 @@ vm_obj smt_tactic_preprocess(vm_obj const & e, vm_obj const & ss, vm_obj const &
LEAN_TACTIC_TRY;
type_context ctx = mk_type_context_for(ts);
smt_goal g = to_smt_goal(head(ss));
simp_result r = preprocess(ctx, g.get_pre_config(), to_expr(e));
defeq_can_state dcs = ts.dcs();
simp_result r = preprocess(ctx, dcs, g.get_pre_config(), to_expr(e));
r = finalize(ctx, get_eq_name(), r);
tactic_state new_ts = set_env_mctx(ts, ctx.env(), ctx.mctx());
tactic_state new_ts = set_mctx_dcs(ts, ctx.mctx(), dcs);
return mk_smt_tactic_success(mk_vm_pair(to_obj(r.get_new()), to_obj(r.get_proof())), ss, to_obj(new_ts));
LEAN_TACTIC_CATCH(ts);
}
@ -780,13 +785,14 @@ vm_obj smt_tactic_add_lemmas(vm_obj const & lemmas, vm_obj const & ss, vm_obj co
tactic_state ts = to_tactic_state(_ts);
if (is_nil(ss)) return mk_smt_state_empty_exception(ts);
type_context ctx = mk_type_context_for(ts);
defeq_can_state dcs = ts.dcs();
smt_goal g = to_smt_goal(head(ss));
smt S(ctx, g);
smt S(ctx, dcs, g);
to_hinst_lemmas(lemmas).for_each([&](hinst_lemma const & lemma) {
if (lemma.m_num_mvars == 0 && lemma.m_num_uvars == 0) {
expr type = lemma.m_prop;
expr h = lemma.m_proof;
std::tie(type, h) = preprocess_forward(ctx, g, type, h);
std::tie(type, h) = preprocess_forward(ctx, dcs, g, type, h);
lean_trace(name({"smt", "ematch"}), scope_trace_env _(ctx.env(), ctx);
tout() << "new ground fact: " << type << "\n";);
S.add(type, h);
@ -797,7 +803,7 @@ vm_obj smt_tactic_add_lemmas(vm_obj const & lemmas, vm_obj const & ss, vm_obj co
}
});
vm_obj new_ss = mk_vm_cons(to_obj(g), tail(ss));
tactic_state new_ts = set_env_mctx(ts, ctx.env(), ctx.mctx());
tactic_state new_ts = set_mctx_dcs(ts, ctx.mctx(), dcs);
return mk_smt_tactic_success(new_ss, new_ts);
}
@ -806,17 +812,18 @@ vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj cons
if (is_nil(ss)) return mk_smt_state_empty_exception(ts);
lean_assert(ts.goals());
LEAN_TACTIC_TRY;
expr target = ts.get_main_goal_decl()->get_type();
type_context ctx = mk_type_context_for(ts);
smt_goal g = to_smt_goal(head(ss));
smt S(ctx, g);
expr target = ts.get_main_goal_decl()->get_type();
type_context ctx = mk_type_context_for(ts);
defeq_can_state dcs = ts.dcs();
smt_goal g = to_smt_goal(head(ss));
smt S(ctx, dcs, g);
S.internalize(target);
buffer<expr_pair> new_instances;
to_hinst_lemmas(hs).for_each([&](hinst_lemma const & lemma) {
if (lemma.m_num_mvars == 0 && lemma.m_num_uvars == 0) {
expr type = lemma.m_prop;
expr h = lemma.m_proof;
std::tie(type, h) = preprocess_forward(ctx, g, type, h);
std::tie(type, h) = preprocess_forward(ctx, dcs, g, type, h);
lean_trace(name({"smt", "ematch"}), scope_trace_env _(ctx.env(), ctx);
tout() << "new ground fact: " << type << "\n";);
S.add(type, h);
@ -829,13 +836,13 @@ vm_obj smt_tactic_ematch_using(vm_obj const & hs, vm_obj const & ss, vm_obj cons
for (expr_pair const & p : new_instances) {
expr type = p.first;
expr proof = p.second;
std::tie(type, proof) = preprocess_forward(ctx, g, type, proof);
std::tie(type, proof) = preprocess_forward(ctx, dcs, g, type, proof);
lean_trace(name({"smt", "ematch"}), scope_trace_env _(ctx.env(), ctx);
tout() << "new instance\n" << type << "\n";);
S.add(type, proof);
}
vm_obj new_ss = mk_vm_cons(to_obj(g), tail(ss));
tactic_state new_ts = set_env_mctx(ts, ctx.env(), ctx.mctx());
tactic_state new_ts = set_mctx_dcs(ts, ctx.mctx(), dcs);
return mk_smt_tactic_success(new_ss, new_ts);
LEAN_TACTIC_CATCH(ts);
}

2
src/library/tactic/smt/smt_state.h
View file

@ -53,7 +53,7 @@ private:
virtual void propagated(unsigned n, expr const * p) override;
public:
smt(type_context & ctx, smt_goal & g);
smt(type_context & ctx, defeq_can_state & dcs, smt_goal & g);
virtual ~smt();
void internalize(expr const & e);

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(env, opts, mctx, to_list(MVAR), 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, 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";)
lean_subst_trace_state(mvar, "initial:\n");
lean_assert(mctx.get_metavar_decl(mvar));

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

@ -49,8 +49,8 @@ void tactic_state_cell::dealloc() {
}
tactic_state::tactic_state(environment const & env, options const & o, metavar_context const & ctx,
list<expr> const & gs, expr const & main) {
m_ptr = new tactic_state_cell(env, o, ctx, gs, main);
list<expr> const & gs, expr const & main, defeq_canonizer::state const & dcs) {
m_ptr = new tactic_state_cell(env, o, ctx, gs, main, dcs);
m_ptr->inc_ref();
}
@ -64,10 +64,9 @@ optional<metavar_decl> tactic_state::get_main_goal_decl() const {
return mctx().get_metavar_decl(head(goals()));
}
tactic_state mk_tactic_state_for(environment const & env, options const & o, metavar_context mctx,
local_context const & lctx, expr const & type) {
tactic_state mk_tactic_state_for(environment const & env, options const & o, metavar_context mctx, local_context const & lctx, expr const & type) {
expr main = mctx.mk_metavar_decl(lctx, type);
return tactic_state(env, o, mctx, list<expr>(main), main);
return tactic_state(env, o, mctx, list<expr>(main), main, defeq_canonizer::state());
}
tactic_state mk_tactic_state_for(environment const & env, options const & o, local_context const & lctx, expr const & type) {
@ -75,20 +74,30 @@ tactic_state mk_tactic_state_for(environment const & env, options const & o, loc
return mk_tactic_state_for(env, o, mctx, lctx, type);
}
tactic_state mk_tactic_state_for_metavar(environment const & env, options const & opts, metavar_context const & mctx, expr const & mvar) {
return tactic_state(env, opts, mctx, list<expr>(mvar), mvar, defeq_canonizer::state());
}
tactic_state set_options(tactic_state const & s, options const & o) {
return tactic_state(s.env(), o, s.mctx(), s.goals(), s.main());
return tactic_state(s.env(), o, s.mctx(), s.goals(), s.main(), s.dcs());
}
tactic_state set_env(tactic_state const & s, environment const & env) {
return tactic_state(env, s.get_options(), s.mctx(), s.goals(), s.main());
return tactic_state(env, s.get_options(), s.mctx(), s.goals(), s.main(), s.dcs());
}
tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx) {
return tactic_state(s.env(), s.get_options(), mctx, s.goals(), s.main());
if (is_eqp(s.mctx(), mctx)) return s;
return tactic_state(s.env(), s.get_options(), mctx, s.goals(), s.main(), s.dcs());
}
tactic_state set_mctx_dcs(tactic_state const & s, metavar_context const & mctx, defeq_can_state const & dcs) {
if (is_eqp(s.mctx(), mctx) && is_eqp(s.dcs(), dcs)) return s;
return tactic_state(s.env(), s.get_options(), mctx, s.goals(), s.main(), dcs);
}
tactic_state set_env_mctx(tactic_state const & s, environment const & env, metavar_context const & mctx) {
return tactic_state(env, s.get_options(), mctx, s.goals(), s.main());
return tactic_state(env, s.get_options(), mctx, s.goals(), s.main(), s.dcs());
}
static list<expr> consume_solved_prefix(metavar_context const & mctx, list<expr> const & gs) {
@ -101,27 +110,40 @@ static list<expr> consume_solved_prefix(metavar_context const & mctx, list<expr>
}
tactic_state set_goals(tactic_state const & s, list<expr> const & gs) {
return tactic_state(s.env(), s.get_options(), s.mctx(), consume_solved_prefix(s.mctx(), gs), s.main());
return tactic_state(s.env(), s.get_options(), s.mctx(), consume_solved_prefix(s.mctx(), gs), s.main(), s.dcs());
}
tactic_state set_mctx_goals_dcs(tactic_state const & s, metavar_context const & mctx, list<expr> const & gs, defeq_can_state const & dcs) {
return tactic_state(s.env(), s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main(), dcs);
}
tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list<expr> const & gs) {
return tactic_state(s.env(), s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main());
return set_mctx_goals_dcs(s, mctx, gs, s.dcs());
}
tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env,
metavar_context const & mctx, list<expr> const & gs) {
return tactic_state(env, s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main());
return tactic_state(env, s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main(), s.dcs());
}
tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, local_context const & lctx) {
if (is_eqp(s.mctx(), mctx)) {
tactic_state set_mctx_lctx_dcs(tactic_state const & s, metavar_context const & mctx, local_context const & lctx, defeq_can_state const & dcs) {
if (is_eqp(s.mctx(), mctx) && is_eqp(s.dcs(), dcs)) {
optional<metavar_decl> mdecl = s.get_main_goal_decl();
if (mdecl && is_decl_eqp(mdecl->get_context(), lctx))
return s;
}
metavar_context new_mctx = mctx;
expr mvar = new_mctx.mk_metavar_decl(lctx, mk_true());
return tactic_state(s.env(), s.get_options(), new_mctx, to_list(mvar), mvar);
return tactic_state(s.env(), s.get_options(), new_mctx, to_list(mvar), mvar, s.dcs());
}
tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, local_context const & lctx) {
return set_mctx_lctx_dcs(s, mctx, lctx, s.dcs());
}
tactic_state set_defeq_can_state(tactic_state const & s, defeq_can_state const & dcs) {
if (is_eqp(s.dcs(), dcs)) return s;
return tactic_state(s.env(), s.get_options(), s.mctx(), s.goals(), s.main(), dcs);
}
format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) const {

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

@ -10,9 +10,12 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "library/metavar_context.h"
#include "library/type_context.h"
#include "library/defeq_canonizer.h"
#include "library/vm/vm.h"
namespace lean {
typedef defeq_canonizer::state defeq_can_state;
class tactic_state_cell {
MK_LEAN_RC();
environment m_env;
@ -20,12 +23,13 @@ class tactic_state_cell {
metavar_context m_mctx;
list<expr> m_goals;
expr m_main;
defeq_can_state m_defeq_can_state;
friend class tactic_state;
void dealloc();
public:
tactic_state_cell(environment const & env, options const & o, metavar_context const & ctx, list<expr> const & gs,
expr const & main):
m_rc(0), m_env(env), m_options(o), m_mctx(ctx), m_goals(gs), m_main(main) {}
expr const & main, defeq_can_state const & s):
m_rc(0), m_env(env), m_options(o), m_mctx(ctx), m_goals(gs), m_main(main), m_defeq_can_state(s) {}
};
class tactic_state {
@ -38,7 +42,7 @@ private:
format pp_goal(formatter_factory const & fmtf, expr const & g) const;
public:
tactic_state(environment const & env, options const & o, metavar_context const & ctx, list<expr> const & gs,
expr const & main);
expr const & main, defeq_can_state const & s);
tactic_state(tactic_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
tactic_state(tactic_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
~tactic_state() { if (m_ptr) m_ptr->dec_ref(); }
@ -51,6 +55,8 @@ public:
metavar_context const & mctx() const { lean_assert(m_ptr); return m_ptr->m_mctx; }
list<expr> const & goals() const { lean_assert(m_ptr); return m_ptr->m_goals; }
expr const & main() const { lean_assert(m_ptr); return m_ptr->m_main; }
defeq_can_state const & get_defeq_canonizer_state() const { return m_ptr->m_defeq_can_state; }
defeq_can_state const & dcs() const { return get_defeq_canonizer_state(); }
tactic_state & operator=(tactic_state const & s) { LEAN_COPY_REF(s); }
tactic_state & operator=(tactic_state && s) { LEAN_MOVE_REF(s); }
@ -78,14 +84,21 @@ tactic_state mk_tactic_state_for(environment const & env, options const & opts,
local_context const & lctx, expr const & type);
tactic_state mk_tactic_state_for(environment const & env, options const & opts,
local_context const & lctx, expr const & type);
tactic_state mk_tactic_state_for_metavar(environment const & env, options const & opts, metavar_context const & mctx, expr const & mvar);
tactic_state set_options(tactic_state const & s, options const & o);
tactic_state set_env(tactic_state const & s, environment const & env);
tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx);
tactic_state set_mctx_dcs(tactic_state const & s, metavar_context const & mctx, defeq_can_state const & dcs);
tactic_state set_env_mctx(tactic_state const & s, environment const & env, metavar_context const & mctx);
tactic_state set_goals(tactic_state const & s, list<expr> const & gs);
tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list<expr> const & gs);
tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env, metavar_context const & mctx, list<expr> const & gs);
tactic_state set_mctx_goals_dcs(tactic_state const & s, metavar_context const & mctx, list<expr> const & gs, defeq_can_state const & dcs);
tactic_state set_defeq_can_state(tactic_state const & s, defeq_can_state const & dcs);
inline tactic_state set_dcs(tactic_state const & s, defeq_can_state const & dcs) { return set_defeq_can_state(s, dcs); }
/* Auxiliary function that returns an updated tactic_state such s' s.t. the metavariable context is mctx and
the main goal is of the form
@ -97,6 +110,7 @@ tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env,
\remark It returns s is is_eqp(s.mctx(), mctx) and is_decl_eqp(s.get_main_goal_decl()->get_context(), lctx) */
tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, local_context const & lctx);
tactic_state set_mctx_lctx_dcs(tactic_state const & s, metavar_context const & mctx, local_context const & lctx, defeq_can_state const & dcs);
template<typename T> tactic_state update_option_if_undef(tactic_state const & s, name const & n, T v) {
return set_options(s, s.get_options().update_if_undef(n, v));
}

31
tests/lean/run/heap.lean Normal file
View file

@ -0,0 +1,31 @@
constant heap : Type
constant ptr : Type
constant val : Type
constant pt : ptr → val → heap
constant hunion : heap → heap → heap
constant is_def : heap → Prop
infix `∙`:60 := hunion
infix `↣`:70 := pt
/-
constant hunion_is_assoc : is_associative heap hunion
constant hunion_is_comm : is_commutative heap hunion
attribute [instance] hunion_is_comm hunion_is_assoc
axiom noalias : ∀ (h : heap) (y₁ y₂ : ptr) (w₁ w₂ : val), is_def (h ∙ y₁ ↣ w₁ ∙ y₂ ↣ w₂) → y₁ ≠ y₂
-/
set_option profiler true
lemma ex
(h₁ h₂ : heap) (x₁ x₂ x₃ x₄ : ptr) (v₁ v₂ v₃ : val)
(hcomm : ∀ x y, x ∙ y = y ∙ x)
(hassoc : ∀ x y z, (x ∙ y) ∙ z = x ∙ (y ∙ z))
(hnoalias : ∀ h y₁ y₂ w₁ w₂, is_def (h ∙ y₁ ↣ w₁ ∙ y₂ ↣ w₂) → y₁ ≠ y₂)
: is_def (h₁ ∙ (x₁ ↣ v₁ ∙ x₂ ↣ v₂) ∙ h₂ ∙ (x₃ ↣ v₃)) → x₁ ≠ x₃ ∧ x₁ ≠ x₂ ∧ x₂ ≠ x₃ :=
begin [smt]
smt_tactic.add_lemmas_from_facts,
repeat {ematch}
end