From 19a1f578b1025f15dbcb7b6f67b01e67d381eac0 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 16 Mar 2026 19:13:08 -0300 Subject: [PATCH] refactor: rename MultiMap to IndexMultiMap --- src/Std/Internal/Http/Data/Headers.lean | 8 +-- src/Std/Internal/Http/Internal.lean | 2 +- .../{MultiMap.lean => IndexMultiMap.lean} | 72 +++++++++---------- 3 files changed, 41 insertions(+), 41 deletions(-) rename src/Std/Internal/Http/Internal/{MultiMap.lean => IndexMultiMap.lean} (70%) diff --git a/src/Std/Internal/Http/Data/Headers.lean b/src/Std/Internal/Http/Data/Headers.lean index a23b245ccc..0468615cf7 100644 --- a/src/Std/Internal/Http/Data/Headers.lean +++ b/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. diff --git a/src/Std/Internal/Http/Internal.lean b/src/Std/Internal/Http/Internal.lean index 0c1398b9cf..c56ec7ca2f 100644 --- a/src/Std/Internal/Http/Internal.lean +++ b/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 diff --git a/src/Std/Internal/Http/Internal/MultiMap.lean b/src/Std/Internal/Http/Internal/IndexMultiMap.lean similarity index 70% rename from src/Std/Internal/Http/Internal/MultiMap.lean rename to src/Std/Internal/Http/Internal/IndexMultiMap.lean index 241ee87147..efb67d6a07 100644 --- a/src/Std/Internal/Http/Internal/MultiMap.lean +++ b/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