refactor(tactic/ext): simplify ext attribute (#8785)

This simplifies the `ext` attribute from taking a list with `*`, `(->)` and names to just `@[ext]` or `@[ext ident]`. The `(->)` option is only used once, in the file that declares the `ext` attribute itself, so it's not worth the parser complexity. The ability to remove attributes with `@[ext -foo]` is removed, but I don't think it was tested because it was never used and doesn't work anyway.

Also fixes an issue with ext attributes being quadratic (in the number of ext attributes applied), and also makes `ext` attributes remove themselves (the real work of ext attributes is done by two internal attributes `_ext_core` and `_ext_lemma_core`), so that they don't pollute `#print` output. Before:
```lean
#print funext

@[_ext_lemma_core, ext list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_numeral (unsigned.of_nat' (has_zero.zero.{0} nat nat.has_zero)) name.anonymous))) (list.cons.{0} ext_param_type (sum.inr.{0 0} (option.{0} name) (option.{0} name) (option.some.{0} name (name.mk_string "thunk" name.anonymous))) (list.nil.{0} ext_param_type)), intro!]
theorem funext : ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : Π (x : α), β x}, (∀ (x : α), f₁ x = f₂ x) → f₁ = f₂ :=
```
After:
```lean
#print funext

@[_ext_lemma_core, intro!]
theorem funext : ∀ {α : Sort u} {β : α → Sort v} {f₁ f₂ : Π (x : α), β x}, (∀ (x : α), f₁ x = f₂ x) → f₁ = f₂ :=
```

Author: digama0

src/tactic/ext.lean

@@ -127,16 +127,6 @@ meta def get_ext_subject : expr → tactic name
 
 open native
 
-@[reducible] def ext_param_type := option name ⊕ option name
-
-meta def opt_minus : lean.parser (option name → ext_param_type) :=
-sum.inl <$ tk "-" <|> pure sum.inr
-
-meta def ext_param :=
-opt_minus <*> ( name.mk_numeral 0 name.anonymous <$ brackets "(" ")" (tk "→" <|> tk "->") <|>
-                none <$  tk "*" <|>
-                some <$> ident )
-
 meta def saturate_fun : name → tactic expr
 | (name.mk_numeral 0 name.anonymous) :=
 do v₀ ← mk_mvar,
@@ -180,7 +170,7 @@ library_note "user attribute parameters"
 For performance reasons, the parameters of the `@[ext]` attribute are stored
 in two auxiliary attributes:
 ```lean
-attribute [ext [thunk]] funext
+attribute [ext thunk] funext
 
 -- is turned into
 attribute [_ext_core (@id name @funext)] thunk
@@ -202,11 +192,9 @@ private meta def ext_attr_core : user_attribute (name_map name) name :=
   descr := "(internal attribute used by ext)",
   cache_cfg := {
     dependencies := [],
-    mk_cache := λ ns, do
-      attrs ← ns.mmap (λ n, do
-        ext_l ← ext_attr_core.get_param_untyped n,
-        pure (n, ext_l.app_arg.const_name)),
-      pure $ rb_map.of_list attrs },
+    mk_cache := λ ns, ns.mfoldl (λ m n, do
+      ext_l ← ext_attr_core.get_param_untyped n,
+      pure (m.insert n ext_l.app_arg.const_name)) mk_name_map },
   parser := failure }
 
 end performance_hack
@@ -231,6 +219,11 @@ Returns the extensionality lemmas in the environment, as a list of lemma names.
 meta def get_ext_lemma_names : tactic (list name) :=
 attribute.get_instances ext_lemma_attr_core.name
 
+/-- Marks `lem` as an extensionality lemma corresponding to type constructor `constr`;
+if `persistent` is true then this is a global attribute, else local. -/
+meta def add_ext_lemma (constr lem : name) (persistent : bool) : tactic unit :=
+ext_attr_core.set constr lem persistent >> ext_lemma_attr_core.set lem () persistent
+
 /--
 Tag lemmas of the form:
 
@@ -247,23 +240,7 @@ the lemma.  In some cases, the same lemma can be used to state the
 extensionality of multiple types that are definitionally equivalent.
 
 ```lean
-attribute [ext [(→),thunk,stream]] funext
-```
-
-Those parameters are cumulative. The following are equivalent:
-
-```lean
-attribute [ext [(→),thunk]] funext
-attribute [ext [stream]] funext
-```
-and
-```lean
-attribute [ext [(→),thunk,stream]] funext
-```
-
-One removes type names from the list for one lemma with:
-```lean
-attribute [ext [-stream,-thunk]] funext
+attribute [ext thunk, ext stream] funext
 ```
 
 Also, the following:
@@ -278,7 +255,7 @@ lemma my_collection.ext (a b : my_collection)
 is equivalent to
 
 ```lean
-@[ext *]
+@[ext my_collection]
 lemma my_collection.ext (a b : my_collection)
   (h : ∀ x, a.lookup x = b.lookup y) :
   a = b := ...
@@ -288,7 +265,7 @@ This allows us specify type synonyms along with the type
 that is referred to in the lemma statement.
 
 ```lean
-@[ext [*,my_type_synonym]]
+@[ext, ext my_type_synonym]
 lemma my_collection.ext (a b : my_collection)
   (h : ∀ x, a.lookup x = b.lookup y) :
   a = b := ...
@@ -316,27 +293,23 @@ x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z == y.z ∧ x.k = y.k
 
 -/
 @[user_attribute]
-meta def extensional_attribute : user_attribute unit (list ext_param_type) :=
+meta def extensional_attribute : user_attribute unit (option name) :=
 { name := `ext,
   descr := "lemmas usable by `ext` tactic",
-  parser := pure <$> ext_param <|> list_of ext_param <|> pure [],
-  after_set := some $ λ n prio b,
-    do ls ← extensional_attribute.get_param n,
-       e ← get_env,
-       n ← if (e.structure_fields n).is_some
-         then derive_struct_ext_lemma n
-         else pure n,
-       s ← mk_const n >>= infer_type >>= get_ext_subject,
-       let (rs,ls'') := if ls.empty
-                           then ([],[s])
-                           else ls.partition_map (sum.map (flip option.get_or_else s)
-                                                    (flip option.get_or_else s)),
-       ls''.mmap' (equiv_type_constr s),
-       ls' ← get_ext_lemmas,
-       let l := ls'' ∪ (ls'.to_list.filter $ λ l, prod.snd l = n).map prod.fst \ rs,
-       l.mmap' $ λ l, do
-        ext_attr_core.set l n b prio,
-        ext_lemma_attr_core.set n () b prio }
+  parser := optional ident,
+  before_unset := some $ λ _ _, pure (),
+  after_set := some $ λ n _ b, do
+    add ← extensional_attribute.get_param n,
+    unset_attribute `ext n,
+    e ← get_env,
+    n ← if (e.structure_fields n).is_some
+      then derive_struct_ext_lemma n
+      else pure n,
+    s ← mk_const n >>= infer_type >>= get_ext_subject,
+    match add with
+    | none := add_ext_lemma s n b
+    | some add := equiv_type_constr s add >> add_ext_lemma add n b
+    end }
 
 add_tactic_doc
 { name                     := "ext",
@@ -361,7 +334,13 @@ library_note "partially-applied ext lemmas"
 
 -- We mark some existing extensionality lemmas.
 attribute [ext] array.ext propext function.hfunext
-attribute [ext [(→),thunk]] _root_.funext
+attribute [ext thunk] _root_.funext
+
+-- This line is equivalent to:
+--   attribute [ext (→)] _root_.funext
+-- but (→) is not actually a binary relation with a constant at the head,
+-- so we use the special name [anon].0 to represent (→).
+run_cmd add_ext_lemma (name.mk_numeral 0 name.anonymous) ``_root_.funext tt
 
 -- We create some extensionality lemmas for existing structures.
 attribute [ext] ulift