diff --git a/src/frontends/smt2/parser.cpp b/src/frontends/smt2/parser.cpp index 7e3fb3725e..3d8328bb32 100644 --- a/src/frontends/smt2/parser.cpp +++ b/src/frontends/smt2/parser.cpp @@ -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(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); diff --git a/src/library/defeq_canonizer.cpp b/src/library/defeq_canonizer.cpp index c83ad790f0..972c0caf83 100644 --- a/src/library/defeq_canonizer.cpp +++ b/src/library/defeq_canonizer.cpp @@ -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()); } -}; - -static defeq_canonizer_ext_reg * g_ext = nullptr; -static defeq_canonizer_ext const & get_extension(environment const & env) { - return static_cast(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(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 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); -} } diff --git a/src/library/defeq_canonizer.h b/src/library/defeq_canonizer.h index 26b173038c..a04222d0b5 100644 --- a/src/library/defeq_canonizer.h +++ b/src/library/defeq_canonizer.h @@ -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 m_C; + rb_expr_map 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> m_M; + name_map> m_M; }; private: type_context & m_ctx; - state m_state; + state & m_state; bool * m_updated{nullptr}; optional 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(); } diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 4079a5c0e8..26c132bdf9 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -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) { diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 4693edab00..ea91bd0b47 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -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); } diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index e451dc9cf8..b34e1606ac 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -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> dsimplify_fn::post(expr const & e) { return optional>(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> 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 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::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::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::max()), + dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits::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); } } diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h index 91cf0702f5..4f152178d2 100644 --- a/src/library/tactic/dsimplify.h +++ b/src/library/tactic/dsimplify.h @@ -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> pre(expr const & e) override; virtual optional> 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(); diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index e273c21433..b704f06ca3 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -701,10 +701,10 @@ optional> simplify_core_fn::post(expr const &, optional< return optional>(); } -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 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> invoke_fn(vm_obj const & fn, expr const & e, optional 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 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 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); diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h index c7f2831228..c04c16be7a 100644 --- a/src/library/tactic/simplify.h +++ b/src/library/tactic/simplify.h @@ -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 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> post(expr const & e, optional const & parent) override; virtual optional 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) {} }; diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp index fe08523f28..22d3ed9924 100644 --- a/src/library/tactic/smt/congruence_closure.cpp +++ b/src/library/tactic/smt/congruence_closure.cpp @@ -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())), diff --git a/src/library/tactic/smt/congruence_closure.h b/src/library/tactic/smt/congruence_closure.h index 6d51fef1ae..e5f04a27d6 100644 --- a/src/library/tactic/smt/congruence_closure.h +++ b/src/library/tactic/smt/congruence_closure.h @@ -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; diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp index e063ce693d..8d175a461a 100644 --- a/src/library/tactic/smt/congruence_tactics.cpp +++ b/src/library/tactic/smt/congruence_tactics.cpp @@ -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({ diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp index b0cddb0c27..e4f990afbe 100644 --- a/src/library/tactic/smt/ematch.cpp +++ b/src/library/tactic/smt/ematch.cpp @@ -623,32 +623,36 @@ vm_obj mk_ematch_result(buffer 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 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 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() { diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index eaf8acf55c..a944b25c21 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -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 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 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 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 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 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); } diff --git a/src/library/tactic/smt/smt_state.h b/src/library/tactic/smt/smt_state.h index 67b4a7b1ee..c6bba772a4 100644 --- a/src/library/tactic/smt/smt_state.h +++ b/src/library/tactic/smt/smt_state.h @@ -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); diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index bba1815d3c..db2ed1b291 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(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)); diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 6b0c7a5e57..6a9bca7525 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -49,8 +49,8 @@ void tactic_state_cell::dealloc() { } tactic_state::tactic_state(environment const & env, options const & o, metavar_context const & ctx, - list const & gs, expr const & main) { - m_ptr = new tactic_state_cell(env, o, ctx, gs, main); + list 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 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(main), main); + return tactic_state(env, o, mctx, list(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(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 consume_solved_prefix(metavar_context const & mctx, list const & gs) { @@ -101,27 +110,40 @@ static list consume_solved_prefix(metavar_context const & mctx, list } tactic_state set_goals(tactic_state const & s, list 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 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 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 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 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 { diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index f9cbcdc55e..afd41c9193 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -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 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 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 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 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 const & gs); tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list const & gs); tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env, metavar_context const & mctx, list const & gs); +tactic_state set_mctx_goals_dcs(tactic_state const & s, metavar_context const & mctx, list 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 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)); } diff --git a/tests/lean/run/heap.lean b/tests/lean/run/heap.lean new file mode 100644 index 0000000000..f86b2b5f68 --- /dev/null +++ b/tests/lean/run/heap.lean @@ -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