def ASet.Apart

bend-ml-tensor-array@0.1.19.0 · main.bend:2117

import Base

2117# ASet.Apart(T, a, n, j, z, k, w): the write's descent (index j, first branch z) and the read's descent (k, w),
2118# both started from the size n, take different branches at some node of a before either reaches a leaf.
2119# It is Empty when both reach the same leaf, and Unit at the node where they split.
2120def ASet.Apart(-T: Data, a: Array<T>, +n: U32, +j: U32, +z: Bool, +k: U32, +w: Bool) -> Type:
2121  match a z w:
2122    case ALeaf{x} _ _:
2123      Empty
2124    case ANode{xs, ys} True{} True{}:
2125      ASet.Apart(T, xs, U32.shr(n), j, U32.is_lt(j, U32.shr(U32.shr(n))), k, U32.is_lt(k, U32.shr(U32.shr(n))))
2126    case ANode{xs, ys} False{} False{}:
2127      ASet.Apart(T, ys, U32.shr(n), U32.sub(j, U32.shr(n)), U32.is_lt(U32.sub(j, U32.shr(n)), U32.shr(U32.shr(n))), U32.sub(k, U32.shr(n)), U32.is_lt(U32.sub(k, U32.shr(n)), U32.shr(U32.shr(n))))
2128    case ANode{xs, ys} True{} False{}:
2129      Unit
2130    case ANode{xs, ys} False{} True{}:
2131      Unit