vec.bend source
vec.bend on the hub · documented module
# Vec: a growable array. push is amortized O(1): a full buffer doubles.## get, set and pop are one Array access. An index at or past the length# answers None (get, pop) or leaves the vector as it was (set).import Basetype Vec<-T: Data> is Type: VNil{} Vec{len: U32, buf: Array<T>}def Vec.new(~T: Data) -> Vec<T>: VNil{}def Vec.len(~T: Data, v: Vec<T>) -> Vec<T> & U32: match v: case VNil{}: (VNil{}, 0) case Vec{+n, buf}: (Vec{n, buf}, n)def Vec.copy( ~T: Data, fuel: Nat, +i: U32, dst: Array<T>, r: Array<T> & T) -> Array<T>: match fuel: case 0n: dst case 1n+p: (src, x) = r +j = U32.inc(i) Vec.copy(~T, p, j, Array.set(T, dst, i, x), Array.get(T, src, j))def Vec.push.grow( ~T: Data, full: Bool, +n: U32, +x: T, buf: Array<T>, +cap: U32) -> Vec<T>: match full: case False{}: Vec{U32.inc(n), Array.set(T, buf, n, x)} case True{}: # Every slot of big starts as x, so slot n needs no write. big = Array.new(T, 1n+U32.log2(cap), x) Vec{U32.inc(n), Vec.copy(~T, U32.to_nat(n), 0, big, Array.get(T, buf, 0))}def Vec.push.at(~T: Data, +n: U32, +x: T, bc: Array<T> & U32) -> Vec<T>: (buf, +cap) = bc Vec.push.grow(~T, U32.is_eq(n, cap), n, x, buf, cap)def Vec.push(~T: Data, v: Vec<T>, +x: T) -> Vec<T>: match v: case VNil{}: Vec{1, ALeaf{x}} case Vec{+n, buf}: Vec.push.at(~T, n, x, Array.size(T, buf))def Vec.get.fin(~T: Data, n: U32, r: Array<T> & T) -> Vec<T> & Maybe<&2, T>: (buf, x) = r (Vec{n, buf}, Some{x})def Vec.get.if( ~T: Data, ok: Bool, +n: U32, buf: Array<T>, +i: U32) -> Vec<T> & Maybe<&2, T>: match ok: case True{}: Vec.get.fin(~T, n, Array.get(T, buf, i)) case False{}: (Vec{n, buf}, None{})def Vec.get(~T: Data, v: Vec<T>, +i: U32) -> Vec<T> & Maybe<&2, T>: match v: case VNil{}: (VNil{}, None{}) case Vec{+n, buf}: Vec.get.if(~T, U32.is_lt(i, n), n, buf, i)def Vec.set.if( ~T: Data, ok: Bool, n: U32, buf: Array<T>, i: U32, x: T) -> Vec<T>: match ok: case True{}: Vec{n, Array.set(T, buf, i, x)} case False{}: Vec{n, buf}def Vec.set(~T: Data, v: Vec<T>, +i: U32, x: T) -> Vec<T>: match v: case VNil{}: VNil{} case Vec{+n, buf}: Vec.set.if(~T, U32.is_lt(i, n), n, buf, i, x)def Vec.pop.if( ~T: Data, empty: Bool, +n: U32, buf: Array<T>) -> Vec<T> & Maybe<&2, T>: match empty: case True{}: (Vec{n, buf}, None{}) case False{}: +m = (n - 1 : U32) Vec.get.fin(~T, m, Array.get(T, buf, m))# The last element, and the vector without it. The buffer keeps its size.def Vec.pop(~T: Data, v: Vec<T>) -> Vec<T> & Maybe<&2, T>: match v: case VNil{}: (VNil{}, None{}) case Vec{+n, buf}: Vec.pop.if(~T, U32.is_zero(n), n, buf)def Vec.to_list.go( ~T: Data, fuel: Nat, +i: U32, acc: List<&2, T>, r: Array<T> & T) -> List<&2, T>: match fuel: case 0n: acc case 1n+p: (buf, x) = r +j = (i - 1 : U32) Vec.to_list.go(~T, p, j, x <> acc, Array.get(T, buf, j))# The elements, first to last.def Vec.to_list(~T: Data, v: Vec<T>) -> List<&2, T>: match v: case VNil{}: Nil{} case Vec{+n, buf}: +last = (n - 1 : U32) Vec.to_list.go(~T, U32.to_nat(n), last, Nil{}, Array.get(T, buf, last))def Vec.from_list.go(~T: Data, xs: List<&2, T>, v: Vec<T>) -> Vec<T>: match xs: case Nil{}: v case h <> t: Vec.from_list.go(~T, t, Vec.push(~T, v, h))def Vec.from_list(~T: Data, xs: List<&2, T>) -> Vec<T>: Vec.from_list.go(~T, xs, VNil{})