From 4f66673fc20d4c663f0d3397efe73226d541c22b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 25 Jul 2017 16:44:05 +0200 Subject: [PATCH] feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers --- doc/changes.md | 2 ++ library/init/default.lean | 2 +- library/init/meta/attribute.lean | 14 +++++++-- library/init/meta/coinductive_predicates.lean | 2 +- library/init/meta/smt/ematch.lean | 31 ++++++++++++------- src/library/attribute_manager.cpp | 2 +- src/library/attribute_manager.h | 4 +-- src/library/tactic/user_attribute.cpp | 30 +++++++++++++++++- tests/lean/run/struct_value.lean | 2 +- tests/lean/user_attribute.lean | 10 +++--- tests/lean/user_attribute.lean.expected.out | 12 +++---- 11 files changed, 78 insertions(+), 33 deletions(-) diff --git a/doc/changes.md b/doc/changes.md index f601c03a11..d5c011b475 100644 --- a/doc/changes.md +++ b/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`. diff --git a/library/init/default.lean b/library/init/default.lean index d1f9143a38..5bed4f5d67 100644 --- a/library/init/default.lean +++ b/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" } diff --git a/library/init/meta/attribute.lean b/library/init/meta/attribute.lean index 5453a3419c..031381a095 100644 --- a/library/init/meta/attribute.lean +++ b/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. -/ diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean index 8c2f00eece..dc1ec9ee12 100644 --- a/library/init/meta/coinductive_predicates.lean +++ b/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) := diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean index c0b03e6eed..b47f810550 100644 --- a/library/init/meta/smt/ematch.lean +++ b/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 diff --git a/src/library/attribute_manager.cpp b/src/library/attribute_manager.cpp index 396949e97b..95853a4a93 100644 --- a/src/library/attribute_manager.cpp +++ b/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() << "]"); diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index 89cd6954be..71377eca99 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -34,7 +34,7 @@ attr_data_ptr get_default_attr_data(); typedef std::function after_set_proc; typedef std::function after_set_check_proc; -typedef std::function before_unset_proc; +typedef std::function 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; }); } diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp index efbc04e61f..06c8067118 100644 --- a/src/library/tactic/user_attribute.cpp +++ b/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); } diff --git a/tests/lean/run/struct_value.lean b/tests/lean/run/struct_value.lean index f9e3675f50..6046a0ab20 100644 --- a/tests/lean/run/struct_value.lean +++ b/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 diff --git a/tests/lean/user_attribute.lean b/tests/lean/user_attribute.lean index ee7eaf3e4a..7d3539bab7 100644 --- a/tests/lean/user_attribute.lean +++ b/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 diff --git a/tests/lean/user_attribute.lean.expected.out b/tests/lean/user_attribute.lean.expected.out index b861d243ec..36ba4ad2ed 100644 --- a/tests/lean/user_attribute.lean.expected.out +++ b/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