From 6ac530aa1a3c4a3cb7c036510d2f4d3744926acb Mon Sep 17 00:00:00 2001 From: Paul Reichert Date: Thu, 13 Feb 2025 12:12:22 +0100 Subject: [PATCH] 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 <6992158+datokrat@users.noreply.github.com> --- src/Std/Data/DTreeMap/Basic.lean | 41 +++++++++++++++++++++++++++++ src/Std/Data/DTreeMap/Raw.lean | 44 +++++++++++++++++++++++++++++++- src/Std/Data/TreeMap/Basic.lean | 24 +++++++++++++++++ src/Std/Data/TreeMap/Raw.lean | 24 +++++++++++++++++ src/Std/Data/TreeSet/Basic.lean | 8 ++++++ src/Std/Data/TreeSet/Raw.lean | 8 ++++++ 6 files changed, 148 insertions(+), 1 deletion(-) diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean index 02ffab441a..368b1583eb 100644 --- a/src/Std/Data/DTreeMap/Basic.lean +++ b/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,6 +248,10 @@ 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. -/ @@ -239,6 +259,10 @@ Tries to retrieve the mapping for the given key, returning `fallback` if no such 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,6 +279,10 @@ 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. -/ @@ -262,6 +290,10 @@ Folds the given function over the mappings in the map in ascending order. 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 /-- diff --git a/src/Std/Data/DTreeMap/Raw.lean b/src/Std/Data/DTreeMap/Raw.lean index c4dd2dba62..ecd0c037b6 100644 --- a/src/Std/Data/DTreeMap/Raw.lean +++ b/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] diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean index 039eade34a..e7f3bcbd37 100644 --- a/src/Std/Data/TreeMap/Basic.lean +++ b/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⟩ diff --git a/src/Std/Data/TreeMap/Raw.lean b/src/Std/Data/TreeMap/Raw.lean index 543906c4aa..6aa336ac33 100644 --- a/src/Std/Data/TreeMap/Raw.lean +++ b/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⟩ diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean index 7a6ca8062e..db970340bd 100644 --- a/src/Std/Data/TreeSet/Basic.lean +++ b/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 := diff --git a/src/Std/Data/TreeSet/Raw.lean b/src/Std/Data/TreeSet/Raw.lean index e44acb2bd8..e3d5b045d5 100644 --- a/src/Std/Data/TreeSet/Raw.lean +++ b/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)