refactor(library/tactic/user_attribute): use attribute for registering attributes. naturally.

library/init/default.lean

@@ -9,8 +9,7 @@ import init.propext init.cc_lemmas init.funext init.category.combinators init.fu
 import init.util init.coe init.wf init.meta init.algebra init.data
 import init.native
 
+@[user_attribute]
 def debugger.attr : user_attribute :=
 { name  := `breakpoint,
   descr := "breakpoint for debugger" }
-
-run_cmd attribute.register `debugger.attr

library/init/meta/attribute.lean

@@ -15,7 +15,8 @@ structure user_attribute :=
 
 /- Registers a new user-defined attribute. The argument must be the name of a definition of type
    `user_attribute` or a sub-structure. -/
-meta constant attribute.register : name → command
+meta def attribute.register (decl : name) : command :=
+tactic.set_basic_attribute ``user_attribute decl tt
 
 meta structure caching_user_attribute (α : Type) extends user_attribute :=
 (mk_cache     : list _root_.name → tactic α)

library/tools/super/prover_state.lean

@@ -379,9 +379,9 @@ end
 
 meta def inference := derived_clause → prover unit
 meta structure inf_decl := (prio : ℕ) (inf : inference)
+@[user_attribute]
 meta def inf_attr : user_attribute :=
 ⟨ `super.inf, "inference for the super prover" ⟩
-run_cmd attribute.register `super.inf_attr
 
 meta def seq_inferences : list inference → inference
 | [] := λgiven, return ()

src/frontends/lean/definition_cmds.cpp

@@ -399,11 +399,12 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
         new_env = ensure_decl_namespaces(new_env, c_real_name);
     }
 
-    new_env = attrs.apply(new_env, p.ios(), c_real_name);
     new_env = compile_decl(p, new_env, c_name, c_real_name, pos);
     if (doc_string) {
         new_env = add_doc_string(new_env, c_real_name, *doc_string);
     }
+    // note: some attribute handlers rely on the new definition being compiled already
+    new_env = attrs.apply(new_env, p.ios(), c_real_name);
     return mk_pair(new_env, c_real_name);
 }
 

src/frontends/lean/notation_cmd.cpp

@@ -830,7 +830,7 @@ void initialize_notation_cmd() {
     register_system_attribute(basic_attribute::with_check(
             "parsing_only", "parsing-only notation declaration",
             [](environment const &, name const &, bool) {
-                throw exception("invalid '[parsing_only]' attribute can only be used in notation declarations");
+                throw exception("invalid '[parsing_only]' attribute, can only be used in notation declarations");
             }));
 }
 void finalize_notation_cmd() {

src/library/tactic/user_attribute.cpp

@@ -62,13 +62,13 @@ static environment update(environment const & env, user_attr_ext const & ext) {
 static environment add_user_attr(environment const & env, name const & d) {
     auto const & ty = env.get(d).get_type();
     if (!is_constant(ty, get_user_attribute_name()) && !is_constant(get_app_fn(ty), get_caching_user_attribute_name()))
-        throw exception("invalid attribute.register argument, must be name of a definition of type user_attribute");
+        throw exception("invalid [user_attribute], must be applied to definition of type user_attribute");
 
     vm_state vm(env, options());
     vm_obj o = vm.invoke(d, {});
     name const & n = to_name(cfield(o, 0));
     if (n.is_anonymous())
-        throw exception(sstream() << "invalid attribute.register, anonymous attribute names are not allowed");
+        throw exception(sstream() << "invalid user_attribute, anonymous attribute names are not allowed");
     if (is_attribute(env, n))
         throw exception(sstream() << "an attribute named [" << n << "] has already been registered");
     std::string descr = to_string(cfield(o, 1));
@@ -118,15 +118,6 @@ vm_obj attribute_get_instances(vm_obj const & vm_n, vm_obj const & vm_s) {
     return tactic::mk_success(to_obj(b), s);
 }
 
-vm_obj attribute_register(vm_obj const & vm_n, vm_obj const & vm_s) {
-    auto const & s = tactic::to_state(vm_s);
-    auto const & n = to_name(vm_n);
-    LEAN_TACTIC_TRY;
-    auto env = module::add_and_perform(s.env(), std::make_shared<user_attr_modification>(n));
-    return tactic::mk_success(set_env(s, env));
-    LEAN_TACTIC_CATCH(s);
-}
-
 vm_obj attribute_fingerprint(vm_obj const & vm_n, vm_obj const & vm_s) {
     auto const & s = tactic::to_state(vm_s);
     auto const & n = to_name(vm_n);
@@ -268,7 +259,6 @@ vm_obj has_attribute(vm_obj const & vm_attr_n, vm_obj const & vm_n, vm_obj const
 
 void initialize_user_attribute() {
     DECLARE_VM_BUILTIN(name({"attribute", "get_instances"}),            attribute_get_instances);
-    DECLARE_VM_BUILTIN(name({"attribute", "register"}),                 attribute_register);
     DECLARE_VM_BUILTIN(name({"attribute", "fingerprint"}),              attribute_fingerprint);
     DECLARE_VM_BUILTIN(name({"caching_user_attribute", "get_cache"}),   caching_user_attribute_get_cache);
     DECLARE_VM_BUILTIN(name({"tactic",    "set_basic_attribute"}),      set_basic_attribute);
@@ -276,6 +266,13 @@ void initialize_user_attribute() {
     DECLARE_VM_BUILTIN(name({"tactic",    "has_attribute"}),            has_attribute);
 
     register_trace_class("user_attributes_cache");
+    register_system_attribute(basic_attribute(
+            "user_attribute", "register a definition of type `user_attribute` in the attribute manager",
+            [](environment const & env, io_state const &, name const & n, unsigned, bool persistent) {
+                if (!persistent)
+                    throw exception("illegal [user_attribute] application, cannot be used locally");
+                return module::add_and_perform(env, std::make_shared<user_attr_modification>(n));
+            }));
     g_ext = new user_attr_ext_reg();
     user_attr_modification::init();
     set_user_attribute_ext(std::unique_ptr<user_attribute_ext>(new actual_user_attribute_ext));

tests/lean/caching_user_attribute.lean

@@ -1,10 +1,9 @@
+@[user_attribute]
 meta def foo_attr : caching_user_attribute string :=
 { name     := `foo, descr := "bar",
   mk_cache := λ ns, return $ list.join ∘ list.map (list.append "\n" ∘ to_string) $ ns,
   dependencies := [] }
 
-run_cmd attribute.register `foo_attr
-
 attribute [foo] eq.refl eq.mp
 
 set_option trace.user_attributes_cache true

tests/lean/run/eval_attr_cache.lean

@@ -1,5 +1,6 @@
 open tactic
 meta def list_name.to_expr (n : list name) : tactic expr := to_expr (quote n)
+@[user_attribute]
 meta def my_attr : caching_user_attribute (name → bool) :=
 { name         := "my_attr",
   descr        := "my attr",
@@ -11,8 +12,6 @@ meta def my_attr : caching_user_attribute (name → bool) :=
   dependencies := []
 }
 
-run_cmd attribute.register `my_attr
-
 meta def my_tac : tactic unit :=
 do f ← caching_user_attribute.get_cache my_attr,
    trace (f `foo),

tests/lean/user_attribute.lean

@@ -1,5 +1,5 @@
+@[user_attribute]
 definition foo_attr : user_attribute := { name := `foo, descr := "bar" }
-run_cmd attribute.register `foo_attr
 
 attribute [foo] eq.refl
 
@@ -9,10 +9,9 @@ run_cmd attribute.get_instances `foo >>= tactic.pp >>= tactic.trace
 #print "---"
 
 -- compound names
+@[user_attribute]
 definition foo_baz_attr : user_attribute := ⟨`foo.baz, "bar"⟩
 
-run_cmd attribute.register `foo_baz_attr
-
 attribute [foo.baz] eq.refl
 
 #print [foo.baz]
@@ -20,17 +19,17 @@ attribute [foo.baz] eq.refl
 run_cmd attribute.get_instances `foo.baz >>= tactic.pp >>= tactic.trace
 
 -- can't redeclare attributes
+@[user_attribute]
 definition duplicate : user_attribute := ⟨`reducible, "bar"⟩
-run_cmd attribute.register `duplicate
 
 
 -- wrong type
+@[user_attribute]
 definition bar := "bar"
-run_cmd attribute.register `bar
 
 section
   variable x : string
 
+  @[user_attribute]
   definition baz_attr : user_attribute := ⟨`baz, x⟩
-  run_cmd attribute.register `baz_attr
 end

tests/lean/user_attribute.lean.expected.out

@@ -7,12 +7,6 @@ eq.refl
 @[foo, foo.baz, refl]
 constructor eq.refl : ∀ {α : Sort u} (a : α), a = a
 [eq.refl]
-user_attribute.lean:24:0: error: an attribute named [reducible] has already been registered
-state:
-⊢ true
-user_attribute.lean:29:0: error: invalid attribute.register argument, must be name of a definition of type user_attribute
-state:
-⊢ true
-user_attribute.lean:35:2: error: invalid attribute.register argument, must be name of a definition of type user_attribute
-state:
-⊢ true
+user_attribute.lean:22:0: error: an attribute named [reducible] has already been registered
+user_attribute.lean:27:0: error: invalid [user_attribute], must be applied to definition of type user_attribute
+user_attribute.lean:33:2: error: invalid [user_attribute], must be applied to definition of type user_attribute