From 95c7c697a6785bfb0db7d681f31ec391eef6a722 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 1 Jul 2017 12:54:37 -0700 Subject: [PATCH] refactor(library/tactic/simp_lemmas): simp set generation should not be affected by transparency setting --- library/init/meta/interactive.lean | 4 +- library/init/meta/simp_tactic.lean | 24 ++----- src/frontends/lean/print_cmd.cpp | 4 +- src/library/constructions/has_sizeof.cpp | 4 +- src/library/constructions/has_sizeof.h | 2 +- src/library/inductive_compiler/nested.cpp | 2 +- src/library/tactic/simp_lemmas.cpp | 86 +++++++++++------------ src/library/tactic/simp_lemmas.h | 6 +- 8 files changed, 57 insertions(+), 75 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 44164514a2..54ca3e1918 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -670,13 +670,13 @@ do let e := p.erase_annotations.get_app_fn.erase_annotations, match e with | const n _ := - (do b ← is_valid_simp_lemma_cnst reducible n, guard b, save_const_type_info n ref, s.add_simp n) + (do b ← is_valid_simp_lemma_cnst n, guard b, save_const_type_info n ref, s.add_simp n) <|> (do eqns ← get_eqn_lemmas_for tt n, guard (eqns.length > 0), save_const_type_info n ref, add_simps s eqns) <|> report_invalid_simp_lemma n | _ := - (do e ← i_to_expr_no_subgoals p, b ← is_valid_simp_lemma reducible e, guard b, try (save_type_info e ref), s.add e) + (do e ← i_to_expr_no_subgoals p, b ← is_valid_simp_lemma e, guard b, try (save_type_info e ref), s.add e) <|> report_invalid_simp_lemma n end diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 840707c375..291ddb744c 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -14,22 +14,10 @@ meta constant simp_lemmas : Type meta constant simp_lemmas.mk : simp_lemmas meta constant simp_lemmas.join : simp_lemmas → simp_lemmas → simp_lemmas meta constant simp_lemmas.erase : simp_lemmas → list name → simp_lemmas -meta constant simp_lemmas.mk_default_core : transparency → tactic simp_lemmas -meta constant simp_lemmas.add_core : transparency → simp_lemmas → expr → tactic simp_lemmas -meta constant simp_lemmas.add_simp_core : transparency → simp_lemmas → name → tactic simp_lemmas -meta constant simp_lemmas.add_congr_core : transparency → simp_lemmas → name → tactic simp_lemmas - -meta def simp_lemmas.mk_default : tactic simp_lemmas := -simp_lemmas.mk_default_core reducible - -meta def simp_lemmas.add : simp_lemmas → expr → tactic simp_lemmas := -simp_lemmas.add_core reducible - -meta def simp_lemmas.add_simp : simp_lemmas → name → tactic simp_lemmas := -simp_lemmas.add_simp_core reducible - -meta def simp_lemmas.add_congr : simp_lemmas → name → tactic simp_lemmas := -simp_lemmas.add_congr_core reducible +meta constant simp_lemmas.mk_default : tactic simp_lemmas +meta constant simp_lemmas.add : simp_lemmas → expr → tactic simp_lemmas +meta constant simp_lemmas.add_simp : simp_lemmas → name → tactic simp_lemmas +meta constant simp_lemmas.add_congr : simp_lemmas → name → tactic simp_lemmas meta def simp_lemmas.append (s : simp_lemmas) (hs : list expr) : tactic simp_lemmas := hs.mfoldl simp_lemmas.add s @@ -52,8 +40,8 @@ meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr meta def simp_lemmas.drewrite : simp_lemmas → expr → tactic expr := simp_lemmas.drewrite_core reducible -meta constant is_valid_simp_lemma_cnst : transparency → name → tactic bool -meta constant is_valid_simp_lemma : transparency → expr → tactic bool +meta constant is_valid_simp_lemma_cnst : name → tactic bool +meta constant is_valid_simp_lemma : expr → tactic bool def default_max_steps := 10000000 diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 9375ec22d1..de8ad08e36 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -459,13 +459,13 @@ static void print_unification_hints(parser & p, message_builder & out) { static void print_simp_rules(parser & p, message_builder & out) { name attr = p.check_id_next("invalid '#print [simp]' command, identifier expected"); - simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr); + simp_lemmas slss = get_simp_lemmas(p.env(), attr); out << slss.pp_simp(out.get_formatter()); } static void print_congr_rules(parser & p, message_builder & out) { name attr = p.check_id_next("invalid '#print [congr]' command, identifier expected"); - simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr); + simp_lemmas slss = get_simp_lemmas(p.env(), attr); out << slss.pp_congr(out.get_formatter()); } diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp index 76dcff523d..4f1d8fed42 100644 --- a/src/library/constructions/has_sizeof.cpp +++ b/src/library/constructions/has_sizeof.cpp @@ -320,8 +320,8 @@ name simp_sizeof_attribute_name() { return *g_simp_sizeof; } -simp_lemmas get_sizeof_simp_lemmas(environment const & env, transparency_mode m) { - return get_simp_lemmas(env, m, g_simp_sizeof_tk); +simp_lemmas get_sizeof_simp_lemmas(environment const & env) { + return get_simp_lemmas(env, g_simp_sizeof_tk); } void initialize_has_sizeof() { diff --git a/src/library/constructions/has_sizeof.h b/src/library/constructions/has_sizeof.h index b4cc95c525..43966847c7 100644 --- a/src/library/constructions/has_sizeof.h +++ b/src/library/constructions/has_sizeof.h @@ -17,7 +17,7 @@ name mk_has_sizeof_name(name const & ind_name); name mk_sizeof_name(name const & ind_name); name mk_sizeof_spec_name(name const & ir_name); name simp_sizeof_attribute_name(); -simp_lemmas get_sizeof_simp_lemmas(environment const & env, transparency_mode m); +simp_lemmas get_sizeof_simp_lemmas(environment const & env); environment set_simp_sizeof(environment const & env, name const & n); void initialize_has_sizeof(); diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 4e6812944b..3eba13ada1 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -2308,7 +2308,7 @@ public: if (m_inner_decl.has_sizeof_lemmas()) { m_nested_decl.set_sizeof_lemmas(m_inner_decl.get_sizeof_lemmas()); } else { - m_nested_decl.set_sizeof_lemmas(get_sizeof_simp_lemmas(m_tctx.env(), m_tctx.mode())); + m_nested_decl.set_sizeof_lemmas(get_sizeof_simp_lemmas(m_tctx.env())); } check_elim_to_type(); diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index ba2937eafb..2d5cf0138c 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -1057,27 +1057,25 @@ class simp_lemmas_cache { struct entry { environment m_env; std::vector m_fingerprints; - unsigned m_reducibility_fingerprint; optional m_lemmas; entry(environment const & env): - m_env(env), m_reducibility_fingerprint(0) {} + m_env(env) {} }; - std::vector m_entries[LEAN_NUM_TRANSPARENCY_MODES]; + std::vector m_entries; public: - void expand(environment const & env, transparency_mode m, unsigned new_sz) { - unsigned midx = static_cast(m); - for (unsigned tk = m_entries[midx].size(); tk < new_sz; tk++) { + void expand(environment const & env, unsigned new_sz) { + for (unsigned tk = m_entries.size(); tk < new_sz; tk++) { auto & cfg = get_simp_lemmas_config(tk); - m_entries[midx].emplace_back(env); - auto & entry = m_entries[midx].back(); + m_entries.emplace_back(env); + auto & entry = m_entries.back(); entry.m_fingerprints.resize(cfg.m_simp_attrs.size() + cfg.m_congr_attrs.size()); } } - simp_lemmas mk_lemmas(environment const & env, transparency_mode m, entry & C, simp_lemmas_token tk) { + simp_lemmas mk_lemmas(environment const & env, entry & C, simp_lemmas_token tk) { lean_trace("simp_lemmas_cache", tout() << "make simp lemmas [" << tk << "]\n";); - type_context ctx(env, m); + type_context ctx(env); C.m_env = env; auto & cfg = get_simp_lemmas_config(tk); simp_lemmas lemmas; @@ -1093,7 +1091,6 @@ public: i++; } C.m_lemmas = lemmas; - C.m_reducibility_fingerprint = get_reducibility_fingerprint(env); return lemmas; } @@ -1105,8 +1102,6 @@ public: bool is_compatible(entry const & C, environment const & env, simp_lemmas_token tk) { if (!env.is_descendant(C.m_env)) return false; - if (get_reducibility_fingerprint(env) != C.m_reducibility_fingerprint) - return false; auto & cfg = get_simp_lemmas_config(tk); unsigned i = 0; for (name const & attr_name : cfg.m_simp_attrs) { @@ -1122,17 +1117,16 @@ public: return true; } - simp_lemmas get(environment const & env, transparency_mode m, simp_lemmas_token tk) { + simp_lemmas get(environment const & env, simp_lemmas_token tk) { lean_assert(tk < g_simp_lemmas_configs->size()); - unsigned midx = static_cast(m); - if (tk >= m_entries[midx].size()) expand(env, m, tk+1); - lean_assert(tk < m_entries[midx].size()); - entry & C = m_entries[midx][tk]; - if (!C.m_lemmas) return mk_lemmas(env, m, C, tk); + if (tk >= m_entries.size()) expand(env, tk+1); + lean_assert(tk < m_entries.size()); + entry & C = m_entries[tk]; + if (!C.m_lemmas) return mk_lemmas(env, C, tk); if (is_eqp(env, C.m_env)) return lemmas_of(C, tk); if (!is_compatible(C, env, tk)) { lean_trace("simp_lemmas_cache", tout() << "creating new cache\n";); - return mk_lemmas(env, m, C, tk); + return mk_lemmas(env, C, tk); } return lemmas_of(C, tk); } @@ -1140,17 +1134,17 @@ public: MK_THREAD_LOCAL_GET_DEF(simp_lemmas_cache, get_cache); -simp_lemmas get_simp_lemmas(environment const & env, transparency_mode m, simp_lemmas_token tk) { - return get_cache().get(env, m, tk); +simp_lemmas get_simp_lemmas(environment const & env, simp_lemmas_token tk) { + return get_cache().get(env, tk); } -simp_lemmas get_default_simp_lemmas(environment const & env, transparency_mode m) { - return get_simp_lemmas(env, m, g_default_token); +simp_lemmas get_default_simp_lemmas(environment const & env) { + return get_simp_lemmas(env, g_default_token); } -simp_lemmas get_simp_lemmas(environment const & env, transparency_mode m, name const & tk_name) { +simp_lemmas get_simp_lemmas(environment const & env, name const & tk_name) { if (simp_lemmas_token const * tk = g_name2simp_token->find(tk_name)) - return get_simp_lemmas(env, m, *tk); + return get_simp_lemmas(env, *tk); else throw exception(sstream() << "unknown simp_lemmas collection '" << tk_name << "'"); } @@ -1261,17 +1255,17 @@ vm_obj to_obj(simp_lemmas const & idx) { return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_simp_lemmas))) vm_simp_lemmas(idx)); } -vm_obj simp_lemmas_mk_default_core(vm_obj const & m, vm_obj const & s) { +vm_obj simp_lemmas_mk_default(vm_obj const & s) { LEAN_TACTIC_TRY; environment const & env = tactic::to_state(s).env(); - simp_lemmas r = get_default_simp_lemmas(env, to_transparency_mode(m)); + simp_lemmas r = get_default_simp_lemmas(env); return tactic::mk_success(to_obj(r), tactic::to_state(s)); LEAN_TACTIC_CATCH(tactic::to_state(s)); } -vm_obj simp_lemmas_add_core(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & s) { +vm_obj simp_lemmas_add(vm_obj const & lemmas, vm_obj const & lemma, vm_obj const & s) { LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s, m); + type_context ctx = mk_type_context_for(s); expr e = to_expr(lemma); name id; if (is_constant(e)) @@ -1293,17 +1287,17 @@ vm_obj simp_lemmas_add_core(vm_obj const & m, vm_obj const & lemmas, vm_obj cons LEAN_TACTIC_CATCH(tactic::to_state(s)); } -vm_obj simp_lemmas_add_simp(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { +vm_obj simp_lemmas_add_simp(vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s, m); + type_context ctx = mk_type_context_for(s); simp_lemmas new_lemmas = add(ctx, to_simp_lemmas(lemmas), to_name(lemma_name), LEAN_DEFAULT_PRIORITY); return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); LEAN_TACTIC_CATCH(tactic::to_state(s)); } -vm_obj simp_lemmas_add_congr(vm_obj const & m, vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { +vm_obj simp_lemmas_add_congr(vm_obj const & lemmas, vm_obj const & lemma_name, vm_obj const & s) { LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s, m); + type_context ctx = mk_type_context_for(s); simp_lemmas new_lemmas = add_congr(ctx, to_simp_lemmas(lemmas), to_name(lemma_name), LEAN_DEFAULT_PRIORITY); return tactic::mk_success(to_obj(new_lemmas), tactic::to_state(s)); LEAN_TACTIC_CATCH(tactic::to_state(s)); @@ -1476,9 +1470,9 @@ vm_obj simp_lemmas_drewrite(vm_obj const & m, vm_obj const & sls, vm_obj const & return simp_lemmas_drewrite_core(to_transparency_mode(m), to_simp_lemmas(sls), to_expr(e), tactic::to_state(s)); } -static bool is_valid_simp_lemma_cnst_core(transparency_mode const & m, name const & cname, tactic_state const & s) { +static bool is_valid_simp_lemma_cnst(name const & cname, tactic_state const & s) { try { - type_context ctx = mk_type_context_for(s, m); + type_context ctx = mk_type_context_for(s); type_context::tmp_mode_scope scope(ctx); declaration const & d = ctx.env().get(cname); levels ls = mk_tmp_levels_for(ctx, d); @@ -1490,14 +1484,14 @@ static bool is_valid_simp_lemma_cnst_core(transparency_mode const & m, name cons } } -vm_obj is_valid_simp_lemma_cnst(vm_obj const & m, vm_obj const & n, vm_obj const & s) { - return tactic::mk_success(mk_vm_bool(is_valid_simp_lemma_cnst_core(to_transparency_mode(m), to_name(n), tactic::to_state(s))), +vm_obj is_valid_simp_lemma_cnst(vm_obj const & n, vm_obj const & s) { + return tactic::mk_success(mk_vm_bool(is_valid_simp_lemma_cnst(to_name(n), tactic::to_state(s))), tactic::to_state(s)); } -static bool is_valid_simp_lemma_core(transparency_mode const & m, expr const & e, tactic_state const & s) { +static bool is_valid_simp_lemma(expr const & e, tactic_state const & s) { try { - type_context ctx = mk_type_context_for(s, m); + type_context ctx = mk_type_context_for(s); expr type = ctx.infer(e); return !is_nil(to_ceqvs(ctx, name(), type, e)); } catch (exception &) { @@ -1505,8 +1499,8 @@ static bool is_valid_simp_lemma_core(transparency_mode const & m, expr const & e } } -vm_obj is_valid_simp_lemma(vm_obj const & m, vm_obj const & e, vm_obj const & s) { - return tactic::mk_success(mk_vm_bool(is_valid_simp_lemma_core(to_transparency_mode(m), to_expr(e), tactic::to_state(s))), +vm_obj is_valid_simp_lemma(vm_obj const & e, vm_obj const & s) { + return tactic::mk_success(mk_vm_bool(is_valid_simp_lemma(to_expr(e), tactic::to_state(s))), tactic::to_state(s)); } @@ -1545,10 +1539,10 @@ void initialize_simp_lemmas() { DECLARE_VM_BUILTIN(name({"simp_lemmas", "mk"}), simp_lemmas_mk); DECLARE_VM_BUILTIN(name({"simp_lemmas", "join"}), simp_lemmas_join); DECLARE_VM_BUILTIN(name({"simp_lemmas", "erase"}), simp_lemmas_erase); - DECLARE_VM_BUILTIN(name({"simp_lemmas", "mk_default_core"}), simp_lemmas_mk_default_core); - DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_core"}), simp_lemmas_add_core); - DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_simp_core"}), simp_lemmas_add_simp); - DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_congr_core"}), simp_lemmas_add_congr); + DECLARE_VM_BUILTIN(name({"simp_lemmas", "mk_default"}), simp_lemmas_mk_default); + DECLARE_VM_BUILTIN(name({"simp_lemmas", "add"}), simp_lemmas_add); + DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_simp"}), simp_lemmas_add_simp); + DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_congr"}), simp_lemmas_add_congr); DECLARE_VM_BUILTIN(name({"simp_lemmas", "rewrite_core"}), simp_lemmas_rewrite); DECLARE_VM_BUILTIN(name({"simp_lemmas", "drewrite_core"}), simp_lemmas_drewrite); DECLARE_VM_BUILTIN(name({"simp_lemmas", "pp"}), simp_lemmas_pp); diff --git a/src/library/tactic/simp_lemmas.h b/src/library/tactic/simp_lemmas.h index 3df3805d53..4ff4f5724b 100644 --- a/src/library/tactic/simp_lemmas.h +++ b/src/library/tactic/simp_lemmas.h @@ -129,9 +129,9 @@ simp_lemmas_token register_simp_attribute(name const & user_name, std::initializer_list const & simp_attrs, std::initializer_list const & congr_attrs); -simp_lemmas get_simp_lemmas(environment const & env, transparency_mode m, simp_lemmas_token tk); -simp_lemmas get_default_simp_lemmas(environment const & env, transparency_mode m); -simp_lemmas get_simp_lemmas(environment const & env, transparency_mode m, name const & tk_name); +simp_lemmas get_simp_lemmas(environment const & env, simp_lemmas_token tk); +simp_lemmas get_default_simp_lemmas(environment const & env); +simp_lemmas get_simp_lemmas(environment const & env, name const & tk_name); simp_lemmas add(type_context & ctx, simp_lemmas const & s, name const & id, unsigned priority); simp_lemmas add(type_context & ctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority);