refactor: make DHashMap.Raw.foldRev(M) internal (#7380)

This PR moves `DHashMap.Raw.foldRev(M)` into `DHashMap.Raw.Internal`.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -1031,11 +1031,11 @@ theorem fold_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} :
 
 theorem foldRevM_eq_foldrM_toList [Monad m'] [LawfulMonad m']
     {f : δ → (a : α) → β a → m' δ} {init : δ} :
-    m.1.foldRevM f init = m.1.toList.foldrM (fun a b => f b a.1 a.2) init := by
+    Raw.Internal.foldRevM f init m.1 = m.1.toList.foldrM (fun a b => f b a.1 a.2) init := by
   simp_to_model [foldRevM, toList]
 
 theorem foldRev_eq_foldr_toList {f : δ → (a : α) → β a → δ} {init : δ} :
-    m.1.foldRev f init = m.1.toList.foldr (fun a b => f b a.1 a.2) init := by
+    Raw.Internal.foldRev f init m.1 = m.1.toList.foldr (fun a b => f b a.1 a.2) init := by
   simp_to_model [foldRev, toList]
 
 theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} :
@@ -1058,11 +1058,13 @@ theorem fold_eq_foldl_keys {f : δ → α → δ} {init : δ} :
 
 theorem foldRevM_eq_foldrM_keys [Monad m'] [LawfulMonad m']
     {f : δ → (a : α) → m' δ} {init : δ} :
-    m.1.foldRevM (fun d a _ => f d a) init = m.1.keys.foldrM (fun a b => f b a) init := by
+    Raw.Internal.foldRevM (fun d a _ => f d a) init m.1 =
+      m.1.keys.foldrM (fun a b => f b a) init := by
   simp_to_model [foldRevM, keys] using List.foldrM_eq_foldrM_keys'
 
 theorem foldRev_eq_foldr_keys {f : δ → (a : α) → δ} {init : δ} :
-    m.1.foldRev (fun d a _ => f d a) init = m.1.keys.foldr (fun a b => f b a) init := by
+    Raw.Internal.foldRev (fun d a _ => f d a) init m.1 =
+      m.1.keys.foldr (fun a b => f b a) init := by
   simp_to_model [foldRev, keys] using List.foldr_eq_foldr_keys'
 
 theorem forM_eq_forM_keys [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
@@ -1089,11 +1091,14 @@ theorem fold_eq_foldl_toList {f : δ → (a : α) → β → δ} {init : δ} :
 
 theorem foldRevM_eq_foldrM_toList [Monad m'] [LawfulMonad m']
     {f : δ → (a : α) → β → m' δ} {init : δ} :
-    m.1.foldRevM f init = (Raw.Const.toList m.1).foldrM (fun a b => f b a.1 a.2) init := by
+    Raw.Internal.foldRevM f init m.1 =
+      (Raw.Const.toList m.1).foldrM (fun a b => f b a.1 a.2) init := by
+  have :=Raw.foldRevM_eq_foldrM_toListModel (m := m') (b := m.1) (init := init) (f := f)
+
   simp_to_model [foldRevM, Const.toList] using List.foldrM_eq_foldrM_toProd'
 
 theorem foldRev_eq_foldr_toList {f : δ → (a : α) → β → δ} {init : δ} :
-    m.1.foldRev f init = (Raw.Const.toList m.1).foldr (fun a b => f b a.1 a.2) init := by
+    Raw.Internal.foldRev f init m.1 = (Raw.Const.toList m.1).foldr (fun a b => f b a.1 a.2) init := by
   simp_to_model [foldRev, Const.toList] using List.foldr_eq_foldr_toProd'
 
 theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : (a : α) → β → m' PUnit} :

src/Std/Data/DHashMap/Internal/WF.lean

@@ -88,12 +88,13 @@ theorem fold_cons_key {l : Raw α β} {acc : List α} :
   rw [fold_cons_apply, keys_eq_map, map_reverse]
 
 theorem foldRev_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
-    l.foldRev f init = l.buckets.foldr (fun l acc => l.foldr (fun a b g => f g a b) acc) init := by
-  simp only [Raw.foldRev, Raw.foldRevM, ← Array.foldrM_toList, Array.foldr_toList,
+    Raw.Internal.foldRev f init l =
+      l.buckets.foldr (fun l acc => l.foldr (fun a b g => f g a b) acc) init := by
+  simp only [Raw.Internal.foldRev, Raw.Internal.foldRevM, ← Array.foldrM_toList, Array.foldr_toList,
     ← List.foldr_eq_foldrM, Id.run, AssocList.foldr]
 
 theorem foldRev_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
-    l.foldRev (fun acc k v => f k v :: acc) acc =
+    Raw.Internal.foldRev (fun acc k v => f k v :: acc) acc l =
       ((toListModel l.buckets).map (fun p => f p.1 p.2)) ++ acc := by
   rw [foldRev_eq, ← Array.foldr_toList, toListModel]
   induction l.buckets.toList generalizing acc with
@@ -103,16 +104,17 @@ theorem foldRev_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β
       simp
 
 theorem foldRev_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
-    l.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc = toListModel l.buckets ++ acc := by
+    Raw.Internal.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc l = toListModel l.buckets ++ acc := by
   simp [foldRev_cons_apply]
 
 theorem foldRev_cons_mk {β : Type v} {l : Raw α (fun _ => β)} {acc : List (α × β)} :
-    l.foldRev (fun acc k v => (k, v) :: acc) acc =
+    Raw.Internal.foldRev (fun acc k v => (k, v) :: acc) acc l =
       (toListModel l.buckets).map (fun ⟨k, v⟩ => (k, v)) ++ acc := by
   simp [foldRev_cons_apply]
 
 theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
-    l.foldRev (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets) ++ acc := by
+    Raw.Internal.foldRev (fun acc k _ => k :: acc) acc l =
+      List.keys (toListModel l.buckets) ++ acc := by
   rw [foldRev_cons_apply, keys_eq_map]
 
 theorem foldM_eq_foldlM_toListModel {δ : Type w} {m : Type w → Type w } [Monad m] [LawfulMonad m]
@@ -138,8 +140,9 @@ theorem fold_eq_foldl_toListModel {l : Raw α β} {f : γ → (a : α) → β a
 
 theorem foldRevM_eq_foldrM_toListModel {δ : Type w} {m : Type w → Type w } [Monad m] [LawfulMonad m]
     {f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :
-    b.foldRevM f init = (toListModel b.buckets).foldrM (fun a b => f b a.1 a.2) init := by
-  simp only [Raw.foldRevM, ← Array.foldrM_toList, toListModel]
+    Raw.Internal.foldRevM f init b =
+      (toListModel b.buckets).foldrM (fun a b => f b a.1 a.2) init := by
+  simp only [Raw.Internal.foldRevM, ← Array.foldrM_toList, toListModel]
   induction b.buckets.toList generalizing init with
   | nil => simp
   | cons hd tl ih =>
@@ -154,8 +157,9 @@ theorem foldRevM_eq_foldrM_toListModel {δ : Type w} {m : Type w → Type w } [M
       rw [ih]
 
 theorem foldRev_eq_foldr_toListModel {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
-    l.foldRev f init = (toListModel l.buckets).foldr (fun a b => f b a.1 a.2) init := by
-  simp [Raw.foldRev, foldRevM_eq_foldrM_toListModel]
+    Raw.Internal.foldRev f init l =
+      (toListModel l.buckets).foldr (fun a b => f b a.1 a.2) init := by
+  simp [Raw.Internal.foldRev, foldRevM_eq_foldrM_toListModel]
 
 theorem toList_eq_toListModel {m : Raw α β} : m.toList = toListModel m.buckets := by
   simp [Raw.toList, foldRev_cons]

src/Std/Data/DHashMap/Raw.lean

@@ -356,7 +356,11 @@ map in some order.
 @[inline] def fold (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ :=
   Id.run (b.foldM f init)
 
+namespace Internal
+
 /--
+Internal implementation detail of the hash map.
+
 Monadically computes a value by folding the given function over the mappings in the hash
 map in the reverse order used by `foldM`.
 -/
@@ -364,10 +368,31 @@ map in the reverse order used by `foldM`.
   b.buckets.foldrM (fun l acc => l.foldrM (fun a b d => f d a b) acc) init
 
 /--
+Internal implementation detail of the hash map.
+
 Folds the given function over the mappings in the hash map in the reverse order used
 by `foldM`. -/
 @[inline] def foldRev (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ :=
-  Id.run (b.foldRevM f init)
+  Id.run (foldRevM f init b)
+
+end Internal
+
+/--
+Monadically computes a value by folding the given function over the mappings in the hash
+map in the reverse order used by `foldM`.
+-/
+@[inline, deprecated "Deprecated without replacement. If the order does not matter, use foldM."
+  (since := "2025-03-07")]
+def foldRevM (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ :=
+  b.buckets.foldrM (fun l acc => l.foldrM (fun a b d => f d a b) acc) init
+
+/--
+Folds the given function over the mappings in the hash map in the reverse order used
+by `foldM`. -/
+@[inline, deprecated "Deprecated without replacement. If the order does not matter, use fold."
+  (since := "2025-03-07")]
+def foldRev (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ :=
+  Id.run (Internal.foldRevM f init b)
 
 /-- Carries out a monadic action on each mapping in the hash map in some order. -/
 @[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit :=
@@ -443,7 +468,7 @@ only those mappings where the function returns `some` value.
 
 /-- Returns a list of all values present in the hash map in some order. -/
 @[inline] def values {β : Type v} (m : Raw α (fun _ => β)) : List β :=
-  m.foldRev (fun acc _ v => v :: acc) []
+  Internal.foldRev (fun acc _ v => v :: acc) [] m
 
 /-- Returns an array of all values present in the hash map in some order. -/
 @[inline] def valuesArray {β : Type v} (m : Raw α (fun _ => β)) : Array β :=
@@ -509,18 +534,18 @@ end Unverified
 
 /-- Transforms the hash map into a list of mappings in some order. -/
 @[inline] def toList (m : Raw α β) : List ((a : α) × β a) :=
-  m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
+  Internal.foldRev (fun acc k v => ⟨k, v⟩ :: acc) [] m
 
 @[inline, inherit_doc Raw.toList] def Const.toList {β : Type v} (m : Raw α (fun _ => β)) :
     List (α × β) :=
-  m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
+  Internal.foldRev (fun acc k v => ⟨k, v⟩ :: acc) [] m
 
 instance [Repr α] [(a : α) → Repr (β a)] : Repr (Raw α β) where
   reprPrec m prec := Repr.addAppParen ("Std.DHashMap.Raw.ofList " ++ reprArg m.toList) prec
 
 /-- Returns a list of all keys present in the hash map in some order. -/
 @[inline] def keys (m : Raw α β) : List α :=
-  m.foldRev (fun acc k _ => k :: acc) []
+  Internal.foldRev (fun acc k _ => k :: acc) [] m
 
 /-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
 occurrence takes precedence. -/