def get_high

bendtorch-core@0.1.0.0 · src/storage/refinement.bend:46

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

46def get_high(-T: Data, -p: Nat, -original: Array<T>, -n: U32, -i: U32,
47  xs: Array<T>,
48  child: Get<T, p, original, U32.shr(n), U32.sub(i, U32.shr(n)),
49    U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))>,
50  ex: Model.Balanced(T, p, xs)) -> Get<T, 1n+p, ANode{xs, original}, n, i, False{}>:
51  match child:
52    case Get{ys, value, equal, kept, observed, ey}:
53      Get{ANode{xs, ys}, value,
54        Equal.cong(Array<T> & T, Array<T> & T, r => Array.swap.hi(T, xs, r),
55          (ys, value), Array.get.go(T, original, U32.shr(n), U32.sub(i, U32.shr(n)),
56            U32.is_lt(U32.sub(i, U32.shr(n)), U32.shr(U32.shr(n)))), equal),
57        Equal.cong(Array<T>, Array<T>, y => ANode{xs, y}, ys, original, kept),
58        observed, (ex, ey)}