src/containers/deque.bend
bend-collections-laws-containers@1.0.0.0 · 167 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/types/deque.bend as E
3
4# Two-list deque: logical order is front ++ reverse(back).
5# Rebalance only when the requested side is empty, moving half the other
6# side. End operations are amortized O(1) along a consumed state history;
7# a rebalance is O(n). to_list is O(n). No arrays, handles or DLL storage.
8type Deque<-T: Data> is Type:
9 DE{front: List<&2, T>, back: List<&2, T>, nf: Nat, nb: Nat}
10
11def new(~T: Data) -> Deque<T>:
12 DE{Nil{}, Nil{}, 0n, 0n}
13
14def length(~T: Data, d: Deque<T>) -> Deque<T> & Nat:
15 DE{f, b, +nf, +nb} = d
16 (DE{f, b, nf, nb}, Nat.add(nf, nb))
17
18def push_front(~T: Data, d: Deque<T>, x: T) -> Deque<T>:
19 DE{f, b, nf, nb} = d
20 DE{Con{x, f}, b, 1n+nf, nb}
21
22def push_back(~T: Data, d: Deque<T>, x: T) -> Deque<T>:
23 DE{f, b, nf, nb} = d
24 DE{f, Con{x, b}, nf, 1n+nb}
25
26# One split traversal; keep the near half, reverse the far half.
27def split_cons(~T: Data, x: T, r: List<&2, T> & List<&2, T>) -> List<&2, T> & List<&2, T>:
28 (keep, moved) = r
29 (Con{x, keep}, moved)
30
31def split(~T: Data, n: Nat, xs: List<&2, T>) -> List<&2, T> & List<&2, T>:
32 match n xs:
33 case 0n ys:
34 (Nil{}, List.reverse(&2, T, ys))
35 case 1n+p Nil{}:
36 (Nil{}, Nil{})
37 case 1n+p Con{x, tail}:
38 split_cons(~T, x, split(~T, p, tail))
39
40def front_split(~T: Data, +n: Nat, +half: Nat, r: List<&2, T> & List<&2, T>) -> Deque<T>:
41 (keep, moved) = r
42 DE{moved, keep, Nat.sub(n, half), half}
43
44def back_split(~T: Data, +n: Nat, +half: Nat, r: List<&2, T> & List<&2, T>) -> Deque<T>:
45 (keep, moved) = r
46 DE{keep, moved, half, Nat.sub(n, half)}
47
48def move_front(~T: Data, b: List<&2, T>, +n: Nat, +half: Nat) -> Deque<T>:
49 front_split(~T, n, half, split(~T, half, b))
50
51def move_back(~T: Data, f: List<&2, T>, +n: Nat, +half: Nat) -> Deque<T>:
52 back_split(~T, n, half, split(~T, half, f))
53
54def ready_front(~T: Data, d: Deque<T>) -> Deque<T>:
55 match d:
56 case DE{Nil{}, b, nf, +nb}:
57 move_front(~T, b, nb, Nat.div(nb, 2n))
58 case DE{Con{x, f}, b, nf, nb}:
59 DE{Con{x, f}, b, nf, nb}
60
61def ready_back(~T: Data, d: Deque<T>) -> Deque<T>:
62 match d:
63 case DE{f, Nil{}, +nf, nb}:
64 move_back(~T, f, nf, Nat.div(nf, 2n))
65 case DE{f, Con{x, b}, nf, nb}:
66 DE{f, Con{x, b}, nf, nb}
67
68def pop_front_ready(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
69 match d:
70 case DE{Nil{}, b, nf, nb}:
71 (DE{Nil{}, b, nf, nb}, Fail{E.EmptyDeque{}})
72 case DE{Con{x, f}, b, nf, nb}:
73 (DE{f, b, Nat.sub(nf, 1n), nb}, Done{x})
74
75def pop_back_ready(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
76 match d:
77 case DE{f, Nil{}, nf, nb}:
78 (DE{f, Nil{}, nf, nb}, Fail{E.EmptyDeque{}})
79 case DE{f, Con{x, b}, nf, nb}:
80 (DE{f, b, nf, Nat.sub(nb, 1n)}, Done{x})
81
82def peek_front_ready(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
83 match d:
84 case DE{Nil{}, b, nf, nb}:
85 (DE{Nil{}, b, nf, nb}, Fail{E.EmptyDeque{}})
86 case DE{Con{+x, f}, b, nf, nb}:
87 (DE{Con{x, f}, b, nf, nb}, Done{x})
88
89def peek_back_ready(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
90 match d:
91 case DE{f, Nil{}, nf, nb}:
92 (DE{f, Nil{}, nf, nb}, Fail{E.EmptyDeque{}})
93 case DE{f, Con{+x, b}, nf, nb}:
94 (DE{f, Con{x, b}, nf, nb}, Done{x})
95
96def pop_front(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
97 pop_front_ready(~T, ready_front(~T, d))
98
99def pop_back(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
100 pop_back_ready(~T, ready_back(~T, d))
101
102def peek_front(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
103 peek_front_ready(~T, ready_front(~T, d))
104
105def peek_back(~T: Data, d: Deque<T>) -> Deque<T> & Result<&2, &2, E.Error, T>:
106 peek_back_ready(~T, ready_back(~T, d))
107
108def to_list(~T: Data, d: Deque<T>) -> Deque<T> & List<&2, T>:
109 DE{+f, +b, nf, nb} = d
110 (DE{f, b, nf, nb}, List.append(&2, T, f, List.reverse(&2, T, b)))
111
112# ---- operation traces ----
113
114def obs_nat(~T: Data, r: Deque<T> & Nat) -> Deque<T> & E.Obs<T>:
115 (d, n) = r
116 (d, E.ONat{n})
117
118def obs_item(~T: Data, r: Deque<T> & Result<&2, &2, E.Error, T>) -> Deque<T> & E.Obs<T>:
119 (d, x) = r
120 (d, E.OItem{x})
121
122def obs_list(~T: Data, r: Deque<T> & List<&2, T>) -> Deque<T> & E.Obs<T>:
123 (d, xs) = r
124 (d, E.OList{xs})
125
126def step(~T: Data, d: Deque<T>, op: E.Op<T>) -> Deque<T> & E.Obs<T>:
127 match op:
128 case E.Length{}:
129 obs_nat(~T, length(~T, d))
130 case E.PushFront{+x}:
131 (push_front(~T, d, x), E.OUnit{})
132 case E.PushBack{+x}:
133 (push_back(~T, d, x), E.OUnit{})
134 case E.PopFront{}:
135 obs_item(~T, pop_front(~T, d))
136 case E.PopBack{}:
137 obs_item(~T, pop_back(~T, d))
138 case E.PeekFront{}:
139 obs_item(~T, peek_front(~T, d))
140 case E.PeekBack{}:
141 obs_item(~T, peek_back(~T, d))
142 case E.ToList{}:
143 obs_list(~T, to_list(~T, d))
144
145def record(~T: Data, acc: List<&2, E.Obs<T>>, r: Deque<T> & E.Obs<T>) -> Deque<T> & List<&2, E.Obs<T>>:
146 (d, o) = r
147 (d, Con{o, acc})
148
149def step_acc(~T: Data, op: E.Op<T>, st: Deque<T> & List<&2, E.Obs<T>>) -> Deque<T> & List<&2, E.Obs<T>>:
150 (d, acc) = st
151 record(~T, acc, step(~T, d, op))
152
153# Runs ops left to right; observations are accumulated newest-first.
154def run_acc(~T: Data, ops: List<&2, E.Op<T>>, st: Deque<T> & List<&2, E.Obs<T>>) -> Deque<T> & List<&2, E.Obs<T>>:
155 match ops:
156 case Nil{}:
157 st
158 case Con{op, rest}:
159 run_acc(~T, rest, step_acc(~T, op, st))
160
161def finish(~T: Data, st: Deque<T> & List<&2, E.Obs<T>>) -> Deque<T> & List<&2, E.Obs<T>>:
162 (d, acc) = st
163 (d, List.reverse(&2, E.Obs<T>, acc))
164
165# Final state and the observation of every operation, in order.
166def run(~T: Data, ops: List<&2, E.Op<T>>, d: Deque<T>) -> Deque<T> & List<&2, E.Obs<T>>:
167 finish(~T, run_acc(~T, ops, (d, Nil{})))