Lean4
/-- `getDeclName cmd id` takes a `Syntax` input `cmd` and returns the `Name` of the declaration defined
by `cmd`.
-/
def getDeclName (cmd : Syntax) : CommandElabM Name := do
let ns ← getCurrNamespace
let id1 ← getId cmd
let id2 := mkIdentFrom id1 (previousInstName id1.getId)
let some declStx := cmd.find? (·.isOfKind ``Parser.Command.declaration) |
pure default
let some modifiersStx := declStx.find? (·.isOfKind ``Parser.Command.declModifiers) |
pure default
let modifiers : TSyntax ``Parser.Command.declModifiers :=
⟨modifiersStx⟩
-- the `get`/`set` state catches issues with elaboration of, for instance, `scoped` attributes
let s ← get
let modifiers ← elabModifiers modifiers
set s
liftCoreM do
((do
let shortName := id1.getId
let view := extractMacroScopes shortName
let name := view.name
let isRootName := (`_root_).isPrefixOf name
let mut fullName :=
if isRootName then { view with name := name.replacePrefix `_root_ Name.anonymous }.review
else ns ++ shortName
match modifiers.visibility with
| .private =>
return mkPrivateName (← getEnv) fullName
| _ =>
return fullName) <|>
-- try the visible name or the current "nameless" `instance` name
realizeGlobalConstNoOverload id1 <|>
-- otherwise, guess what the previous "nameless" `instance` name was
realizeGlobalConstNoOverload id2 <|>
-- failing everything, use the current namespace followed by the visible name
return ns ++ id1.getId)
