chore(init/meta/attribute): rename user_attribute.set_param to `use…

…r_attribute.set`

Setting the parameter value really is a side effect of setting the whole attribute

doc/changes.md

@@ -137,7 +137,7 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
   `⟨h1, h2⟩`. This change is motivated by the previous one. Without it, `and.intro h1 h2` would be
   pretty printed as `{left := h1, right := h2}`.
 
-* User attributes can no longer be set with `set_basic_attribute`.  You need to use `user_attribute.set_param` now.
+* User attributes can no longer be set with `set_basic_attribute`.  You need to use `user_attribute.set` now.
 
 *API name changes*
 

library/init/meta/attribute.lean

@@ -47,15 +47,15 @@ meta def user_attribute.parse_reflect {α β : Type} (attr : user_attribute α 
 
 meta constant user_attribute.get_param_untyped {α β : Type} (attr : user_attribute α β) (decl : name)
   : tactic expr
-meta constant user_attribute.set_param_untyped {α β : Type} [reflected β] (attr : user_attribute α β) (decl : name)
+meta constant user_attribute.set_untyped {α β : Type} [reflected β] (attr : user_attribute α β) (decl : name)
   (val : expr) (persistent : bool) (prio : option nat := none) : tactic unit
 
 meta def user_attribute.get_param {α β : Type} [reflected β] (attr : user_attribute α β) (n : name) : tactic β :=
 attr.get_param_untyped n >>= tactic.eval_expr β
 
-meta def user_attribute.set_param {α β : Type} [reflected β] (attr : user_attribute α β) (n : name)
+meta def user_attribute.set {α β : Type} [reflected β] (attr : user_attribute α β) (n : name)
   (val : β) (persistent : bool) (prio : option nat := none) : tactic unit :=
-attr.set_param_untyped n (attr.reflect_param val) persistent prio
+attr.set_untyped n (attr.reflect_param val) persistent prio
 
 open tactic
 

src/library/tactic/user_attribute.cpp

@@ -93,27 +93,27 @@ vm_obj user_attribute_get_param_untyped(vm_obj const &, vm_obj const &, vm_obj c
     LEAN_TACTIC_CATCH(s);
 }
 
-vm_obj user_attribute_set_param_untyped(expr const & beta, name const & attr_n, name const & n, expr const & val,
+vm_obj user_attribute_set_untyped(expr const & beta, name const & attr_n, name const & n, expr const & val,
                                         bool persistent, unsigned prio, tactic_state const & s) {
     type_context ctx(s.env(), s.get_options());
     if (!ctx.is_def_eq(beta, ctx.infer(val))) {
-        return tactic::mk_exception(sstream() << "set_param_untyped failed, '" << val << "' is not of type '" << beta << "'", s);
+        return tactic::mk_exception(sstream() << "set_untyped failed, '" << val << "' is not of type '" << beta << "'", s);
     }
     LEAN_TACTIC_TRY;
         attribute const & attr = get_attribute(s.env(), attr_n);
         if (user_attribute const * user_attr = dynamic_cast<user_attribute const *>(&attr)) {
             environment new_env = user_attr->set(s.env(), get_global_ios(), n, prio, user_attribute_data(val), persistent);
             return tactic::mk_success(set_env(s, new_env));
         } else {
-            return tactic::mk_exception(sstream() << "set_param_untyped failed, '" << attr_n << "' is not a user attribute", s);
+            return tactic::mk_exception(sstream() << "set_untyped failed, '" << attr_n << "' is not a user attribute", s);
         }
     LEAN_TACTIC_CATCH(s);
 }
 
-vm_obj user_attribute_set_param_untyped(unsigned DEBUG_CODE(num), vm_obj const * args) {
+vm_obj user_attribute_set_untyped(unsigned DEBUG_CODE(num), vm_obj const * args) {
     lean_assert(num == 9);
     unsigned prio = is_none(args[7]) ? LEAN_DEFAULT_PRIORITY : to_unsigned(get_some_value(args[7]));
-    return user_attribute_set_param_untyped(to_expr(args[2]), to_name(cfield(args[3], 0)), to_name(args[4]),
+    return user_attribute_set_untyped(to_expr(args[2]), to_name(cfield(args[3], 0)), to_name(args[4]),
                                             to_expr(args[5]), to_bool(args[6]), prio, tactic::to_state(args[8]));
 }
 
@@ -350,8 +350,8 @@ void initialize_user_attribute() {
     DECLARE_VM_BUILTIN(name({"attribute", "fingerprint"}),              attribute_fingerprint);
     DECLARE_VM_BUILTIN(name({"user_attribute", "get_cache"}),           user_attribute_get_cache_core);
     DECLARE_VM_BUILTIN(name({"user_attribute", "get_param_untyped"}),   user_attribute_get_param_untyped);
-    declare_vm_builtin(name({"user_attribute", "set_param_untyped"}), "user_attribute_set_param_untyped",
-                       9, user_attribute_set_param_untyped);
+    declare_vm_builtin(name({"user_attribute", "set_untyped"}), "user_attribute_set_untyped",
+                       9, user_attribute_set_untyped);
     DECLARE_VM_BUILTIN(name({"tactic",    "set_basic_attribute"}),      set_basic_attribute);
     DECLARE_VM_BUILTIN(name({"tactic",    "unset_attribute"}),          unset_attribute);
     DECLARE_VM_BUILTIN(name({"tactic",    "has_attribute"}),            has_attribute);

tests/lean/caching_user_attribute.lean

@@ -14,7 +14,7 @@ run_cmd do
   tactic.trace s,
   s : string ← foo_attr.get_cache,
   tactic.trace s,
-  foo_attr.set_param `eq.mpr () tt,
+  foo_attr.set `eq.mpr () tt,
   s : string ← foo_attr.get_cache,
   tactic.trace s,
   tactic.set_basic_attribute `reducible ``eq.mp, -- should not affect [foo] cache