feat: basic support for scoped attributes

src/Lean/Attributes.lean

@@ -33,6 +33,11 @@ structure AttributeImplCore where
 
 structure AttributeImpl extends AttributeImplCore where
   add (decl : Name) (args : Syntax) (persistent : Bool) : AttrM Unit
+  addScoped (decl : Name) (args : Syntax) : AttrM Unit  := throwError "scoped attribute not supported for this kind of attribute"
+  erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased"
+  activateScoped (namespaceName : Name) : AttrM Unit := pure ()
+  pushScope : AttrM Unit := pure ()
+  popScope : AttrM Unit := pure ()
 
 instance : Inhabited AttributeImpl :=
   ⟨{ name := arbitrary, descr := arbitrary, add := fun env _ _ _ => pure () }⟩
@@ -169,10 +174,30 @@ def registerAttributeOfBuilder (env : Environment) (builderId : Name) (args : Li
   else
     pure $ attributeExtension.addEntry env (AttributeExtensionOLeanEntry.builder builderId args, attrImpl)
 
-def addAttribute (decl : Name) (attrName : Name) (args : Syntax) (persistent : Bool := true) : AttrM Unit := do
-  let env ← getEnv
-  let attr ← ofExcept $ getAttributeImpl env attrName
-  attr.add decl args persistent
+def Attribute.add (declName : Name) (attrName : Name) (args : Syntax) (persistent : Bool := true) : AttrM Unit := do
+  let attr ← ofExcept <| getAttributeImpl (← getEnv) attrName
+  attr.add declName args persistent
+
+def Attribute.addScoped (declName : Name) (attrName : Name) (args : Syntax) : AttrM Unit := do
+  let attr ← ofExcept <| getAttributeImpl (← getEnv) attrName
+  attr.addScoped declName args
+
+def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
+  let attr ← ofExcept <| getAttributeImpl (← getEnv) attrName
+  attr.erase declName
+
+@[inline]
+def Attribute.forEach (f : AttributeImpl → AttrM Unit) : AttrM Unit := do
+  (attributeExtension.getState (← getEnv)).map.forM fun _ attrImpl => f attrImpl
+
+def Attribute.pushScope : AttrM Unit := do
+  forEach fun attr => attr.pushScope
+
+def Attribute.popScope : AttrM Unit := do
+  forEach fun attr => attr.popScope
+
+def Attribute.activateScoped (namespaceName : Name) : AttrM Unit := do
+  forEach fun attr => attr.activateScoped namespaceName
 
 /--
   Tag attributes are simple and efficient. They are useful for marking declarations in the modules where
@@ -250,7 +275,9 @@ def registerParametricAttribute {α : Type} [Inhabited α] (impl : ParametricAtt
       r.qsort (fun a b => Name.quickLt a.1 b.1),
     statsFn         := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
   }
-  let attrImpl : AttributeImpl := { impl with
+  let attrImpl : AttributeImpl := {
+    name  := impl.name
+    descr := impl.descr
     add   := fun decl args persistent => do
       unless persistent do throwError! "invalid attribute '{impl.name}', must be persistent"
       let env ← getEnv

src/Lean/Elab/Attributes.lean

@@ -9,27 +9,31 @@ import Lean.MonadEnv
 namespace Lean.Elab
 
 structure Attribute where
-  name : Name
-  args : Syntax := Syntax.missing
+  scoped : Bool := false
+  name   : Name
+  args   : Syntax := Syntax.missing
 
-instance : ToFormat Attribute := ⟨fun attr =>
-  Format.bracket "@[" f!"{attr.name}{if attr.args.isMissing then "" else toString attr.args}" "]"⟩
+instance : ToFormat Attribute where
+  format attr :=
+    Format.bracket "@[" f!"{if attr.scoped then "scoped" else ""}{attr.name}{if attr.args.isMissing then "" else toString attr.args}" "]"
 
-instance : Inhabited Attribute := ⟨{ name := arbitrary }⟩
+instance : Inhabited Attribute where
+  default := { name := arbitrary }
 
 def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (stx : Syntax) : m Attribute := do
-  -- rawIdent >> many attrArg
-  let nameStx := stx[0]
+  -- optional "scoped" >> rawIdent >> many attrArg
+  let scoped  := false -- !stx[0].isNone
+  let nameStx := stx[0] -- TODO: change to 1
   let attrName ← match nameStx.isIdOrAtom? with
     | none     => withRef nameStx $ throwError "identifier expected"
     | some str => pure $ Name.mkSimple str
   unless isAttribute (← getEnv) attrName do
     throwError! "unknown attribute [{attrName}]"
-  let mut args := stx[1]
+  let mut args := stx[1] -- TODO: change to 2
   -- the old frontend passes Syntax.missing for empty args, for reasons
   if args.getNumArgs == 0 then
     args := Syntax.missing
-  pure { name := attrName, args := args }
+  pure { scoped := scoped, name := attrName, args := args }
 
 -- sepBy1 attrInstance ", "
 def elabAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) := do

src/Lean/Elab/Command.lean

@@ -13,7 +13,6 @@ import Lean.Elab.DeclModifiers
 namespace Lean.Elab.Command
 
 structure Scope where
-  kind          : String
   header        : String
   opts          : Options := {}
   currNamespace : Name := Name.anonymous
@@ -21,12 +20,12 @@ structure Scope where
   levelNames    : List Name := []
   varDecls      : Array Syntax := #[]
 
-instance : Inhabited Scope := ⟨{ kind := "", header := "" }⟩
+instance : Inhabited Scope := ⟨{ header := "" }⟩
 
 structure State where
   env            : Environment
   messages       : MessageLog := {}
-  scopes         : List Scope := [{ kind := "root", header := "" }]
+  scopes         : List Scope := [{ header := "" }]
   nextMacroScope : Nat := firstFrontendMacroScope + 1
   maxRecDepth    : Nat
   nextInstIdx    : Nat := 1 -- for generating anonymous instance names
@@ -37,7 +36,7 @@ instance : Inhabited State := ⟨{ env := arbitrary, maxRecDepth := 0 }⟩
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
   env := env,
   messages := messages,
-  scopes := [{ kind := "root", header := "", opts := opts }],
+  scopes := [{ header := "", opts := opts }],
   maxRecDepth := getMaxRecDepth opts
 }
 
@@ -307,23 +306,29 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
 @[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>
   EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
 
-private def addScope (kind : String) (header : String) (newNamespace : Name) : CommandElabM Unit :=
+private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
+  liftCoreM x
+
+private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name) : CommandElabM Unit := do
   modify fun s => {
     s with
     env    := s.env.registerNamespace newNamespace,
-    scopes := { s.scopes.head! with kind := kind, header := header, currNamespace := newNamespace } :: s.scopes
+    scopes := { s.scopes.head! with header := header, currNamespace := newNamespace } :: s.scopes
   }
+  liftAttrM Attribute.pushScope
+  if isNewNamespace then
+    liftAttrM <| Attribute.activateScoped newNamespace
 
-private def addScopes (kind : String) (updateNamespace : Bool) : Name → CommandElabM Unit
+private def addScopes (isNewNamespace : Bool) : Name → CommandElabM Unit
   | Name.anonymous => pure ()
   | Name.str p header _ => do
-    addScopes kind updateNamespace p
+    addScopes isNewNamespace p
     let currNamespace ← getCurrNamespace
-    addScope kind header (if updateNamespace then Name.mkStr currNamespace header else currNamespace)
+    addScope isNewNamespace header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace)
   | _ => throwError "invalid scope"
 
 private def addNamespace (header : Name) : CommandElabM Unit :=
-  addScopes "namespace" true header
+  addScopes (isNewNamespace := true) header
 
 @[builtinCommandElab «namespace»] def elabNamespace : CommandElab := fun stx =>
   match_syntax stx with
@@ -332,8 +337,8 @@ private def addNamespace (header : Name) : CommandElabM Unit :=
 
 @[builtinCommandElab «section»] def elabSection : CommandElab := fun stx =>
   match_syntax stx with
-  | `(section $header:ident) => addScopes "section" false header.getId
-  | `(section)               => do let currNamespace ← getCurrNamespace; addScope "section" "" currNamespace
+  | `(section $header:ident) => addScopes (isNewNamespace := false) header.getId
+  | `(section)               => do let currNamespace ← getCurrNamespace; addScope (isNewNamespace := false) "" currNamespace
   | _                        => throwUnsupportedSyntax
 
 def getScopes : CommandElabM (List Scope) := do
@@ -348,6 +353,10 @@ private def checkEndHeader : Name → List Scope → Bool
   | Name.str p s _, { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
   | _,              _                             => false
 
+private def popAttributeScopes (numScopes : Nat) : CommandElabM Unit :=
+  for i in [0:numScopes] do
+    liftAttrM <| Attribute.popScope
+
 @[builtinCommandElab «end»] def elabEnd : CommandElab := fun stx => do
   let header? := (stx.getArg 1).getOptionalIdent?;
   let endSize := match header? with
@@ -356,8 +365,11 @@ private def checkEndHeader : Name → List Scope → Bool
   let scopes ← getScopes
   if endSize < scopes.length then
     modify fun s => { s with scopes := s.scopes.drop endSize }
+    popAttributeScopes endSize
   else -- we keep "root" scope
-    modify fun s => { s with scopes := s.scopes.drop (s.scopes.length - 1) }
+    let n := (← get).scopes.length - 1
+    modify fun s => { s with scopes := s.scopes.drop n }
+    popAttributeScopes n
     throwError "invalid 'end', insufficient scopes"
   match header? with
   | none        => unless checkAnonymousScope scopes do throwError "invalid 'end', name is missing"
@@ -444,6 +456,7 @@ def elabOpenSimple (n : SyntaxNode) : CommandElabM Unit :=
   nss.forArgsM fun ns => do
     let ns ← resolveNamespace ns.getId
     addOpenDecl (OpenDecl.simple ns [])
+    liftAttrM <| Attribute.activateScoped ns
 
 -- `open` id `(` id+ `)`
 def elabOpenOnly (n : SyntaxNode) : CommandElabM Unit := do

src/Lean/Elab/Term.lean

@@ -466,22 +466,29 @@ def mkFreshIdent (ref : Syntax) : TermElabM Syntax :=
   return mkIdentFrom ref (← mkFreshBinderName)
 
 private def liftAttrM {α} (x : AttrM α) : TermElabM α := do
-  let ctx ← read
   liftCoreM x
 
 private def applyAttributesCore
     (declName : Name) (attrs : Array Attribute)
     (applicationTime? : Option AttributeApplicationTime) (persistent : Bool) : TermElabM Unit :=
   for attr in attrs do
-   let env ← getEnv
-   match getAttributeImpl env attr.name with
-   | Except.error errMsg => throwError errMsg
-   | Except.ok attrImpl  =>
-     match applicationTime? with
-     | none => liftAttrM $ attrImpl.add declName attr.args persistent
-     | some applicationTime =>
-       if applicationTime ==  attrImpl.applicationTime then
-         liftAttrM $ attrImpl.add declName attr.args persistent
+    let env ← getEnv
+    match getAttributeImpl env attr.name with
+    | Except.error errMsg => throwError errMsg
+    | Except.ok attrImpl  =>
+      match applicationTime? with
+      | none => apply attrImpl declName attr.scoped attr.args persistent
+      | some applicationTime =>
+        if applicationTime == attrImpl.applicationTime then
+          apply attrImpl declName attr.scoped attr.args persistent
+where
+  apply attrImpl declName scoped args persistent := do
+    if !persistent && scoped then
+      throwError "scoped attributes must be persistent"
+    if scoped then
+      liftAttrM <| attrImpl.addScoped declName args
+    else
+      liftAttrM <| attrImpl.add declName args persistent
 
 /-- Apply given attributes **at** a given application time -/
 def applyAttributesAt (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) (persistent : Bool := true) : TermElabM Unit :=

src/Lean/Parser/Extension.lean

@@ -278,8 +278,6 @@ builtin_initialize
   registerAlias "sepByT" (sepBy (allowTrailingSep := true))
   registerAlias "sepBy1T" (sepBy1 (allowTrailingSep := true))
 
-
-
 partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser :=
   let rec visit : ParserDescr → ImportM Parser
     | ParserDescr.const n                             => getConstAlias parserAliasesRef n

src/Lean/Parser/Term.lean

@@ -152,7 +152,11 @@ def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
 @[builtinTermParser] def «let*» := parser!:leadPrec withPosition ("let* " >> letDecl) >> optSemicolon termParser
 def attrArg : Parser := ident <|> strLit <|> numLit
 -- use `rawIdent` because of attribute names such as `instance`
-def attrInstance     := ppGroup $ parser! rawIdent >> many (ppSpace >> attrArg)
+def attrInstance     := ppGroup $ parser!
+  (checkInsideQuot >> optional "scoped" >> rawIdent >> many (ppSpace >> attrArg))
+  <|>
+  (checkOutsideQuot >> rawIdent >> many (ppSpace >> attrArg))
+
 def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
 def letRecDecls      := sepBy1 (group (optional «attributes» >> letDecl)) ", "
 @[builtinTermParser]

src/Lean/ParserCompiler.lean

@@ -111,7 +111,7 @@ def compileCategoryParser {α} (ctx : Context α) (declName : Name) (builtin : B
   -- We assume that for tagged parsers, the kind is equal to the declaration name. This is automatically true for parsers
   -- using `parser!` or `syntax`.
   let kind := declName
-  addAttribute c' (if builtin then ctx.categoryAttr.defn.builtinName else ctx.categoryAttr.defn.name) (mkNullNode #[mkIdent kind])
+  Attribute.add c' (if builtin then ctx.categoryAttr.defn.builtinName else ctx.categoryAttr.defn.name) (mkNullNode #[mkIdent kind])
 
 variables {α} (ctx : Context α) in
 def compileEmbeddedParsers : ParserDescr → MetaM Unit

tests/lean/decimals.lean

@@ -10,7 +10,7 @@ theorem ex : 31416e-4 = 3.1416 :=
 
 #eval 3.4e-100 * 1e98
 
-#eval 12.3e90 * 1e-90
+#eval 12.3e90 * 1E-90
 #eval 3.00e-100 * 1e100
 #eval 3.00e-100 * 1.e100
 #eval 3.00e-100 * 1.0e100