feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers

doc/changes.md

@@ -50,6 +50,8 @@ master branch (aka work in progress branch)
 * Tactics that accept a location parameter, like `rw thm at h`, may now use `⊢` or the ASCII version `|-`
   to select the goal as well as any hypotheses, for example `rw thm at h1 h2 ⊢`.
 
+* Add `user_attribute.after_set/before_unset` handlers that can be used for validation as well as side-effecting attributes.
+
 *Changes*
 
 * We now have two type classes for converting to string: `has_to_string` and `has_repr`.

library/init/default.lean

@@ -10,6 +10,6 @@ import init.util init.coe init.wf init.meta init.meta.well_founded_tactics init.
 import init.native
 
 @[user_attribute]
-def debugger.attr : user_attribute :=
+meta def debugger.attr : user_attribute :=
 { name  := `breakpoint,
   descr := "breakpoint for debugger" }

library/init/meta/attribute.lean

@@ -9,9 +9,17 @@ import init.meta.tactic init.meta.rb_map init.meta.has_reflect
 meta constant attribute.get_instances : name → tactic (list name)
 meta constant attribute.fingerprint : name → tactic nat
 
-structure user_attribute :=
-(name  : name)
-(descr : string)
+meta structure user_attribute :=
+(name         : name)
+(descr        : string)
+/- Optional handler that will be called after the attribute has been applied to a declaration.
+   Failing the tactic will fail the entire `attribute/def/...` command, i.e. the attribute will
+   not be applied after all.
+   Declaring an `after_set` handler without a `before_unset` handler will make the attribute
+   non-removable. -/
+(after_set    : option (Π (decl : _root_.name) (prio : nat) (persistent : bool), command) := none)
+/- Optional handler that will be called before the attribute is removed from a declaration. -/
+(before_unset : option (Π (decl : _root_.name) (persistent : bool), command) := none)
 
 /- Registers a new user-defined attribute. The argument must be the name of a definition of type
    `user_attribute` or a sub-structure. -/

library/init/meta/coinductive_predicates.lean

@@ -112,7 +112,7 @@ section
 universe u
 
 @[user_attribute]
-def monotonicity := { user_attribute . name := `monotonicity, descr := "Monotonicity rules for predicates" }
+meta def monotonicity := { user_attribute . name := `monotonicity, descr := "Monotonicity rules for predicates" }
 
 lemma monotonicity.pi {α : Sort u} {p q : α → Prop} (h : ∀a, implies (p a) (q a)) :
   implies (Πa, p a) (Πa, q a) :=

library/init/meta/smt/ematch.lean

@@ -81,9 +81,14 @@ meta def to_hinst_lemmas_core (m : transparency) : bool → list name → hinst_
 meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) : command :=
 do let t := `(caching_user_attribute hinst_lemmas),
    let v := `({name     := attr_name,
-                 descr    := "hinst_lemma attribute",
-                 mk_cache := λ ns, to_hinst_lemmas_core reducible as_simp ns hinst_lemmas.mk,
-                 dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas),
+               descr    := "hinst_lemma attribute",
+               after_set := some $ λ n _ _,
+                 to_hinst_lemmas_core reducible as_simp [n] hinst_lemmas.mk >> skip <|>
+                 fail format!"invalid ematch lemma '{n}'",
+               -- allow unsetting
+               before_unset := some $ λ _ _, skip,
+               mk_cache := λ ns, to_hinst_lemmas_core reducible as_simp ns hinst_lemmas.mk,
+               dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas),
    add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
    attribute.register attr_name
 
@@ -117,15 +122,17 @@ do mk_hinst_lemma_attrs_core ff attr_names,
    mk_hinst_lemma_attrs_core tt simp_attr_names,
    let t  := `(caching_user_attribute hinst_lemmas),
    let v  := `({name     := attr_name,
-                   descr    := "hinst_lemma attribute set",
-                   mk_cache := λ ns,
-                      let aux1 : list name := attr_names,
-                          aux2 : list name := simp_attr_names in
-                      do {
-                      hs₁ ← to_hinst_lemmas_core reducible ff ns hinst_lemmas.mk,
-                      hs₂ ← merge_hinst_lemma_attrs reducible ff aux1 hs₁,
-                      merge_hinst_lemma_attrs reducible tt aux2 hs₂},
-                    dependencies := [`reducibility] ++ attr_names ++ simp_attr_names } : caching_user_attribute hinst_lemmas),
+                descr    := "hinst_lemma attribute set",
+                after_set := some $ λ n _ _,
+                  to_hinst_lemmas_core reducible ff [n] hinst_lemmas.mk >> skip <|>
+                  fail format!"invalid ematch lemma '{n}'",
+                -- allow unsetting
+                before_unset := some $ λ _ _, skip,
+                mk_cache := λ ns, do {
+                   hs₁ ← to_hinst_lemmas_core reducible ff ns hinst_lemmas.mk,
+                   hs₂ ← merge_hinst_lemma_attrs reducible ff attr_names hs₁,
+                   merge_hinst_lemma_attrs reducible tt simp_attr_names hs₂},
+                dependencies := [`reducibility] ++ attr_names ++ simp_attr_names } : caching_user_attribute hinst_lemmas),
    add_decl (declaration.defn attr_name [] t v reducibility_hints.abbrev ff),
    attribute.register attr_name
 

src/library/attribute_manager.cpp

@@ -167,7 +167,7 @@ environment attribute::set_core(environment const & env, io_state const & ios, n
 
 environment attribute::unset(environment env, io_state const & ios, name const & n, bool persistent) const {
     if (m_before_unset) {
-        env = m_before_unset(env, n, persistent);
+        env = m_before_unset(env, ios, n, persistent);
     } else {
         if (m_after_set)
             throw exception(sstream() << "cannot remove attribute [" << get_name() << "]");

src/library/attribute_manager.h

@@ -34,7 +34,7 @@ attr_data_ptr get_default_attr_data();
 
 typedef std::function<environment(environment const &, io_state const &, name const &, unsigned, bool)> after_set_proc;
 typedef std::function<void(environment const &, name const &, bool)> after_set_check_proc;
-typedef std::function<environment(environment const &, name const &, bool)> before_unset_proc;
+typedef std::function<environment(environment const &, io_state const &, name const &, bool)> before_unset_proc;
 
 class attribute {
     friend struct attr_config;
@@ -93,7 +93,7 @@ public:
                     after_set(env, n, persistent);
                     return env;
                 },
-                [](environment const & env, name const &, bool) {
+                [](environment const & env, io_state const &, name const &, bool) {
                     return env;
                 });
     }

src/library/tactic/user_attribute.cpp

@@ -57,9 +57,37 @@ static environment add_user_attr(environment const & env, name const & d) {
     if (is_attribute(env, n))
         throw exception(sstream() << "an attribute named [" << n << "] has already been registered");
     std::string descr = to_string(cfield(o, 1));
+    after_set_proc after_set;
+    if (!is_none(cfield(o, 2))) {
+        after_set = [=](environment const & env, io_state const & ios, name const & n, unsigned prio, bool persistent) {
+            vm_state vm(env, ios.get_options());
+            scope_vm_state scope(vm);
+            vm_obj o = vm.invoke(d, {});
+            if (is_constant(get_app_fn(ty), get_caching_user_attribute_name()))
+                o = cfield(o, 0);
+            tactic_state s = mk_tactic_state_for(env, options(), {}, local_context(), mk_true());
+            auto vm_r = vm.invoke(get_some_value(cfield(o, 2)), to_obj(n), to_obj(prio), mk_vm_bool(persistent), to_obj(s));
+            tactic::report_exception(vm, vm_r);
+            return tactic::to_state(tactic::get_result_state(vm_r)).env();
+        };
+    }
+    before_unset_proc before_unset;
+    if (!is_none(cfield(o, 3))) {
+        before_unset = [=](environment const & env, io_state const & ios, name const & n, bool persistent) {
+            vm_state vm(env, ios.get_options());
+            scope_vm_state scope(vm);
+            vm_obj o = vm.invoke(d, {});
+            if (is_constant(get_app_fn(ty), get_caching_user_attribute_name()))
+                o = cfield(o, 0);
+            tactic_state s = mk_tactic_state_for(env, options(), {}, local_context(), mk_true());
+            auto vm_r = vm.invoke(get_some_value(cfield(o, 3)), to_obj(n), mk_vm_bool(persistent), to_obj(s));
+            tactic::report_exception(vm, vm_r);
+            return tactic::to_state(tactic::get_result_state(vm_r)).env();
+        };
+    }
 
     user_attr_ext ext = get_extension(env);
-    ext.m_attrs.insert(n, attribute_ptr(new basic_attribute(n, descr.c_str())));
+    ext.m_attrs.insert(n, attribute_ptr(new basic_attribute(n, descr.c_str(), after_set, before_unset)));
     return update(env, ext);
 }
 

tests/lean/run/struct_value.lean

@@ -7,7 +7,7 @@ definition p : nat × nat :=
 
 #print p
 
-definition attr : user_attribute :=
+meta def attr : user_attribute :=
 { name := `foo, descr := "hello world" }
 
 #print attr

tests/lean/user_attribute.lean

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

tests/lean/user_attribute.lean.expected.out

@@ -7,11 +7,11 @@ eq.refl
 @[foo, foo.baz, refl]
 constructor eq.refl : ∀ {α : Sort u} (a : α), a = a
 [eq.refl]
-user_attribute.lean:23:0: error: an attribute named [reducible] has already been registered
-user_attribute.lean:23:0: warning: declaration 'duplicate' uses sorry
-user_attribute.lean:28:0: error: invalid [user_attribute], must be applied to definition of type user_attribute
-user_attribute.lean:28:11: error: don't know how to synthesize placeholder
+user_attribute.lean:23:5: error: an attribute named [reducible] has already been registered
+user_attribute.lean:23:5: warning: declaration 'duplicate' uses sorry
+user_attribute.lean:28:5: error: invalid [user_attribute], must be applied to definition of type user_attribute
+user_attribute.lean:28:9: error: don't know how to synthesize placeholder
 context:
 ⊢ Sort ?
-user_attribute.lean:34:2: error: invalid [user_attribute], must be applied to definition of type user_attribute
-user_attribute.lean:34:2: warning: declaration 'baz_attr' uses sorry
+user_attribute.lean:34:7: error: invalid [user_attribute], must be applied to definition of type user_attribute
+user_attribute.lean:34:7: warning: declaration 'baz_attr' uses sorry