def tswap

lawful-arrays@0.1.0.0 · proof_index.bend:547

import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

547# The tree a swap leaves, as a Tree (so the written array has a mirror too).
548def tswap(-T: Data, t: P.Tree<T>, +n: U32, +i: U32, v: T, z: Bool) -> P.Tree<T>:
549  match t z:
550    case P.TLeaf{x} _:
551      P.TLeaf{v}
552    case P.TNode{l, r} True{}:
553      +h = U32.shr(n)
554      P.TNode{tswap(T, l, h, i, v, U32.is_lt(i, U32.shr(h))), r}
555    case P.TNode{l, r} False{}:
556      +h = U32.shr(n)
557      +j = U32.sub(i, h)
558      P.TNode{l, tswap(T, r, h, j, v, U32.is_lt(j, U32.shr(h)))}