From c23528b5d86658bba270df1e2c5dd4d2b02744ef Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 26 Feb 2016 21:10:13 -0800 Subject: [PATCH] feat(library/blast/blast): use defeq_simplifier to normalize --- library/init/logic.lean | 3 + src/frontends/lean/builtin_cmds.cpp | 4 +- src/library/blast/blast.cpp | 157 +++++++++++++++++- src/library/blast/blast.h | 6 +- src/library/defeq_simp_lemmas.cpp | 7 +- src/library/defeq_simplifier.cpp | 101 ++++++----- src/library/defeq_simplifier.h | 3 +- src/library/tmp_type_context.h | 20 +++ src/library/type_context.cpp | 3 +- src/library/type_context.h | 1 + tests/lean/defeq_simp_lemmas1.lean | 4 +- .../lean/defeq_simp_lemmas1.lean.expected.out | 4 +- tests/lean/defeq_simp_lemmas2.lean | 8 +- .../lean/defeq_simp_lemmas2.lean.expected.out | 18 +- 14 files changed, 260 insertions(+), 79 deletions(-) diff --git a/library/init/logic.lean b/library/init/logic.lean index a33f62365..947bd4e4a 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -53,6 +53,8 @@ false.rec c H notation a = b := eq a b definition rfl {A : Type} {a : A} : a = a := eq.refl a +definition id.def [defeq] {A : Type} (a : A) : id a = a := rfl + -- proof irrelevance is built in theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ := rfl @@ -142,6 +144,7 @@ rfl /- ne -/ definition ne [reducible] {A : Type} (a b : A) := ¬(a = b) +definition ne.def [defeq] {A : Type} (a b : A) : ne a b = ¬ (a = b) := rfl notation a ≠ b := ne a b namespace ne diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 42ab8fe96..559e668f3 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -574,8 +574,8 @@ static environment defeq_simplify_cmd(parser & p) { std::tie(e, ls) = parse_local_expr(p); auto tc = mk_type_checker(p.env()); - - expr e_simp = defeq_simplify(env, p.get_options(), sls, e); + default_tmp_type_context_pool pool(p.env(), p.get_options()); + expr e_simp = defeq_simplify(pool, p.get_options(), sls, e); if (!tc->is_def_eq(e, e_simp).first) { throw parser_error("defeq_simplify result not definitionally equal to input expression", pos); } diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index e7a730553..86f99daad 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -10,9 +10,13 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "kernel/find_fn.h" #include "kernel/replace_fn.h" +#include "kernel/instantiate.h" +#include "kernel/abstract.h" #include "kernel/type_checker.h" #include "library/replace_visitor.h" #include "library/util.h" +#include "library/defeq_simp_lemmas.h" +#include "library/defeq_simplifier.h" #include "library/trace.h" #include "library/reducible.h" #include "library/class.h" @@ -21,6 +25,7 @@ Author: Leonardo de Moura #include "library/relation_manager.h" #include "library/congr_lemma_manager.h" #include "library/abstract_expr_manager.h" +#include "library/proof_irrel_expr_manager.h" #include "library/light_lt_manager.h" #include "library/projection.h" #include "library/scoped_ext.h" @@ -67,6 +72,15 @@ struct imp_extension_entry { m_ext_state(ext_state), m_ext_id(ext_id), m_ext_of_ext_state(ext_of_ext_state) {} }; +unsigned proof_irrel_hash(expr const & e); +bool proof_irrel_is_equal(expr const & e1, expr const & e2); + +class tmp_tctx_pool : public tmp_type_context_pool { +public: + virtual tmp_type_context * mk_tmp_type_context() override; + virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override; +}; + class blastenv { friend class scope_assignment; friend class scope_unfold_macro_pred; @@ -103,6 +117,7 @@ class blastenv { fun_info_manager m_fun_info_manager; congr_lemma_manager m_congr_lemma_manager; abstract_expr_manager m_abstract_expr_manager; + proof_irrel_expr_manager m_proof_irrel_expr_manager; light_lt_manager m_light_lt_manager; imp_extension_entries m_imp_extension_entries; relation_info_getter m_rel_getter; @@ -517,8 +532,34 @@ class blastenv { } tctx m_tctx; + + /* Normalizing instances */ normalizer m_normalizer; - expr_map m_norm_cache; // normalization cache + + struct inst_key { + expr m_e; + unsigned m_hash; + + inst_key(expr const & e): + m_e(e), m_hash(blast::proof_irrel_hash(e)) { } + }; + + struct inst_key_hash_fn { + unsigned operator()(inst_key const & k) const { return k.m_hash; } + }; + + struct inst_key_eq_fn { + bool operator()(inst_key const & k1, inst_key const & k2) const { + return blast::proof_irrel_is_equal(k1.m_e, k2.m_e); + } + }; + + typedef std::unordered_map inst_cache; + inst_cache m_inst_nf_to_cf; + expr_map m_inst_to_nf; + + expr_map m_norm_cache; // normalization cache + void save_initial_context() { hypothesis_idx_buffer hidxs; @@ -528,6 +569,8 @@ class blastenv { ctx.push_back(mk_href(hidx)); } m_initial_context = to_list(ctx); + for (auto ctx : m_tmp_ctx_pool) delete ctx; + m_tmp_ctx_pool.clear(); } name_map mk_uref2uvar() const { @@ -636,6 +679,7 @@ public: m_fun_info_manager(*m_tmp_ctx), m_congr_lemma_manager(m_app_builder, m_fun_info_manager), m_abstract_expr_manager(m_congr_lemma_manager), + m_proof_irrel_expr_manager(m_fun_info_manager), m_light_lt_manager(env), m_rel_getter(mk_relation_info_getter(env)), m_refl_getter(mk_refl_info_getter(env)), @@ -709,6 +753,10 @@ public: return m_projection_info.find(n); } + unfold_macro_pred get_unfold_macro_pred() const { + return m_unfold_macro_pred; + } + expr mk_fresh_local(expr const & type, binder_info const & bi) { return m_tctx.mk_tmp_local(type, bi); } @@ -793,6 +841,10 @@ public: return m_abstract_expr_manager.hash(e); } + unsigned proof_irrel_hash(expr const & e) { + return m_proof_irrel_expr_manager.hash(e); + } + void init_imp_extension_entries() { for (auto & p : get_imp_extension_manager().get_entries()) { branch_extension & b_ext = curr_state().get_extension(p.second); @@ -849,6 +901,10 @@ public: return m_abstract_expr_manager.is_equal(e1, e2); } + bool proof_irrel_is_equal(expr const & e1, expr const & e2) { + return m_proof_irrel_expr_manager.is_equal(e1, e2); + } + bool is_light_lt(expr const & e1, expr const & e2) { return m_light_lt_manager.is_lt(e1, e2); } @@ -870,11 +926,74 @@ public: return m_tctx; } + expr normalize_instance(expr const & inst) { + auto it1 = m_inst_to_nf.find(inst); + expr inst_nf; + if (it1 != m_inst_to_nf.end()) { + inst_nf = it1->second; + } else { + inst_nf = m_normalizer(inst); + m_inst_to_nf.insert(mk_pair(inst, inst_nf)); + } + + auto it2 = m_inst_nf_to_cf.find(inst_nf); + expr inst_cf; + if (it2 != m_inst_nf_to_cf.end()) { + inst_cf = it2->second; + } else { + inst_cf = inst; + m_inst_nf_to_cf.insert(mk_pair(inst_nf, inst_cf)); + } + lean_trace(name({"debug", "blast", "inst_cache"}), + tout() << "\n" << inst << "\n==>\n" << inst_nf << "\n==>\n" << inst_cf << "\n";); + return inst_cf; + } + + expr normalize_instances(expr const & e) { + expr b, l, d; + switch (e.kind()) { + case expr_kind::Constant: + case expr_kind::Local: + case expr_kind::Meta: + case expr_kind::Sort: + case expr_kind::Var: + case expr_kind::Macro: + return e; + case expr_kind::Lambda: + case expr_kind::Pi: + d = normalize_instances(binding_domain(e)); + l = mk_fresh_local(d, binding_info(e)); + b = abstract(normalize_instances(instantiate(binding_body(e), l)), l); + return update_binding(e, d, b); + case expr_kind::App: + buffer args; + expr const & f = get_app_args(e, args); + unsigned prefix_sz = get_specialization_prefix_size(f, args.size()); + expr new_f = e; + unsigned rest_sz = args.size() - prefix_sz; + for (unsigned i = 0; i < rest_sz; i++) + new_f = app_fn(new_f); + fun_info info = get_fun_info(new_f, rest_sz); + lean_assert(length(info.get_params_info()) == rest_sz); + unsigned i = prefix_sz; + for_each(info.get_params_info(), [&](param_info const & p_info) { + if (p_info.is_inst_implicit()) { + args[i] = normalize_instance(args[i]); + } else { + args[i] = normalize_instances(args[i]); + } + i++; + }); + return mk_app(f, args); + } + lean_unreachable(); + } + expr normalize(expr const & e) { auto it = m_norm_cache.find(e); - if (it != m_norm_cache.end()) - return it->second; - expr r = m_normalizer(e); + if (it != m_norm_cache.end()) return it->second; + tmp_tctx_pool pool; + expr r = normalize_instances(defeq_simplify(pool, m_ios.get_options(), get_defeq_simp_lemmas(m_env), e)); m_norm_cache.insert(mk_pair(e, r)); return r; } @@ -1114,6 +1233,11 @@ optional mk_subsingleton_instance(expr const & type) { return g_blastenv->mk_subsingleton_instance(type); } +unfold_macro_pred get_unfold_macro_pred() { + lean_assert(g_blastenv); + return g_blastenv->get_unfold_macro_pred(); +} + expr mk_fresh_local(expr const & type, binder_info const & bi) { lean_assert(g_blastenv); return g_blastenv->mk_fresh_local(type, bi); @@ -1194,6 +1318,11 @@ unsigned abstract_hash(expr const & e) { return g_blastenv->abstract_hash(e); } +unsigned proof_irrel_hash(expr const & e) { + lean_assert(g_blastenv); + return g_blastenv->proof_irrel_hash(e); +} + unsigned register_imp_extension(std::function & ext_state_maker) { return get_imp_extension_manager().register_imp_extension(ext_state_maker); } @@ -1208,6 +1337,11 @@ bool abstract_is_equal(expr const & e1, expr const & e2) { return g_blastenv->abstract_is_equal(e1, e2); } +bool proof_irrel_is_equal(expr const & e1, expr const & e2) { + lean_assert(g_blastenv); + return g_blastenv->proof_irrel_is_equal(e1, e2); +} + bool is_light_lt(expr const & e1, expr const & e2) { lean_assert(g_blastenv); return g_blastenv->is_light_lt(e1, e2); @@ -1313,6 +1447,10 @@ public: tmp_tctx(environment const & env, options const & o): tmp_type_context(env, o) {} + virtual bool should_unfold_macro(expr const & e) const override { + return get_unfold_macro_pred()(e); + } + /** \brief Return the type of a local constant (local or not). \remark This method allows the customer to store the type of local constants in a different place. */ @@ -1358,6 +1496,16 @@ tmp_type_context * blastenv::mk_tmp_type_context() { return r; } +tmp_type_context * tmp_tctx_pool::mk_tmp_type_context() { + lean_assert(g_blastenv); + return g_blastenv->mk_tmp_type_context(); +} + +void tmp_tctx_pool::recycle_tmp_type_context(tmp_type_context * tmp_tctx) { + lean_assert(g_blastenv); + g_blastenv->recycle_tmp_type_context(tmp_tctx); +} + blast_tmp_type_context::blast_tmp_type_context(unsigned num_umeta, unsigned num_emeta) { lean_assert(g_blastenv); m_ctx = g_blastenv->mk_tmp_type_context(); @@ -1400,6 +1548,7 @@ void initialize_blast() { register_trace_class(name{"blast", "search"}); register_trace_class(name{"blast", "deadend"}); register_trace_class(name{"debug", "blast"}); + register_trace_class(name{"debug", "blast", "inst_cache"}); register_trace_class_alias("app_builder", name({"blast", "event"})); register_trace_class_alias(name({"simplifier", "failure"}), name({"blast", "event"})); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index 8679fbc47..683f61ab3 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -168,10 +168,14 @@ fun_info get_specialized_fun_info(expr const & a); /** \brief Return the given function specialization prefix size. */ unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs); -/** \brief Hash and equality test for abstract expressions */ +/** \brief Hash and equality test that ignore subsingleton arguments */ unsigned abstract_hash(expr const & e); bool abstract_is_equal(expr const & e1, expr const & e2); +/** \brief Hash and equality test that ignore arguments that are proofs */ +unsigned proof_irrel_hash(expr const & e); +bool proof_irrel_is_equal(expr const & e1, expr const & e2); + /** \brief Order on expressions that supports the "light" annotation */ bool is_light_lt(expr const & e1, expr const & e2); diff --git a/src/library/defeq_simp_lemmas.cpp b/src/library/defeq_simp_lemmas.cpp index 85d3765bb..84c18d21e 100644 --- a/src/library/defeq_simp_lemmas.cpp +++ b/src/library/defeq_simp_lemmas.cpp @@ -129,10 +129,11 @@ defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env) { } defeq_simp_lemmas get_defeq_simp_lemmas(environment const & env, name const & ns) { - list const * entries = defeq_simp_lemmas_ext::get_entries(env, ns); + list const * _entries = defeq_simp_lemmas_ext::get_entries(env, ns); defeq_simp_lemmas_state s; - if (entries) { - for (auto const & e : *entries) { + if (_entries) { + list entries = reverse(*_entries); + for (auto const & e : entries) { tmp_type_context tctx(env, get_dummy_ios().get_options()); s.register_defeq_simp_lemma(tctx, e.m_decl_name, e.m_priority); } diff --git a/src/library/defeq_simplifier.cpp b/src/library/defeq_simplifier.cpp index 419bca33e..1d648558b 100644 --- a/src/library/defeq_simplifier.cpp +++ b/src/library/defeq_simplifier.cpp @@ -15,10 +15,10 @@ Author: Daniel Selsam #include "library/normalize.h" #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS -#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 1000 +#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS 5000 #endif #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS -#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS 1000 +#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_REWRITE_ROUNDS 5000 #endif #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN #define LEAN_DEFAULT_DEFEQ_SIMPLIFY_TOP_DOWN false @@ -29,9 +29,6 @@ Author: Daniel Selsam #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE #define LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE true #endif -#ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS -#define LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS false -#endif namespace lean { @@ -42,7 +39,6 @@ static name * g_simplify_max_rewrite_rounds = nullptr; static name * g_simplify_top_down = nullptr; static name * g_simplify_exhaustive = nullptr; static name * g_simplify_memoize = nullptr; -static name * g_simplify_expand_macros = nullptr; static unsigned get_simplify_max_simp_rounds(options const & o) { return o.get_unsigned(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS); @@ -64,29 +60,23 @@ static bool get_simplify_memoize(options const & o) { return o.get_bool(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE); } -static bool get_simplify_expand_macros(options const & o) { - return o.get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS); -} - /* Main simplifier class */ class defeq_simplify_fn { - tmp_type_context m_tmp_tctx; - normalizer m_normalizer; + tmp_type_context_pool & m_tmp_tctx_pool; + tmp_type_context * m_tmp_tctx; + defeq_simp_lemmas m_simp_lemmas; unsigned m_num_simp_rounds{0}; unsigned m_num_rewrite_rounds{0}; - options const & m_options; - /* Options */ unsigned m_max_simp_rounds; unsigned m_max_rewrite_rounds; bool m_top_down; bool m_exhaustive; bool m_memoize; - bool m_expand_macros; /* Cache */ expr_struct_map m_cache; @@ -131,9 +121,7 @@ class defeq_simplify_fn { case expr_kind::Var: lean_unreachable(); case expr_kind::Macro: - if (m_expand_macros) { - if (auto m = m_tmp_tctx.expand_macro(e)) e = defeq_simplify(whnf_eta(*m)); - } + e = defeq_simplify_macro(e); break; case expr_kind::Lambda: e = try_eta(defeq_simplify_binding(e)); @@ -152,12 +140,20 @@ class defeq_simplify_fn { if (!m_exhaustive || e == e_start) break; } if (m_memoize) cache_save(_e, e); + lean_assert(m_tmp_tctx->is_def_eq(_e, e)); return e; } + expr defeq_simplify_macro(expr const & e) { + buffer new_args; + for (unsigned i = 0; i < macro_num_args(e); i++) + new_args.push_back(defeq_simplify(macro_arg(e, i))); + return update_macro(e, new_args.size(), new_args.data()); + } + expr defeq_simplify_binding(expr const & e) { expr d = defeq_simplify(binding_domain(e)); - expr l = m_tmp_tctx.mk_tmp_local(binding_name(e), d, binding_info(e)); + expr l = m_tmp_tctx->mk_tmp_local(binding_name(e), d, binding_info(e)); expr b = abstract(defeq_simplify(instantiate(binding_body(e), l)), l); return update_binding(e, d, b); } @@ -168,7 +164,7 @@ class defeq_simplify_fn { expr f = get_app_rev_args(e, args); for (expr & a : args) { expr new_a = a; - if (!m_tmp_tctx.is_prop(m_tmp_tctx.infer(a))) + if (!m_tmp_tctx->is_prop(m_tmp_tctx->infer(a))) new_a = defeq_simplify(a); if (new_a != a) modified = true; @@ -176,15 +172,18 @@ class defeq_simplify_fn { } if (is_constant(f)) { - if (auto idx = inductive::get_elim_major_idx(m_tmp_tctx.env(), const_name(f))) { - if (auto r = m_normalizer.unfold_recursor_major(f, *idx, args)) + if (auto idx = inductive::get_elim_major_idx(m_tmp_tctx->env(), const_name(f))) { + if (auto r = normalizer(*m_tmp_tctx).unfold_recursor_major(f, *idx, args)) return *r; } } + if (!modified) return e; + expr r = mk_rev_app(f, args); - if (is_constant(f) && m_tmp_tctx.env().is_recursor(const_name(f))) { + + if (is_constant(f) && m_tmp_tctx->env().is_recursor(const_name(f))) { return defeq_simplify(r); } else { return r; @@ -214,31 +213,32 @@ class defeq_simplify_fn { } expr rewrite(expr const & e, defeq_simp_lemma const & sl) { - tmp_type_context tmp_tctx(m_tmp_tctx.env(), m_options); - tmp_tctx.clear(); - tmp_tctx.set_next_uvar_idx(sl.get_num_umeta()); - tmp_tctx.set_next_mvar_idx(sl.get_num_emeta()); + tmp_type_context * tmp_tctx = m_tmp_tctx_pool.mk_tmp_type_context(); + tmp_tctx->clear(); + tmp_tctx->set_next_uvar_idx(sl.get_num_umeta()); + tmp_tctx->set_next_mvar_idx(sl.get_num_emeta()); - if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) return e; + if (!tmp_tctx->is_def_eq(e, sl.get_lhs())) return e; lean_trace(name({"defeq_simplifier", "rewrite"}), - expr new_lhs = tmp_tctx.instantiate_uvars_mvars(sl.get_lhs()); - expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs()); + expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sl.get_lhs()); + expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sl.get_rhs()); tout() << "(" << sl.get_id() << ") " << "[" << new_lhs << " --> " << new_rhs << "]\n";); if (!instantiate_emetas(tmp_tctx, sl.get_emetas(), sl.get_instances())) return e; for (unsigned i = 0; i < sl.get_num_umeta(); i++) { - if (!tmp_tctx.is_uvar_assigned(i)) return e; + if (!tmp_tctx->is_uvar_assigned(i)) return e; } - expr new_rhs = tmp_tctx.instantiate_uvars_mvars(sl.get_rhs()); + expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sl.get_rhs()); + m_tmp_tctx_pool.recycle_tmp_type_context(tmp_tctx); return new_rhs; } - bool instantiate_emetas(tmp_type_context & tmp_tctx, list const & _emetas, list const & _instances) { + bool instantiate_emetas(tmp_type_context * tmp_tctx, list const & _emetas, list const & _instances) { buffer emetas; buffer instances; to_buffer(_emetas, emetas); @@ -248,17 +248,17 @@ class defeq_simplify_fn { for (unsigned i = 0; i < emetas.size(); ++i) { expr m = emetas[i]; unsigned mvar_idx = emetas.size() - 1 - i; - expr m_type = tmp_tctx.instantiate_uvars_mvars(tmp_tctx.infer(m)); + expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m)); lean_assert(!has_metavar(m_type)); - if (tmp_tctx.is_mvar_assigned(mvar_idx)) continue; + if (tmp_tctx->is_mvar_assigned(mvar_idx)) continue; if (instances[i]) { - if (auto v = tmp_tctx.mk_class_instance(m_type)) { - if (!tmp_tctx.assign(m, *v)) { + if (auto v = tmp_tctx->mk_class_instance(m_type)) { + if (!tmp_tctx->assign(m, *v)) { lean_trace(name({"defeq_simplifier", "failure"}), tout() << "unable to assign instance for: " << m_type << "\n";); return false; } else { - lean_assert(tmp_tctx.is_mvar_assigned(mvar_idx)); + lean_assert(tmp_tctx->is_mvar_assigned(mvar_idx)); continue; } } else { @@ -276,22 +276,24 @@ class defeq_simplify_fn { } expr whnf_eta(expr const & e) { - return try_eta(m_tmp_tctx.whnf(e)); + return try_eta(m_tmp_tctx->whnf(e)); } public: - defeq_simplify_fn(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas): - m_tmp_tctx(env, o), - m_normalizer(m_tmp_tctx), + defeq_simplify_fn(tmp_type_context_pool & tmp_tctx_pool, options const & o, defeq_simp_lemmas const & simp_lemmas): + m_tmp_tctx_pool(tmp_tctx_pool), + m_tmp_tctx(m_tmp_tctx_pool.mk_tmp_type_context()), m_simp_lemmas(simp_lemmas), - m_options(o), m_max_simp_rounds(get_simplify_max_simp_rounds(o)), m_max_rewrite_rounds(get_simplify_max_rewrite_rounds(o)), m_top_down(get_simplify_top_down(o)), m_exhaustive(get_simplify_exhaustive(o)), - m_memoize(get_simplify_memoize(o)), - m_expand_macros(get_simplify_expand_macros(o)) {} + m_memoize(get_simplify_memoize(o)) + { } + ~defeq_simplify_fn() { + m_tmp_tctx_pool.recycle_tmp_type_context(m_tmp_tctx); + } expr operator()(expr const & e) { return defeq_simplify(e); } }; @@ -307,7 +309,6 @@ void initialize_defeq_simplifier() { g_simplify_top_down = new name{"defeq_simplify", "top_down"}; g_simplify_exhaustive = new name{"defeq_simplify", "exhaustive"}; g_simplify_memoize = new name{"defeq_simplify", "memoize"}; - g_simplify_expand_macros = new name{"defeq_simplify", "expand_macros"}; register_unsigned_option(*g_simplify_max_simp_rounds, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS, "(defeq_simplify) max allowed simplification rounds"); @@ -319,12 +320,9 @@ void initialize_defeq_simplifier() { "(defeq_simplify) simplify exhaustively"); register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_DEFEQ_SIMPLIFY_MEMOIZE, "(defeq_simplify) memoize simplifications"); - register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_DEFEQ_SIMPLIFY_EXPAND_MACROS, - "(defeq_simplify) expand macros"); } void finalize_defeq_simplifier() { - delete g_simplify_expand_macros; delete g_simplify_memoize; delete g_simplify_exhaustive; delete g_simplify_top_down; @@ -333,9 +331,8 @@ void finalize_defeq_simplifier() { } /* Entry point */ -expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e) { - return defeq_simplify_fn(env, o, simp_lemmas)(e); +expr defeq_simplify(tmp_type_context_pool & tmp_tctx_pool, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e) { + return defeq_simplify_fn(tmp_tctx_pool, o, simp_lemmas)(e); } - } diff --git a/src/library/defeq_simplifier.h b/src/library/defeq_simplifier.h index 849686ffb..4fa82b561 100644 --- a/src/library/defeq_simplifier.h +++ b/src/library/defeq_simplifier.h @@ -5,11 +5,12 @@ Author: Daniel Selsam */ #pragma once #include "kernel/expr.h" +#include "library/tmp_type_context.h" #include "library/defeq_simp_lemmas.h" namespace lean { -expr defeq_simplify(environment const & env, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e); +expr defeq_simplify(tmp_type_context_pool & tmp_tctx_pool, options const & o, defeq_simp_lemmas const & simp_lemmas, expr const & e); void initialize_defeq_simplifier(); void finalize_defeq_simplifier(); diff --git a/src/library/tmp_type_context.h b/src/library/tmp_type_context.h index aff334213..f67c03dd0 100644 --- a/src/library/tmp_type_context.h +++ b/src/library/tmp_type_context.h @@ -90,4 +90,24 @@ public: return static_cast(m_eassignment[idx]); } }; + +class tmp_type_context_pool { +public: + virtual tmp_type_context * mk_tmp_type_context() =0; + virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) =0; + + virtual ~tmp_type_context_pool() {} +}; + +class default_tmp_type_context_pool : public tmp_type_context_pool { + environment m_env; + options m_options; +public: + default_tmp_type_context_pool(environment const & env, options const & o): + m_env(env), m_options(o) {} + + virtual tmp_type_context * mk_tmp_type_context() override { return new tmp_type_context(m_env, m_options); } + virtual void recycle_tmp_type_context(tmp_type_context * tmp_tctx) override { delete tmp_tctx; } +}; + } diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 58df70df2..32e94be26 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -170,7 +170,7 @@ optional type_context::is_transparent(name const & n) { optional type_context::expand_macro(expr const & m) { lean_assert(is_macro(m)); - if (should_unfold_macro(m)) + if (m_in_is_def_eq || should_unfold_macro(m)) return macro_def(m).expand(m, *m_ext_ctx); else return none_expr(); @@ -1064,6 +1064,7 @@ bool type_context::process_postponed(unsigned old_sz) { bool type_context::is_def_eq(expr const & e1, expr const & e2) { scope s(*this); + flet in_is_def_eq(m_in_is_def_eq, true); unsigned psz = m_postponed.size(); if (!is_def_eq_core(e1, e2)) { return false; diff --git a/src/library/type_context.h b/src/library/type_context.h index 7a481d508..d167c62bc 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -116,6 +116,7 @@ class type_context : public abstract_type_context { // postponed universe constraints std::vector> m_postponed; name_map m_proj_info; + bool m_in_is_def_eq{false}; // Internal (configuration) options for customers diff --git a/tests/lean/defeq_simp_lemmas1.lean b/tests/lean/defeq_simp_lemmas1.lean index 6679295fe..1fda928e1 100644 --- a/tests/lean/defeq_simp_lemmas1.lean +++ b/tests/lean/defeq_simp_lemmas1.lean @@ -1,3 +1,4 @@ +namespace foo universe l constants (A : Type.{l}) @@ -12,4 +13,5 @@ definition g.def [defeq] (x y : A) : g x y = h y := rfl definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl -print [defeq] +print [defeq] foo +end foo diff --git a/tests/lean/defeq_simp_lemmas1.lean.expected.out b/tests/lean/defeq_simp_lemmas1.lean.expected.out index 30dba9002..80bf01b95 100644 --- a/tests/lean/defeq_simp_lemmas1.lean.expected.out +++ b/tests/lean/defeq_simp_lemmas1.lean.expected.out @@ -1,5 +1,5 @@ -defeq simp lemmas: -#2, g ?M_1 ?M_2 ↦ h ?M_2 +defeq simp lemmas at namespace 'foo': #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3) #3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3 +#2, g ?M_1 ?M_2 ↦ h ?M_2 #1, h ?M_1 ↦ q ?M_1 diff --git a/tests/lean/defeq_simp_lemmas2.lean b/tests/lean/defeq_simp_lemmas2.lean index a9e5ff29c..9fc4d5711 100644 --- a/tests/lean/defeq_simp_lemmas2.lean +++ b/tests/lean/defeq_simp_lemmas2.lean @@ -1,3 +1,4 @@ +namespace foo universe l constants (A : Type.{l}) @@ -18,7 +19,7 @@ definition f.def [defeq] (x y z : A) : f x y z = g (g x y) z := rfl definition d.def [defeq] (x y z w : A) : d x y z w = f (f x y z) (f y z w) (f x w z) := rfl -- Confirm that more recent annotations get priority -print [defeq] +print [defeq] foo attribute h.rfl [defeq] [priority 1001] attribute g.rfl [defeq] [priority 1001] @@ -26,7 +27,7 @@ attribute f.rfl [defeq] [priority 1001] attribute d.rfl [defeq] [priority 1001] -- Confirm that priority annotations override -print [defeq] +print [defeq] foo attribute h.def [defeq] [priority 1001] attribute g.def [defeq] [priority 1001] @@ -34,4 +35,5 @@ attribute f.def [defeq] [priority 1001] attribute d.def [defeq] [priority 1001] -- Confirm that most recent annotations get priority to break explicit priority ties -print [defeq] +print [defeq] foo +end foo diff --git a/tests/lean/defeq_simp_lemmas2.lean.expected.out b/tests/lean/defeq_simp_lemmas2.lean.expected.out index 8f7e13230..ae40582a2 100644 --- a/tests/lean/defeq_simp_lemmas2.lean.expected.out +++ b/tests/lean/defeq_simp_lemmas2.lean.expected.out @@ -1,27 +1,27 @@ -defeq simp lemmas: -#2, g ?M_1 ?M_2 ↦ h ?M_2 -#2, g ?M_1 ?M_2 ↦ ?M_2 +defeq simp lemmas at namespace 'foo': #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3) #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3 #3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3 #3, f ?M_1 ?M_2 ?M_3 ↦ ?M_3 +#2, g ?M_1 ?M_2 ↦ h ?M_2 +#2, g ?M_1 ?M_2 ↦ ?M_2 #1, h ?M_1 ↦ q ?M_1 #1, h ?M_1 ↦ ?M_1 -defeq simp lemmas: -#2 (1001), g ?M_1 ?M_2 ↦ ?M_2 -#2, g ?M_1 ?M_2 ↦ h ?M_2 +defeq simp lemmas at namespace 'foo': #4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3 #4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3) #3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3 #3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3 +#2 (1001), g ?M_1 ?M_2 ↦ ?M_2 +#2, g ?M_1 ?M_2 ↦ h ?M_2 #1 (1001), h ?M_1 ↦ ?M_1 #1, h ?M_1 ↦ q ?M_1 -defeq simp lemmas: -#2 (1001), g ?M_1 ?M_2 ↦ h ?M_2 -#2 (1001), g ?M_1 ?M_2 ↦ ?M_2 +defeq simp lemmas at namespace 'foo': #4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3) #4 (1001), d ?M_1 ?M_2 ?M_3 ?M_4 ↦ ?M_3 #3 (1001), f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3 #3 (1001), f ?M_1 ?M_2 ?M_3 ↦ ?M_3 +#2 (1001), g ?M_1 ?M_2 ↦ h ?M_2 +#2 (1001), g ?M_1 ?M_2 ↦ ?M_2 #1 (1001), h ?M_1 ↦ q ?M_1 #1 (1001), h ?M_1 ↦ ?M_1