DupNamespace.lean

/-
Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Różowski

Copyright (c) 2023 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/
module

prelude
public import Lean.Elab.Command
public import Lean.Linter.Basic

public section

namespace Lean.Linter.Extra
open Lean Parser Elab Command Meta Linter

/--
The `dupNamespace` linter is set off by default.  Lean emits a warning on any declaration that
contains the same namespace more than once.

By default, only consecutive duplication is reported: `Nat.Nat.foo` and `One.two.two` trigger a
warning, while `Nat.One.Nat` does not. Setting `linter.extra.dupNamespace.consecutiveOnly` to
`false` also reports non-consecutive duplication, so that `Nat.One.Nat` triggers a warning as well.
-/

register_builtin_option linter.extra.dupNamespace : Bool := {
  defValue := false
  descr := "enable the duplicated namespace linter"
}

register_builtin_option linter.extra.dupNamespace.consecutiveOnly : Bool := {
  defValue := true
  descr := "only warn on consecutive duplicated namespaces"
}

namespace DupNamespaceLinter

open Lean Parser Elab Command Meta Linter

/--
If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers
for the names of the declarations whose syntax begins in position at least `pos`.
-/
def getNamesFrom {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos.Raw) :
    m (Array Syntax) := do
  -- declarations from parallelism branches should not be interesting here, so use `local`
  let drs := declRangeExt.toPersistentEnvExtension.getState (asyncMode := .local) (← getEnv)
  let fm ← getFileMap
  let mut nms := #[]
  for (nm, rgs) in drs do
    if pos ≤ fm.ofPosition rgs.range.pos then
      let ofPos1 := fm.ofPosition rgs.selectionRange.pos
      let ofPos2 := fm.ofPosition rgs.selectionRange.endPos
      nms := nms.push (mkIdentFrom (.ofRange ⟨ofPos1, ofPos2⟩) nm)
  return nms

/--
If `stx` is a syntax node for an `export` statement, then `getAliasSyntax stx` returns the array of
identifiers with the "exported" names.
-/
def getAliasSyntax {m} [Monad m] [MonadResolveName m] (stx : Syntax) : m (Array Syntax) := do
  let mut aliases := #[]
  if let `(export $_ ($ids*)) := stx then
    let currNamespace ← getCurrNamespace
    for idStx in ids do
      let id := idStx.getId
      aliases := aliases.push
        (mkIdentFrom (.ofRange (idStx.raw.getRange?.getD default)) (currNamespace ++ id))
  return aliases

@[inherit_doc linter.extra.dupNamespace]
def dupNamespace : Linter where run := withSetOptionIn fun stx ↦ do
  if getLinterValue linter.extra.dupNamespace (← getLinterOptions) then
    let mut aliases := #[]
    if let some exp := stx.find? (·.isOfKind `Lean.Parser.Command.export) then
      aliases ← getAliasSyntax exp
    for id in (← getNamesFrom (stx.getPos?.getD default)) ++ aliases do
      let declName := id.getId
      if declName.hasMacroScopes || isPrivateName declName then continue
      let nm := declName.components
      let duplicated :=
        if (← getBoolOption `linter.extra.dupNamespace.consecutiveOnly (defValue := true)) then
          -- Only check consecutive components
          nm.zip (nm.tailD []) |>.filterMap fun (x, y) ↦ if x == y then some x else none
        else
          -- Collect distinct components which appear more than once.
          List.eraseDups <| nm.filter (fun comp ↦ nm.count comp > 1)
      match duplicated with
      | [] => continue
      | [ns] =>
        Linter.logLint linter.extra.dupNamespace id
          m!"The namespace `{ns}` is duplicated in the declaration \
          `{.ofConstName (fullNames := true) declName}`."
      | _ =>
        let ns := MessageData.andList (duplicated.map (m!"`{·}`"))
        Linter.logLint linter.extra.dupNamespace id
          m!"The namespaces {ns} are duplicated in the declaration \
          `{.ofConstName (fullNames := true) declName}`."

end DupNamespaceLinter

builtin_initialize addLinter DupNamespaceLinter.dupNamespace

end Lean.Linter.Extra