deque.bend
bend-kit-collections@0.1.4.0 · 289 lines · 0 definitions
1# Deque: a double-ended queue, as a front list and a reversed back list.
2#
3# Pushing and popping on either end is amortized O(1), in any mix of ends
4# (the refill below says why). Like List, the queries consume the deque: a
5# Data deque is shared with +.
6#
7# The laws at the bottom are checked every time this file is imported.
8import Base
9
10type Deque<a, -A: Kind(a)> is Kind(a):
11 Deq{front: List<a, A>, back: List<a, A>}
12
13def Deque.new(a, -A: Kind(a)) -> Deque<a, A>:
14 Deq{Nil{}, Nil{}}
15
16# the list's first element is the deque's front
17def Deque.from_list(a, -A: Kind(a), xs: List<a, A>) -> Deque<a, A>:
18 Deq{xs, Nil{}}
19
20def Deque.push_front(a, -A: Kind(a), x: A, d: Deque<a, A>) -> Deque<a, A>:
21 match d:
22 case Deq{f, b}:
23 Deq{x <> f, b}
24
25def Deque.push_back(a, -A: Kind(a), x: A, d: Deque<a, A>) -> Deque<a, A>:
26 match d:
27 case Deq{f, b}:
28 Deq{f, x <> b}
29
30def Deque.count.put(
31 a, -A: Kind(a), h: A, rn: List<a, A> & Nat
32) -> List<a, A> & Nat:
33 (rest, n) = rn
34 (h <> rest, 1n+n)
35
36# a list and its length, in one pass that hands the list back
37def Deque.count(a, -A: Kind(a), xs: List<a, A>) -> List<a, A> & Nat:
38 match xs:
39 case Nil{}:
40 (Nil{}, 0n)
41 case h <> t:
42 Deque.count.put(a, A, h, Deque.count(a, A, t))
43
44def Deque.half(n: Nat) -> Nat:
45 match n:
46 case 0n:
47 0n
48 case 1n+p:
49 match p:
50 case 0n:
51 0n
52 case 1n+q:
53 1n+Deque.half(q)
54
55def Deque.split.put(
56 a, -A: Kind(a), h: A, lr: List<a, A> & List<a, A>
57) -> List<a, A> & List<a, A>:
58 (l, r) = lr
59 (h <> l, r)
60
61# the first n elements, and the rest
62def Deque.split(a, -A: Kind(a), n: Nat, xs: List<a, A>) ->
63 List<a, A> & List<a, A>:
64 match n:
65 case 0n:
66 (Nil{}, xs)
67 case 1n+p:
68 match xs:
69 case Nil{}:
70 (Nil{}, Nil{})
71 case h <> t:
72 Deque.split.put(a, A, h, Deque.split(a, A, p, t))
73
74# When one end runs out, the other list is split in half and only the half
75# nearest the empty end is reversed over. Moving everything would let pops
76# that alternate ends reverse the whole deque each time; halving keeps the
77# lists balanced, so every operation stays amortized O(1).
78
79def Deque.pop_front.go(
80 a, -A: Kind(a), xs: List<a, A>, b: List<a, A>
81) -> Maybe<&1, A & Deque<a, A>>:
82 match xs:
83 case Nil{}:
84 None{}
85 case h <> t:
86 Some{(h, Deq{t, b})}
87
88def Deque.pop_front.halves(
89 a, -A: Kind(a), sm: List<a, A> & List<a, A>
90) -> Maybe<&1, A & Deque<a, A>>:
91 (stay, move) = sm
92 Deque.pop_front.go(a, A, List.reverse(a, A, move), stay)
93
94def Deque.pop_front.refill(
95 a, -A: Kind(a), bn: List<a, A> & Nat
96) -> Maybe<&1, A & Deque<a, A>>:
97 (b, n) = bn
98 Deque.pop_front.halves(a, A, Deque.split(a, A, Deque.half(n), b))
99
100def Deque.pop_front(
101 a, -A: Kind(a), d: Deque<a, A>
102) -> Maybe<&1, A & Deque<a, A>>:
103 match d:
104 case Deq{f, b}:
105 match f:
106 case h <> t:
107 Some{(h, Deq{t, b})}
108 case Nil{}:
109 Deque.pop_front.refill(a, A, Deque.count(a, A, b))
110
111def Deque.pop_back.go(
112 a, -A: Kind(a), xs: List<a, A>, f: List<a, A>
113) -> Maybe<&1, A & Deque<a, A>>:
114 match xs:
115 case Nil{}:
116 None{}
117 case h <> t:
118 Some{(h, Deq{f, t})}
119
120def Deque.pop_back.halves(
121 a, -A: Kind(a), sm: List<a, A> & List<a, A>
122) -> Maybe<&1, A & Deque<a, A>>:
123 (stay, move) = sm
124 Deque.pop_back.go(a, A, List.reverse(a, A, move), stay)
125
126def Deque.pop_back.refill(
127 a, -A: Kind(a), fn: List<a, A> & Nat
128) -> Maybe<&1, A & Deque<a, A>>:
129 (f, n) = fn
130 Deque.pop_back.halves(a, A, Deque.split(a, A, Deque.half(n), f))
131
132def Deque.pop_back(
133 a, -A: Kind(a), d: Deque<a, A>
134) -> Maybe<&1, A & Deque<a, A>>:
135 match d:
136 case Deq{f, b}:
137 match b:
138 case h <> t:
139 Some{(h, Deq{f, t})}
140 case Nil{}:
141 Deque.pop_back.refill(a, A, Deque.count(a, A, f))
142
143# the elements, front to back
144def Deque.to_list(a, -A: Kind(a), d: Deque<a, A>) -> List<a, A>:
145 match d:
146 case Deq{f, b}:
147 List.append(a, A, f, List.reverse(a, A, b))
148
149def Deque.length(a, -A: Kind(a), d: Deque<a, A>) -> Nat:
150 match d:
151 case Deq{f, b}:
152 Nat.add(List.length(a, A, f), List.length(a, A, b))
153
154def Deque.is_empty(a, -A: Kind(a), d: Deque<a, A>) -> Bool:
155 match d:
156 case Deq{f, b}:
157 Bool.and(List.is_empty(a, A, f), List.is_empty(a, A, b))
158
159# Laws
160# ----
161# Each law reads a deque through to_list, the only view a user has of it.
162
163# LAW: a new deque reads as the empty list
164law Deque.to_list.new:
165 for -A: Data
166 {Deque.to_list(&2, A, Deque.new(&2, A)) == Nil{} : List<&2, A>}
167
168def Deque.to_list.new(A):
169 {==}
170
171# LAW: push_front puts the element at the head of the list
172law Deque.to_list.push_front:
173 for -A: Data
174 for -x: A
175 for d: Deque<&2, A>
176 {Deque.to_list(&2, A, Deque.push_front(&2, A, x, d))
177 == x <> Deque.to_list(&2, A, d) : List<&2, A>}
178
179def Deque.to_list.push_front(A, x, d):
180 match d:
181 case Deq{f, b}:
182 {==}
183
184# LAW: pop_front undoes push_front
185law Deque.pop_front.push_front:
186 for -A: Data
187 for -x: A
188 for d: Deque<&2, A>
189 {Deque.pop_front(&2, A, Deque.push_front(&2, A, x, d))
190 == Some{(x, d)} : Maybe<&1, A & Deque<&2, A>>}
191
192def Deque.pop_front.push_front(A, x, d):
193 match d:
194 case Deq{f, b}:
195 {==}
196
197# LAW: pop_back undoes push_back
198law Deque.pop_back.push_back:
199 for -A: Data
200 for -x: A
201 for d: Deque<&2, A>
202 {Deque.pop_back(&2, A, Deque.push_back(&2, A, x, d))
203 == Some{(x, d)} : Maybe<&1, A & Deque<&2, A>>}
204
205def Deque.pop_back.push_back(A, x, d):
206 match d:
207 case Deq{f, b}:
208 {==}
209
210# Lemmas over Base's List, by induction on the first list
211
212law Deque.lemma.append_nil:
213 for -A: Data
214 for xs: List<&2, A>
215 {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}
216
217def Deque.lemma.append_nil(A, xs):
218 match xs:
219 case Nil{}:
220 {==}
221 case h <> t:
222 %Deque.lemma.append_nil(A, t) : {h <> List.append(&2, A, t, Nil{})
223 == h <> _ : List<&2, A>}
224 {==}
225
226law Deque.lemma.append_assoc:
227 for -A: Data
228 for xs: List<&2, A>
229 for -ys: List<&2, A>
230 for -zs: List<&2, A>
231 {List.append(&2, A, List.append(&2, A, xs, ys), zs)
232 == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}
233
234def Deque.lemma.append_assoc(A, xs, ys, zs):
235 match xs:
236 case Nil{}:
237 {==}
238 case h <> t:
239 %Deque.lemma.append_assoc(A, t, ys, zs) : {h <> List.append(&2, A,
240 List.append(&2, A, t, ys), zs) == h <> _ : List<&2, A>}
241 {==}
242
243# LAW: a list read into a deque reads back as itself
244law Deque.to_list.from_list:
245 for -A: Data
246 for xs: List<&2, A>
247 {Deque.to_list(&2, A, Deque.from_list(&2, A, xs)) == xs : List<&2, A>}
248
249def Deque.to_list.from_list(A, xs):
250 Deque.lemma.append_nil(A, xs)
251
252# reversing onto an accumulator is reversing, then appending it
253law Deque.lemma.reverse_go:
254 for -A: Data
255 for xs: List<&2, A>
256 for -acc: List<&2, A>
257 {List.append(&2, A, List.reverse.go(&2, A, xs, Nil{}), acc)
258 == List.reverse.go(&2, A, xs, acc) : List<&2, A>}
259
260def Deque.lemma.reverse_go(A, xs, acc):
261 match xs:
262 case Nil{}:
263 {==}
264 case +h <> +t:
265 %Deque.lemma.reverse_go(A, t, [h]) : {List.append(&2, A, _, acc)
266 == List.reverse.go(&2, A, t, h <> acc) : List<&2, A>}
267 %Deque.lemma.reverse_go(A, t, h <> acc) : {List.append(&2, A,
268 List.append(&2, A, List.reverse.go(&2, A, t, Nil{}), [h]), acc)
269 == _ : List<&2, A>}
270 Deque.lemma.append_assoc(A, List.reverse.go(&2, A, t, Nil{}), [h], acc)
271
272# LAW: push_back puts the element at the end of the list
273law Deque.to_list.push_back:
274 for -A: Data
275 for -x: A
276 for d: Deque<&2, A>
277 {Deque.to_list(&2, A, Deque.push_back(&2, A, x, d))
278 == List.append(&2, A, Deque.to_list(&2, A, d), [x]) : List<&2, A>}
279
280def Deque.to_list.push_back(A, x, d):
281 match d:
282 case Deq{+f, +b}:
283 %Deque.lemma.reverse_go(A, b, [x]) : {List.append(&2, A, f, _)
284 == List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, b)),
285 [x]) : List<&2, A>}
286 %Deque.lemma.append_assoc(A, f, List.reverse(&2, A, b), [x]) : {_
287 == List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, b)),
288 [x]) : List<&2, A>}
289 {==}