Association lists

AssocList α β is a List (α × β) with the pair structure flattened into the list constructor. This file defines the type and its operations; the lemmas relating those operations to the corresponding List operations along AssocList.toList are in Batteries.Data.AssocList.Lemmas.

inductive Batteries.AssocList (α : Type u) (β : Type v) : Type (max u v)

AssocList α β is "the same as" List (α × β), but flattening the structure leads to one fewer pointer indirection (in the current code generator). It is mainly intended as a component of HashMap, but it can also be used as a plain key-value map.

• nil {α : Type u} {β : Type v} : AssocList α β

  An empty list

• cons {α : Type u} {β : Type v} (key : α) (value : β) (tail : AssocList α β) : AssocList α β

  Add a key, value pair to the list

@[instance_reducible]

instance Batteries.instInhabitedAssocList {a✝ : Type u_1} {a✝¹ : Type u_2} : Inhabited (AssocList a✝ a✝¹)

Equations

• Batteries.instInhabitedAssocList = { default := Batteries.instInhabitedAssocList.default }

def Batteries.AssocList.toList {α : Type u_1} {β : Type u_2} : AssocList α β → List (α × β)

O(n). Convert an AssocList α β into the equivalent List (α × β). This is used to give specifications for all the AssocList functions in terms of corresponding list functions.

Equations

• Batteries.AssocList.nil.toList = []
• (Batteries.AssocList.cons a b es).toList = (a, b) :: es.toList

@[instance_reducible]

instance Batteries.AssocList.instEmptyCollection {α : Type u_1} {β : Type u_2} : EmptyCollection (AssocList α β)

Equations

• Batteries.AssocList.instEmptyCollection = { emptyCollection := Batteries.AssocList.nil }

def Batteries.AssocList.isEmpty {α : Type u_1} {β : Type u_2} : AssocList α β → Bool

O(1). Is the list empty?

Equations

• Batteries.AssocList.nil.isEmpty = true
• x✝.isEmpty = false

def Batteries.AssocList.length {α : Type u_1} {β : Type u_2} (L : AssocList α β) : Nat

The number of entries in an AssocList.

Equations

• Batteries.AssocList.nil.length = 0
• (Batteries.AssocList.cons a b es).length = es.length + 1

@[specialize #[]]

def Batteries.AssocList.foldlM {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δ → α → β → m δ) (init : δ) : AssocList α β → m δ

O(n). Fold a monadic function over the list, from head to tail.

Equations

• Batteries.AssocList.foldlM f x✝ Batteries.AssocList.nil = pure x✝
• Batteries.AssocList.foldlM f x✝ (Batteries.AssocList.cons a b es) = do let __do_lift ← f x✝ a b Batteries.AssocList.foldlM f __do_lift es

@[inline]

def Batteries.AssocList.foldl {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (as : AssocList α β) : δ

O(n). Fold a function over the list, from head to tail.

Equations

• Batteries.AssocList.foldl f init as = (Batteries.AssocList.foldlM (fun (d : δ) (a : α) (b : β) => pure (f d a b)) init as).run

@[simp]

theorem Batteries.AssocList.foldlM_eq {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [Monad m] (f : δ → α → β → m δ) (init : δ) (l : AssocList α β) : foldlM f init l = List.foldlM (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init l.toList

@[simp]

theorem Batteries.AssocList.foldl_eq {δ : Type u_1} {α : Type u_2} {β : Type u_3} (f : δ → α → β → δ) (init : δ) (l : AssocList α β) : foldl f init l = List.foldl (fun (d : δ) (x : α × β) => match x with | (a, b) => f d a b) init l.toList

def Batteries.AssocList.toListTR {α : Type u_1} {β : Type u_2} (as : AssocList α β) : List (α × β)

Optimized version of toList.

Equations

• as.toListTR = (Batteries.AssocList.foldl (fun (r : Array (α × β)) (a : α) (b : β) => r.push (a, b)) #[] as).toList

@[csimp]

theorem Batteries.AssocList.toList_eq_toListTR : @toList = @toListTR

@[specialize #[]]

def Batteries.AssocList.forM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] (f : α → β → m PUnit) : AssocList α β → m PUnit

O(n). Run monadic function f on all elements in the list, from head to tail.

Equations

• Batteries.AssocList.forM f Batteries.AssocList.nil = pure PUnit.unit
• Batteries.AssocList.forM f (Batteries.AssocList.cons a b es) = do f a b Batteries.AssocList.forM f es

def Batteries.AssocList.mapKey {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ) : AssocList α β → AssocList δ β

O(n). Map a function f over the keys of the list.

Equations

• Batteries.AssocList.mapKey f Batteries.AssocList.nil = Batteries.AssocList.nil
• Batteries.AssocList.mapKey f (Batteries.AssocList.cons a b es) = Batteries.AssocList.cons (f a) b (Batteries.AssocList.mapKey f es)

def Batteries.AssocList.mapVal {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) : AssocList α β → AssocList α δ

O(n). Map a function f over the values of the list.

Equations

• Batteries.AssocList.mapVal f Batteries.AssocList.nil = Batteries.AssocList.nil
• Batteries.AssocList.mapVal f (Batteries.AssocList.cons a b es) = Batteries.AssocList.cons a (f a b) (Batteries.AssocList.mapVal f es)

@[specialize #[]]

def Batteries.AssocList.findEntryP? {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : AssocList α β → Option (α × β)

O(n). Returns the first entry in the list whose entry satisfies p.

Equations

• Batteries.AssocList.findEntryP? p Batteries.AssocList.nil = none
• Batteries.AssocList.findEntryP? p (Batteries.AssocList.cons a b es) = bif p a b then some (a, b) else Batteries.AssocList.findEntryP? p es

@[inline]

def Batteries.AssocList.findEntry? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : Option (α × β)

O(n). Returns the first entry in the list whose key is equal to a.

Equations

• Batteries.AssocList.findEntry? a l = Batteries.AssocList.findEntryP? (fun (k : α) (x : β) => k == a) l

def Batteries.AssocList.find? {α : Type u_1} {β : Type u_2} [BEq α] (a : α) : AssocList α β → Option β

O(n). Returns the first value in the list whose key is equal to a.

Equations

• Batteries.AssocList.find? a Batteries.AssocList.nil = none
• Batteries.AssocList.find? a (Batteries.AssocList.cons a_1 b es) = match a_1 == a with | true => some b | false => Batteries.AssocList.find? a es

@[specialize #[]]

def Batteries.AssocList.any {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : AssocList α β → Bool

O(n). Returns true if any entry in the list satisfies p.

Equations

• Batteries.AssocList.any p Batteries.AssocList.nil = false
• Batteries.AssocList.any p (Batteries.AssocList.cons a b es) = (p a b || Batteries.AssocList.any p es)

@[specialize #[]]

def Batteries.AssocList.all {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : AssocList α β → Bool

O(n). Returns true if every entry in the list satisfies p.

Equations

• Batteries.AssocList.all p Batteries.AssocList.nil = true
• Batteries.AssocList.all p (Batteries.AssocList.cons a b es) = (p a b && Batteries.AssocList.all p es)

def Batteries.AssocList.All {α : Type u_1} {β : Type u_2} (p : α → β → Prop) (l : AssocList α β) : Prop

Returns true if every entry in the list satisfies p.

Equations

• Batteries.AssocList.All p l = ∀ (a : α × β), a ∈ l.toList → p a.fst a.snd

@[inline]

def Batteries.AssocList.contains {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : Bool

O(n). Returns true if there is an element in the list whose key is equal to a.

Equations

• Batteries.AssocList.contains a l = Batteries.AssocList.any (fun (k : α) (x : β) => k == a) l

def Batteries.AssocList.replace {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β

O(n). Replace the first entry in the list with key equal to a to have key a and value b.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.AssocList.replace a b Batteries.AssocList.nil = Batteries.AssocList.nil

@[specialize #[]]

def Batteries.AssocList.eraseP {α : Type u_1} {β : Type u_2} (p : α → β → Bool) : AssocList α β → AssocList α β

O(n). Remove the first entry in the list with key equal to a.

Equations

• Batteries.AssocList.eraseP p Batteries.AssocList.nil = Batteries.AssocList.nil
• Batteries.AssocList.eraseP p (Batteries.AssocList.cons a b es) = bif p a b then es else Batteries.AssocList.cons a b (Batteries.AssocList.eraseP p es)

@[inline]

def Batteries.AssocList.erase {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (l : AssocList α β) : AssocList α β

O(n). Remove the first entry in the list with key equal to a.

Equations

• Batteries.AssocList.erase a l = Batteries.AssocList.eraseP (fun (k : α) (x : β) => k == a) l

def Batteries.AssocList.modify {α : Type u_1} {β : Type u_2} [BEq α] (a : α) (f : α → β → β) : AssocList α β → AssocList α β

O(n). Replace the first entry a', b in the list with key equal to a to have key a and value f a' b.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.AssocList.modify a f Batteries.AssocList.nil = Batteries.AssocList.nil

@[specialize #[]]

def Batteries.AssocList.forIn {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [Monad m] (as : AssocList α β) (init : δ) (f : α × β → δ → m (ForInStep δ)) : m δ

The implementation of ForIn, which enables for (k, v) in aList do ... notation.

Equations

• Batteries.AssocList.nil.forIn init f = pure init
• (Batteries.AssocList.cons a b es).forIn init f = do let __do_lift ← f (a, b) init match __do_lift with | ForInStep.done d => pure d | ForInStep.yield d => es.forIn d f

@[instance_reducible]

instance Batteries.AssocList.instForInProdOfMonad {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [Monad m] : ForIn m (AssocList α β) (α × β)

Equations

• Batteries.AssocList.instForInProdOfMonad = { forIn := fun {β_1 : Type ?u.4} => Batteries.AssocList.forIn }

def Batteries.AssocList.pop? {α : Type u_1} {β : Type u_2} : AssocList α β → Option ((α × β) × AssocList α β)

Split the list into head and tail, if possible.

Equations

• Batteries.AssocList.nil.pop? = none
• (Batteries.AssocList.cons a b es).pop? = some ((a, b), es)

@[instance_reducible]

instance Batteries.AssocList.instToStream {α : Type u_1} {β : Type u_2} : Std.ToStream (AssocList α β) (AssocList α β)

Equations

• Batteries.AssocList.instToStream = { toStream := fun (x : Batteries.AssocList α β) => x }

@[instance_reducible]

instance Batteries.AssocList.instStreamProd {α : Type u_1} {β : Type u_2} : Std.Stream (AssocList α β) (α × β)

Equations

• Batteries.AssocList.instStreamProd = { next? := Batteries.AssocList.pop? }

def List.toAssocList {α : Type u_1} {β : Type u_2} : List (α × β) → Batteries.AssocList α β

Converts a list into an AssocList. This is the inverse function to AssocList.toList.

Equations

• [].toAssocList = Batteries.AssocList.nil
• ((a, b) :: es).toAssocList = Batteries.AssocList.cons a b es.toAssocList

def Batteries.AssocList.beq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : AssocList α β → AssocList α β → Bool

Implementation of == on AssocList.

Equations

• Batteries.AssocList.nil.beq Batteries.AssocList.nil = true
• (Batteries.AssocList.cons key value tail).beq Batteries.AssocList.nil = false
• Batteries.AssocList.nil.beq (Batteries.AssocList.cons key value tail) = false
• (Batteries.AssocList.cons a b t).beq (Batteries.AssocList.cons a' b' t') = (a == a' && b == b' && t.beq t')

@[instance_reducible]

instance Batteries.AssocList.instBEq {α : Type u_1} {β : Type u_2} [BEq α] [BEq β] : BEq (AssocList α β)

Boolean equality for AssocList. (This relation cares about the ordering of the key-value pairs.)

Equations

• Batteries.AssocList.instBEq = { beq := Batteries.AssocList.beq }