pure/BMapInternal

Reference for mo:core/pure/BMapInternal in the core library.

This module contains the internal B+tree machinery behind pure/BMap: node splits, rebalancing, cursor state, and bulk-build buffers. Treat it as implementation detail unless you are extending the map itself.

Import

mo:core/pure/BMapInternal

Status

• Pure immutable collection module

Public API

Types

• BMap, Order, Node, Leaf, Internal, SearchResult, InsertResult, DeleteResult, DeleteTopResult, GrowResult, SplitResult, BorrowResult, MergeResult, NodeCursor, IterDirection, IterState, Buffer, BuildLeaf, BuildInternal, BuildNode, Builder

Values

• btreeOrder
• maxKeys
• minKeys
• maxChildren
• minChildren
• iterStackSize

Functions

trapUnreachable<T>(msg : Text) : T

Traps on a path that should be unreachable and typechecks as any result type.

Use when: code or specifications need this operation with the documented contract.

getNode<K, V>(node : Node<K, V>, compare : (K, K) -> Order, key : K) : ?V

Reads the requested value from the structure.

Use when: reading this value is part of an implementation or postcondition.

sortPairsInPlace<K, V>(array : [var (K, V)], compare : (K, K) -> Order)

Sorts key/value pairs in-place according to the supplied key comparator.

Use when: code or specifications need this operation with the documented contract.

newBuffer<K, V>(capacity : Nat) : Buffer<K, V>

Allocates, appends to, or freezes an internal B+tree build buffer.

Contract

ensures result.count == 0;
ensures result.data[0].size() == capacity;

Use when: code or specifications need this operation with the documented contract.

bufferAppend<K, V>(buffer : Buffer<K, V>, kv : (K, V)) : ()

Allocates, appends to, or freezes an internal B+tree build buffer.

Contract

ensures buffer.count > 0;

Use when: code or specifications need this operation with the documented contract.

bufferToVarArray<K, V>(buffer : Buffer<K, V>) : [var (K, V)]

Allocates, appends to, or freezes an internal B+tree build buffer.

Contract

ensures result.size() == buffer.count;

Use when: code or specifications need this operation with the documented contract.

leafReplaceValueAt<K, V>(leaf : Leaf<K, V>, index : Nat, value : V) : Node<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

internalReplaceChildMaybeReuseKeys<K, V>(node : Internal<K, V>, compare : (K, K) -> Order, childIndex : Nat, newChild : Node<K, V>) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

rebalanceChild<K, V>(parent : Internal<K, V>, childIndex : Nat, underflowChild : Node<K, V>, min : Nat) : Node<K, V>

Repairs an underfull B+tree child during deletion.

Use when: code or specifications need this operation with the documented contract.

splitLeafFull<K, V>(leaf : Leaf<K, V>) : SplitResult<K, V>

Splits a full B+tree node and returns the promoted separator/result.

Use when: code or specifications need this operation with the documented contract.

splitInternalFull<K, V>(nodeInternal : Internal<K, V>) : SplitResult<K, V>

Splits a full B+tree node and returns the promoted separator/result.

Use when: code or specifications need this operation with the documented contract.

splitNodeFull<K, V>(node : Node<K, V>) : SplitResult<K, V>

Splits a full B+tree node and returns the promoted separator/result.

Use when: code or specifications need this operation with the documented contract.

insertNodeTopDown<K, V>(node : Node<K, V>, compare : (K, K) -> Order, key : K, value : V, max : Nat) : (Node<K, V>, ?V)

Returns or applies the corresponding update to the structure.

Use when: the postcondition must relate the updated value to the previous one.

pushCursor<K, V>(state : IterState<K, V>, node : Node<K, V>, index : Nat)

Returns or applies the corresponding update to the structure.

Use when: the postcondition must relate the updated value to the previous one.

buildNewLeaf<K, V>() : BuildLeaf<K, V>

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildNewInternal<K, V>() : BuildInternal<K, V>

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildRefreshRightmostPath<K, V>(builder : Builder<K, V>)

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildSplitLeafAppend<K, V>(leaf : BuildLeaf<K, V>, key : K, value : V) : (K, BuildNode<K, V>)

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildSplitInternalAppend<K, V>(nodeInternal : BuildInternal<K, V>, separator : K, rightChild : BuildNode<K, V>) : (K, BuildNode<K, V>)

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildPropagateSplit<K, V>(builder : Builder<K, V>, separator : K, rightNode : BuildNode<K, V>)

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildAppendNew<K, V>(builder : Builder<K, V>, key : K, value : V)

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildReplaceLast<K, V>(builder : Builder<K, V>, value : V)

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildAppendChecked<K, V>(builder : Builder<K, V>, compare : (K, K) -> Order, key : K, value : V) : Bool

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildFreezeNode<K, V>(node : BuildNode<K, V>) : Node<K, V>

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

buildToMap<K, V>(builder : Builder<K, V>) : BMap<K, V>

Maintains the incremental B+tree builder during bulk construction.

Use when: code or specifications need this operation with the documented contract.

emptyLeaf<K, V>() : Node<K, V>

Constructs the empty value for this module's data structure.

Use when: code or specifications need this operation with the documented contract.

leafFromArray<K, V>(keys : [K], values : [V], count : Nat) : Node<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

internalFromArrays<K, V>(keys : [K], children : [?Node<K, V>], count : Nat) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

internalFromChildren<K, V>(children : [?Node<K, V>]) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

singletonLeaf<K, V>(key : K, value : V) : Node<K, V>

Constructs a value containing exactly the supplied element or entry.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithInsertAt<T>(arr : [?T], index : Nat, elem : T, count : Nat) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithInsertAtValue<T>(arr : [T], index : Nat, elem : T, count : Nat) : [T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithRemoveAt<T>(arr : [?T], index : Nat, count : Nat) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithRemoveAtValue<T>(arr : [T], index : Nat, count : Nat) : [T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithReplaceAt<T>(arr : [?T], index : Nat, elem : T) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithReplaceAtValue<T>(arr : [T], index : Nat, elem : T) : [T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithReplaceTwo<T>(arr : [?T], indexA : Nat, elemA : T, indexB : Nat, elemB : T) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithSplitChild<T>(arr : [?T], index : Nat, leftElem : T, rightElem : T) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArrayWithRemoveAtAndReplaceAt<T>(arr : [?T], removeIndex : Nat, replaceIndex : Nat, replacement : T) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

copyArraySlice<T>(arr : [?T], start : Nat, end : Nat) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

concatArrays<T>(left : [?T], mid : ?T, right : [?T]) : [?T]

Builds a copied array with the requested insertion, removal, replacement, split, or concatenation.

Use when: code or specifications need this operation with the documented contract.

subNat(a : Nat, b : Nat, msg : Text) : Nat

Subtracts natural numbers on an internal path that supplies a trap message for invalid underflow.

Use when: code or specifications need this operation with the documented contract.

leafInsertAt<K, V>(leaf : Leaf<K, V>, index : Nat, kv : (K, V)) : Node<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

leafRemoveAt<K, V>(leaf : Leaf<K, V>, index : Nat) : Node<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

leafReplaceAt<K, V>(leaf : Leaf<K, V>, index : Nat, kv : (K, V)) : Node<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

leafInsert<K, V>(leaf : Leaf<K, V>, compare : (K, K) -> Order, key : K, value : V, max : Nat) : InsertResult<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

leafSplitInsert<K, V>(leaf : Leaf<K, V>, insertIndex : Nat, kv : (K, V), max : Nat) : SplitResult<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

leafDelete<K, V>(leaf : Leaf<K, V>, compare : (K, K) -> Order, key : K, min : Nat) : DeleteResult<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

internalReplaceChild<K, V>(node : Internal<K, V>, childIndex : Nat, newChild : Node<K, V>) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

internalInsertChild<K, V>(node : Internal<K, V>, index : Nat, leftChild : Node<K, V>, rightChild : Node<K, V>) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

internalRemoveAtWithChild<K, V>(node : Internal<K, V>, keyIndex : Nat, childIndex : Nat) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

internalRemoveAt<K, V>(node : Internal<K, V>, index : Nat) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

internalRemoveAtWithChildMerge<K, V>(node : Internal<K, V>, keyIndex : Nat, mergedChild : Node<K, V>) : Node<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

tryBorrowFromLeft<K, V>(parent : Internal<K, V>, childIndex : Nat, underflowChild : Node<K, V>, min : Nat) : ?Node<K, V>

Repairs an underfull B+tree child during deletion.

Use when: code or specifications need this operation with the documented contract.

tryBorrowFromRight<K, V>(parent : Internal<K, V>, childIndex : Nat, underflowChild : Node<K, V>, min : Nat) : ?Node<K, V>

Repairs an underfull B+tree child during deletion.

Use when: code or specifications need this operation with the documented contract.

mergeWithSibling<K, V>(parent : Internal<K, V>, childIndex : Nat, underflowChild : Node<K, V>) : MergeResult<K, V>

Repairs an underfull B+tree child during deletion.

Use when: code or specifications need this operation with the documented contract.

growChildForDelete<K, V>(parent : Internal<K, V>, childIndex : Nat, min : Nat) : GrowResult<K, V>

Repairs an underfull B+tree child during deletion.

Use when: code or specifications need this operation with the documented contract.

leafDeleteTopDown<K, V>(leaf : Leaf<K, V>, compare : (K, K) -> Order, key : K) : DeleteTopResult<K, V>

Applies the corresponding B+tree leaf operation.

Use when: code or specifications need this operation with the documented contract.

removeMinTopDown<K, V>(node : Node<K, V>, min : Nat) : (Node<K, V>, (K, V))

Returns the updated collection or value described by the contract.

Use when: the postcondition must relate the updated value to the previous one.

removeMaxTopDown<K, V>(node : Node<K, V>, min : Nat) : (Node<K, V>, (K, V))

Returns the updated collection or value described by the contract.

Use when: the postcondition must relate the updated value to the previous one.

deleteNodeTopDown<K, V>(node : Node<K, V>, compare : (K, K) -> Order, key : K, min : Nat) : DeleteTopResult<K, V>

Returns the updated collection or value described by the contract.

Use when: the postcondition must relate the updated value to the previous one.

internalDeleteTopDown<K, V>(node : Internal<K, V>, compare : (K, K) -> Order, key : K, min : Nat) : DeleteTopResult<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

deleteNode<K, V>(node : Node<K, V>, compare : (K, K) -> Order, key : K, min : Nat) : DeleteResult<K, V>

Returns the updated collection or value described by the contract.

Use when: the postcondition must relate the updated value to the previous one.

removeMin<K, V>(node : Node<K, V>, min : Nat) : (Node<K, V>, (K, V))

Returns the updated collection or value described by the contract.

Use when: the postcondition must relate the updated value to the previous one.

removeMax<K, V>(node : Node<K, V>, min : Nat) : (Node<K, V>, (K, V))

Returns the updated collection or value described by the contract.

Use when: the postcondition must relate the updated value to the previous one.

internalDelete<K, V>(node : Internal<K, V>, compare : (K, K) -> Order, key : K, min : Nat) : DeleteResult<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

insertNode<K, V>(node : Node<K, V>, compare : (K, K) -> Order, key : K, value : V, max : Nat) : InsertResult<K, V>

Returns or applies the corresponding update to the structure.

Use when: the postcondition must relate the updated value to the previous one.

internalInsert<K, V>(node : Internal<K, V>, compare : (K, K) -> Order, key : K, value : V, max : Nat) : InsertResult<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

internalSplitInsert<K, V>(node : Internal<K, V>, childIndex : Nat, leftChild : Node<K, V>, rightChild : Node<K, V>, max : Nat) : SplitResult<K, V>

Applies the corresponding B+tree internal-node operation.

Use when: code or specifications need this operation with the documented contract.

rootInsert<K, V>(root : Node<K, V>, compare : (K, K) -> Order, key : K, value : V, max : Nat) : (Node<K, V>, ?V)

Applies the corresponding top-down B+tree update helper.

Use when: code or specifications need this operation with the documented contract.

shrinkRootIfNeeded<K, V>(root : Node<K, V>) : Node<K, V>

Applies the corresponding top-down B+tree update helper.

Use when: code or specifications need this operation with the documented contract.

pushLeftSpine<K, V>(state : IterState<K, V>, node : Node<K, V>)

Returns or applies the corresponding update to the structure.

Use when: the postcondition must relate the updated value to the previous one.

pushRightSpine<K, V>(state : IterState<K, V>, node : Node<K, V>)

Returns or applies the corresponding update to the structure.

Use when: the postcondition must relate the updated value to the previous one.

initForward<K, V>(root : Node<K, V>) : IterState<K, V>

Maintains iterator state for traversing or seeking inside the B+tree.

Use when: code or specifications need this operation with the documented contract.

initBackward<K, V>(root : Node<K, V>) : IterState<K, V>

Maintains iterator state for traversing or seeking inside the B+tree.

Use when: code or specifications need this operation with the documented contract.

advanceForward<K, V>(state : IterState<K, V>) : ?(K, V)

Maintains iterator state for traversing or seeking inside the B+tree.

Use when: code or specifications need this operation with the documented contract.

advanceBackward<K, V>(state : IterState<K, V>) : ?(K, V)

Maintains iterator state for traversing or seeking inside the B+tree.

Use when: code or specifications need this operation with the documented contract.

seekForward<K, V>(root : Node<K, V>, compare : (K, K) -> Order, key : K) : IterState<K, V>

Maintains iterator state for traversing or seeking inside the B+tree.

Use when: code or specifications need this operation with the documented contract.

seekBackward<K, V>(root : Node<K, V>, compare : (K, K) -> Order, key : K) : IterState<K, V>

Maintains iterator state for traversing or seeking inside the B+tree.

Use when: code or specifications need this operation with the documented contract.

binarySearchKV<K>(keys : [K], compare : (K, K) -> Order, key : K, count : Nat) : SearchResult

Searches an internal key array to find the matching slot or child index.

Use when: code or specifications need this operation with the documented contract.

childIndexForKey<K>(keys : [K], compare : (K, K) -> Order, key : K, count : Nat) : Nat

Searches an internal key array to find the matching slot or child index.

Use when: code or specifications need this operation with the documented contract.

nodeLen<K, V>(node : Node<K, V>) : Nat

Reads structural information from a B+tree node.

Use when: code or specifications need this operation with the documented contract.

nodeIsFull<K, V>(node : Node<K, V>, max : Nat) : Bool

Reads structural information from a B+tree node.

Use when: code or specifications need this operation with the documented contract.

nodeIsUnderflow<K, V>(node : Node<K, V>, min : Nat) : Bool

Reads structural information from a B+tree node.

Use when: code or specifications need this operation with the documented contract.

isLeaf<K, V>(node : Node<K, V>) : Bool

Checks the predicate described by the return contract.

Use when: a branch condition or contract needs this predicate as a named fact.

getKeyAt<K, V>(node : Node<K, V>, index : Nat) : (K, V)

Reads the requested value from the structure.

Use when: reading this value is part of an implementation or postcondition.

getChildAt<K, V>(node : Node<K, V>, index : Nat) : Node<K, V>

Reads the requested value from the structure.

Use when: reading this value is part of an implementation or postcondition.

findMin<K, V>(node : Node<K, V>) : (K, V)

Reads the requested value from the structure.

Use when: reading this value is part of an implementation or postcondition.

findMax<K, V>(node : Node<K, V>) : (K, V)

Reads the requested value from the structure.

Use when: reading this value is part of an implementation or postcondition.

Summary

• Pure immutable collection module under mo:core/pure/BMapInternal.
• Exposes 89 public functions.