PersistentHashMap iterator

This module provides an iterator for Lean.PersistentHashMap that is accessible via Lean.PersistentHashMap.iter.

inductive Lean.PersistentHashMap.Zipper (α : Type u) (β : Type v) : Type (max u v)

A zipper for traversing a PersistentHashMap. This is an inductive structure representing the remaining key-value pairs to yield.

• done {α : Type u} {β : Type v} : Zipper α β

  No more elements to yield.

• consEntries {α : Type u} {β : Type v} : Subarray (Entry α β (Node α β)) → Zipper α β → Zipper α β

  A frame of entries from a trie node.

• consCollision {α : Type u} {β : Type v} (keys : Subarray α) (vals : Subarray β) : Std.Slice.size keys = Std.Slice.size vals → Zipper α β → Zipper α β

  A frame of key-value pairs from a collision node.

def Lean.PersistentHashMap.Zipper.prependNode {α : Type u_1} {β : Type u_2} (node : Node α β) (z : Zipper α β) : Zipper α β

Equations

• One or more equations did not get rendered due to their size.
• Lean.PersistentHashMap.Zipper.prependNode (Lean.PersistentHashMap.Node.entries es) z = Lean.PersistentHashMap.Zipper.consEntries es.toSubarray z

@[inline]

def Lean.PersistentHashMap.Zipper.step {α : Type u_1} {β : Type u_2} (it : Std.IterM Id (α × β)) : Std.IterStep (Std.IterM Id (α × β)) (α × β)

Equations

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

@[implicit_reducible]

instance Lean.PersistentHashMap.instIterator {α : Type u_1} {β : Type u_2} : Std.Iterator (Zipper α β) Id (α × β)

Equations

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

@[irreducible]

def Lean.PersistentHashMap.Node.measure {α : Type u_1} {β : Type u_2} (node : Node α β) : Nat

Counts the total number of entries reachable from a node, including nested children.

Equations

• (Lean.PersistentHashMap.Node.entries es).measure = Lean.PersistentHashMap.Node.measure.measureEntries✝ es 0
• (Lean.PersistentHashMap.Node.collision keys vals hsz).measure = vals.size

def Lean.PersistentHashMap.Entry.measure {α : Type u_1} {β : Type u_2} (entry : Entry α β (Node α β)) : Nat

Equations

• Lean.PersistentHashMap.Entry.null.measure = 1
• (Lean.PersistentHashMap.Entry.entry k v).measure = 1
• (Lean.PersistentHashMap.Entry.ref node).measure = 2 + node.measure

def Lean.PersistentHashMap.subarrayMeasure {α : Type u_1} {β : Type u_2} (es : Subarray (Entry α β (Node α β))) : Nat

Counts entries remaining in a subarray, including nested children.

Equations

• Lean.PersistentHashMap.subarrayMeasure es = (List.map (fun (x : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) => x.measure) (Std.Slice.toList es)).sum

def Lean.PersistentHashMap.Zipper.measure {α : Type u_1} {β : Type u_2} : Zipper α β → Nat

Counts the total remaining work in a zipper, including entries nested in child nodes.

Equations

• Lean.PersistentHashMap.Zipper.done.measure = 0
• (Lean.PersistentHashMap.Zipper.consEntries es z').measure = Lean.PersistentHashMap.subarrayMeasure es + z'.measure + 1
• (Lean.PersistentHashMap.Zipper.consCollision keys vals hsz z').measure = Std.Slice.size vals + z'.measure + 1

instance Lean.PersistentHashMap.instFinite {α : Type u_1} {β : Type u_2} : Std.Iterators.Finite (Zipper α β) Id

@[implicit_reducible, inline]

instance Lean.PersistentHashMap.instIteratorLoop {α : Type u_1} {β : Type u_2} {n : Type u_3 → Type u_4} [Monad n] : Std.IteratorLoop (Zipper α β) Id n

Equations

• Lean.PersistentHashMap.instIteratorLoop = Std.IteratorLoop.defaultImplementation

@[inline]

def Lean.PersistentHashMap.iter {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (map : PersistentHashMap α β) : Std.Iter (α × β)

Returns a finite iterator over the key-value pairs of the given PersistentHashMap. The iteration order is unspecified.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• map.iter = { internalState := Lean.PersistentHashMap.Zipper.prependNode map.root Lean.PersistentHashMap.Zipper.done }