1	import Base
2	import ./doubly_linked_list.bend as D
3	import ./internal/dlist_storage.bend as R
4	import ./types/doubly_linked_list.bend as E
5	import ./types/internal_dlist.bend as H
6	
7	def 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.
16	type Error is Data:
17	  Exhausted{}
18	  NoCurrent{}
19	  Storage{error: E.Error}
20	
21	type 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.
27	def 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	
32	def first_result(~T: Data, r: D.DList<T> & U32) -> Iterator<T>:
33	  (s, h) = r
34	  IT{s, h, 0, True{}, 0n}
35	
36	def iter_first(~T: Data, s: D.DList<T>) -> Iterator<T>:
37	  first_result(~T, endpoint(~T, s, True{}))
38	
39	def last_result(~T: Data, r: D.DList<T> & Nat) -> Iterator<T>:
40	  (s, n) = r
41	  IT{s, 0, 0, True{}, n}
42	
43	def iter_last(~T: Data, s: D.DList<T>) -> Iterator<T>:
44	  last_result(~T, D.length(~T, s))
45	
46	def finish(~T: Data, it: Iterator<T>) -> D.DList<T>:
47	  IT{s, n, last, f, i} = it
48	  s
49	
50	def present(h: U32) -> Bool:
51	  U32.is_lt(0, h)
52	
53	def 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	
57	def 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	
61	def 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	
65	def 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	
69	def 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	
73	def 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	
77	def 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	
84	def 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	
88	def 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.
93	def 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	
97	type Move<-T: Data> is Data:
98	  M{next: U32, last: U32, forward: Bool, index: Nat, result: Result<&2, &2, Error, T>}
99	
100	def 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	
107	def 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	
111	def 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	
118	type Forward<-T: Data> is Type:
119	  F{vals: Array<Maybe<&2, T>>, nexts: Array<U32>, after: U32, value: Result<&2, &2, Error, T>}
120	
121	def 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	
125	def 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	
129	def 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	
136	def 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	
140	def 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	
144	def 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	
148	def 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	
152	def 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	
159	def 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	
163	def 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	
167	def 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	
171	def 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	
175	def 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	
179	def 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	
186	def 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	
193	def 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	
200	def 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	
204	def 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	
208	def 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	
212	def 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	
219	def 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	
223	def 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	
227	def 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	
234	def 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	
238	def 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