1	import Base
2	import ./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.
8	type Deque<-T: Data> is Type:
9	  DE{front: List<&2, T>, back: List<&2, T>, nf: Nat, nb: Nat}
10	
11	def new(~T: Data) -> Deque<T>:
12	  DE{Nil{}, Nil{}, 0n, 0n}
13	
14	def 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	
18	def 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	
22	def 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.
27	def 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	
31	def 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	
40	def 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	
44	def 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	
48	def 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	
51	def 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	
54	def 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	
61	def 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	
68	def 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	
75	def 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	
82	def 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	
89	def 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	
96	def 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	
99	def 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	
102	def 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	
105	def 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	
108	def 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	
114	def obs_nat(~T: Data, r: Deque<T> & Nat) -> Deque<T> & E.Obs<T>:
115	  (d, n) = r
116	  (d, E.ONat{n})
117	
118	def 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	
122	def 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	
126	def 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	
145	def 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	
149	def 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.
154	def 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	
161	def 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.
166	def 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{})))