def join

bendtorch-core@0.1.0.0 · src/storage/size.bend:18

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

18def join(-T: Data, -d: Nat, -original: Array<T>, ys: Array<T>,
19  child: Sized<T, d, original>, valid: Model.Balanced(T, d, ys)) ->
20  Sized<T, 1n+d, ANode{original, ys}>:
21  match child:
22    case Sized{xs, n, retained, measured, extent, balanced}:
23      Sized{ANode{xs, ys}, U32.shl(n),
24        Equal.cong(Array<T>, Array<T>, x => ANode{x, ys}, xs, original, retained),
25        Equal.cong(Array<T> & U32, Array<T> & U32, r => Array.size.node(T, ys, r),
26          (xs, n), Array.size(T, original), measured),
27        Equal.cong(U32, U32, x => U32.shl(x), n, capacity(d), extent), (balanced, valid)}