hex

1.3. Ordered-map traversal and merging🔗

The additions to Std.ExtTreeMap are representation-independent building blocks used by sparse polynomial and other canonical-map code.

🔗def
Std.ExtTreeMap.foldl₂.{u, v, w, x} {α : Type u} {β : Type v}
  {γ : Type w} {δ : Type x} {cmp : α → α → Ordering} [Std.TransCmp cmp]
  (f : δ → α → Option β → Option γ → δ) (init : δ)
  (left : Std.ExtTreeMap α β cmp) (right : Std.ExtTreeMap α γ cmp) : δ
Std.ExtTreeMap.foldl₂.{u, v, w, x}
  {α : Type u} {β : Type v} {γ : Type w}
  {δ : Type x} {cmp : α → α → Ordering}
  [Std.TransCmp cmp]
  (f : δ → α → Option β → Option γ → δ)
  (init : δ)
  (left : Std.ExtTreeMap α β cmp)
  (right : Std.ExtTreeMap α γ cmp) : δ

Joint ordered fold over two maps in increasing comparator order.

The callback sees some exactly on the sides that contain a comparator-equivalent key; at a shared entry it receives the left map's key representative. The implementation performs linear merge work after materializing the two ordered streams.

🔗def
Std.ExtTreeMap.mergeWith?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (f : α → β → β → Option β) (left right : Std.ExtTreeMap α β cmp) :
  Std.ExtTreeMap α β cmp
Std.ExtTreeMap.mergeWith?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (f : α → β → β → Option β)
  (left right : Std.ExtTreeMap α β cmp) :
  Std.ExtTreeMap α β cmp

Merge two maps, allowing a collision to delete its key.

Left-only and right-only entries are retained unchanged. The smaller map is folded into the larger map, so the operation performs O(min(m,n) * log(max(m,n))) tree work. The collision callback always receives the left value before the right value, independent of which map is smaller. LawfulEqCmp makes comparator-equivalent keys propositionally equal, so the choice of the larger map cannot observably change the stored collision key.

foldl₂ presents left-only, shared, and right-only entries in key order. mergeWith? retains unmatched entries and lets the collision callback update or delete a shared key. Its lookup theorem is the public specification, so callers do not need to unfold the tree traversal.

🔗theorem
Std.ExtTreeMap.getElem?_mergeWith?.{u, v} {α : Type u} {β : Type v}
  {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (f : α → β → β → Option β) (left right : Std.ExtTreeMap α β cmp)
  (key : α) :
  (Std.ExtTreeMap.mergeWith? f left right)[key]? =
    Std.ExtTreeMap.mergeValue? f key left[key]? right[key]?
Std.ExtTreeMap.getElem?_mergeWith?.{u, v}
  {α : Type u} {β : Type v}
  {cmp : α → α → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (f : α → β → β → Option β)
  (left right : Std.ExtTreeMap α β cmp)
  (key : α) :
  (Std.ExtTreeMap.mergeWith? f left
        right)[key]? =
    Std.ExtTreeMap.mergeValue? f key
      left[key]? right[key]?

Lookup specification for a deletion-capable merge.