def swap_final

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

import Base
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size

328def swap_final(-T: Data, -d: Nat, -original: Array<T>, -sized_array: Array<T>, -n: U32,
329  -i: U32, -new: T,
330  measured: {(sized_array, n) == Array.size(T, original) : Array<T> & U32},
331  +retained: {sized_array == original : Array<T>}, +extent: {n == Size.capacity(d) : U32},
332  child: Swap<T, d, sized_array, n, masked(n, i), U32.is_lt(masked(n, i), U32.shr(n)), new>) ->
333  SwapFull<T, d, original, i, new>:
334  match child:
335    case Swap{array, old, equal, written, observed, valid}:
336      SwapFull{array, old,
337        Equal.trans(Array<T> & T, (array, old), Array.swap.at(T, i, new, (sized_array, n)),
338          Array.swap(T, original, i, new), equal,
339          Equal.cong(Array<T> & U32, Array<T> & T, r => Array.swap.at(T, i, new, r),
340            (sized_array, n), Array.size(T, original), measured)),
341        written_transport(T, d, sized_array, original, n, i, new, array, retained, extent, written),
342        observed_transport(T, d, sized_array, original, n, i, old, retained, extent, observed),
343        valid}