def clear_go_at

bend-collections@1.0.0.0 · src/containers/dynamic_array.bend:423

import Base

423# The executable clear resets the occupied slots [0, length) to None, top
424# down, and keeps the block: O(length), no allocation. Dropping the old block
425# and allocating a fresh one (what the parametric `clear` describes) walks
426# every one of the 2^depth slots twice in the runtime. Every slot at or past
427# the length already holds None, so the result is the same all-None block;
428# proofs/containers/dynamic_array/clear.bend proves it on every good state.
429def clear_go_at(~T: Data, k: Nat, arr: Array<Maybe<&2, T>>) -> Array<Maybe<&2, T>>:
430  match k:
431    case 0n:
432      arr
433    case 1n+ +m:
434      clear_go_at(~T, m, Array.set(Maybe<&2, T>, arr, U32.from_nat(m), None{}))