From d747fcb17c02ac61becebe4dabf550786dec16dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Oct 2016 20:20:01 -0700 Subject: [PATCH] refactor(library/tactic/simp_lemmas): new caching mechanism --- library/init/meta/simp_tactic.lean | 8 +- src/frontends/lean/print_cmd.cpp | 41 +--- src/library/attribute_manager.cpp | 5 +- src/library/attribute_manager.h | 1 + src/library/constructions/has_sizeof.cpp | 13 +- src/library/constructions/has_sizeof.h | 2 +- src/library/inductive_compiler/nested.cpp | 2 +- src/library/tactic/simplifier/simp_lemmas.cpp | 230 ++++++++++++------ src/library/tactic/simplifier/simp_lemmas.h | 12 +- tests/lean/run/rw_set1.lean | 2 +- tests/lean/run/rw_set3.lean | 2 +- tests/lean/run/rw_set4.lean | 2 +- tests/lean/run/simp_ext1.lean | 23 -- .../lean/run/simplifier_custom_relations.lean | 4 +- 14 files changed, 193 insertions(+), 154 deletions(-) delete mode 100644 tests/lean/run/simp_ext1.lean diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 8ad0ea1211..6447bbb362 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -14,11 +14,7 @@ meta constant simp_lemmas.erase : simp_lemmas → list name → simp_lemmas namespace tactic open list nat -/- Create a data-structure containing a simp lemma for every constant in the first list of - attributes, and a congr lemma for every constant in the second list of attributes. - Lemmas with type ` ` are indexed using the head-symbol of ``, - computed with respect to the given transparency setting. -/ -meta constant mk_simp_lemmas_core : transparency → list name → list name → tactic simp_lemmas +meta constant mk_default_simp_lemmas_core : transparency → tactic simp_lemmas /- (simp_lemmas_insert_core m lemmas lemma priority) adds the given lemma to the set simp_lemmas. -/ meta constant simp_lemmas_insert_core : transparency → simp_lemmas → expr → tactic simp_lemmas /- (simp_lemmas_insert_constant_core m lemmas cname) -/ @@ -28,7 +24,7 @@ meta def simp_lemmas_insert_constant : simp_lemmas → name → tactic simp_lemm simp_lemmas_insert_constant_core reducible meta def mk_simp_lemmas : tactic simp_lemmas := -mk_simp_lemmas_core reducible [`simp] [`congr] +mk_default_simp_lemmas_core reducible meta def simp_lemmas_add_extra : transparency → simp_lemmas → list expr → tactic simp_lemmas | m sls [] := return sls diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index f39f0d2850..550f403864 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -471,44 +471,21 @@ static void print_rfl_lemmas(parser & p) { } static void print_simp_rules(parser & p) { - type_context aux_tctx(p.env(), p.get_options()); name attr = p.check_id_next("invalid 'print [simp]' command, identifier expected"); - buffer attrs; - attrs.push_back(attr); - buffer no_congr; - simp_lemmas slss = get_simp_lemmas(aux_tctx, attrs, no_congr); + simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr); type_checker tc(p.env()); auto out = regular(p.env(), p.ios(), tc); out << slss.pp_simp(out.get_formatter()); } static void print_congr_rules(parser & p) { - type_context aux_tctx(p.env(), p.get_options()); name attr = p.check_id_next("invalid 'print [congr]' command, identifier expected"); - buffer no_simp; - buffer attrs; - attrs.push_back(attr); - simp_lemmas slss = get_simp_lemmas(aux_tctx, no_simp, attrs); + simp_lemmas slss = get_simp_lemmas(p.env(), transparency_mode::Reducible, attr); type_checker tc(p.env()); auto out = regular(p.env(), p.ios(), tc); out << slss.pp_congr(out.get_formatter()); } -static void print_simp_extensions(parser & p) { - type_checker tc(p.env()); - auto out = regular(p.env(), p.ios(), tc); - out << pp_simp_extensions(p.env()); -} - -#if 0 -static void print_light_rules(parser & p) { - type_checker tc(p.env()); - auto out = regular(p.env(), p.ios(), tc); - light_rule_set lrs = get_light_rule_set(p.env()); - out << lrs; -} -#endif - static void print_aliases(parser const & p) { std::ostream & out = p.ios().get_regular_stream(); for_each_expr_alias(p.env(), [&](name const & n, list const & as) { @@ -647,20 +624,16 @@ environment print_cmd(parser & p) { auto name = p.check_id_next("invalid attribute declaration, identifier expected"); p.check_token_next(get_rbracket_tk(), "invalid 'print []', ']' expected"); - if (name == "recursor") + if (name == "recursor") { print_recursor_info(p); - else if (name == "unify") + } else if (name == "unify") { print_unification_hints(p); - else if (name == "defeq") + } else if (name == "defeq") { print_rfl_lemmas(p); - else if (name == "simp") + } else if (name == "simp") { print_simp_rules(p); - else if (name == "simp_ext") - print_simp_extensions(p); - else if (name == "congr") + } else if (name == "congr") { print_congr_rules(p); - else if (name == "light") { - // print_light_rules(p); } else { if (!is_attribute(p.env(), name)) throw parser_error(sstream() << "unknown attribute [" << name << "]", pos); diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index a0073fbb2b..02c2c1f8b0 100644 --- a/src/library/attribute_manager.cpp +++ b/src/library/attribute_manager.cpp @@ -34,14 +34,13 @@ static std::vector> * g_incomp = nullptr; static std::string * g_key = nullptr; -static bool is_system_attribute(name const & attr) { - return g_system_attributes->find(attr) != nullptr; +bool is_system_attribute(name const & attr) { + return g_system_attributes->contains(attr); } void register_system_attribute(attribute_ptr attr) { lean_assert(!is_system_attribute(attr->get_name())); (*g_system_attributes)[attr->get_name()] = attr; } - bool is_attribute(environment const & env, name const & attr) { return is_system_attribute(attr) || g_user_attribute_ext->get_attributes(env).find(attr) != nullptr; } diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index b0eb22bb19..bdf4a138b5 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -233,6 +233,7 @@ void register_system_attribute(Attribute attr) { } void register_incompatible(char const * attr1, char const * attr2); +bool is_system_attribute(name const & attr_name); bool is_attribute(environment const & env, name const & attr); attribute const & get_attribute(environment const & env, name const & attr); attribute const & get_system_attribute(name const & attr); diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp index 6dc78c0954..49f0a92907 100644 --- a/src/library/constructions/has_sizeof.cpp +++ b/src/library/constructions/has_sizeof.cpp @@ -27,8 +27,8 @@ Author: Daniel Selsam #include "library/constructions/has_sizeof.h" namespace lean { - static name * g_simp_sizeof = nullptr; +static simp_lemmas_token g_simp_sizeof_tk; static basic_attribute const & get_simp_sizeof_attribute() { return static_cast(get_system_attribute(*g_simp_sizeof)); @@ -293,16 +293,13 @@ name simp_sizeof_attribute_name() { return *g_simp_sizeof; } -simp_lemmas get_sizeof_simp_lemmas(type_context & tctx) { - buffer simp_attrs, congr_attrs; - simp_attrs.push_back(simp_sizeof_attribute_name()); - return get_simp_lemmas(tctx, simp_attrs, congr_attrs); +simp_lemmas get_sizeof_simp_lemmas(environment const & env, transparency_mode m) { + return get_simp_lemmas(env, m, g_simp_sizeof_tk); } void initialize_has_sizeof() { - g_simp_sizeof = new name{"simp", "sizeof"}; - register_system_attribute(basic_attribute::with_check(*g_simp_sizeof, "simplification lemma", on_add_simp_lemma)); - + g_simp_sizeof = new name{"simp", "sizeof"}; + g_simp_sizeof_tk = register_simp_attribute("ssizeof", {*g_simp_sizeof}, {}); register_trace_class(name({"constructions", "has_sizeof"})); } diff --git a/src/library/constructions/has_sizeof.h b/src/library/constructions/has_sizeof.h index 826259ef73..58b1062e93 100644 --- a/src/library/constructions/has_sizeof.h +++ b/src/library/constructions/has_sizeof.h @@ -16,7 +16,7 @@ environment mk_has_sizeof(environment const & env, name const & ind_name); name mk_has_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(type_context & tctx); +simp_lemmas get_sizeof_simp_lemmas(environment const & env, transparency_mode m); 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 9eb1cd9b70..f047286d10 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -1689,7 +1689,7 @@ public: construct_inner_decl(); add_inner_decl(); check_elim_to_type(); - m_sizeof_lemmas = get_sizeof_simp_lemmas(m_tctx); + m_sizeof_lemmas = get_sizeof_simp_lemmas(m_tctx.env(), m_tctx.mode()); define_nested_inds(); diff --git a/src/library/tactic/simplifier/simp_lemmas.cpp b/src/library/tactic/simplifier/simp_lemmas.cpp index aa6c20c4b9..ba43ecb879 100644 --- a/src/library/tactic/simplifier/simp_lemmas.cpp +++ b/src/library/tactic/simplifier/simp_lemmas.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "kernel/instantiate.h" #include "library/trace.h" +#include "library/reducible.h" #include "library/num.h" #include "library/cache_helper.h" #include "library/scoped_ext.h" @@ -31,32 +32,7 @@ Author: Leonardo de Moura #include "library/tactic/simplifier/simp_lemmas.h" namespace lean { - -/* Caching */ -struct simp_lemma_cache { - typedef name_hash_map cache; - - environment m_env; - cache m_simp_lemma_cache; - cache m_congr_lemma_cache; - - simp_lemma_cache(environment const & env): m_env(env) {} - environment const & env() const { return m_env; } - - cache & simp_cache() { return m_simp_lemma_cache; } - cache & congr_cache() { return m_congr_lemma_cache; } -}; - -typedef cache_compatibility_helper simp_lemma_cache_helper; - -MK_THREAD_LOCAL_GET_DEF(simp_lemma_cache_helper, get_slch); - -simp_lemma_cache & get_simp_lemma_cache_for(type_context const & ctx) { - return get_slch().get_cache_for(ctx); -} - /* Validation */ - LEAN_THREAD_VALUE(bool, g_throw_ex, false); void validate_simp(type_context & tctx, name const & n); void validate_congr(type_context & tctx, name const & n); @@ -72,7 +48,6 @@ void on_add_congr_lemma(environment const & env, name const & c, bool) { } /* Getters/checkers */ - static void report_failure(sstream const & strm) { if (g_throw_ex){ throw exception(strm); @@ -288,7 +263,8 @@ simp_lemmas add_poly(type_context & tctx, simp_lemmas const & s, name const & id return add_core(tmp_tctx, s, id, priority); } -simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority) { +simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, + unsigned priority) { tmp_type_context tmp_tctx(tctx); return add_core(tmp_tctx, s, id, list(), e, h, priority); } @@ -574,62 +550,170 @@ format simp_lemmas::pp(formatter const & fmt) const { return pp(fmt, format(), true, true); } -simp_lemmas get_simp_lemmas_for_attr(simp_lemma_cache & sl_cache, type_context & tctx, name const & simp_attr) { - auto it = sl_cache.simp_cache().find(simp_attr); - if (it != sl_cache.simp_cache().end()) - return it->second; - - auto const & attr = get_attribute(tctx.env(), simp_attr); - simp_lemmas r; +simp_lemmas get_simp_lemmas_from_attribute(type_context & ctx, name const & attr_name, simp_lemmas result) { + auto const & attr = get_attribute(ctx.env(), attr_name); buffer simp_lemmas; - attr.get_instances(tctx.env(), simp_lemmas); + attr.get_instances(ctx.env(), simp_lemmas); unsigned i = simp_lemmas.size(); while (i > 0) { i--; name const & id = simp_lemmas[i]; - tmp_type_context tmp_tctx(tctx); - r = add_core(tmp_tctx, r, id, attr.get_prio(tctx.env(), id)); + // TODO(Leo): fix the following hack + tmp_type_context tmp_tctx(ctx); + result = add_core(tmp_tctx, result, id, attr.get_prio(ctx.env(), id)); } - sl_cache.simp_cache().insert({simp_attr, r}); - return r; + return result; } -simp_lemmas get_congr_lemmas_for_attr(simp_lemma_cache & sl_cache, type_context & tctx, name const & congr_attr) { - auto it = sl_cache.congr_cache().find(congr_attr); - if (it != sl_cache.congr_cache().end()) - return it->second; - - auto const & attr = get_attribute(tctx.env(), congr_attr); - simp_lemmas r; +simp_lemmas get_congr_lemmas_from_attribute(type_context & ctx, name const & attr_name, simp_lemmas result) { + auto const & attr = get_attribute(ctx.env(), attr_name); buffer congr_lemmas; - attr.get_instances(tctx.env(), congr_lemmas); + attr.get_instances(ctx.env(), congr_lemmas); unsigned i = congr_lemmas.size(); while (i > 0) { i--; name const & id = congr_lemmas[i]; - tmp_type_context tmp_tctx(tctx); - r = add_congr_core(tmp_tctx, r, id, attr.get_prio(tctx.env(), id)); + tmp_type_context tmp_tctx(ctx); + result = add_congr_core(tmp_tctx, result, id, attr.get_prio(ctx.env(), id)); } - sl_cache.congr_cache().insert({congr_attr, r}); - return r; + return result; } -simp_lemmas get_simp_lemmas(type_context & tctx, buffer const & simp_attrs, buffer const & congr_attrs) { - simp_lemma_cache & sl_cache = get_simp_lemma_cache_for(tctx); - simp_lemmas r; +struct simp_lemmas_config { + std::vector m_simp_attrs; + std::vector m_congr_attrs; +}; - // Optimization for the case when there is only one simp attr - // (we avoid the redundant head_map_prio inserts) - if (simp_attrs.size() > 0) - r = get_simp_lemmas_for_attr(sl_cache, tctx, simp_attrs[0]); +static std::vector * g_simp_lemmas_configs = nullptr; +static name_map * g_name2simp_token = nullptr; +static simp_lemmas_token g_default_token; - for (unsigned i = 1; i < simp_attrs.size(); ++i) - r = join(r, get_simp_lemmas_for_attr(sl_cache, tctx, simp_attrs[i])); +simp_lemmas_token register_simp_attribute(name const & user_name, std::initializer_list const & simp_attrs, std::initializer_list const & congr_attrs) { + simp_lemmas_config cfg; + for (name const & attr_name : simp_attrs) { + cfg.m_simp_attrs.push_back(attr_name); + if (!is_system_attribute(attr_name)) { + register_system_attribute(basic_attribute::with_check(attr_name, "simplification lemma", on_add_simp_lemma)); + } + } + for (name const & attr_name : congr_attrs) { + cfg.m_congr_attrs.push_back(attr_name); + if (!is_system_attribute(attr_name)) { + register_system_attribute(basic_attribute::with_check(attr_name, "congruence lemma", on_add_congr_lemma)); + } + } + simp_lemmas_token tk = g_simp_lemmas_configs->size(); + g_simp_lemmas_configs->push_back(cfg); + g_name2simp_token->insert(user_name, tk); + return tk; +} - for (unsigned i = 0; i < congr_attrs.size(); ++i) - r = join(r, get_congr_lemmas_for_attr(sl_cache, tctx, congr_attrs[i])); +simp_lemmas_config const & get_simp_lemmas_config(simp_lemmas_token tk) { + lean_assert(tk < g_simp_lemmas_configs->size()); + return (*g_simp_lemmas_configs)[tk]; +} - return r; +/* This is the cache for internally used simp_lemma collections */ +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) {} + }; + std::vector m_entries[4]; + +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++) { + auto & cfg = get_simp_lemmas_config(tk); + m_entries[midx].emplace_back(env); + auto & entry = m_entries[midx].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) { + lean_trace("simp_lemmas_cache", tout() << "make simp lemmas [" << tk << "]\n";); + type_context ctx(env, m); + C.m_env = env; + auto & cfg = get_simp_lemmas_config(tk); + simp_lemmas lemmas; + unsigned i = 0; + for (name const & attr_name : cfg.m_simp_attrs) { + lemmas = get_simp_lemmas_from_attribute(ctx, attr_name, lemmas); + C.m_fingerprints[i] = get_attribute_fingerprint(env, attr_name); + i++; + } + for (name const & attr_name : cfg.m_congr_attrs) { + lemmas = get_congr_lemmas_from_attribute(ctx, attr_name, lemmas); + C.m_fingerprints[i] = get_attribute_fingerprint(env, attr_name); + i++; + } + C.m_lemmas = lemmas; + C.m_reducibility_fingerprint = get_reducibility_fingerprint(env); + return lemmas; + } + + simp_lemmas lemmas_of(entry const & C, simp_lemmas_token tk) { + lean_trace("simp_lemmas_cache", tout() << "reusing cached simp lemmas [" << tk << "]\n";); + return *C.m_lemmas; + } + + 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) { + if (get_attribute_fingerprint(env, attr_name) != C.m_fingerprints[i]) + return false; + i++; + } + for (name const & attr_name : cfg.m_congr_attrs) { + if (get_attribute_fingerprint(env, attr_name) != C.m_fingerprints[i]) + return false; + i++; + } + return true; + } + + simp_lemmas get(environment const & env, transparency_mode m, 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 (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 lemmas_of(C, tk); + } +}; + +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_default_simp_lemmas(environment const & env, transparency_mode m) { + return get_simp_lemmas(env, m, g_default_token); +} + +simp_lemmas get_simp_lemmas(environment const & env, transparency_mode m, name const & tk_name) { + if (simp_lemmas_token const * tk = g_name2simp_token->find(tk_name)) + return get_simp_lemmas(env, m, *tk); + else + throw exception(sstream() << "unknown simp_lemmas collection '" << tk_name << "'"); } struct vm_simp_lemmas : public vm_external { @@ -649,13 +733,11 @@ 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 tactic_mk_simp_lemmas(vm_obj const & m, vm_obj const & sattrs, vm_obj const & cattrs, vm_obj const & s) { +vm_obj tactic_mk_default_simp_lemmas(vm_obj const & m, vm_obj const & s) { LEAN_TACTIC_TRY; - type_context ctx = mk_type_context_for(s, m); - buffer simp_attrs, congr_attrs; - to_buffer(to_list_name(sattrs), simp_attrs); - to_buffer(to_list_name(cattrs), congr_attrs); - return mk_tactic_success(to_obj(get_simp_lemmas(ctx, simp_attrs, congr_attrs)), to_tactic_state(s)); + environment const & env = to_tactic_state(s).env(); + simp_lemmas r = get_default_simp_lemmas(env, to_transparency_mode(m)); + return mk_tactic_success(to_obj(r), to_tactic_state(s)); LEAN_TACTIC_CATCH(to_tactic_state(s)); } @@ -827,17 +909,21 @@ static vm_obj tactic_simp_lemmas_apply(vm_obj const & m, vm_obj const & sls, vm_ } void initialize_simp_lemmas() { + g_simp_lemmas_configs = new std::vector(); + g_name2simp_token = new name_map(); + g_default_token = register_simp_attribute("default", {"simp"}, {"congr"}); + register_trace_class("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({"tactic", "mk_simp_lemmas_core"}), tactic_mk_simp_lemmas); + DECLARE_VM_BUILTIN(name({"tactic", "mk_default_simp_lemmas_core"}), tactic_mk_default_simp_lemmas); DECLARE_VM_BUILTIN(name({"tactic", "simp_lemmas_insert_core"}), tactic_simp_lemmas_insert); DECLARE_VM_BUILTIN(name({"tactic", "simp_lemmas_insert_constant_core"}), tactic_simp_lemmas_insert_constant); DECLARE_VM_BUILTIN(name({"tactic", "simp_lemmas_apply_core"}), tactic_simp_lemmas_apply); - register_system_attribute(basic_attribute::with_check("simp", "simplification lemma", on_add_simp_lemma)); - register_system_attribute(basic_attribute::with_check("congr", "congruence lemma", on_add_congr_lemma)); } void finalize_simp_lemmas() { + delete g_simp_lemmas_configs; + delete g_name2simp_token; } } diff --git a/src/library/tactic/simplifier/simp_lemmas.h b/src/library/tactic/simplifier/simp_lemmas.h index 22620205f1..80c500031a 100644 --- a/src/library/tactic/simplifier/simp_lemmas.h +++ b/src/library/tactic/simplifier/simp_lemmas.h @@ -141,7 +141,17 @@ public: format pp(formatter const & fmt) const; }; -simp_lemmas get_simp_lemmas(type_context & tctx, buffer const & simp_attrs, buffer const & congr_attrs); +typedef unsigned simp_lemmas_token; + +/* Create a token for accessing a simp_lemmas that contains the given simp and attributes. + The attributes are automatically registered in the system IF they have not already been registered. */ +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 add_poly(type_context & tctx, simp_lemmas const & s, name const & id, unsigned priority); simp_lemmas add(type_context & tctx, simp_lemmas const & s, name const & id, expr const & e, expr const & h, unsigned priority); diff --git a/tests/lean/run/rw_set1.lean b/tests/lean/run/rw_set1.lean index 3ba26e919a..37f971f97c 100644 --- a/tests/lean/run/rw_set1.lean +++ b/tests/lean/run/rw_set1.lean @@ -13,5 +13,5 @@ namespace foo attribute [simp] nat.add_comm open nat print "---------" - print [simp] simp + print [simp] default end foo diff --git a/tests/lean/run/rw_set3.lean b/tests/lean/run/rw_set3.lean index 25ead28123..e96522db7f 100644 --- a/tests/lean/run/rw_set3.lean +++ b/tests/lean/run/rw_set3.lean @@ -9,6 +9,6 @@ axiom bla : ∀ x, f x = 2 attribute [simp] foo attribute [simp] bla -print [simp] simp +print [simp] default example : f 5 = 2 := by simp diff --git a/tests/lean/run/rw_set4.lean b/tests/lean/run/rw_set4.lean index a8235b76ab..b562b0c296 100644 --- a/tests/lean/run/rw_set4.lean +++ b/tests/lean/run/rw_set4.lean @@ -5,7 +5,7 @@ theorem forall_congr_prop_eq {P₁ P₂ Q₁ Q₂ : Prop} : P₁ = P₂ → (P₂ → Q₁ = Q₂) → (P₁ → Q₁) = (P₂ → Q₂) := sorry -print [congr] congr +print [congr] default example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by (simp >> intros >> reflexivity) example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by (simp >> intros >> reflexivity) diff --git a/tests/lean/run/simp_ext1.lean b/tests/lean/run/simp_ext1.lean deleted file mode 100644 index b5bcceec41..0000000000 --- a/tests/lean/run/simp_ext1.lean +++ /dev/null @@ -1,23 +0,0 @@ -open list tactic option -constants (A : Type.{1}) (x y z : A) (Hy : x = y) (Hz : y = z) -constants (f₁ : A → A) (f₂ : A → A → A) - -meta definition simp_x_to_y : tactic unit := mk_eq_simp_ext $ - λ e, do res ← mk_const `y, - pf ← mk_const `Hy, - return (res, pf) - -meta definition simp_y_to_z : tactic unit := mk_eq_simp_ext $ - λ e, do res ← mk_const `z, - pf ← mk_const `Hz, - return (res, pf) - -register_simp_ext x simp_x_to_y -register_simp_ext y simp_y_to_z - -print [simp_ext] - -example : x = z := by simp -example : f₁ x = f₁ y := by simp -example : f₁ (f₂ x y) = f₁ (f₂ z z) := by simp -example : f₁ (f₂ x y) = f₁ (f₂ y x) := by simp diff --git a/tests/lean/run/simplifier_custom_relations.lean b/tests/lean/run/simplifier_custom_relations.lean index 42dfca51b7..cf0fa9a555 100644 --- a/tests/lean/run/simplifier_custom_relations.lean +++ b/tests/lean/run/simplifier_custom_relations.lean @@ -20,8 +20,8 @@ constants (x y z : A) (f g h : A → A) attribute [simp] H₁ H₂ attribute [congr] Hf Hg Hh -print [simp] simp -print [congr] congr +print [simp] default +print [congr] default meta definition relsimp_core (e : expr) : tactic (expr × expr) := do simp_lemmas ← mk_simp_lemmas,