user attribute vs basic attribute

Stream: general

[Floris van Doorn]

Is there a tactic that takes the name for a user attribute (say `to_additive) and returns its declaration name (of type user_attribute, in this case `to_additive.attr)?
In order to not #xy the problem: I am given a name of an attribute (that can either be a basic attribute or a user attribute), and I want to add it to a declaration. If it is a user attribute, then it's param_ty may be assumed to be unit.

[Simon Hudon]

Have you tried eval_expr?

[Floris van Doorn]

On what expression?

[Simon Hudon]

mk_const attr_n >>= eval_expr user_attribute

[Simon Hudon]

That will only take care of the user_attribute case

[Floris van Doorn]

I'm given the name of the user attribute, i.e. the name field in the definition i.e. the thing you write inside @[...].
So I don't think your suggestion works.

[Simon Hudon]

Ah! In that case, you might need to query the user_attribute attribute and search for the record with the right name

[Simon Hudon]

I don't know if user_attribute has a cache, I'm hoping it does

[Floris van Doorn]

To explain my second problem (which might still be #xy): I try to provide a user interface for the @[simps] attribute so the user can tag the generated definitions with any attributes they want. Some actual attributes you want to give include @[simp] (a basic attribute) and any attribute generated by mk_simp_attribute (a user attribute). I could change the interface to avoid this problem.

[Floris van Doorn]

@Simon Hudon: That is a good idea! I may do it (or maybe I'll change the behavior so that I don't need it anymore).

[Gabriel Ebner]

If you're sure the parameter is unit, then you can just define your user_attribute instance ad-hoc. That is, something like user_attribute.set { name := attr_name, descr := "" } decl_name. There is no requirement to use the existing definition.

[Floris van Doorn]

Interesting! I would not have guessed that would work.
That trick apparently even "works" for attributes where the parameter is non-unit, but in that case you'll just get an error when you call get_param. Here are some tests:

import tactic.core

open tactic

def foo : unit := ()

@[user_attribute] meta def my_user_attr : user_attribute := { name := `my_user, descr := "" }

run_cmd user_attribute.set { name := `my_user, descr := "" } `foo () tt

run_cmd attribute.get_instances `my_user >>= trace -- [foo]
run_cmd my_user_attr.get_param `foo >>= trace -- ()


@[user_attribute] meta def my_user2_attr : user_attribute unit bool :=
  { name := `my_user2, descr := "", parser := return tt }

run_cmd user_attribute.set { name := `my_user2, descr := "" } `foo () tt -- no error

run_cmd attribute.get_instances `my_user2 >>= trace -- [foo]
run_cmd my_user2_attr.get_param `foo >>= trace -- error

[Floris van Doorn]

Ok, I'm still stuck on this.

I can get Gabriel's suggestion to work, but as Rob pointed out when reviewing #3477, this is very dangerous: we don't test whether the parameter type really is unit. This means we can accidentally assign it to a user attribute with a parameter without receiving an error.

So I want to add a test that get_param still works.

• Gabriel's suggestion doesn't work for get_param, since user_attribute.get_param { name := attr_name, descr := "" } decl_name will just succeed: the parameter type of the attribute we provided is unit after all, independent of whether this attribute has been declared with a different parameter
• I tried Simon's suggestion of querying all user_attributes, and returning the one with the right name. This works for terms of type user_attributes unit unit, i.e. user attributes which also have no cache type. However, it doesn't work (read: I cannot get it to work) for attributes with a non-unit cache type, since at some point I have to do eval_expr (user_attribute _ unit) e_attr and I don't know what goes in _. Furthermore, I don't think I can evaluate the cache type first, since eval_expr Type _ doesn't work for the lack of reflected instances.

Any ideas how I can run get_param / test whether I added a value safely for user attributes with a cache type?

[Gabriel Ebner]

A very easy way to make eval_expr work is to evaluate the set:

eval_pexpr (tactic unit) ``(user_attribute.set %%user_attr_const %%decl_name () %%persistent)

[Floris van Doorn]

Neat trick!

I am missing the following instance for this to work. Shall I add that as well?

@[priority 100] meta instance {α} [has_reflect α] : has_to_pexpr α := ⟨λ b, pexpr.of_expr (reflect b)⟩