From 1d1711971045c6e962f114c166fbcd084f4743e5 Mon Sep 17 00:00:00 2001 From: Paul Reichert Date: Mon, 10 Mar 2025 10:51:41 +0100 Subject: [PATCH] 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 | 17 +++++---- src/Std/Data/DHashMap/Internal/WF.lean | 24 +++++++------ src/Std/Data/DHashMap/Raw.lean | 35 ++++++++++++++++--- 3 files changed, 55 insertions(+), 21 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 4a26a97115..a2912a2e32 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/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} : diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index a76c04ec83..4f98850d7d 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/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] diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index bda260b93d..8d92812863 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/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. -/