vec.bend
bend-kit-collections@0.1.1.0 · 136 lines · 0 definitions
1# Vec: a growable array. push is amortized O(1): a full buffer doubles.
2#
3# get, set and pop are one Array access. An index at or past the length
4# answers None (get, pop) or leaves the vector as it was (set).
5import Base
6
7type Vec<-T: Data> is Type:
8 VNil{}
9 Vec{len: U32, buf: Array<T>}
10
11def Vec.new(~T: Data) -> Vec<T>:
12 VNil{}
13
14def Vec.len(~T: Data, v: Vec<T>) -> Vec<T> & U32:
15 match v:
16 case VNil{}:
17 (VNil{}, 0)
18 case Vec{+n, buf}:
19 (Vec{n, buf}, n)
20
21def Vec.copy(
22 ~T: Data, fuel: Nat, +i: U32, dst: Array<T>, r: Array<T> & T
23) -> Array<T>:
24 match fuel:
25 case 0n:
26 dst
27 case 1n+p:
28 (src, x) = r
29 +j = U32.inc(i)
30 Vec.copy(~T, p, j, Array.set(T, dst, i, x), Array.get(T, src, j))
31
32def Vec.push.grow(
33 ~T: Data, full: Bool, +n: U32, +x: T, buf: Array<T>, +cap: U32
34) -> Vec<T>:
35 match full:
36 case False{}:
37 Vec{U32.inc(n), Array.set(T, buf, n, x)}
38 case True{}:
39 # Every slot of big starts as x, so slot n needs no write.
40 big = Array.new(T, 1n+U32.log2(cap), x)
41 Vec{U32.inc(n), Vec.copy(~T, U32.to_nat(n), 0, big, Array.get(T, buf, 0))}
42
43def Vec.push.at(~T: Data, +n: U32, +x: T, bc: Array<T> & U32) -> Vec<T>:
44 (buf, +cap) = bc
45 Vec.push.grow(~T, U32.is_eq(n, cap), n, x, buf, cap)
46
47def Vec.push(~T: Data, v: Vec<T>, +x: T) -> Vec<T>:
48 match v:
49 case VNil{}:
50 Vec{1, ALeaf{x}}
51 case Vec{+n, buf}:
52 Vec.push.at(~T, n, x, Array.size(T, buf))
53
54def Vec.get.fin(~T: Data, n: U32, r: Array<T> & T) -> Vec<T> & Maybe<&2, T>:
55 (buf, x) = r
56 (Vec{n, buf}, Some{x})
57
58def Vec.get.if(
59 ~T: Data, ok: Bool, +n: U32, buf: Array<T>, +i: U32
60) -> Vec<T> & Maybe<&2, T>:
61 match ok:
62 case True{}:
63 Vec.get.fin(~T, n, Array.get(T, buf, i))
64 case False{}:
65 (Vec{n, buf}, None{})
66
67def Vec.get(~T: Data, v: Vec<T>, +i: U32) -> Vec<T> & Maybe<&2, T>:
68 match v:
69 case VNil{}:
70 (VNil{}, None{})
71 case Vec{+n, buf}:
72 Vec.get.if(~T, U32.is_lt(i, n), n, buf, i)
73
74def Vec.set.if(
75 ~T: Data, ok: Bool, n: U32, buf: Array<T>, i: U32, x: T
76) -> Vec<T>:
77 match ok:
78 case True{}:
79 Vec{n, Array.set(T, buf, i, x)}
80 case False{}:
81 Vec{n, buf}
82
83def Vec.set(~T: Data, v: Vec<T>, +i: U32, x: T) -> Vec<T>:
84 match v:
85 case VNil{}:
86 VNil{}
87 case Vec{+n, buf}:
88 Vec.set.if(~T, U32.is_lt(i, n), n, buf, i, x)
89
90def Vec.pop.if(
91 ~T: Data, empty: Bool, +n: U32, buf: Array<T>
92) -> Vec<T> & Maybe<&2, T>:
93 match empty:
94 case True{}:
95 (Vec{n, buf}, None{})
96 case False{}:
97 +m = (n - 1 : U32)
98 Vec.get.fin(~T, m, Array.get(T, buf, m))
99
100# The last element, and the vector without it. The buffer keeps its size.
101def Vec.pop(~T: Data, v: Vec<T>) -> Vec<T> & Maybe<&2, T>:
102 match v:
103 case VNil{}:
104 (VNil{}, None{})
105 case Vec{+n, buf}:
106 Vec.pop.if(~T, U32.is_zero(n), n, buf)
107
108def Vec.to_list.go(
109 ~T: Data, fuel: Nat, +i: U32, acc: List<&2, T>, r: Array<T> & T
110) -> List<&2, T>:
111 match fuel:
112 case 0n:
113 acc
114 case 1n+p:
115 (buf, x) = r
116 +j = (i - 1 : U32)
117 Vec.to_list.go(~T, p, j, x <> acc, Array.get(T, buf, j))
118
119# The elements, first to last.
120def Vec.to_list(~T: Data, v: Vec<T>) -> List<&2, T>:
121 match v:
122 case VNil{}:
123 Nil{}
124 case Vec{+n, buf}:
125 +last = (n - 1 : U32)
126 Vec.to_list.go(~T, U32.to_nat(n), last, Nil{}, Array.get(T, buf, last))
127
128def Vec.from_list.go(~T: Data, xs: List<&2, T>, v: Vec<T>) -> Vec<T>:
129 match xs:
130 case Nil{}:
131 v
132 case h <> t:
133 Vec.from_list.go(~T, t, Vec.push(~T, v, h))
134
135def Vec.from_list(~T: Data, xs: List<&2, T>) -> Vec<T>:
136 Vec.from_list.go(~T, xs, VNil{})