IndexMultiMap

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.

structure Std.Internal.IndexMultiMap (α : Type u) (β : Type v) [BEq α] [Hashable α] : Type (max u v)

A structure for managing ordered key-value pairs where each key can have multiple values.

• entries : Array (α × β)

  Flat array of all key-value entries in insertion order.

• indexes : HashMap α (Array Nat)

  Maps each key to its indices in entries. Each array is non-empty.

• validity (k : α) (p : k ∈ self.indexes) : let idx := self.indexes.get k p; idx.size > 0 ∧ ∀ (i : Nat), i ∈ idx → i < self.entries.size

  Invariant: every key in indexes maps to a non-empty array of valid indices into entries.

@[implicit_reducible]

instance Std.Internal.instReprIndexMultiMap {α✝ : Type u_1} {β✝ : Type u_2} {inst✝ : BEq α✝} {inst✝¹ : Hashable α✝} [Repr α✝] [Repr β✝] : Repr (IndexMultiMap α✝ β✝)

Equations

• Std.Internal.instReprIndexMultiMap = { reprPrec := Std.Internal.instReprIndexMultiMap.repr }

def Std.Internal.instReprIndexMultiMap.repr {α✝ : Type u_1} {β✝ : Type u_2} {inst✝ : BEq α✝} {inst✝¹ : Hashable α✝} [Repr α✝] [Repr β✝] : IndexMultiMap α✝ β✝ → Nat → Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Internal.instInhabitedIndexMultiMap {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] [Inhabited α] [Inhabited β] : Inhabited (IndexMultiMap α β)

Equations

• Std.Internal.instInhabitedIndexMultiMap = { default := { entries := #[], indexes := Std.HashMap.emptyWithCapacity, validity := ⋯ } }

@[implicit_reducible]

instance Std.Internal.IndexMultiMap.instMembership {α : Type u} {β : Type v} [BEq α] [Hashable α] : Membership α (IndexMultiMap α β)

Equations

• Std.Internal.IndexMultiMap.instMembership = { mem := fun (map : Std.Internal.IndexMultiMap α β) (key : α) => key ∈ map.indexes }

@[implicit_reducible]

instance Std.Internal.IndexMultiMap.instDecidableMem {α : Type u} {β : Type v} [BEq α] [Hashable α] (key : α) (map : IndexMultiMap α β) : Decidable (key ∈ map)

Equations

• Std.Internal.IndexMultiMap.instDecidableMem key map = (map.indexes.inner.contains key).decEq true

@[inline]

def Std.Internal.IndexMultiMap.getAll {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) (h : key ∈ map) : Array β

Retrieves all values for the given key.

Equations

• map.getAll key h = (map.indexes.get key h).mapFinIdx fun (idx x : Nat) (h₁ : idx < (map.indexes.get key h).size) => have proof := ⋯; map.entries[(map.indexes.get key h)[idx]].snd

@[inline]

def Std.Internal.IndexMultiMap.get {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) (h : key ∈ map) : β

Retrieves the first value for the given key.

Equations

• map.get key h = match ⋯ with | ⋯ => let entry := (map.indexes.get key h)[0]; have proof := ⋯; map.entries[entry].snd

@[inline]

def Std.Internal.IndexMultiMap.getAll? {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) : Option (Array β)

Retrieves all values for the given key, or none if the key is absent.

Equations

• map.getAll? key = if h : key ∈ map then some (map.getAll key h) else none

@[inline]

def Std.Internal.IndexMultiMap.get? {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) : Option β

Retrieves the first value for the given key, or none if the key is absent.

Equations

• map.get? key = if h : key ∈ map then some (map.get key h) else none

@[inline]

def Std.Internal.IndexMultiMap.hasEntry {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) [BEq β] (key : α) (value : β) : Bool

Checks if the key-value pair is present in the map.

Equations

• map.hasEntry key value = ((map.getAll? key).bind fun (arr : Array β) => Array.find? (fun (x : β) => x == value) arr).isSome

@[inline]

def Std.Internal.IndexMultiMap.getLast? {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) : Option β

Retrieves the last value for the given key. Returns none if the key is absent.

Equations

• map.getLast? key = match map.getAll? key with | none => none | some idxs => idxs.back?

@[inline]

def Std.Internal.IndexMultiMap.getD {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) (d : β) : β

Like get?, but returns a default value if absent.

Equations

• map.getD key d = (map.get? key).getD d

@[inline]

def Std.Internal.IndexMultiMap.get! {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (map : IndexMultiMap α β) (key : α) : β

Like get?, but panics if absent.

Equations

• map.get! key = (map.get? key).get!

@[inline]

def Std.Internal.IndexMultiMap.insert {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (value : β) : IndexMultiMap α β

Inserts a new key-value pair into the map. If the key already exists, appends the value to existing values.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Internal.IndexMultiMap.insertMany {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (values : Array β) : IndexMultiMap α β

Inserts multiple values for a given key, appending to any existing values.

Equations

• map.insertMany key values = Array.foldl (fun (x : Std.Internal.IndexMultiMap α β) => x.insert key) map values

def Std.Internal.IndexMultiMap.empty {α : Type u} {β : Type v} [BEq α] [Hashable α] : IndexMultiMap α β

Creates an empty multimap.

Equations

• Std.Internal.IndexMultiMap.empty = { entries := #[], indexes := Std.HashMap.emptyWithCapacity, validity := ⋯ }

def Std.Internal.IndexMultiMap.ofList {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (pairs : List (α × β)) : IndexMultiMap α β

Creates a multimap from a list of key-value pairs.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Internal.IndexMultiMap.contains {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) : Bool

Checks if a key exists in the map.

Equations

• map.contains key = map.indexes.contains key

@[inline]

def Std.Internal.IndexMultiMap.update {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) (f : β → β) : IndexMultiMap α β

Updates all values associated with key by applying f to each one. If the key is absent, returns the map unchanged.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Internal.IndexMultiMap.replaceLast {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) (key : α) (value : β) : IndexMultiMap α β

Replaces the last value associated with key with value. If the key is absent, returns the map unchanged.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Internal.IndexMultiMap.erase {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (map : IndexMultiMap α β) (key : α) : IndexMultiMap α β

Removes a key and all its values from the map. This function rebuilds the entire entries array and indexes map from scratch by filtering out all pairs whose key matches, then re-inserting the survivors.

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def Std.Internal.IndexMultiMap.size {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) : Nat

Gets the number of entries in the map.

Equations

• map.size = map.entries.size

@[inline]

def Std.Internal.IndexMultiMap.isEmpty {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) : Bool

Checks if the map is empty.

Equations

• map.isEmpty = map.entries.isEmpty

def Std.Internal.IndexMultiMap.toArray {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) : Array (α × β)

Converts the multimap to an array of key-value pairs (flattened).

Equations

• map.toArray = map.entries

def Std.Internal.IndexMultiMap.toList {α : Type u} {β : Type v} [BEq α] [Hashable α] (map : IndexMultiMap α β) : List (α × β)

Converts the multimap to a list of key-value pairs (flattened).

Equations

• map.toList = map.entries.toList

def Std.Internal.IndexMultiMap.merge {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m1 m2 : IndexMultiMap α β) : IndexMultiMap α β

Merges two multimaps, combining values for shared keys.

Equations

• m1.merge m2 = Array.foldl (fun (acc : Std.Internal.IndexMultiMap α β) (x : α × β) => match x with | (k, v) => acc.insert k v) m1 m2.entries

@[implicit_reducible]

instance Std.Internal.IndexMultiMap.instEmptyCollection {α : Type u} {β : Type v} [BEq α] [Hashable α] : EmptyCollection (IndexMultiMap α β)

Equations

• Std.Internal.IndexMultiMap.instEmptyCollection = { emptyCollection := Std.Internal.IndexMultiMap.empty }

@[implicit_reducible]

instance Std.Internal.IndexMultiMap.instSingletonProdOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : Singleton (α × β) (IndexMultiMap α β)

Equations

• Std.Internal.IndexMultiMap.instSingletonProdOfEquivBEqOfLawfulHashable = { singleton := fun (x : α × β) => match x with | (a, b) => ∅.insert a b }

@[implicit_reducible]

instance Std.Internal.IndexMultiMap.instInsertProdOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : Insert (α × β) (IndexMultiMap α β)

Equations

• Std.Internal.IndexMultiMap.instInsertProdOfEquivBEqOfLawfulHashable = { insert := fun (x : α × β) (m : Std.Internal.IndexMultiMap α β) => match x with | (a, b) => m.insert a b }

@[implicit_reducible]

instance Std.Internal.IndexMultiMap.instUnionOfEquivBEqOfLawfulHashable {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : Union (IndexMultiMap α β)

Equations

• Std.Internal.IndexMultiMap.instUnionOfEquivBEqOfLawfulHashable = { union := Std.Internal.IndexMultiMap.merge }

@[implicit_reducible]

instance Std.Internal.IndexMultiMap.instForInProdOfMonad {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Type u_1 → Type u_2} [Monad m] : ForIn m (IndexMultiMap α β) (α × β)

Equations

• One or more equations did not get rendered due to their size.