From aa03dc03b4e213bea68c9a562b6b1417bb127d9d Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 21 Nov 2016 09:52:58 -0500 Subject: [PATCH] refactor(library/tactic/simp_lemmas): mark rfl-lemmas with a _refl_lemma attribute --- src/frontends/lean/definition_cmds.cpp | 40 +++++++++++--------------- src/library/tactic/eqn_lemmas.cpp | 6 +++- src/library/tactic/simp_lemmas.cpp | 30 +++++++++++++++---- src/library/tactic/simp_lemmas.h | 6 ++++ 4 files changed, 53 insertions(+), 29 deletions(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index d5f7125ced..a8711abf65 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -481,14 +481,6 @@ static void get_args_for_instantiating_lemma(unsigned arity, } } -/* Return true iff e is of the form (fun (a_1 : A_1) ... (a_n : A_n), eq.refl ...) */ -static bool is_refl_lemma(expr e) { - while (is_lambda(e)) - e = binding_body(e); - expr const & fn = get_app_fn(e); - return is_constant(fn, get_eq_refl_name()) || is_constant(fn, get_rfl_name()); -} - /** Given a declaration d defined as (fun (a_1 : A_1) ... (a_n : A_n), d._main a_1' ... a_n') @@ -555,22 +547,11 @@ static environment copy_equation_lemmas(environment const & env, name const & d_ new_eqn_type = locals.mk_pi(new_eqn_type); name new_eqn_name = d_name + eqn_suffix; expr new_eqn_value; - if (is_refl_lemma(eqn_decl->get_value())) { - /* Create a refl-lemma to make sure it can be used by the defeq simplifier. */ - type_context::tmp_locals extra_locals(ctx); - while (is_pi(eqn_type)) { - expr local = extra_locals.push_local_from_binding(eqn_type); - eqn_type = instantiate(binding_body(eqn_type), local); - } - expr lhs, rhs; - lean_verify(is_eq(eqn_type, lhs, rhs)); - new_eqn_value = mk_eq_refl(ctx, lhs); - new_eqn_value = extra_locals.mk_lambda(new_eqn_value); - } else { - new_eqn_value = mk_app(mk_constant(eqn_name, eqn_levels), args); - } + new_eqn_value = mk_app(mk_constant(eqn_name, eqn_levels), args); new_eqn_value = locals.mk_lambda(new_eqn_value); declaration new_decl = mk_theorem(new_eqn_name, d.get_univ_params(), new_eqn_type, new_eqn_value); + if (is_rfl_lemma(env, eqn_name)) + new_env = mark_rfl_lemma(env, new_eqn_name); new_env = module::add(new_env, check(new_env, new_decl, true)); new_env = add_eqn_lemma(new_env, new_eqn_name); i++; @@ -600,6 +581,8 @@ class proof_elaboration_task : public module_task { std::vector m_params; expr m_fn, m_val; elaborator::theorem_finalization_info m_finfo; + bool m_is_rfl_lemma; + expr m_final_type; metavar_context m_mctx; local_context m_lctx; @@ -610,11 +593,13 @@ public: options const & opts, buffer const & params, expr const & fn, expr const & val, elaborator::theorem_finalization_info const & finfo, + bool is_rfl_lemma, expr const & final_type, metavar_context const & mctx, local_context const & lctx, parser_pos_provider const & prov) : module_task(optional(prov.get_some_pos()), task_kind::elab), m_decl_env(decl_env), m_opts(opts), m_use_info_manager(get_global_info_manager() != nullptr), m_params(params.begin(), params.end()), m_fn(fn), m_val(val), m_finfo(finfo), + m_is_rfl_lemma(is_rfl_lemma), m_final_type(final_type), m_mctx(mctx), m_lctx(lctx), m_pos_provider(prov) {} void description(std::ostream & out) const override { @@ -636,6 +621,8 @@ public: std::tie(val, type) = elab.elaborate_with_type(m_val, mk_as_is(type)); buffer params; for (auto & e : m_params) params.push_back(e); finalize_theorem_proof(elab, params, val, m_finfo); + if (m_is_rfl_lemma && !is_rfl_lemma(m_final_type, val)) + throw exception("not a rfl-lemma, even though marked as rfl"); return inline_new_defs(m_decl_env, elab.env(), val); } catch (exception & ex) { message_builder error_msg(&m_pos_provider, tc, m_decl_env, get_global_ios(), @@ -723,6 +710,10 @@ public: } }; +static bool is_rfl_preexpr(expr const & e) { + return is_constant(e, get_rfl_name()); +} + environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modifiers modifiers, decl_attributes attrs) { buffer lp_names; buffer params; @@ -734,6 +725,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif bool is_example = (kind == def_cmd_kind::Example); bool is_instance = modifiers.m_is_instance; bool aux_lemmas = scope.gen_aux_lemmas(); + bool is_rfl = false; if (is_instance) attrs.set_attribute(p.env(), "instance"); std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance); @@ -750,6 +742,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif name c_name = mlocal_name(fn); pair env_n; if (kind == Theorem) { + is_rfl = is_rfl_preexpr(val); type = elab.elaborate_type(mlocal_type(fn)); elab.ensure_no_unassigned_metavars(type); expr new_fn = update_mlocal(fn, type); @@ -758,7 +751,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif finalize_theorem_type(elab, new_params, type, lp_names, thm_finfo); auto decl_env = elab.env(); auto elab_task = get_global_task_queue().submit( - decl_env, p.get_options(), new_params, new_fn, val, thm_finfo, + decl_env, p.get_options(), new_params, new_fn, val, thm_finfo, is_rfl, type, elab.mctx(), elab.lctx(), p.get_parser_pos_provider(header_pos)); env_n = declare_definition(p, elab.env(), kind, lp_names, c_name, type, opt_val, elab_task, modifiers, attrs, doc_string, header_pos); @@ -787,6 +780,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif } environment new_env = env_n.first; name c_real_name = env_n.second; + if (is_rfl) new_env = mark_rfl_lemma(new_env, c_real_name); new_env = add_local_ref(p, new_env, c_name, c_real_name, lp_names, params); if (eqns && aux_lemmas) { new_env = copy_equation_lemmas(new_env, c_real_name); diff --git a/src/library/tactic/eqn_lemmas.cpp b/src/library/tactic/eqn_lemmas.cpp index 5f09f9dad7..3399bfefaf 100644 --- a/src/library/tactic/eqn_lemmas.cpp +++ b/src/library/tactic/eqn_lemmas.cpp @@ -62,7 +62,11 @@ environment add_eqn_lemma_core(environment const & env, name const & eqn_lemma) } environment add_eqn_lemma(environment const & env, name const & eqn_lemma) { - environment new_env = add_eqn_lemma_core(env, eqn_lemma); + environment new_env = env; + auto d = env.get(eqn_lemma); + if (is_rfl_lemma(d.get_type(), d.get_value())) + new_env = mark_rfl_lemma(new_env, eqn_lemma); + new_env = add_eqn_lemma_core(new_env, eqn_lemma); return module::add(new_env, *g_eqn_lemmas_key, [=](environment const &, serializer & s) { s << eqn_lemma; }); } diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index 99a83b3e5b..0afba39534 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -685,11 +685,7 @@ static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name cons return new_s; } -static bool is_rfl_lemma(environment const & env, name const & cname) { - declaration const & d = env.get(cname); - if (!d.is_definition()) return false; - expr type = d.get_type(); - expr pf = d.get_value(); +bool is_rfl_lemma(expr type, expr pf) { while (is_pi(type)) { if (!is_lambda(pf)) return false; pf = binding_body(pf); @@ -701,7 +697,18 @@ static bool is_rfl_lemma(environment const & env, name const & cname) { return lhs != rhs; } +<<<<<<< HEAD static levels mk_tmp_levels_for(type_context & ctx, declaration const & d) { +======= +bool is_rfl_lemma(environment const & env, name const & cname) { + return get_refl_lemma_attribute().is_instance(env, cname); +} + +static simp_lemmas add_core(type_context & ctx, simp_lemmas const & s, name const & cname, unsigned priority) { + environment const & env = ctx.env(); + type_context::tmp_mode_scope scope(ctx); + declaration const & d = env.get(cname); +>>>>>>> refactor(library/tactic/simp_lemmas): mark rfl-lemmas with a _refl_lemma attribute buffer us; unsigned num_univs = d.get_num_univ_params(); for (unsigned i = 0; i < num_univs; i++) { @@ -1421,14 +1428,27 @@ vm_obj is_valid_simp_lemma(vm_obj const & m, vm_obj const & e, vm_obj const & s) to_tactic_state(s)); } +static name * g_refl_lemma_attr = nullptr; + +basic_attribute const & get_refl_lemma_attribute() { + return static_cast(get_system_attribute(*g_refl_lemma_attr)); +} + +environment mark_rfl_lemma(environment const & env, name const & cname) { + return get_refl_lemma_attribute().set(env, get_dummy_ios(), cname, LEAN_DEFAULT_PRIORITY, true); +} + void initialize_simp_lemmas() { g_dummy = new simp_lemma_cell(); g_simp_lemmas_configs = new std::vector(); g_name2simp_token = new name_map(); g_default_token = register_simp_attribute("default", {"simp", "wrapper_eq"}, {"congr"}); + g_refl_lemma_attr = new name{"_refl_lemma"}; register_trace_class("simp_lemmas"); register_trace_class("simp_lemmas_cache"); register_trace_class(name{"simp_lemmas", "failure"}); + register_system_attribute(basic_attribute( + *g_refl_lemma_attr, "marks that a lemma that can be used by the defeq simplifier")); DECLARE_VM_BUILTIN(name({"simp_lemmas", "mk"}), simp_lemmas_mk); DECLARE_VM_BUILTIN(name({"simp_lemmas", "join"}), simp_lemmas_join); diff --git a/src/library/tactic/simp_lemmas.h b/src/library/tactic/simp_lemmas.h index 860a665da8..b8072c9d40 100644 --- a/src/library/tactic/simp_lemmas.h +++ b/src/library/tactic/simp_lemmas.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "library/type_context.h" #include "library/head_map.h" #include "library/vm/vm.h" +#include "library/attribute_manager.h" namespace lean { enum class simp_lemma_kind { Refl, Simp, Congr }; @@ -148,6 +149,11 @@ expr refl_lemma_rewrite(type_context & ctx, expr const & e, simp_lemma const & s simp_lemmas const & to_simp_lemmas(vm_obj const & o); vm_obj to_obj(simp_lemmas const & s); +basic_attribute const & get_refl_lemma_attribute(); +bool is_rfl_lemma(expr type, expr pf); +bool is_rfl_lemma(environment const & env, name const & cname); +environment mark_rfl_lemma(environment const & env, name const & cname); + void initialize_simp_lemmas(); void finalize_simp_lemmas(); }