refactor(library/normalize): remove unfold and unfold_full attributes

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
 

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
 

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₁)
 

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]

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<unsigned> 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);
     }

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);
 }

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);
 }

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);
 }

src/library/constructions/projection.cpp

@@ -257,7 +257,6 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
                                                             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);

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);
 }

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<indices_attribute const &>(get_system_attribute("unfold"));
-}
-environment add_unfold_hint(environment const & env, name const & n, list<unsigned> const & idxs, bool persistent) {
-    return get_unfold_attribute().set(env, get_dummy_ios(), n, LEAN_DEFAULT_PRIORITY, idxs, persistent);
-}
-list<unsigned> 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<unsigned>();
-}
-
-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<unsigned> has_unfold_hint(expr const & f) {
-        if (!is_constant(f))
-            return list<unsigned>();
-        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<expr> 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<expr> 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))

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<bool(expr const&)> 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<unsigned> 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<unsigned> 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);

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
 

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]

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