feat: upstream mathlib definitions used for ImportGraph (#481)

Std.lean

@@ -93,6 +93,7 @@ import Std.Lean.Float
 import Std.Lean.Format
 import Std.Lean.HashMap
 import Std.Lean.HashSet
+import Std.Lean.IO.Process
 import Std.Lean.InfoTree
 import Std.Lean.Json
 import Std.Lean.LocalContext
@@ -108,11 +109,13 @@ import Std.Lean.Meta.Simp
 import Std.Lean.Meta.UnusedNames
 import Std.Lean.MonadBacktrack
 import Std.Lean.Name
+import Std.Lean.NameMap
 import Std.Lean.NameMapAttribute
 import Std.Lean.Parser
 import Std.Lean.PersistentHashMap
 import Std.Lean.PersistentHashSet
 import Std.Lean.Position
+import Std.Lean.SMap
 import Std.Lean.System.IO
 import Std.Lean.Tactic
 import Std.Lean.TagAttribute

Std/Lean/IO/Process.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+/-!
+# Running external commands.
+-/
+
+namespace IO.Process
+
+open System (FilePath)
+
+/--
+Pipe `input` into stdin of the spawned process,
+then return `(exitCode, stdout, stdErr)` upon completion.
+-/
+def runCmdWithInput' (cmd : String) (args : Array String)
+    (input : String := "") (throwFailure := true) : IO Output := do
+  let child ← spawn
+    { cmd := cmd, args := args, stdin := .piped, stdout := .piped, stderr := .piped }
+  let (stdin, child) ← child.takeStdin
+  stdin.putStr input
+  stdin.flush
+  let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
+  let err ← child.stderr.readToEnd
+  let exitCode ← child.wait
+  if exitCode != 0 && throwFailure then
+    throw $ IO.userError err
+  else
+    let out ← IO.ofExcept stdout.get
+    return ⟨exitCode, out, err⟩
+
+/--
+Pipe `input` into stdin of the spawned process,
+then return the entire content of stdout as a `String` upon completion.
+-/
+def runCmdWithInput (cmd : String) (args : Array String)
+    (input : String := "") (throwFailure := true) : IO String := do
+  return (← runCmdWithInput' cmd args input throwFailure).stdout

Std/Lean/NameMap.lean

@@ -0,0 +1,43 @@
+/-
+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.NameMap
+
+/-!
+# Additional functions on `Lean.NameMap`.
+
+We provide `NameMap.filter` and `NameMap.filterMap`.
+-/
+
+namespace Lean.NameMap
+
+instance : ForIn m (NameMap β) (Name × β) :=
+  inferInstanceAs <| ForIn m (RBMap Name β _) _
+
+/--
+`filter f m` returns the `NameMap` consisting of all
+"`key`/`val`"-pairs in `m` where `f key val` returns `true`.
+-/
+def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α :=
+  m.fold process {}
+where
+  /-- see `Lean.NameMap.filter` -/
+  process (r : NameMap α) (n : Name) (i : α) :=
+    if f n i then r.insert n i else r
+
+/--
+`filterMap f m` allows to filter a `NameMap` and simultaneously modify the filtered values.
+
+It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`.
+The resulting entries with non-`none` value are collected to form the output `NameMap`.
+-/
+def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β :=
+  m.fold process {}
+where
+  /-- see `Lean.NameMap.filterMap` -/
+  process (r : NameMap β) (n : Name) (i : α) :=
+    match f n i with
+    | none => r
+    | some b => r.insert n b

Std/Lean/SMap.lean

@@ -0,0 +1,17 @@
+/-
+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
+-/
+
+set_option autoImplicit true
+
+/-- 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)