diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean index 8cc0c22536..67056dbda3 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean @@ -10,6 +10,11 @@ import Init.NotationExtra This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file. +Note that some functions in this file (in particular, `foldrM`, `foldr`, `toList`, `replace`, and +`erase`) are not tail-recursive. This is not a problem because they are only used internally by +`HashMap`, where `AssocList` is always small. Before making this API public, we would need to add +`@[csimp]` lemmas for tail-recursive implementations. + File contents: Operations on associative lists -/ @@ -46,6 +51,17 @@ namespace AssocList @[inline] def foldl (f : δ → (α : α) → β α → δ) (init : δ) (as : AssocList α β) : δ := Id.run (foldlM f init as) +/-- Internal implementation detail of the hash map -/ +@[specialize] def foldrM (f : (a : α) → β a → δ → m δ) : (init : δ) → AssocList α β → m δ + | d, nil => pure d + | d, cons a b es => do + let d ← foldrM f d es + f a b d + +/-- Internal implementation detail of the hash map -/ +@[inline] def foldr (f : (a : α) → β a → δ → δ) (init : δ) (as : AssocList α β) : δ := + Id.run (foldrM f init as) + /-- Internal implementation detail of the hash map -/ @[inline] def forM (f : (a : α) → β a → m PUnit) (as : AssocList α β) : m PUnit := as.foldlM (fun _ => f) ⟨⟩ diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index ebb0500223..e93eeea4dd 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -204,4 +204,9 @@ theorem foldl_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM, Id.run] +theorem foldr_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) : + l.foldr (fun k v acc => f k v :: acc) acc = + (l.toList.map (fun p => f p.1 p.2)) ++ acc := by + induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM, Id.run] + end Std.DHashMap.Internal.AssocList diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index eb9740b82e..a18eb53c2c 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -83,12 +83,36 @@ theorem fold_cons_key {l : Raw α β} {acc : List α} : l.fold (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets).reverse ++ acc := by 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, + ← 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 = + ((toListModel l.buckets).map (fun p => f p.1 p.2)) ++ acc := by + rw [foldRev_eq, ← Array.foldr_toList, toListModel] + generalize l.buckets.toList = l + induction l generalizing acc with + | nil => simp + | cons x xs ih => + rw [foldr_cons, ih, AssocList.foldr_apply] + 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 + 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 + rw [foldRev_cons_apply, keys_eq_map] + theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by - simp [Raw.toList, fold_cons] + simp [Raw.toList, foldRev_cons] theorem keys_perm_keys_toListModel {m : Raw α β} : Perm m.keys (List.keys (toListModel m.buckets)) := by - simp [Raw.keys, fold_cons_key, keys_eq_map] + simp [Raw.keys, foldRev_cons_key, keys_eq_map] theorem length_keys_eq_length_keys {m : Raw α β} : m.keys.length = (List.keys (toListModel m.buckets)).length := diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 153cc4c652..8074021b89 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -333,6 +333,19 @@ map in some order. @[inline] def fold (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := Id.run (b.foldM f init) +/-- +Monadically computes a value by folding the given function over the mappings in the hash +map in the reverse order used by `foldM`. +-/ +@[inline] 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] def foldRev (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := + Id.run (b.foldRevM f init) + /-- 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 := b.buckets.forM (AssocList.forM f) @@ -349,7 +362,7 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where /-- Transforms the hash map into a list of mappings in some order. -/ @[inline] def toList (m : Raw α β) : List ((a : α) × β a) := - m.fold (fun acc k v => ⟨k, v⟩ :: acc) [] + m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) [] /-- Transforms the hash map into an array of mappings in some order. -/ @[inline] def toArray (m : Raw α β) : Array ((a : α) × β a) := @@ -357,7 +370,7 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where @[inline, inherit_doc Raw.toList] def Const.toList {β : Type v} (m : Raw α (fun _ => β)) : List (α × β) := - m.fold (fun acc k v => ⟨k, v⟩ :: acc) [] + m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) [] @[inline, inherit_doc Raw.toArray] def Const.toArray {β : Type v} (m : Raw α (fun _ => β)) : Array (α × β) := @@ -369,7 +382,7 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where /-- Returns a list of all values present in the hash map in some order. -/ @[inline] def values {β : Type v} (m : Raw α (fun _ => β)) : List β := - m.fold (fun acc _ v => v :: acc) [] + m.foldRev (fun acc _ v => v :: acc) [] /-- Returns an array of all values present in the hash map in some order. -/ @[inline] def valuesArray {β : Type v} (m : Raw α (fun _ => β)) : Array β := @@ -455,7 +468,7 @@ end Unverified /-- Returns a list of all keys present in the hash map in some order. -/ @[inline] def keys (m : Raw α β) : List α := - m.fold (fun acc k _ => k :: acc) [] + m.foldRev (fun acc k _ => k :: acc) [] section WF diff --git a/tests/lean/run/hashmap.lean b/tests/lean/run/hashmap.lean index 5574090e58..b0eefff15c 100644 --- a/tests/lean/run/hashmap.lean +++ b/tests/lean/run/hashmap.lean @@ -15,7 +15,7 @@ def m : DHashMap.Raw Nat (fun _ => Nat) := #guard_msgs in #eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList -/-- info: [⟨3, none⟩, ⟨2, some 8⟩, ⟨1, none⟩] -/ +/-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/ #guard_msgs in #eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList @@ -50,7 +50,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do ans := (k, v) :: ans return ans -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/ +/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval m.toList @@ -58,7 +58,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray -/-- info: [(3, 6), (2, 4), (1, 2)] -/ +/-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DHashMap.Raw.Const.toList m @@ -66,7 +66,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval DHashMap.Raw.Const.toArray m -/-- info: [3, 2, 1] -/ +/-- info: [1, 2, 3] -/ #guard_msgs in #eval m.keys @@ -74,19 +74,19 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray -/-- info: [6, 4, 2] -/ +/-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/ +/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (m.insertMany [⟨16, 8⟩, ⟨16, 9⟩]).toList -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/ +/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (DHashMap.Raw.Const.insertMany m [(16, 8), (16, 9)]).toList -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/ +/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (DHashMap.Raw.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList @@ -105,7 +105,7 @@ def m : DHashMap Nat (fun _ => Nat) := #guard_msgs in #eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList -/-- info: [⟨3, none⟩, ⟨2, some 8⟩, ⟨1, none⟩] -/ +/-- info: [⟨1, none⟩, ⟨2, some 8⟩, ⟨3, none⟩] -/ #guard_msgs in #eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList @@ -140,7 +140,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do ans := (k, v) :: ans return ans -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/ +/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval m.toList @@ -148,7 +148,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray -/-- info: [(3, 6), (2, 4), (1, 2)] -/ +/-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval DHashMap.Const.toList m @@ -156,7 +156,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval DHashMap.Const.toArray m -/-- info: [3, 2, 1] -/ +/-- info: [1, 2, 3] -/ #guard_msgs in #eval m.keys @@ -164,19 +164,19 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray -/-- info: [6, 4, 2] -/ +/-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/ +/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (m.insertMany [⟨16, 8⟩, ⟨16, 9⟩]).toList -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩, ⟨16, 9⟩] -/ +/-- info: [⟨16, 9⟩, ⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (DHashMap.Const.insertMany m [(16, 8), (16, 9)]).toList -/-- info: [⟨3, 6⟩, ⟨2, 4⟩, ⟨1, 2⟩] -/ +/-- info: [⟨1, 2⟩, ⟨2, 4⟩, ⟨3, 6⟩] -/ #guard_msgs in #eval (DHashMap.Const.ofList [(1, 2), (2, 4), (3, 6)]).toList @@ -195,7 +195,7 @@ def m : HashMap.Raw Nat Nat := #guard_msgs in #eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList -/-- info: [(3, none), (2, some 8), (1, none)] -/ +/-- info: [(1, none), (2, some 8), (3, none)] -/ #guard_msgs in #eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList @@ -230,7 +230,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do ans := (k, v) :: ans return ans -/-- info: [(3, 6), (2, 4), (1, 2)] -/ +/-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval m.toList @@ -238,7 +238,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray -/-- info: [3, 2, 1] -/ +/-- info: [1, 2, 3] -/ #guard_msgs in #eval m.keys @@ -246,11 +246,11 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray -/-- info: [6, 4, 2] -/ +/-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values -/-- info: [(3, 6), (2, 4), (1, 2), (16, 9)] -/ +/-- info: [(16, 9), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval (m.insertMany [(16, 8), (16, 9)]).toList @@ -269,7 +269,7 @@ def m : HashMap Nat Nat := #guard_msgs in #eval (m.filterMap fun k v => if k % 2 == 0 then some (2 * v) else none).toList -/-- info: [(3, none), (2, some 8), (1, none)] -/ +/-- info: [(1, none), (2, some 8), (3, none)] -/ #guard_msgs in #eval (m.map fun k v => if k % 2 == 0 then some (2 * v) else none).toList @@ -304,7 +304,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do ans := (k, v) :: ans return ans -/-- info: [(3, 6), (2, 4), (1, 2)] -/ +/-- info: [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval m.toList @@ -312,7 +312,7 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray -/-- info: [3, 2, 1] -/ +/-- info: [1, 2, 3] -/ #guard_msgs in #eval m.keys @@ -320,11 +320,11 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.keysArray -/-- info: [6, 4, 2] -/ +/-- info: [2, 4, 6] -/ #guard_msgs in #eval m.values -/-- info: [(3, 6), (2, 4), (1, 2), (16, 9)] -/ +/-- info: [(16, 9), (1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval (m.insertMany [(16, 8), (16, 9)]).toList @@ -332,35 +332,35 @@ def addValueToState (_ : Nat) (v : Nat) : StateM Nat PUnit := do #guard_msgs in #eval HashMap.ofList [(1, 2), (1, 4)] -/-- info: Std.HashMap.ofList [(37, 37), (4, 5), (3, 6), (2, 4), (1, 2)] -/ +/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6), (4, 5), (37, 37)] -/ #guard_msgs in #eval m ∪ {(4, 5), (37, 37)} -/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 3)] -/ +/-- info: Std.HashMap.ofList [(1, 3), (2, 4), (3, 6)] -/ #guard_msgs in #eval m.modify 1 (fun v => v + 1) -/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 2)] -/ +/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval m.modify 4 (fun v => v + 1) -/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 2)] -/ +/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval m.alter 4 (fun v? => v?.map (· + 2)) -/-- info: Std.HashMap.ofList [(4, 7), (3, 6), (2, 4), (1, 2)] -/ +/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6), (4, 7)] -/ #guard_msgs in #eval m.alter 4 (fun _ => some 7) -/-- info: Std.HashMap.ofList [(3, 6), (2, 4), (1, 2)] -/ +/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 6)] -/ #guard_msgs in #eval m.alter 4 (fun _ => none) -/-- info: Std.HashMap.ofList [(2, 4), (1, 2)] -/ +/-- info: Std.HashMap.ofList [(1, 2), (2, 4)] -/ #guard_msgs in #eval m.alter 3 (fun _ => none) -/-- info: Std.HashMap.ofList [(3, 37), (2, 4), (1, 2)] -/ +/-- info: Std.HashMap.ofList [(1, 2), (2, 4), (3, 37)] -/ #guard_msgs in #eval m.alter 3 (fun _ => some 37) @@ -418,7 +418,7 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.all fun x => x > 4 -/-- info: [1000000000, 2, 1] -/ +/-- info: [1, 2, 1000000000] -/ #guard_msgs in #eval m.toList @@ -426,15 +426,15 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray -/-- info: Std.HashSet.Raw.ofList [1000000000, 2, 1, 16] -/ +/-- info: Std.HashSet.Raw.ofList [16, 1, 2, 1000000000] -/ #guard_msgs in #eval m ∪ {16, 16} -/-- info: [1000000000, 2, 1, 16] -/ +/-- info: [16, 1, 2, 1000000000] -/ #guard_msgs in #eval (m.insertMany [16, 16]).toList -/-- info: Std.HashSet.Raw.ofList [100, 1] -/ +/-- info: Std.HashSet.Raw.ofList [1, 100] -/ #guard_msgs in #eval HashSet.Raw.ofList [1, 100] @@ -492,7 +492,7 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.all fun x => x > 4 -/-- info: [1000000000, 2, 1] -/ +/-- info: [1, 2, 1000000000] -/ #guard_msgs in #eval m.toList @@ -500,15 +500,15 @@ def addKeyToState (k : Nat) : StateM Nat PUnit := do #guard_msgs in #eval m.toArray -/-- info: Std.HashSet.ofList [1000000000, 2, 1, 16] -/ +/-- info: Std.HashSet.ofList [16, 1, 2, 1000000000] -/ #guard_msgs in #eval m ∪ {16, 16} -/-- info: [1000000000, 2, 1, 16] -/ +/-- info: [16, 1, 2, 1000000000] -/ #guard_msgs in #eval (m.insertMany [16, 16]).toList -/-- info: Std.HashSet.ofList [100, 1] -/ +/-- info: Std.HashSet.ofList [1, 100] -/ #guard_msgs in #eval HashSet.ofList [1, 100]