src/containers/dlist_iterator.bend
bend-collections-laws-containers@1.0.0.0 · 241 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/doubly_linked_list.bend as D
3import bend-collections-laws-containers@1.0.0.0/src/containers/internal/dlist_storage.bend as R
4import bend-collections-laws-containers@1.0.0.0/src/containers/types/doubly_linked_list.bend as E
5import bend-collections-laws-containers@1.0.0.0/src/containers/types/internal_dlist.bend as H
6
7def choose(-A: Data, b: Bool, x: A, y: A) -> A:
8 match b:
9 case True{}:
10 x
11 case False{}:
12 y
13
14# Owning, bidirectional gap cursor. The list cannot be used independently until
15# finish() returns it. last is cleared by add/remove, retained by set and seeks.
16type Error is Data:
17 Exhausted{}
18 NoCurrent{}
19 Storage{error: E.Error}
20
21type Iterator<-T: Data> is Type:
22 IT{list: D.DList<T>, next: U32, last: U32, forward: Bool, index: Nat}
23
24# Cursor links are arena indices plus one; zero is the gap past the end.
25# Only this owning iterator can mutate the list until finish. Public handles
26# retain their owner and generation; a cursor is never exposed as a handle.
27def endpoint(~T: Data, s: D.DList<T>, +front: Bool) -> D.DList<T> & U32:
28 D.DL{tag, depth, cap, raw, gens} = s
29 R.DL{owner, fresh, free, count, +head, +tail, rd, rc, vals, prevs, nexts} = raw
30 (D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, choose(U32, front, head, tail))
31
32def first_result(~T: Data, r: D.DList<T> & U32) -> Iterator<T>:
33 (s, h) = r
34 IT{s, h, 0, True{}, 0n}
35
36def iter_first(~T: Data, s: D.DList<T>) -> Iterator<T>:
37 first_result(~T, endpoint(~T, s, True{}))
38
39def last_result(~T: Data, r: D.DList<T> & Nat) -> Iterator<T>:
40 (s, n) = r
41 IT{s, 0, 0, True{}, n}
42
43def iter_last(~T: Data, s: D.DList<T>) -> Iterator<T>:
44 last_result(~T, D.length(~T, s))
45
46def finish(~T: Data, it: Iterator<T>) -> D.DList<T>:
47 IT{s, n, last, f, i} = it
48 s
49
50def present(h: U32) -> Bool:
51 U32.is_lt(0, h)
52
53def has_next(~T: Data, it: Iterator<T>) -> Iterator<T> & Bool:
54 IT{s, +n, last, f, i} = it
55 (IT{s, n, last, f, i}, present(n))
56
57def has_previous(~T: Data, it: Iterator<T>) -> Iterator<T> & Bool:
58 IT{s, n, last, f, +i} = it
59 (IT{s, n, last, f, i}, Nat.is_lt(0n, i))
60
61def position(~T: Data, it: Iterator<T>) -> Iterator<T> & Nat:
62 IT{s, n, last, f, +i} = it
63 (IT{s, n, last, f, i}, i)
64
65def cursor_set(~T: Data, s: D.DList<T>, link: U32, x: T) -> D.DList<T> & Result<&2, &2, E.Error, Unit>:
66 D.DL{+tag, depth, cap, raw, gens} = s
67 D.set_result(~T, tag, depth, cap, gens, R.set(~T, raw, H.H{tag, U32.sub(link, 1)}, x))
68
69def cursor_remove_gen(~T: Data, +tag: U32, depth: Nat, cap: U32, raw: R.DList<T>, +id: U32, r: Array<U32> & U32) -> D.DList<T> & Result<&2, &2, E.Error, T>:
70 (gens, generation) = r
71 D.project_value(~T, D.removed(~T, tag, depth, cap, gens, id, generation, R.remove(~T, raw, H.H{tag, id})))
72
73def cursor_remove(~T: Data, s: D.DList<T>, +link: U32) -> D.DList<T> & Result<&2, &2, E.Error, T>:
74 D.DL{tag, depth, cap, raw, gens} = s
75 cursor_remove_gen(~T, tag, depth, cap, raw, U32.sub(link, 1), Array.get(U32, gens, U32.sub(link, 1)))
76
77def gap_left(prevs: Array<U32>, tail: U32, n: U32, empty: Bool) -> Array<U32> & U32:
78 match empty:
79 case True{}:
80 (prevs, tail)
81 case False{}:
82 Array.get(U32, prevs, U32.sub(n, 1))
83
84def insert_gap_result(~T: Data, r: D.DList<T> & E.Handle) -> D.DList<T> & Result<&2, &2, E.Error, E.Handle>:
85 (s, h) = r
86 (s, Done{h})
87
88def insert_gap(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, owner: U32, fresh: U32, free: U32, count: Nat, head: U32, tail: U32, rd: Nat, rc: U32, vals: Array<Maybe<&2, T>>, nexts: Array<U32>, n: U32, x: T, r: Array<U32> & U32) -> D.DList<T> & Result<&2, &2, E.Error, E.Handle>:
89 (prevs, before) = r
90 insert_gap_result(~T, D.inserted(~T, tag, depth, cap, gens, R.insert_between_free(~T, owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts, before, n, x)))
91
92# n is a live cursor link, or zero for the gap following the tail.
93def cursor_insert_gap(~T: Data, s: D.DList<T>, +n: U32, x: T) -> D.DList<T> & Result<&2, &2, E.Error, E.Handle>:
94 D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, +tail, rd, rc, vals, prevs, nexts}, gens} = s
95 insert_gap(~T, tag, depth, cap, gens, owner, fresh, free, count, head, tail, rd, rc, vals, nexts, n, x, gap_left(prevs, tail, n, U32.is_eq(n, 0)))
96
97type Move<-T: Data> is Data:
98 M{next: U32, last: U32, forward: Bool, index: Nat, result: Result<&2, &2, Error, T>}
99
100def move_meta(~T: Data, n: U32, last: U32, f: Bool, +i: Nat, h: U32, next: U32, +forward: Bool, r: Result<&2, &2, Error, T>) -> Move<T>:
101 match r:
102 case Fail{e}:
103 M{n, last, f, i, Fail{e}}
104 case Done{x}:
105 M{next, h, forward, choose(Nat, forward, 1n+i, Nat.sub(i, 1n)), Done{x}}
106
107def attach_move(~T: Data, s: D.DList<T>, m: Move<T>) -> Iterator<T> & Result<&2, &2, Error, T>:
108 M{n, last, f, i, out} = m
109 (IT{s, n, last, f, i}, out)
110
111def storage_result(~T: Data, r: Result<&2, &2, E.Error, T>) -> Result<&2, &2, Error, T>:
112 match r:
113 case Fail{e}:
114 Fail{Storage{e}}
115 case Done{x}:
116 Done{x}
117
118type Forward<-T: Data> is Type:
119 F{vals: Array<Maybe<&2, T>>, nexts: Array<U32>, after: U32, value: Result<&2, &2, Error, T>}
120
121def forward_link(~T: Data, vals: Array<Maybe<&2, T>>, value: Maybe<&2, T>, r: Array<U32> & U32) -> Forward<T>:
122 (nexts, after) = r
123 F{vals, nexts, after, storage_result(~T, D.item_result(~T, R.value_of(~T, value)))}
124
125def forward_value(~T: Data, nexts: Array<U32>, n: U32, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> Forward<T>:
126 (vals, value) = r
127 forward_link(~T, vals, value, Array.get(U32, nexts, U32.sub(n, 1)))
128
129def forward_arrays(~T: Data, vals: Array<Maybe<&2, T>>, nexts: Array<U32>, +n: U32, empty: Bool) -> Forward<T>:
130 match empty:
131 case True{}:
132 F{vals, nexts, 0, Fail{Exhausted{}}}
133 case False{}:
134 forward_value(~T, nexts, n, Array.get(Maybe<&2, T>, vals, U32.sub(n, 1)))
135
136def forward_finish(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, owner: U32, fresh: U32, free: U32, count: Nat, head: U32, tail: U32, rd: Nat, rc: U32, prevs: Array<U32>, +n: U32, last: U32, f: Bool, i: Nat, r: Forward<T>) -> Iterator<T> & Result<&2, &2, Error, T>:
137 F{vals, nexts, after, value} = r
138 attach_move(~T, D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, move_meta(~T, n, last, f, i, n, after, True{}, value))
139
140def next_checked(~T: Data, it: Iterator<T>, empty: Bool) -> Iterator<T> & Result<&2, &2, Error, T>:
141 IT{D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, +n, last, f, i} = it
142 forward_finish(~T, tag, depth, cap, gens, owner, fresh, free, count, head, tail, rd, rc, prevs, n, last, f, i, forward_arrays(~T, vals, nexts, n, empty))
143
144def next(~T: Data, it: Iterator<T>) -> Iterator<T> & Result<&2, &2, Error, T>:
145 IT{s, +n, last, f, i} = it
146 next_checked(~T, IT{s, n, last, f, i}, U32.is_eq(n, 0))
147
148def backward_value_result(~T: Data, r: Array<Maybe<&2, T>> & Maybe<&2, T>) -> Array<Maybe<&2, T>> & Result<&2, &2, Error, T>:
149 (vals, value) = r
150 (vals, storage_result(~T, D.item_result(~T, R.value_of(~T, value))))
151
152def backward_value(~T: Data, vals: Array<Maybe<&2, T>>, h: U32, empty: Bool) -> Array<Maybe<&2, T>> & Result<&2, &2, Error, T>:
153 match empty:
154 case True{}:
155 (vals, Fail{Exhausted{}})
156 case False{}:
157 backward_value_result(~T, Array.get(Maybe<&2, T>, vals, U32.sub(h, 1)))
158
159def backward_finish(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, owner: U32, fresh: U32, free: U32, count: Nat, head: U32, tail: U32, rd: Nat, rc: U32, prevs: Array<U32>, nexts: Array<U32>, n: U32, last: U32, f: Bool, i: Nat, +h: U32, r: Array<Maybe<&2, T>> & Result<&2, &2, Error, T>) -> Iterator<T> & Result<&2, &2, Error, T>:
160 (vals, value) = r
161 attach_move(~T, D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, move_meta(~T, n, last, f, i, h, h, False{}, value))
162
163def previous_found(~T: Data, n: U32, last: U32, f: Bool, i: Nat, r: D.DList<T> & U32) -> Iterator<T> & Result<&2, &2, Error, T>:
164 (D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, +h) = r
165 backward_finish(~T, tag, depth, cap, gens, owner, fresh, free, count, head, tail, rd, rc, prevs, nexts, n, last, f, i, h, backward_value(~T, vals, h, U32.is_eq(h, 0)))
166
167def previous_target(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, owner: U32, fresh: U32, free: U32, count: Nat, head: U32, tail: U32, rd: Nat, rc: U32, vals: Array<Maybe<&2, T>>, nexts: Array<U32>, n: U32, last: U32, f: Bool, i: Nat, r: Array<U32> & U32) -> Iterator<T> & Result<&2, &2, Error, T>:
168 (prevs, target) = r
169 previous_found(~T, n, last, f, i, (D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, target))
170
171def previous_checked(~T: Data, it: Iterator<T>, empty: Bool) -> Iterator<T> & Result<&2, &2, Error, T>:
172 IT{D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, +tail, rd, rc, vals, prevs, nexts}, gens}, +n, last, f, i} = it
173 previous_target(~T, tag, depth, cap, gens, owner, fresh, free, count, head, tail, rd, rc, vals, nexts, n, last, f, i, gap_left(prevs, tail, n, empty))
174
175def previous(~T: Data, it: Iterator<T>) -> Iterator<T> & Result<&2, &2, Error, T>:
176 IT{s, +n, last, f, i} = it
177 previous_checked(~T, IT{s, n, last, f, i}, U32.is_eq(n, 0))
178
179def set_result(~T: Data, n: U32, last: U32, f: Bool, i: Nat, r: D.DList<T> & Result<&2, &2, E.Error, Unit>) -> Iterator<T> & Result<&2, &2, Error, Unit>:
180 match r:
181 case Tuple{s, Fail{e}}:
182 (IT{s, n, last, f, i}, Fail{Storage{e}})
183 case Tuple{s, Done{x}}:
184 (IT{s, n, last, f, i}, Done{Unit{}})
185
186def set_checked(~T: Data, it: Iterator<T>, x: T, empty: Bool) -> Iterator<T> & Result<&2, &2, Error, Unit>:
187 match it empty:
188 case IT{s, n, last, f, i} True{}:
189 (IT{s, n, 0, f, i}, Fail{NoCurrent{}})
190 case IT{s, n, +h, f, i} False{}:
191 set_result(~T, n, h, f, i, cursor_set(~T, s, h, x))
192
193def add_meta(n: U32, last: U32, f: Bool, i: Nat, r: Result<&2, &2, E.Error, E.Handle>) -> Move<Unit>:
194 match r:
195 case Fail{e}:
196 M{n, last, f, i, Fail{Storage{e}}}
197 case Done{h}:
198 M{n, 0, f, 1n+i, Done{Unit{}}}
199
200def attach_unit(~T: Data, s: D.DList<T>, m: Move<Unit>) -> Iterator<T> & Result<&2, &2, Error, Unit>:
201 M{n, last, f, i, out} = m
202 (IT{s, n, last, f, i}, out)
203
204def added(~T: Data, n: U32, last: U32, f: Bool, i: Nat, r: D.DList<T> & Result<&2, &2, E.Error, E.Handle>) -> Iterator<T> & Result<&2, &2, Error, Unit>:
205 (s, out) = r
206 attach_unit(~T, s, add_meta(n, last, f, i, out))
207
208def add(~T: Data, it: Iterator<T>, x: T) -> Iterator<T> & Result<&2, &2, Error, Unit>:
209 IT{s, +n, last, f, i} = it
210 added(~T, n, last, f, i, cursor_insert_gap(~T, s, n, x))
211
212def remove_meta(~T: Data, n: U32, last: U32, +f: Bool, +i: Nat, after: U32, r: Result<&2, &2, E.Error, T>) -> Move<Unit>:
213 match r:
214 case Fail{e}:
215 M{n, last, f, i, Fail{Storage{e}}}
216 case Done{x}:
217 M{after, 0, f, choose(Nat, f, Nat.sub(i, 1n), i), Done{Unit{}}}
218
219def removed(~T: Data, n: U32, last: U32, f: Bool, i: Nat, after: U32, r: D.DList<T> & Result<&2, &2, E.Error, T>) -> Iterator<T> & Result<&2, &2, Error, Unit>:
220 (s, out) = r
221 attach_unit(~T, s, remove_meta(~T, n, last, f, i, after, out))
222
223def remove_target(~T: Data, tag: U32, depth: Nat, cap: U32, gens: Array<U32>, owner: U32, fresh: U32, free: U32, count: Nat, head: U32, tail: U32, rd: Nat, rc: U32, vals: Array<Maybe<&2, T>>, prevs: Array<U32>, n: U32, +h: U32, f: Bool, i: Nat, r: Array<U32> & U32) -> Iterator<T> & Result<&2, &2, Error, Unit>:
224 (nexts, after) = r
225 removed(~T, n, h, f, i, after, cursor_remove(~T, D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, h))
226
227def remove_checked(~T: Data, it: Iterator<T>, empty: Bool) -> Iterator<T> & Result<&2, &2, Error, Unit>:
228 match it empty:
229 case IT{s, n, last, f, i} True{}:
230 (IT{s, n, 0, f, i}, Fail{NoCurrent{}})
231 case IT{D.DL{tag, depth, cap, R.DL{owner, fresh, free, count, head, tail, rd, rc, vals, prevs, nexts}, gens}, +n, +h, +f, i} False{}:
232 remove_target(~T, tag, depth, cap, gens, owner, fresh, free, count, head, tail, rd, rc, vals, prevs, n, h, f, i, gap_left(nexts, n, h, f))
233
234def set(~T: Data, it: Iterator<T>, x: T) -> Iterator<T> & Result<&2, &2, Error, Unit>:
235 IT{s, n, +last, f, i} = it
236 set_checked(~T, IT{s, n, last, f, i}, x, U32.is_eq(last, 0))
237
238def remove(~T: Data, it: Iterator<T>) -> Iterator<T> & Result<&2, &2, Error, Unit>:
239 IT{s, n, +last, f, i} = it
240 remove_checked(~T, IT{s, n, last, f, i}, U32.is_eq(last, 0))
241