Attribute example

Stream: lean4

[Patrick Massot]

Does anyone has an example of creating an attribute can be local or global and take an optional priority parameter?

[Patrick Massot]

I know about register_label_attr from Std but it cannot be used with local and cannot take parameters. So I’m looking for a slightly more sophisticated gadget.

[Patrick Massot]

I am really confused by the attribute system. Is there a way to define an attribute with parameters that would be stored and modified in any file? It seems every variant has limitations like being added only in the file defining the declaration or modifications are not persisted across files.

[Tomas Skrivan]

There might be an easier way but you can do it with SimpleScopedEnvExtension

Test file:

import Doodle.MyScopedAttr

#eval hasMyAttr ``id -- false

-- global
attribute [myAttr] id

#eval hasMyAttr ``id -- true


namespace TestScope

-- local attribute
attribute [local myAttr] Nat

#eval hasMyAttr ``Nat -- true

end  TestScope

#eval hasMyAttr ``Nat -- false

MyScopedAttr.lean

import Lean

open Lean Meta

syntax (name:=my_attr) "myAttr" (prio)? : attr

initialize myScopedAttrExt : SimpleScopedEnvExtension Name NameSet ←
  registerSimpleScopedEnvExtension {
    name := by exact decl_name%
    initial := {}
    addEntry := fun set name => set.insert name
  }

initialize myScopedAttr : Unit ←
  registerBuiltinAttribute {
    name  := ``my_attr
    descr := ""
    applicationTime := AttributeApplicationTime.afterCompilation
    add   := fun declName stx attrKind => do
      myScopedAttrExt.add declName attrKind
    erase := fun _declqName =>
      pure ()
  }

def hasMyAttr (name : Name) : CoreM Bool := do
  let a := myScopedAttrExt.getState (← getEnv)
  return a.contains name

[Tomas Skrivan]

Then in the function add inside registerBuiltinAttribute you can extract the priority information from stx which gives you the syntax of the attribute.

You will of course also need to modify the SimpleScopedEnvExtension Name NameSet such that you can store the priority information e.g. SimpleScopedEnvExtension (Name×Nat) (NameMap Nat)

[Patrick Massot]

Thanks Tomas. Can you actually remove the attribute later with this example?

[Tomas Skrivan]

Patrick Massot said:

I am really confused by the attribute system. Is there a way to define an attribute with parameters that would be stored and modified in any file? It seems every variant has limitations like being added only in the file defining the declaration or modifications are not persisted across files.

Yeah I also do not understand the limitation that you can add the attribute only in the file where you declare the function. For that reason I just use the above setup.

[Tomas Skrivan]

Patrick Massot said:

Thanks Tomas. Can you actually remove the attribute later with this example?

Sure, you just need to implement the erase function.

[Patrick Massot]

I would have no idea how to do that. But I also realize that maybe my question doesn’t really make sense. It isn’t clear what would be the expected behavior if you import one file adding the attribute and one file removing it. I guess this is why the simp attribute does not allow this.

[Tomas Skrivan]

What is the syntax to remove attribute? attribute [-myAttr] Nat does not work.

[Patrick Massot]

This is meant to work.

[Tomas Skrivan]

Ohh attribute [-my_attr] Nat works. There is the syntax of an attribute syntax (name:=my_attr) "myAttr" (prio)? and its name my_attr. I guess the convention is to have myAttr=my_attr.

[Tomas Skrivan]

Revised version:

import Lean

open Lean Meta


syntax (name:=myAttr) "myAttr" (prio)? : attr

initialize myScopedAttrExt : SimpleScopedEnvExtension Name NameSet ←
  registerSimpleScopedEnvExtension {
    name := by exact decl_name%
    initial := {}
    addEntry := fun set name => set.insert name
  }

def hasMyAttr (name : Name) : CoreM Bool := do
  let a := myScopedAttrExt.getState (← getEnv)
  return a.contains name


initialize myScopedAttr : Unit ←
  registerBuiltinAttribute {
    name  := ``myAttr
    descr := ""
    applicationTime := AttributeApplicationTime.afterCompilation
    add   := fun declName stx attrKind => do
      myScopedAttrExt.add declName attrKind
    erase := fun declName => do
      unless ← hasMyAttr declName do
        throwError s!"{declName} does not have `myAttr` attribute!"

      modifyEnv fun env =>
        myScopedAttrExt.modifyState env fun s =>
          s.erase declName
  }

import Doodle.MyScopedAttr

#eval hasMyAttr ``id -- false

-- global
attribute [myAttr] id

#eval hasMyAttr ``id -- true


namespace TestScope

attribute [-myAttr] id

#eval hasMyAttr ``id -- false

-- local attribute
attribute [local myAttr mid] Nat

#eval hasMyAttr ``Nat -- true

attribute [-myAttr] Nat

#eval hasMyAttr ``Nat -- false

end  TestScope

#eval hasMyAttr ``Nat -- false

[Patrick Massot]

Thanks a lot!

[Jannis Limperg]

Patrick Massot said:

It isn’t clear what would be the expected behavior if you import one file adding the attribute and one file removing it. I guess this is why the simp attribute does not allow this.

That's right. As a result, erasing only works locally, i.e. attribute [-attr] foo only removes attr from foo for the remainder of the current file.