feat: command to list declarations with long names (#3122)

This adds commands `#long_names` and `#long_instances`, useful for finding declarations with excessively long names.

~~I also add explicit names to some of the files that produce instances with names over 80 characters; can do more later.~~



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

Mathlib.lean

@@ -1242,6 +1242,8 @@ import Mathlib.Lean.LocalContext
 import Mathlib.Lean.Message
 import Mathlib.Lean.Meta
 import Mathlib.Lean.Meta.Simp
+import Mathlib.Lean.Name
+import Mathlib.Lean.SMap
 import Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
 import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
@@ -1839,6 +1841,7 @@ import Mathlib.Util.AssertNoSorry
 import Mathlib.Util.AtomM
 import Mathlib.Util.Export
 import Mathlib.Util.IncludeStr
+import Mathlib.Util.LongNames
 import Mathlib.Util.MemoFix
 import Mathlib.Util.Syntax
 import Mathlib.Util.SynthesizeUsing

Mathlib/Lean/Name.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Std.Data.HashMap
+import Mathlib.Lean.SMap
+import Mathlib.Lean.Expr.Basic
+
+/-!
+# Additional functions on `Lean.Name`.
+
+We provide `Name.getModule : Name → CoreM (Option Name)`,
+and `allNames` and `allNamesByModule`.
+-/
+
+open Lean Meta Elab
+
+private def isBlackListed (declName : Name) : CoreM Bool := do
+  if declName.toString.startsWith "Lean" then return true
+  let env ← getEnv
+  pure $ declName.isInternal'
+   || isAuxRecursor env declName
+   || isNoConfusion env declName
+  <||> isRec declName <||> isMatcher declName
+
+/--
+Retrieve all names in the environment satisfying a predicate.
+-/
+def allNames (p : Name → Bool) : CoreM (Array Name) := do
+  (← getEnv).constants.foldM (init := #[]) fun names n _ => do
+    if p n && !(← isBlackListed n) then
+      return names.push n
+    else
+      return names
+
+/--
+Retrieve all names in the environment satisfying a predicate,
+gathered together into a `HashMap` according to the module they are defined in.
+-/
+def allNamesByModule (p : Name → Bool) : CoreM (Std.HashMap Name (Array Name)) := do
+  (← getEnv).constants.foldM (init := Std.HashMap.empty) fun names n _ => do
+    if p n && !(← isBlackListed n) then
+      let some m ← findModuleOf? n | return names
+      -- TODO use `Std.HashMap.modify` when we bump Std4 (or `alter` if that is written).
+      match names.find? m with
+      | some others => return names.insert m (others.push n)
+      | none => return names.insert m #[n]
+    else
+      return names

Mathlib/Lean/SMap.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Lean.Data.SMap
+
+/-!
+# Extra functions on Lean.SMap
+-/
+
+/-- Monadic fold over a staged map. -/
+def Lean.SMap.foldM {m : Type w → Type w} [Monad m] [BEq α] [Hashable α]
+    (f : σ → α → β → m σ) (init : σ) (map : SMap α β) : m σ := do
+  map.map₂.foldlM f (← map.map₁.foldM f init)

Mathlib/Util/LongNames.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Mathlib.Lean.Name
+import Mathlib.Lean.Expr.Basic
+
+/-!
+# Commands `#long_names` and `#long_instances`
+
+For finding declarations with excessively long names.
+-/
+
+open Lean Meta Elab
+
+/-- Helper function for `#long_names` and `#long_instances`. -/
+def printNameHashMap (h : Std.HashMap Name (Array Name)) : IO Unit :=
+  for (m, names) in h.toList do
+    IO.println "----"
+    IO.println $ m.toString ++ ":"
+    for n in names do
+      IO.println n
+
+/--
+Lists all declarations with a long name, gathered according to the module they are defined in.
+Use as `#long_names` or `#long_names 100` to specify the length.
+-/
+elab "#long_names " N:(num)? : command =>
+  Command.runTermElabM fun _ => do
+    let N := N.map TSyntax.getNat |>.getD 50
+    let namesByModule ← allNamesByModule (fun n => n.toString.length > N)
+    let namesByModule := namesByModule.filter fun m _ => m.getRoot.toString = "Mathlib"
+    printNameHashMap namesByModule
+
+/--
+Lists all instances with a long name beginning with `inst`,
+gathered according to the module they are defined in.
+This is useful for finding automatically named instances with absurd names.
+
+Use as `#long_names` or `#long_names 100` to specify the length.
+-/
+elab "#long_instances " N:(num)?: command =>
+  Command.runTermElabM fun _ => do
+    let N := N.map TSyntax.getNat |>.getD 50
+    let namesByModule ← allNamesByModule
+      (fun n => n.getString.startsWith "inst" && n.getString.length > N)
+    let namesByModule := namesByModule.filter fun m _ => m.getRoot.toString = "Mathlib"
+    printNameHashMap namesByModule