feat: deprecated find, fold, foldM, mergeBy functions for the tree map (

#7036)

This PR adds some deprecated function aliases to the tree map in order
to ease the transition from the `RBMap` to the tree map.

---------

Co-authored-by: Paul Reichert <[email protected]>

src/Std/Data/DTreeMap/Basic.lean

@@ -179,6 +179,10 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 def get? [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) : Option (β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.get? a
 
+@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
+def find? [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) : Option (β a) :=
+  t.get? a
+
 /--
 Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.
 
@@ -197,6 +201,10 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 def get! [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) [Inhabited (β a)]  : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.get! a
 
+@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
+def find! [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) [Inhabited (β a)]  : β a :=
+  t.get! a
+
 /--
 Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 
@@ -206,6 +214,10 @@ Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 def getD [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (fallback : β a) : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.getD a fallback
 
+@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
+def findD [LawfulEqCmp cmp] (t : DTreeMap α β cmp) (a : α) (fallback : β a) : β a :=
+  t.getD a fallback
+
 namespace Const
 open Internal (Impl)
 
@@ -218,6 +230,10 @@ Tries to retrieve the mapping for the given key, returning `none` if no such map
 def get? (t : DTreeMap α β cmp) (a : α) : Option β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get? a t.inner
 
+@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
+def find? (t : DTreeMap α β cmp) (a : α) : Option β :=
+  get? t a
+
 /--
 Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.
 -/
@@ -232,13 +248,21 @@ Tries to retrieve the mapping for the given key, panicking if no such mapping is
 def get! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get! a t.inner
 
+@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
+def find! (t : DTreeMap α β cmp) (a : α) [Inhabited β] : β :=
+  get! t a
+
 /--
 Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 -/
 @[inline]
 def getD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.getD a t.inner fallback
 
+@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
+def findD (t : DTreeMap α β cmp) (a : α) (fallback : β) : β :=
+  getD t a fallback
+
 end Const
 
 variable {δ : Type w} {m : Type w → Type w₂} [Monad m]
@@ -255,13 +279,21 @@ Folds the given monadic function over the mappings in the map in ascending order
 def foldlM (f : δ → (a : α) → β a → m δ) (init : δ) (t : DTreeMap α β cmp) : m δ :=
   t.inner.foldlM f init
 
+@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
+def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (t : DTreeMap α β cmp) : m δ :=
+  t.foldlM f init
+
 /--
 Folds the given function over the mappings in the map in ascending order.
 -/
 @[inline]
 def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
   t.inner.foldl f init
 
+@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
+def fold (f : δ → (a : α) → β a → δ) (init : δ) (t : DTreeMap α β cmp) : δ :=
+  t.foldl f init
+
 /-- Carries out a monadic action on each mapping in the tree map in ascending order. -/
 @[inline]
 def forM (f : (a : α) → β a → m PUnit) (t : DTreeMap α β cmp) : m PUnit :=
@@ -332,6 +364,11 @@ def mergeWith [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a)
     DTreeMap α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.mergeWith mergeFn t₂.inner t₁.wf.balanced |>.impl, t₁.wf.mergeWith⟩
 
+@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
+def mergeBy [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : DTreeMap α β cmp) :
+    DTreeMap α β cmp :=
+  mergeWith mergeFn t₁ t₂
+
 namespace Const
 
 variable {β : Type v}
@@ -349,6 +386,10 @@ def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : DTreeMap α β cm
   letI : Ord α := ⟨cmp⟩;
   ⟨Impl.Const.mergeWith mergeFn t₁.inner t₂.inner t₁.wf.balanced |>.impl, t₁.wf.constMergeBy⟩
 
+@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
+def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp :=
+  mergeWith mergeFn t₁ t₂
+
 end Const
 
 /--

src/Std/Data/DTreeMap/Raw.lean

@@ -150,6 +150,10 @@ def erase (t : Raw α β cmp) (a : α) : Raw α β cmp :=
 def get? [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) : Option (β a) :=
   letI : Ord α := ⟨cmp⟩; t.inner.get? a
 
+@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
+def find? [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) : Option (β a) :=
+  t.get? a
+
 @[inline, inherit_doc DTreeMap.get]
 def get [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.get a h
@@ -158,18 +162,31 @@ def get [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : β a :=
 def get! [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) [Inhabited (β a)]  : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.get! a
 
+@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
+def find! [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) [Inhabited (β a)]  : β a :=
+  t.get! a
+
 @[inline, inherit_doc DTreeMap.getD]
 def getD [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (fallback : β a) : β a :=
   letI : Ord α := ⟨cmp⟩; t.inner.getD a fallback
 
+@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
+def findD [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (fallback : β a) : β a :=
+  t.getD a fallback
+
 namespace Const
 open Internal (Impl)
 
 variable {β : Type v}
 
-@[inline, inherit_doc DTreeMap.get?] def get? (t : Raw α β cmp) (a : α) : Option β :=
+@[inline, inherit_doc DTreeMap.get?]
+def get? (t : Raw α β cmp) (a : α) : Option β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get? a t.inner
 
+@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
+def find? (t : Raw α β cmp) (a : α) : Option β :=
+  get? t a
+
 @[inline, inherit_doc DTreeMap.get]
 def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get a t.inner h
@@ -178,10 +195,18 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
 def get! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.get! a t.inner
 
+@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
+def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
+  get! t a
+
 @[inline, inherit_doc DTreeMap.getD]
 def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
   letI : Ord α := ⟨cmp⟩; Impl.Const.getD a t.inner fallback
 
+@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
+def findD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
+  getD t a fallback
+
 end Const
 
 variable {δ : Type w} {m : Type w → Type w₂} [Monad m]
@@ -194,10 +219,18 @@ def filter (f : (a : α) → β a → Bool) (t : Raw α β cmp) : Raw α β cmp
 def foldlM (f : δ → (a : α) → β a → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.foldlM f init
 
+@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
+def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
+  t.foldlM f init
+
 @[inline, inherit_doc DTreeMap.foldl]
 def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : Raw α β cmp) : δ :=
   t.inner.foldl f init
 
+@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
+def fold (f : δ → (a : α) → β a → δ) (init : δ) (t : Raw α β cmp) : δ :=
+  t.foldl f init
+
 @[inline, inherit_doc DTreeMap.forM]
 def forM (f : (a : α) → β a → m PUnit) (t : Raw α β cmp) : m PUnit :=
   t.inner.forM f
@@ -244,6 +277,11 @@ def toArray (t : Raw α β cmp) : Array ((a : α) × β a) :=
 def mergeWith [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.mergeWith! mergeFn t₂.inner⟩
 
+@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
+def mergeBy [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Raw α β cmp) :
+    Raw α β cmp :=
+  mergeWith mergeFn t₁ t₂
+
 namespace Const
 open Internal (Impl)
 
@@ -261,6 +299,10 @@ def toArray (t : Raw α β cmp) : Array (α × β) :=
 def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
   letI : Ord α := ⟨cmp⟩; ⟨Impl.Const.mergeWith! mergeFn t₁.inner t₂.inner⟩
 
+@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
+def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
+  mergeWith mergeFn t₁ t₂
+
 end Const
 
 @[inline, inherit_doc DTreeMap.eraseMany]

src/Std/Data/TreeMap/Basic.lean

@@ -129,6 +129,10 @@ def erase (t : TreeMap α β cmp) (a : α) : TreeMap α β cmp :=
 def get? (t : TreeMap α β cmp) (a : α) : Option β :=
   DTreeMap.Const.get? t.inner a
 
+@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
+def find? (t : TreeMap α β cmp) (a : α) : Option β :=
+  get? t a
+
 @[inline, inherit_doc DTreeMap.get]
 def get (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
    DTreeMap.Const.get t.inner a h
@@ -137,10 +141,18 @@ def get (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β :=
 def get! (t : TreeMap α β cmp) (a : α) [Inhabited β]  : β :=
   DTreeMap.Const.get! t.inner a
 
+@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
+def find! (t : TreeMap α β cmp) (a : α) [Inhabited β] : β :=
+  get! t a
+
 @[inline, inherit_doc DTreeMap.getD]
 def getD (t : TreeMap α β cmp) (a : α) (fallback : β) : β :=
   DTreeMap.Const.getD t.inner a fallback
 
+@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
+def findD (t : TreeMap α β cmp) (a : α) (fallback : β) : β :=
+  getD t a fallback
+
 instance : GetElem? (TreeMap α β cmp) α β (fun m a => a ∈ m) where
   getElem m a h := m.get a h
   getElem? m a := m.get? a
@@ -156,10 +168,18 @@ def filter (f : α → β → Bool) (m : TreeMap α β cmp) : TreeMap α β cmp
 def foldlM (f : δ → (a : α) → β → m δ) (init : δ) (t : TreeMap α β cmp) : m δ :=
   t.inner.foldlM f init
 
+@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
+def foldM (f : δ → (a : α) → β → m δ) (init : δ) (t : TreeMap α β cmp) : m δ :=
+  t.foldlM f init
+
 @[inline, inherit_doc DTreeMap.foldl]
 def foldl (f : δ → (a : α) → β → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
   t.inner.foldl f init
 
+@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
+def fold (f : δ → (a : α) → β → δ) (init : δ) (t : TreeMap α β cmp) : δ :=
+  t.foldl f init
+
 @[inline, inherit_doc DTreeMap.forM]
 def forM (f : α → β → m PUnit) (t : TreeMap α β cmp) : m PUnit :=
   t.inner.forM f
@@ -202,6 +222,10 @@ def toArray (t : TreeMap α β cmp) : Array (α × β) :=
 def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
   ⟨DTreeMap.Const.mergeWith mergeFn t₁.inner t₂.inner⟩
 
+@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
+def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp :=
+  mergeWith mergeFn t₁ t₂
+
 @[inline, inherit_doc DTreeMap.eraseMany]
 def eraseMany {ρ} [ForIn Id ρ α] (t : TreeMap α β cmp) (l : ρ) : TreeMap α β cmp :=
   ⟨t.inner.eraseMany l⟩

src/Std/Data/TreeMap/Raw.lean

@@ -147,6 +147,10 @@ def erase (t : Raw α β cmp) (a : α) : Raw α β cmp :=
 def get? (t : Raw α β cmp) (a : α) : Option β :=
   DTreeMap.Raw.Const.get? t.inner a
 
+@[inline, inherit_doc get?, deprecated get? (since := "2025-02-12")]
+def find? (t : Raw α β cmp) (a : α) : Option β :=
+  get? t a
+
 @[inline, inherit_doc DTreeMap.Raw.Const.get]
 def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
   DTreeMap.Raw.Const.get t.inner a h
@@ -155,10 +159,18 @@ def get (t : Raw α β cmp) (a : α) (h : a ∈ t) : β :=
 def get! (t : Raw α β cmp) (a : α) [Inhabited β]  : β :=
   DTreeMap.Raw.Const.get! t.inner a
 
+@[inline, inherit_doc get!, deprecated get! (since := "2025-02-12")]
+def find! (t : Raw α β cmp) (a : α) [Inhabited β] : β :=
+  get! t a
+
 @[inline, inherit_doc DTreeMap.Raw.Const.getD]
 def getD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
   DTreeMap.Raw.Const.getD t.inner a fallback
 
+@[inline, inherit_doc getD, deprecated getD (since := "2025-02-12")]
+def findD (t : Raw α β cmp) (a : α) (fallback : β) : β :=
+  getD t a fallback
+
 instance : GetElem? (Raw α β cmp) α β (fun m a => a ∈ m) where
   getElem m a h := m.get a h
   getElem? m a := m.get? a
@@ -174,10 +186,18 @@ def filter (f : α → β → Bool) (t : Raw α β cmp) : Raw α β cmp :=
 def foldlM (f : δ → (a : α) → β → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
   t.inner.foldlM f init
 
+@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
+def foldM (f : δ → (a : α) → β → m δ) (init : δ) (t : Raw α β cmp) : m δ :=
+  t.foldlM f init
+
 @[inline, inherit_doc DTreeMap.Raw.foldl]
 def foldl (f : δ → (a : α) → β → δ) (init : δ) (t : Raw α β cmp) : δ :=
   t.inner.foldl f init
 
+@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
+def fold (f : δ → (a : α) → β → δ) (init : δ) (t : Raw α β cmp) : δ :=
+  t.foldl f init
+
 @[inline, inherit_doc DTreeMap.Raw.forM]
 def forM (f : α → β → m PUnit) (t : Raw α β cmp) : m PUnit :=
   t.inner.forM f
@@ -220,6 +240,10 @@ def toArray (t : Raw α β cmp) : Array (α × β) :=
 def mergeWith (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
   ⟨DTreeMap.Raw.Const.mergeWith mergeFn t₁.inner t₂.inner⟩
 
+@[inline, inherit_doc mergeWith, deprecated mergeWith (since := "2025-02-12")]
+def mergeBy (mergeFn : α → β → β → β) (t₁ t₂ : Raw α β cmp) : Raw α β cmp :=
+  mergeWith mergeFn t₁ t₂
+
 @[inline, inherit_doc DTreeMap.Raw.eraseMany]
 def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α β cmp) (l : ρ) : Raw α β cmp :=
   ⟨t.inner.eraseMany l⟩

src/Std/Data/TreeSet/Basic.lean

@@ -162,11 +162,19 @@ ascending order.
 def foldlM {m δ} [Monad m] (f : δ → (a : α) → m δ) (init : δ) (t : TreeSet α cmp) : m δ :=
   t.inner.foldlM (fun c a _ => f c a) init
 
+@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
+def foldM (f : δ → (a : α) → m δ) (init : δ) (t : TreeSet α cmp) : m δ :=
+  t.foldlM f init
+
 /-- Folds the given function over the elements of the tree set in ascending order. -/
 @[inline]
 def foldl (f : δ → (a : α) → δ) (init : δ) (t : TreeSet α cmp) : δ :=
   t.inner.foldl (fun c a _ => f c a) init
 
+@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
+def fold (f : δ → (a : α) → δ) (init : δ) (t : TreeSet α cmp) : δ :=
+  t.foldl f init
+
 /-- Carries out a monadic action on each element in the tree set in ascending order. -/
 @[inline]
 def forM (f : α → m PUnit) (t : TreeSet α cmp) : m PUnit :=

src/Std/Data/TreeSet/Raw.lean

@@ -143,10 +143,18 @@ def filter (f : α → Bool) (t : Raw α cmp) : Raw α cmp :=
 def foldlM (f : δ → (a : α) → m δ) (init : δ) (t : Raw α cmp) : m δ :=
   t.inner.foldlM (fun c a _ => f c a) init
 
+@[inline, inherit_doc foldlM, deprecated foldlM (since := "2025-02-12")]
+def foldM (f : δ → (a : α) → m δ) (init : δ) (t : Raw α cmp) : m δ :=
+  t.foldlM f init
+
 @[inline, inherit_doc TreeSet.empty]
 def foldl (f : δ → (a : α) → δ) (init : δ) (t : Raw α cmp) : δ :=
   t.inner.foldl (fun c a _ => f c a) init
 
+@[inline, inherit_doc foldl, deprecated foldl (since := "2025-02-12")]
+def fold (f : δ → (a : α) → δ) (init : δ) (t : Raw α cmp) : δ :=
+  t.foldl f init
+
 @[inline, inherit_doc TreeSet.empty]
 def forM (f : α → m PUnit) (t : Raw α cmp) : m PUnit :=
   t.inner.forM (fun a _ => f a)