From 16e97002242a48a7c2a96c72131bb1d03a3bfa2a Mon Sep 17 00:00:00 2001
From: Paul Reichert <datokrat@users.noreply.github.com>
Date: Mon, 17 Feb 2025 16:57:11 +0100
Subject: [PATCH] feat: values and valuesArray functions for the tree map
 (#7114)

This PR implements the methods `values` and `valuesArray` on the tree
map.

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
---
 src/Std/Data/DTreeMap/Basic.lean            | 10 ++++++++++
 src/Std/Data/DTreeMap/Internal/Queries.lean |  8 ++++++++
 src/Std/Data/DTreeMap/Raw.lean              |  8 ++++++++
 src/Std/Data/TreeMap/Basic.lean             |  8 ++++++++
 src/Std/Data/TreeMap/Raw.lean               |  8 ++++++++
 5 files changed, 42 insertions(+)

diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean
index b2394507f7..61f06e4d17 100644
--- a/src/Std/Data/DTreeMap/Basic.lean
+++ b/src/Std/Data/DTreeMap/Basic.lean
@@ -786,6 +786,16 @@ def keys (t : DTreeMap α β cmp) : List α :=
 def keysArray (t : DTreeMap α β cmp) : Array α :=
   t.inner.keysArray
 
+/-- Returns a list of all values present in the tree map in ascending  order. -/
+@[inline]
+def values {β : Type v} (t : DTreeMap α β cmp) : List β :=
+  t.inner.values
+
+/-- Returns an array of all values present in the tree map in ascending  order. -/
+@[inline]
+def valuesArray {β : Type v} (t : DTreeMap α β cmp) : Array β :=
+  t.inner.valuesArray
+
 /-- Transforms the tree map into a list of mappings in ascending order. -/
 @[inline]
 def toList (t : DTreeMap α β cmp) : List ((a : α) × β a) :=
diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean
index 3e3a9e9aa8..29d2735db6 100644
--- a/src/Std/Data/DTreeMap/Internal/Queries.lean
+++ b/src/Std/Data/DTreeMap/Internal/Queries.lean
@@ -204,6 +204,14 @@ def forIn {m} [Monad m] (f : δ → (a : α) → β a → m (ForInStep δ)) (ini
 @[inline] def keysArray (t : Impl α β) : Array α :=
   t.foldl (init := #[]) fun l k _ => l.push k
 
+/-- Returns a `List` of the values in order. -/
+@[inline] def values {β : Type v} (t : Impl α β) : List β :=
+  t.foldr (init := []) fun l _ v => v :: l
+
+/-- Returns an `Array` of the values in order. -/
+@[inline] def valuesArray {β : Type v} (t : Impl α β) : Array β :=
+  t.foldl (init := #[]) fun l _ v => l.push v
+
 /-- Returns a `List` of the key/value pairs in order. -/
 @[inline] def toList (t : Impl α β) : List ((a : α) × β a) :=
   t.foldr (init := []) fun l k v => ⟨k, v⟩ :: l
diff --git a/src/Std/Data/DTreeMap/Raw.lean b/src/Std/Data/DTreeMap/Raw.lean
index 51fc4179c7..f1ff8c4f67 100644
--- a/src/Std/Data/DTreeMap/Raw.lean
+++ b/src/Std/Data/DTreeMap/Raw.lean
@@ -575,6 +575,14 @@ def keys (t : Raw α β cmp) : List α :=
 def keysArray (t : Raw α β cmp) : Array α :=
   t.inner.keysArray
 
+@[inline, inherit_doc DTreeMap.values]
+def values {β : Type v} (t : Raw α β cmp) : List β :=
+  t.inner.values
+
+@[inline, inherit_doc DTreeMap.valuesArray]
+def valuesArray {β : Type v} (t : Raw α β cmp) : Array β :=
+  t.inner.valuesArray
+
 @[inline, inherit_doc DTreeMap.toList]
 def toList (t : Raw α β cmp) : List ((a : α) × β a) :=
   t.inner.toList
diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean
index 0e47858655..6c711d3159 100644
--- a/src/Std/Data/TreeMap/Basic.lean
+++ b/src/Std/Data/TreeMap/Basic.lean
@@ -424,6 +424,14 @@ def keys (t : TreeMap α β cmp) : List α :=
 def keysArray (t : TreeMap α β cmp) : Array α :=
   t.inner.keysArray
 
+@[inline, inherit_doc DTreeMap.values]
+def values (t : TreeMap α β cmp) : List β :=
+  t.inner.values
+
+@[inline, inherit_doc DTreeMap.valuesArray]
+def valuesArray (t : TreeMap α β cmp) : Array β :=
+  t.inner.valuesArray
+
 @[inline, inherit_doc DTreeMap.Const.toList]
 def toList (t : TreeMap α β cmp) : List (α × β) :=
   DTreeMap.Const.toList t.inner
diff --git a/src/Std/Data/TreeMap/Raw.lean b/src/Std/Data/TreeMap/Raw.lean
index b3b1e8daa1..51d1177fda 100644
--- a/src/Std/Data/TreeMap/Raw.lean
+++ b/src/Std/Data/TreeMap/Raw.lean
@@ -432,6 +432,14 @@ def keys (t : Raw α β cmp) : List α :=
 def keysArray (t : Raw α β cmp) : Array α :=
   t.inner.keysArray
 
+@[inline, inherit_doc DTreeMap.Raw.values]
+def values (t : Raw α β cmp) : List β :=
+  t.inner.values
+
+@[inline, inherit_doc DTreeMap.Raw.valuesArray]
+def valuesArray (t : Raw α β cmp) : Array β :=
+  t.inner.valuesArray
+
 @[inline, inherit_doc DTreeMap.Raw.Const.toList]
 def toList (t : Raw α β cmp) : List (α × β) :=
   DTreeMap.Raw.Const.toList t.inner