reduce copied stuff

ImportGraph.lean

@@ -1,8 +1,5 @@
 import ImportGraph.Cli
 import ImportGraph.Imports
-import ImportGraph.Lean.List
-import ImportGraph.Lean.NameMap
-import ImportGraph.Lean.Process
-import ImportGraph.Lean.TermUnsafe
-import ImportGraph.Name
+import ImportGraph.CurrentModule
+import ImportGraph.Lean.Name
 import ImportGraph.RequiredModules

ImportGraph/Cli.lean

@@ -5,12 +5,12 @@ Authors: Scott Morrison
 -/
 import Lean
 import Cli.Basic
+import Std.Lean.IO.Process
+import Std.Lean.Util.Path
+import Std.Util.TermUnsafe
 import ImportGraph.CurrentModule
-import ImportGraph.Lean.Path
-import ImportGraph.Lean.Process
-import ImportGraph.Lean.TermUnsafe
 import ImportGraph.Imports
-import ImportGraph.Name
+import ImportGraph.Lean.Name
 
 open Cli
 
@@ -75,3 +75,5 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
         IO.eprintln s!"Make sure you have `graphviz` installed and the file is writable."
         throw ex
   return 0
+
+#minimize_imports

ImportGraph/Imports.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean
+import Std.Lean.NameMap
 import ImportGraph.RequiredModules
-import ImportGraph.Lean.List
-import ImportGraph.Lean.NameMap
 
 /-!
 # Tools for analyzing imports.
@@ -140,7 +139,7 @@ def transitiveFilteredUpstream (node : Name) (graph : NameMap (Array Name))
         | none => transitiveFilteredUpstream source graph filter
         | some repl => .cons repl <| transitiveFilteredUpstream source graph filter
       -- If the node is not filtered, we leave the edge `source → node` intact.
-      else [source]).eraseDup'
+      else [source]).eraseDups
 
 /--
 Filters the `graph` removing all nodes where `filter n` returns false. Additionally,
@@ -159,13 +158,13 @@ def filterGraph (graph : NameMap (Array Name)) (filter : Name → Bool)
   -- and remove all imports starting with `Mathlib` to avoid loops.
   let replImports := graph.toList.bind
     (fun ⟨n, i⟩ => if filter n then i.toList else [])
-    |>.eraseDup' |>.filter (¬ Name.isPrefixOf `Mathlib ·) |>.toArray
+    |>.eraseDups |>.filter (¬ Name.isPrefixOf `Mathlib ·) |>.toArray
   let graph := graph.filterMap (fun node edges => if filter node then none else some <|
     -- If the node `node` is not filtered, modify the `edges` going into `node`.
     edges.toList.bind (fun source =>
       if filter source then
         transitiveFilteredUpstream source graph filter (replacement := replacement)
-      else [source]) |>.eraseDup'.toArray)
+      else [source]) |>.eraseDups.toArray)
   -- Add a replacement node if provided.
   match replacement with
   | none => graph

ImportGraph/Lean/Name.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2023 Jon Eugster. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jon Eugster
+-/
+import Lean.Data.Name
+import Lean.CoreM
+import Std.Data.HashMap.Basic
+import Std.Lean.Name
+import Std.Lean.SMap
+
+namespace Lean.Name
+
+open Lean Meta Elab
+open Std
+
+/-- Note: copied from `Mathlib.Lean.Name` -/
+private def isBlackListed (declName : Name) : CoreM Bool := do
+  if declName.toString.startsWith "Lean" then return true
+  let env ← getEnv
+  pure $ declName.isInternalDetail
+   || isAuxRecursor env declName
+   || isNoConfusion env declName
+  <||> isRec declName <||> isMatcher declName
+
+/--
+Retrieve all names in the environment satisfying a predicate.
+
+Note: copied from `Mathlib.Lean.Name`
+-/
+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.
+
+Note: copied from `Mathlib.Lean.Name`
+-/
+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
+
+/-- Returns the very first part of a name: for `ImportGraph.Lean.NameMap` it
+returns `ImportGraph`.
+-/
+def getModule (name : Name) (s := "") : Name :=
+  match name with
+    | .anonymous => s
+    | .num _ _ => panic s!"panic in `getModule`: did not expect numerical name: {name}."
+    | .str pre s => getModule pre s