refactor: rename MultiMap to IndexMultiMap

src/Std/Internal/Http/Data/Headers.lean

@@ -36,7 +36,7 @@ structure Headers where
   /--
   The underlying multimap that stores headers.
   -/
-  map : MultiMap Header.Name Header.Value
+  map : IndexMultiMap Header.Name Header.Value
 deriving Inhabited, Repr
 
 instance : Membership Header.Name Headers where
@@ -147,7 +147,7 @@ def empty : Headers :=
 Creates headers from a list of key-value pairs.
 -/
 def ofList (pairs : List (Header.Name × Header.Value)) : Headers :=
-  { map := MultiMap.ofList pairs }
+  { map := IndexMultiMap.ofList pairs }
 
 /--
 Checks if a header with the given name exists.
@@ -208,7 +208,7 @@ Maps a function over all header values, producing new headers.
 -/
 def mapValues (headers : Headers) (f : Header.Name → Header.Value → Header.Value) : Headers :=
   let pairs := headers.map.toArray.map (fun (k, v) => (k, f k v))
-  { map := pairs.foldl (fun acc (k, v) => acc.insert k v) MultiMap.empty }
+  { map := pairs.foldl (fun acc (k, v) => acc.insert k v) IndexMultiMap.empty }
 
 /--
 Filters and maps over header key-value pairs. Returns only the pairs for which the function returns `some`.
@@ -218,7 +218,7 @@ def filterMap (headers : Headers) (f : Header.Name → Header.Value → Option H
     match f k v with
     | some v' => some (k, v')
     | none => none)
-  { map := pairs.foldl (fun acc (k, v) => acc.insert k v) MultiMap.empty }
+  { map := pairs.foldl (fun acc (k, v) => acc.insert k v) IndexMultiMap.empty }
 
 /--
 Filters header key-value pairs, keeping only those that satisfy the predicate.

src/Std/Internal/Http/Internal.lean

@@ -9,7 +9,7 @@ prelude
 public import Std.Internal.Http.Internal.Char
 public import Std.Internal.Http.Internal.ChunkedBuffer
 public import Std.Internal.Http.Internal.LowerCase
-public import Std.Internal.Http.Internal.MultiMap
+public import Std.Internal.Http.Internal.IndexMultiMap
 public import Std.Internal.Http.Internal.Encode
 public import Std.Internal.Http.Internal.String
 public import Std.Internal.Http.Internal.Char

src/Std/Internal/Http/Internal/IndexMultiMap.lean

@@ -13,9 +13,9 @@ public import Std.Data.HashMap
 public section
 
 /-!
-# MultiMap
+# IndexMultiMap
 
-This module defines a generic `MultiMap` type that maps keys to multiple values.
+This module defines a generic `IndexMultiMap` type that maps keys to multiple values.
 The implementation stores entries in a flat array for iteration and an index HashMap
 for fast key lookups. Each key always has at least one associated value.
 -/
@@ -29,7 +29,7 @@ set_option linter.all true
 /--
 A structure for managing ordered key-value pairs where each key can have multiple values.
 -/
-structure MultiMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+structure IndexMultiMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
 
   /--
   Flat array of all key-value entries in insertion order.
@@ -50,24 +50,24 @@ structure MultiMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
 
 deriving Repr
 
-instance [BEq α] [Hashable α] [Inhabited α] [Inhabited β] : Inhabited (MultiMap α β) where
+instance [BEq α] [Hashable α] [Inhabited α] [Inhabited β] : Inhabited (IndexMultiMap α β) where
   default := ⟨#[], .emptyWithCapacity, by intro h p; simp at p⟩
 
-namespace MultiMap
+namespace IndexMultiMap
 
 variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
 
-instance : Membership α (MultiMap α β) where
+instance : Membership α (IndexMultiMap α β) where
   mem map key := key ∈ map.indexes
 
-instance (key : α) (map : MultiMap α β) : Decidable (key ∈ map) :=
+instance (key : α) (map : IndexMultiMap α β) : Decidable (key ∈ map) :=
   inferInstanceAs (Decidable (key ∈ map.indexes))
 
 /--
 Retrieves all values for the given key.
 -/
 @[inline]
-def getAll (map : MultiMap α β) (key : α) (h : key ∈ map) : Array β :=
+def getAll (map : IndexMultiMap α β) (key : α) (h : key ∈ map) : Array β :=
   let entries := map.indexes.get key h |>.mapFinIdx fun idx _ h₁ =>
     let proof := map.validity key h |>.right _ (Array.getElem_mem h₁)
     map.entries[(map.indexes.get key h)[idx]]'proof |>.snd
@@ -78,7 +78,7 @@ def getAll (map : MultiMap α β) (key : α) (h : key ∈ map) : Array β :=
 Retrieves the first value for the given key.
 -/
 @[inline]
-def get (map : MultiMap α β) (key : α) (h : key ∈ map) : β :=
+def get (map : IndexMultiMap α β) (key : α) (h : key ∈ map) : β :=
   let ⟨nonEmpty, isIn⟩ := map.validity key h
   let entry := ((map.indexes.get key h)[0]'nonEmpty)
 
@@ -92,7 +92,7 @@ def get (map : MultiMap α β) (key : α) (h : key ∈ map) : β :=
 Retrieves all values for the given key, or `none` if the key is absent.
 -/
 @[inline]
-def getAll? (map : MultiMap α β) (key : α) : Option (Array β) :=
+def getAll? (map : IndexMultiMap α β) (key : α) : Option (Array β) :=
   if h : key ∈ map then
     some (map.getAll key h)
   else
@@ -102,7 +102,7 @@ def getAll? (map : MultiMap α β) (key : α) : Option (Array β) :=
 Retrieves the first value for the given key, or `none` if the key is absent.
 -/
 @[inline]
-def get? (map : MultiMap α β) (key : α) : Option β :=
+def get? (map : IndexMultiMap α β) (key : α) : Option β :=
   if h : key ∈ map then
     some (map.get key h)
   else
@@ -112,7 +112,7 @@ def get? (map : MultiMap α β) (key : α) : Option β :=
 Checks if the key-value pair is present in the map.
 -/
 @[inline]
-def hasEntry (map : MultiMap α β) [BEq β] (key : α) (value : β) : Bool :=
+def hasEntry (map : IndexMultiMap α β) [BEq β] (key : α) (value : β) : Bool :=
   map.getAll? key
   |>.bind (fun arr => arr.find? (· == value))
   |>.isSome
@@ -122,7 +122,7 @@ Retrieves the last value for the given key.
 Returns `none` if the key is absent.
 -/
 @[inline]
-def getLast? (map : MultiMap α β) (key : α) : Option β :=
+def getLast? (map : IndexMultiMap α β) (key : α) : Option β :=
   match map.getAll? key with
   | none => none
   | some idxs => idxs.back?
@@ -131,14 +131,14 @@ def getLast? (map : MultiMap α β) (key : α) : Option β :=
 Like `get?`, but returns a default value if absent.
 -/
 @[inline]
-def getD (map : MultiMap α β) (key : α) (d : β) : β :=
+def getD (map : IndexMultiMap α β) (key : α) (d : β) : β :=
   map.get? key |>.getD d
 
 /--
 Like `get?`, but panics if absent.
 -/
 @[inline]
-def get! [Inhabited β] (map : MultiMap α β) (key : α) : β :=
+def get! [Inhabited β] (map : IndexMultiMap α β) (key : α) : β :=
   map.get? key |>.get!
 
 /--
@@ -146,7 +146,7 @@ Inserts a new key-value pair into the map.
 If the key already exists, appends the value to existing values.
 -/
 @[inline]
-def insert [EquivBEq α] [LawfulHashable α] (map : MultiMap α β) (key : α) (value : β) : MultiMap α β :=
+def insert [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (value : β) : IndexMultiMap α β :=
   let i := map.entries.size
   let entries := map.entries.push (key, value)
 
@@ -165,26 +165,26 @@ where finally
 Inserts multiple values for a given key, appending to any existing values.
 -/
 @[inline]
-def insertMany [EquivBEq α] [LawfulHashable α] (map : MultiMap α β) (key : α) (values : Array β) : MultiMap α β :=
+def insertMany [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (values : Array β) : IndexMultiMap α β :=
   values.foldl (insert · key) map
 
 /--
 Creates an empty multimap.
 -/
-def empty : MultiMap α β :=
+def empty : IndexMultiMap α β :=
   ⟨#[], .emptyWithCapacity, by intro h p; simp at p⟩
 
 /--
 Creates a multimap from a list of key-value pairs.
 -/
-def ofList [EquivBEq α] [LawfulHashable α] (pairs : List (α × β)) : MultiMap α β :=
+def ofList [EquivBEq α] [LawfulHashable α] (pairs : List (α × β)) : IndexMultiMap α β :=
   pairs.foldl (fun acc (k, v) => acc.insert k v) empty
 
 /--
 Checks if a key exists in the map.
 -/
 @[inline]
-def contains (map : MultiMap α β) (key : α) : Bool :=
+def contains (map : IndexMultiMap α β) (key : α) : Bool :=
   map.indexes.contains key
 
 /--
@@ -192,7 +192,7 @@ Updates all values associated with `key` by applying `f` to each one.
 If the key is absent, returns the map unchanged.
 -/
 @[inline]
-def update [EquivBEq α] [LawfulHashable α] (map : MultiMap α β) (key : α) (f : β → β) : MultiMap α β :=
+def update [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (f : β → β) : IndexMultiMap α β :=
   if key ∉ map then
     map
   else
@@ -203,7 +203,7 @@ Replaces the last value associated with `key` with `value`.
 If the key is absent, returns the map unchanged.
 -/
 @[inline]
-def replaceLast (map : MultiMap α β) (key : α) (value : β) : MultiMap α β :=
+def replaceLast (map : IndexMultiMap α β) (key : α) (value : β) : IndexMultiMap α β :=
   if h : key ∈ map then
     let idxs := map.indexes.get key h
     let ⟨nonEmpty, isIn⟩ := map.validity key h
@@ -224,7 +224,7 @@ Removes a key and all its values from the map. This function rebuilds the entire
 key matches, then re-inserting the survivors.
 -/
 @[inline]
-def erase [EquivBEq α] [LawfulHashable α] (map : MultiMap α β) (key : α) : MultiMap α β :=
+def erase [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) : IndexMultiMap α β :=
   if key ∉ map then
     map
   else
@@ -235,47 +235,47 @@ def erase [EquivBEq α] [LawfulHashable α] (map : MultiMap α β) (key : α) :
 Gets the number of entries in the map.
 -/
 @[inline]
-def size (map : MultiMap α β) : Nat :=
+def size (map : IndexMultiMap α β) : Nat :=
   map.entries.size
 
 /--
 Checks if the map is empty.
 -/
 @[inline]
-def isEmpty (map : MultiMap α β) : Bool :=
+def isEmpty (map : IndexMultiMap α β) : Bool :=
   map.entries.isEmpty
 
 /--
 Converts the multimap to an array of key-value pairs (flattened).
 -/
-def toArray (map : MultiMap α β) : Array (α × β) :=
+def toArray (map : IndexMultiMap α β) : Array (α × β) :=
   map.entries
 
 /--
 Converts the multimap to a list of key-value pairs (flattened).
 -/
-def toList (map : MultiMap α β) : List (α × β) :=
+def toList (map : IndexMultiMap α β) : List (α × β) :=
   map.entries.toList
 
 /--
 Merges two multimaps, combining values for shared keys.
 -/
-def merge [EquivBEq α] [LawfulHashable α] (m1 m2 : MultiMap α β) : MultiMap α β :=
+def merge [EquivBEq α] [LawfulHashable α] (m1 m2 : IndexMultiMap α β) : IndexMultiMap α β :=
   m2.entries.foldl (fun acc (k, v) => acc.insert k v) m1
 
-instance : EmptyCollection (MultiMap α β) :=
-  ⟨MultiMap.empty⟩
+instance : EmptyCollection (IndexMultiMap α β) :=
+  ⟨IndexMultiMap.empty⟩
 
-instance [EquivBEq α] [LawfulHashable α] : Singleton (α × β) (MultiMap α β) :=
-  ⟨fun ⟨a, b⟩ => (∅ : MultiMap α β).insert a b⟩
+instance [EquivBEq α] [LawfulHashable α] : Singleton (α × β) (IndexMultiMap α β) :=
+  ⟨fun ⟨a, b⟩ => (∅ : IndexMultiMap α β).insert a b⟩
 
-instance [EquivBEq α] [LawfulHashable α] : Insert (α × β) (MultiMap α β) :=
+instance [EquivBEq α] [LawfulHashable α] : Insert (α × β) (IndexMultiMap α β) :=
   ⟨fun ⟨a, b⟩ m => m.insert a b⟩
 
-instance [EquivBEq α] [LawfulHashable α] : Union (MultiMap α β) :=
+instance [EquivBEq α] [LawfulHashable α] : Union (IndexMultiMap α β) :=
   ⟨merge⟩
 
-instance [Monad m] : ForIn m (MultiMap α β) (α × β) where
+instance [Monad m] : ForIn m (IndexMultiMap α β) (α × β) where
   forIn map b f := forIn map.entries b f
 
-end Std.Internal.MultiMap
+end Std.Internal.IndexMultiMap