From 81a30a69d2c6992e72e025f701b2fce598ad2bb2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Sep 2016 08:40:58 -0700 Subject: [PATCH] refactor(library/normalize): remove unfold and unfold_full attributes --- library/init/function.lean | 20 ++++----- library/init/logic.lean | 2 +- library/init/nat.lean | 1 - library/init/quot.lean | 9 ---- src/frontends/lean/structure_cmd.cpp | 2 - src/library/constructions/brec_on.cpp | 4 -- src/library/constructions/cases_on.cpp | 3 -- src/library/constructions/no_confusion.cpp | 2 - src/library/constructions/projection.cpp | 1 - src/library/constructions/rec_on.cpp | 2 - src/library/normalize.cpp | 51 ---------------------- src/library/normalize.h | 20 --------- tests/lean/attributes.lean | 22 ---------- tests/lean/attributes.lean.expected.out | 17 +------- tests/lean/run/808.lean | 1 - 15 files changed, 13 insertions(+), 144 deletions(-) diff --git a/library/init/function.lean b/library/init/function.lean index de37ccc57a..3b71a7ae54 100644 --- a/library/init/function.lean +++ b/library/init/function.lean @@ -12,11 +12,11 @@ notation f ` $ `:1 a:1 := f a variables {A : Type} {B : Type} {C : Type} {D : Type} {E : Type} -attribute [inline, reducible, unfold_full] +attribute [inline, reducible] definition function.comp (f : B → C) (g : A → B) : A → C := λx, f (g x) -attribute [inline, reducible, unfold_full] +attribute [inline, reducible] definition function.dcomp {B : A → Type} {C : Π {x : A}, B x → Type} (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) := λx, f (g x) @@ -26,28 +26,28 @@ infixr ` ∘' `:80 := function.dcomp namespace function -attribute [reducible, unfold_full] +attribute [reducible] definition comp_right (f : B → B → B) (g : A → B) : B → A → B := λ b a, f b (g a) -attribute [reducible, unfold_full] +attribute [reducible] definition comp_left (f : B → B → B) (g : A → B) : A → B → B := λ a b, f (g a) b -attribute [reducible, unfold_full] +attribute [reducible] definition on_fun (f : B → B → C) (g : A → B) : A → A → C := λx y, f (g x) (g y) -attribute [reducible, unfold_full] +attribute [reducible] definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E := λx y, op (f x y) (g x y) -attribute [reducible, unfold_full] +attribute [reducible] definition const (B : Type) (a : A) : B → A := λx, a -attribute [reducible, unfold_full] +attribute [reducible] definition swap {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y := λy x, f x y @@ -55,11 +55,11 @@ attribute [reducible] definition app {B : A → Type} (f : Πx, B x) (x : A) : B x := f x -attribute [reducible, unfold_full] +attribute [reducible] definition curry : (A × B → C) → A → B → C := λ f a b, f (a, b) -attribute [reducible, unfold 5] +attribute [reducible] definition uncurry : (A → B → C) → (A × B → C) := λ f p, match p with (a, b) := f a b end diff --git a/library/init/logic.lean b/library/init/logic.lean index 80cde00907..eb791a4bbf 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -7,7 +7,7 @@ prelude import init.datatypes set_option simplify.theory false -attribute [reducible, unfold_full] +attribute [reducible] definition id {A : Type} (a : A) : A := a diff --git a/library/init/nat.lean b/library/init/nat.lean index aa127eb940..90d44271dc 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -29,7 +29,6 @@ namespace nat attribute [instance, priority nat.prio] definition nat_has_lt : has_lt nat := has_lt.mk nat.lt - attribute [unfold 1] definition pred (a : nat) : nat := nat.cases_on a zero (λ a₁, a₁) diff --git a/library/init/quot.lean b/library/init/quot.lean index 63132690ef..131e95b0d9 100644 --- a/library/init/quot.lean +++ b/library/init/quot.lean @@ -186,15 +186,6 @@ namespace quot end quot attribute quot.mk [constructor] -attribute quot.lift_on [unfold 4] -attribute quot.rec [unfold 6] -attribute quot.rec_on [unfold 4] -attribute quot.hrec_on [unfold 4] -attribute quot.rec_on_subsingleton [unfold 5] -attribute quot.lift₂ [unfold 8] -attribute quot.lift_on₂ [unfold 6] -attribute quot.hrec_on₂ [unfold 6] -attribute quot.rec_on_subsingleton₂ [unfold 7] open decidable attribute [instance] diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 94aac23f58..55325c8d90 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -750,8 +750,6 @@ struct structure_cmd_fn { reducibility_hints::mk_abbreviation()); m_env = module::add(m_env, check(m_env, new_decl)); m_env = set_reducible(m_env, n, reducible_status::Reducible, true); - if (list idx = has_unfold_hint(m_env, rec_on_name)) - m_env = add_unfold_hint(m_env, n, idx, true); save_def_info(n); add_alias(n); } diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 731c45c913..42d0f1b42b 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -147,8 +147,6 @@ static environment mk_below(environment const & env, name const & n, bool ibelow reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true); - if (!ibelow) - new_env = add_unfold_hint(new_env, below_name, nparams + nindices + ntypeformers, true); return add_protected(new_env, below_name); } @@ -331,8 +329,6 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible, true); - if (!ind) - new_env = add_unfold_hint(new_env, brec_on_name, nparams + nindices + ntypeformers, true); new_env = add_aux_recursor(new_env, brec_on_name); return add_protected(new_env, brec_on_name); } diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp index bbc2d9feb1..6c2163f275 100644 --- a/src/library/constructions/cases_on.cpp +++ b/src/library/constructions/cases_on.cpp @@ -128,8 +128,6 @@ environment mk_cases_on(environment const & env, name const & n) { // Add indices and major-premise to rec_params for (unsigned i = 0; i < num_idx_major; i++) cases_on_params.push_back(rec_params[num_params + num_types + num_minors + i]); - unsigned cases_on_major_idx = cases_on_params.size() - 1; - // Add minor premises to rec_params and rec_args i = num_params + num_types; for (auto const & d : idecls) { @@ -182,7 +180,6 @@ environment mk_cases_on(environment const & env, name const & n) { reducibility_hints::mk_abbreviation()); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible, true); - new_env = add_unfold_hint(new_env, cases_on_name, cases_on_major_idx, false); new_env = add_aux_recursor(new_env, cases_on_name); return add_protected(new_env, cases_on_name); } diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp index 2d585eef50..396e041c01 100644 --- a/src/library/constructions/no_confusion.cpp +++ b/src/library/constructions/no_confusion.cpp @@ -202,7 +202,6 @@ environment mk_no_confusion(environment const & env, name const & n) { no_confusion_type_args.push_back(P); no_confusion_type_args.push_back(v1); no_confusion_type_args.push_back(v1); - unsigned unfold_hint_idx = no_confusion_type_args.size(); expr no_confusion_type_app = mk_app(mk_constant(no_confusion_type_decl.get_name(), ls), no_confusion_type_args); expr type_former = Fun(type_former_args, no_confusion_type_app); // create cases_on @@ -274,7 +273,6 @@ environment mk_no_confusion(environment const & env, name const & n) { reducibility_hints::mk_abbreviation()); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible, true); - new_env = add_unfold_hint(new_env, no_confusion_name, unfold_hint_idx, true); new_env = add_no_confusion(new_env, no_confusion_name); return add_protected(new_env, no_confusion_name); } diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp index 6dbd5d3917..588dc3c690 100644 --- a/src/library/constructions/projection.cpp +++ b/src/library/constructions/projection.cpp @@ -257,7 +257,6 @@ environment mk_projections(environment const & env, name const & n, buffer reducibility_hints::mk_abbreviation()); new_env = module::add(new_env, check(new_env, new_d)); new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true); - new_env = add_unfold_hint(new_env, proj_name, nparams, true); new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit); expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); intro_type = instantiate(binding_body(intro_type), proj); diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp index a4fcc1fe3f..2158cfa43e 100644 --- a/src/library/constructions/rec_on.cpp +++ b/src/library/constructions/rec_on.cpp @@ -46,7 +46,6 @@ environment mk_rec_on(environment const & env, name const & n) { new_locals.push_back(locals[i]); for (unsigned i = 0; i < idx_major_sz; i++) new_locals.push_back(locals[AC_sz + minor_sz + i]); - unsigned rec_on_major_idx = new_locals.size() - 1; for (unsigned i = 0; i < minor_sz; i++) new_locals.push_back(locals[AC_sz + i]); expr rec_on_type = Pi(new_locals, rec_type); @@ -59,7 +58,6 @@ environment mk_rec_on(environment const & env, name const & n) { check(env, mk_definition_inferring_trusted(env, rec_on_name, rec_decl.get_univ_params(), rec_on_type, rec_on_val, reducibility_hints::mk_abbreviation()))); new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible, true); - new_env = add_unfold_hint(new_env, rec_on_name, rec_on_major_idx, true); new_env = add_aux_recursor(new_env, rec_on_name); return add_protected(new_env, rec_on_name); } diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 957955f1a9..521e3fc1de 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -21,41 +21,11 @@ Author: Leonardo de Moura #include "library/old_type_checker.h" namespace lean { -/** - \brief unfold hints instruct the normalizer (and simplifier) that - a function application. We have two kinds of hints: - - [unfold] (f a_1 ... a_i ... a_n) should be unfolded - when argument a_i is a constructor. - - [unfold-full] (f a_1 ... a_i ... a_n) should be unfolded when it is fully applied. - - constructor (f ...) should be unfolded when it is the major premise of a recursor-like operator -*/ - -static indices_attribute const & get_unfold_attribute() { - return static_cast(get_system_attribute("unfold")); -} -environment add_unfold_hint(environment const & env, name const & n, list const & idxs, bool persistent) { - return get_unfold_attribute().set(env, get_dummy_ios(), n, LEAN_DEFAULT_PRIORITY, idxs, persistent); -} -list has_unfold_hint(environment const & env, name const & d) { - if (auto data = get_unfold_attribute().get(env, d)) - return data->m_idxs; - else - return list(); -} - -bool has_unfold_full_hint(environment const & env, name const & d) { - return has_attribute(env, "unfold_full", d); -} - bool has_constructor_hint(environment const & env, name const & d) { return has_attribute(env, "constructor", d); } void initialize_normalize() { - register_system_attribute( - indices_attribute("unfold", "unfold definition when the given positions are constructors")); - register_system_attribute(basic_attribute("unfold_full", - "instructs normalizer (and simplifier) that function application (f a_1 ... a_n) should be unfolded when it is fully applied")); register_system_attribute(basic_attribute("constructor", "instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator")); } @@ -87,16 +57,6 @@ class normalize_fn { return update_binding(e, d, b); } - list has_unfold_hint(expr const & f) { - if (!is_constant(f)) - return list(); - return ::lean::has_unfold_hint(env(), const_name(f)); - } - - bool has_unfold_full_hint(expr const & f) { - return is_constant(f) && ::lean::has_unfold_full_hint(env(), const_name(f)); - } - optional is_constructor_like(expr const & e) { if (is_constructor_app(env(), e)) return some_expr(e); @@ -158,17 +118,6 @@ class normalize_fn { modified = true; a = new_a; } - if (has_unfold_full_hint(f)) { - if (!is_pi(m_full_tc.whnf(m_full_tc.infer(e).first).first)) { - if (optional r = unfold_app(env(), mk_rev_app(f, args))) { - return normalize(*r); - } - } - } - if (auto idxs = has_unfold_hint(f)) { - if (auto r = unfold_recursor_like(f, idxs, args)) - return *r; - } if (is_constant(f)) { if (auto idx = inductive::get_elim_major_idx(env(), const_name(f))) { if (auto r = unfold_recursor_major(f, *idx, args)) diff --git a/src/library/normalize.h b/src/library/normalize.h index 23f2b5511a..0c956b6b85 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -32,26 +32,6 @@ expr normalize(old_type_checker & tc, expr const & e, constraint_seq & cs, bool expr normalize(old_type_checker & tc, expr const & e, std::function const & pred, // NOLINT constraint_seq & cs, bool eta = false); -/** \brief [unfold] hint instructs the normalizer (and simplifier) that - a function application (f a_1 ... a_i ... a_n) should be unfolded - when argument a_i is a constructor. - - The constant will be unfolded even if it the whnf procedure did not unfolded it. - - Of course, kernel opaque constants are not unfolded. -*/ -environment add_unfold_hint(environment const & env, name const & n, list const & idxs, bool persistent); -inline environment add_unfold_hint(environment const & env, name const & n, unsigned idx, bool persistent) { - return add_unfold_hint(env, n, to_list(idx), persistent); -} -/** \brief Retrieve the hint added with the procedure add_unfold_hint. */ -list has_unfold_hint(environment const & env, name const & d); - -/** \brief [unfold-full] hint instructs normalizer (and simplifier) that function application - (f a_1 ... a_n) should be unfolded when it is fully applied */ -bool has_unfold_full_hint(environment const & env, name const & d); - - /** \brief unfold-m hint instructs normalizer (and simplifier) that function application (f ...) should be unfolded when it is the major premise of a constructor like operator */ bool has_constructor_hint(environment const & env, name const & d); diff --git a/tests/lean/attributes.lean b/tests/lean/attributes.lean index be0d3f7cb0..224c9de088 100644 --- a/tests/lean/attributes.lean +++ b/tests/lean/attributes.lean @@ -1,27 +1,5 @@ definition foo (A : Type) := A -local attribute [-unfold] foo - -local attribute [unfold 1] foo - -attribute [-unfold] - -section - local attribute [-unfold] foo - print foo -end -print foo - -local attribute [-unfold] foo -print foo - -local attribute [-unfold] foo - -local attribute [unfold] foo -print foo - --- - local attribute [reducible] foo local attribute [-reducible] foo -- use [semireducible] instead diff --git a/tests/lean/attributes.lean.expected.out b/tests/lean/attributes.lean.expected.out index f3f0b31ad5..2afd7af8d7 100644 --- a/tests/lean/attributes.lean.expected.out +++ b/tests/lean/attributes.lean.expected.out @@ -1,15 +1,2 @@ -attributes.lean:3:0: error: cannot remove attribute [unfold]: no prior declaration on foo -attributes.lean:7:11: error: cannot remove attribute globally (solution: use 'local attribute') -definition foo : Type → Type := -λ A, A -attribute [unfold 1] -definition foo : Type → Type := -λ A, A -definition foo : Type → Type := -λ A, A -attributes.lean:18:0: error: cannot remove attribute [unfold]: no prior declaration on foo -attribute [unfold] -definition foo : Type → Type := -λ A, A -attributes.lean:26:0: error: cannot remove attribute [reducible] -attributes.lean:30:0: error: cannot remove attribute [instance] +attributes.lean:4:0: error: cannot remove attribute [reducible] +attributes.lean:8:0: error: cannot remove attribute [instance] diff --git a/tests/lean/run/808.lean b/tests/lean/run/808.lean index c493ea77f2..0faaab7952 100644 --- a/tests/lean/run/808.lean +++ b/tests/lean/run/808.lean @@ -7,5 +7,4 @@ postfix [priority 1] `y`:max := eq attribute [instance, priority 1] definition foo : inhabited nat := inhabited.mk nat.zero -attribute [unfold 1] definition bar := @eq