omap.bend checks

raw source on the hub · import 0x9d83ddf966d11f828944383c8c9577cc/omap.bend as Omap

OMap: an ordered map keyed by any Data type, as a weight-balanced tree.

The order is a template cmp, as in List.sort: OMap.put(~U32, ~U32, ~U32.cmp, m, 7, 70). put, get and del are O(log n) comparisons. Balance follows Hirai and Yamamoto (delta 3, gamma 2), which is correct for both insertion and deletion with one rebalance per level.

1 import

import Base

Types

type OMap source · line 9 · raw

@-K:Data -> @-V:Data -> Data

OTip
```
@-K:Data -> @-V:Data -> OMap<K, V>
```

OBin

@-K:Data -> @-V:Data -> @size:U32 -> @key:K -> @val:V -> @lo:OMap<K, V> -> @hi:OMap<K, V> -> OMap<K, V>

Definitions

def OMap.new source · line 13 · raw

@-K:Data -> @-V:Data -> OMap<K, V>

def OMap.size source · line 16 · raw

@-K:Data -> @-V:Data -> @m:OMap<K, V> -> U32

def Cmp.case source · line 25 · raw

@-A:Type -> @c:Cmp -> @lt:(@_:Unit -> A) -> @eq:(@_:Unit -> A) -> @gt:(@_:Unit -> A) -> A

The recursion on cmp's result: a match cannot scrutinize cmp(k, key), and a template cannot call a law filled below it, so each branch is a closure.

def OMap.bin source · line 36 · raw

@-K:Data -> @-V:Data -> @k:K -> @v:V -> @+lo:OMap<K, V> -> @+hi:OMap<K, V> -> OMap<K, V>

def OMap.rot_lo.double source · line 41 · raw

@-K:Data -> @-V:Data -> @k:K -> @v:V -> @lo:OMap<K, V> -> @hk:K -> @hv:V -> @hl:OMap<K, V> -> @hh:OMap<K, V> -> OMap<K, V>

def OMap.rot_lo.pick source · line 52 · raw

@-K:Data -> @-V:Data -> @single:Bool -> @k:K -> @v:V -> @lo:OMap<K, V> -> @hk:K -> @hv:V -> @hl:OMap<K, V> -> @hh:OMap<K, V> -> OMap<K, V>

def OMap.rot_lo source · line 63 · raw

@-K:Data -> @-V:Data -> @k:K -> @v:V -> @lo:OMap<K, V> -> @hi:OMap<K, V> -> OMap<K, V>

The hi side is too heavy: move weight toward lo.

def OMap.rot_hi.double source · line 75 · raw

@-K:Data -> @-V:Data -> @k:K -> @v:V -> @lk:K -> @lv:V -> @ll:OMap<K, V> -> @lh:OMap<K, V> -> @hi:OMap<K, V> -> OMap<K, V>

def OMap.rot_hi.pick source · line 86 · raw

@-K:Data -> @-V:Data -> @single:Bool -> @k:K -> @v:V -> @lk:K -> @lv:V -> @ll:OMap<K, V> -> @lh:OMap<K, V> -> @hi:OMap<K, V> -> OMap<K, V>

def OMap.rot_hi source · line 97 · raw

@-K:Data -> @-V:Data -> @k:K -> @v:V -> @lo:OMap<K, V> -> @hi:OMap<K, V> -> OMap<K, V>

The lo side is too heavy: move weight toward hi.

def OMap.balance.if source · line 109 · raw

@-K:Data -> @-V:Data -> @heavy_hi:Bool -> @heavy_lo:Bool -> @k:K -> @v:V -> @lo:OMap<K, V> -> @hi:OMap<K, V> -> OMap<K, V>

def OMap.balance source · line 122 · raw

@-K:Data -> @-V:Data -> @k:K -> @v:V -> @+lo:OMap<K, V> -> @+hi:OMap<K, V> -> OMap<K, V>

A node whose sides were balanced before one insertion or deletion.

def OMap.pop_min.fin source · line 159 · raw

@-K:Data -> @-V:Data -> @k:K -> @v:V -> @hi:OMap<K, V> -> @r:Pair(K, Pair(V, OMap<K, V>)) -> Pair(K, Pair(V, OMap<K, V>))

def OMap.pop_min source · line 167 · raw

@-K:Data -> @-V:Data -> @lo:OMap<K, V> -> @k:K -> @v:V -> @hi:OMap<K, V> -> Pair(K, Pair(V, OMap<K, V>))

The least entry of the node lo < (k, v) < hi, and the node without it.

def OMap.glue.fin source · line 176 · raw

@-K:Data -> @-V:Data -> @lo:OMap<K, V> -> @r:Pair(K, Pair(V, OMap<K, V>)) -> OMap<K, V>

def OMap.glue source · line 183 · raw

@-K:Data -> @-V:Data -> @lo:OMap<K, V> -> @hi:OMap<K, V> -> OMap<K, V>

Joins two sides of a deleted node.

def OMap.keys.go source · line 202 · raw

@-K:Data -> @-V:Data -> @m:OMap<K, V> -> @acc:List<&2, K> -> List<&2, K>

def OMap.keys source · line 212 · raw

@-K:Data -> @-V:Data -> @m:OMap<K, V> -> List<&2, K>

The keys in ascending order.

def OMap.to_list.go source · line 215 · raw

@-K:Data -> @-V:Data -> @m:OMap<K, V> -> @acc:List<&1, Pair(K, V)> -> List<&1, Pair(K, V)>

def OMap.to_list source · line 225 · raw

@-K:Data -> @-V:Data -> @m:OMap<K, V> -> List<&1, Pair(K, V)>

The entries in ascending key order.

def OSet source · line 228 · raw

@-K:Data -> Data

def OSet.new source · line 231 · raw

@-K:Data -> OSet(K)

def OSet.size source · line 234 · raw

@-K:Data -> @s:OSet(K) -> U32

def OSet.to_list source · line 247 · raw

@-K:Data -> @s:OSet(K) -> List<&2, K>

The elements in ascending order.

Templates

template OMap.put source · line 130 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:OMap<K, V> -> @+k:K -> @+v:V -> OMap<K, V>

template OMap.get source · line 142 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:OMap<K, V> -> @+k:K -> Maybe<&2, V>

template OMap.has source · line 154 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:OMap<K, V> -> @+k:K -> Bool

template OMap.del source · line 190 · raw

@-K:Data -> @-V:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @m:OMap<K, V> -> @+k:K -> OMap<K, V>

template OSet.add source · line 237 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @s:OSet(K) -> @+k:K -> OSet(K)

template OSet.has source · line 240 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @s:OSet(K) -> @+k:K -> Bool

template OSet.del source · line 243 · raw

@-K:Data -> @-cmp:(@_:K -> @_:K -> Cmp) -> @s:OSet(K) -> @+k:K -> OSet(K)