`unfold` don't work as expected in binder attributes

[TWal]

See the following example:

module UnfoldAttr

open FStar.Tactics

irreducible let attrib (#a:Type) (x:a) = ()
unfold let string_attrib (s:string) = attrib ("[" ^ s ^ "]")

type test = {
  [@@@ attrib 1337]
  test_field_1: unit;
  [@@@ string_attrib "hello"]
  test_field_2: unit;
}

val print_record_attrs: name -> Tac unit
let print_record_attrs type_name =
  let env = top_env () in
  let type_declaration =
    match lookup_typ env type_name with
    | Some x -> x
    | None -> fail ""
  in
  match inspect_sigelt type_declaration with
  | Sg_Inductive name [] params typ constructors -> (
    match constructors with
    | [(_, ctor_type)] -> (
      let (binders, _) = collect_arr_bs ctor_type in
      Tactics.Util.iter (fun binder ->
        let (_, (_, attribs)) = inspect_binder binder in
        Tactics.Util.iter (fun attrib ->
          dump (term_to_string attrib)
        ) attribs
      ) binders
    )
    | _ -> fail ""
  )
  | _ -> fail ""

let _ = run_tactic (fun () -> print_record_attrs (explode_qn "UnfoldAttr.test"))

// Gives:
//   UnfoldAttr.attrib 1337 @ …lib/FStar.Tactics.Util.fst(45,13-45,16)
//   UnfoldAttr.string_attrib "hello" @ …lib/FStar.Tactics.Util.fst(45,13-45,16)
// and not
//   UnfoldAttr.attrib 1337 @ …lib/FStar.Tactics.Util.fst(45,13-45,16)
//   UnfoldAttr.attrib ("[" ^ "hello" ^ "]") @ …lib/FStar.Tactics.Util.fst(45,13-45,16)
// as expected.

This would be very useful to define new attributes in a retro-compatible way for existing meta-programs.

In my use-case, doing a norm_term pass on the attribute is not an option, because it doesn't work well with dependant types (i.e. the annotation is used with a type that contains a bound variable which is not in the context).

[nikswamy]

Thanks @TWal . This is an interesting example.

I don't think the attribute annotations were designed to be programmable in this sense. The attributes are interpreted literally, and not up to reduction. However, because the syntax allows you to write any term as an attribute, I can see how it's tempting to use attributes that compute.

I can't think of another language that allows this kind of computable attributes. Do you know of any?

It'll take a bit of work to support in the compiler ... wherever we look up an attribute, we'll have to call the normalizer on it first. Then again, might we also want attributes that are not meant to be reduced?

I wonder what others think. Do we really want computable attributes?