feat: improved export command and namespace aliases

This PR gives the `export` command the ability to create aliases to namespaces,
in addition to its current ability to create aliases to individual declarations.
It adds a number of `open`-like variations to the syntax.
* `export NS1 ... NSn` makes the current namespace be an alias for the provided namespaces.
* `export NS (def1 ... defn)` has the same meaning as before, but if any `NS.defi` is a namespace
  then the alias also serves as a namespace alias. For example, if one were to do
  ```lean
  namespace MyNS
  export _root_ (Nat)
  end MyNS
  ```
  then not only is `MyNS.Nat` available as an alias for `Nat`,
  but additionally `MyNS.Nat.succ` is now an alias for `Nat.succ`.
* `export NS hiding def1 ... defn` is like `export NS`, but the given names in `NS` do not get aliases.
* `export NS renaming def1 -> def1', ..., defn -> defn'` creates aliases for the given names `def1` through `defn`,
  but the aliases respectively use the names `def1'` through `defn'`.

src/Lean/Data/ExportDecl.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Init.Meta
+
+namespace Lean
+
+/--
+Data for representing `export` commands.
+-/
+inductive ExportDecl where
+  /-- The name `aDeclName` is an alias for the declaration `declName`. -/
+  | explicit (aDeclName : Name) (declName : Name)
+  /-- The namespace `ans` is an alias for the namespace `ns`,
+  except, if `e` is in `except`, `ans ++ e` is not an alias for `ns ++ e`.
+  Alias resolution is recursive. `ns` must be a registered namespace. -/
+  | namespace (ans ns : Name) (except : List Name)
+  deriving BEq
+
+namespace ExportDecl
+
+instance : ToString ExportDecl := ⟨fun decl =>
+  match decl with
+  | .explicit adecl decl => toString adecl ++ " → " ++ toString decl
+  | .namespace ans ns ex  => toString ans ++ ".* → " ++ toString ns ++ ".*" ++ (if ex == [] then "" else " hiding " ++ toString ex)⟩
+
+end ExportDecl
+
+end Lean

src/Lean/Elab/BuiltinCommand.lean

@@ -128,19 +128,52 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   | Except.ok env   => setEnv env
   | Except.error ex => throwError (ex.toMessageData (← getOptions))
 
-@[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do
-  let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax
-  let nss ← resolveNamespace ns
+def elabExportDecl (stx : TSyntax ``Parser.Command.exportDecl) : CommandElabM Unit := do
   let currNamespace ← getCurrNamespace
-  if nss == [currNamespace] then throwError "invalid 'export', self export"
-  let mut aliases := #[]
-  for idStx in ids do
-    let id := idStx.getId
-    let declName ← resolveNameUsingNamespaces nss idStx
-    if (← getInfoState).enabled then
-      addConstInfo idStx declName
-    aliases := aliases.push (currNamespace ++ id, declName)
-  modify fun s => { s with env := aliases.foldl (init := s.env) fun env p => addAlias env p.1 p.2 }
+  match stx with
+  | `(Parser.Command.exportDecl| $nss*) =>
+    for ns in nss do
+      let ns ← resolveUniqueNamespace ns
+      modifyEnv fun env => addNamespaceAlias env currNamespace ns []
+  | `(Parser.Command.exportDecl| $ns ($ids*)) =>
+    let nss ← resolveNamespace ns
+    let mut aliases := #[]
+    for idStx in ids do
+      let declName ← resolveNameUsingNamespaces nss idStx
+      if (← getInfoState).enabled then
+        addConstInfo idStx declName
+      let aDeclName := currNamespace ++ idStx.getId
+      if aDeclName == declName then
+        throwErrorAt idStx "invalid 'export', self export"
+      aliases := aliases.push (aDeclName, declName)
+    addAliases aliases
+  | `(Parser.Command.exportDecl| $ns hiding $ids*) =>
+    let ns ← resolveUniqueNamespace ns
+    for id in ids do
+      let declName ← resolveNameUsingNamespaces [ns] id
+      if (← getInfoState).enabled then
+        addConstInfo id declName
+    let except := ids.map (·.getId) |>.toList
+    modifyEnv fun env => addNamespaceAlias env currNamespace ns except
+  | `(Parser.Command.exportDecl| $ns renaming $[$froms -> $tos],*) =>
+    let ns ← resolveUniqueNamespace ns
+    let mut aliases := #[]
+    for «from» in froms, to in tos do
+      let declName ← resolveNameUsingNamespaces [ns] «from»
+      if (← getInfoState).enabled then
+        addConstInfo «from» declName
+        addConstInfo to declName
+      let aDeclName := currNamespace ++ to.getId
+      aliases := aliases.push (aDeclName, declName)
+    addAliases aliases
+  | _ => throwUnsupportedSyntax
+where
+  addAliases (aliases : Array (Name × Name)) : CommandElabM Unit :=
+    modifyEnv fun env => aliases.foldl (init := env) fun env p => addAlias env p.1 p.2
+
+@[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do
+  let decl : TSyntax ``Parser.Command.exportDecl := ⟨stx[1]⟩
+  elabExportDecl decl
 
 @[builtin_command_elab «open»] def elabOpen : CommandElab
   | `(open $decl:openDecl) => do

src/Lean/Parser/Command.lean

@@ -539,12 +539,44 @@ def eraseAttr := leading_parser
   "attribute " >> "[" >>
     withoutPosition (sepBy1 (eraseAttr <|> Term.attrInstance) ", ") >>
   "]" >> many1 (ppSpace >> ident)
-/-- Adds names from other namespaces to the current namespace.
+def exportHiding       := leading_parser
+  ppSpace >> atomic (ident >> " hiding") >> many1 (ppSpace >> checkColGt >> ident)
+def exportRenamingItem := leading_parser
+  ident >> unicodeSymbol " → " " -> " >> checkColGt >> ident
+def exportRenaming     := leading_parser
+  ppSpace >> atomic (ident >> " renaming ") >> sepBy1 exportRenamingItem ", "
+def exportOnly         := leading_parser
+  ppSpace >> atomic (ident >> " (") >> many1 ident >> ")"
+def exportNamespace    := leading_parser
+  many1 (ppSpace >> checkColGt >> ident)
+/-- `exportDecl` is the body of an `export` declaration (see `export`) -/
+@[builtin_doc] def exportDecl :=
+  withAntiquot (mkAntiquot "exportDecl" `Lean.Parser.Command.exportDecl (isPseudoKind := true)) <|
+    exportHiding <|> exportRenaming <|> exportOnly <|> exportNamespace
+/--
+Adds aliases into the current namespaces for names from other namespaces.
+
+There are two kinds of aliases:
+* Name aliases make a name `aDecl` refer to another name `dDecl`.
+* Namespace aliases make all names in a namespace `ans` refer to names in another namespace `ns`.
+
+The `export` command be used in a few different ways:
+
+* `export NS₁ … NSₙ` makes the current namespace be an alias for the namespaces `NS₁`, …, `NSₙ`.
+  If the current namespace is `A` and `NSᵢ.x` exists, then this causes `A.x` to be an alias for `NSᵢ.x`.
+
+* `export NS hiding def₁ … defₙ` makes the current namespace be an alias for the namespace `NS`
+  like in `export NS`, but none of the `NS.defᵢ` names are aliased.
+
+* `export NS (def₁ … defₙ)` creates aliases for the names `NS.def₁`, …, `NS.defₙ` in the current namespace.
+  If the current namespace is `A`, then `A.defᵢ` refers to whatever `NS.defᵢ` resolves to.
 
-The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`:
+* `export NS renaming def₁ → def₁', …, defₙ → defₙ'` is like `export NS (def₁ … defₙ)` but it enables
+  naming the aliases; `A.defᵢ'` refers to whatever `NS.defᵢ` resolves to.
 
-- visible in the current namespace without prefix `Some.Namespace`, like `open`, and
-- visible from outside the current namespace `N` as `N.name₁` and `N.name₂`.
+Aliases make names visible in the current namespace without a prefix (like `open`).
+The only rule for `protected` declarations is that when resolving an atomic identifier,
+only non-`protected` declarations are considered.
 
 ## Examples
 
@@ -564,7 +596,7 @@ end Evening.Sky
 ```
 -/
 @[builtin_command_parser] def «export»       := leading_parser
-  "export " >> ident >> " (" >> many1 ident >> ")"
+  withPosition ("export " >> exportDecl)
 @[builtin_command_parser] def «import»       := leading_parser
   "import" -- not a real command, only for error messages
 def openHiding       := leading_parser