1	import Base
2	import ./types/queue.bend as E
3	
4	# Two-list FIFO queue: front ++ reverse(back). Reverse back only when front
5	# is empty. Enqueue/dequeue/peek are amortized O(1) on consumed histories.
6	# length is cached; to_list is O(n). Independent of the deque and DLL.
7	type Queue<-T: Data> is Type:
8	  QU{front: List<&2, T>, back: List<&2, T>, count: Nat}
9	
10	def new(~T: Data) -> Queue<T>:
11	  QU{Nil{}, Nil{}, 0n}
12	
13	def length(~T: Data, q: Queue<T>) -> Queue<T> & Nat:
14	  QU{f, b, +n} = q
15	  (QU{f, b, n}, n)
16	
17	def enqueue(~T: Data, q: Queue<T>, x: T) -> Queue<T>:
18	  QU{f, b, n} = q
19	  QU{f, Con{x, b}, 1n+n}
20	
21	def ready(~T: Data, q: Queue<T>) -> Queue<T>:
22	  match q:
23	    case QU{Nil{}, b, n}:
24	      QU{List.reverse(&2, T, b), Nil{}, n}
25	    case QU{Con{x, f}, b, n}:
26	      QU{Con{x, f}, b, n}
27	
28	def dequeue_ready(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
29	  match q:
30	    case QU{Nil{}, b, n}:
31	      (QU{Nil{}, b, n}, Fail{E.EmptyQueue{}})
32	    case QU{Con{x, f}, b, n}:
33	      (QU{f, b, Nat.sub(n, 1n)}, Done{x})
34	
35	def peek_ready(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
36	  match q:
37	    case QU{Nil{}, b, n}:
38	      (QU{Nil{}, b, n}, Fail{E.EmptyQueue{}})
39	    case QU{Con{+x, f}, b, n}:
40	      (QU{Con{x, f}, b, n}, Done{x})
41	
42	def dequeue(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
43	  dequeue_ready(~T, ready(~T, q))
44	
45	def peek(~T: Data, q: Queue<T>) -> Queue<T> & Result<&2, &2, E.Error, T>:
46	  peek_ready(~T, ready(~T, q))
47	
48	def to_list(~T: Data, q: Queue<T>) -> Queue<T> & List<&2, T>:
49	  QU{+f, +b, n} = q
50	  (QU{f, b, n}, List.append(&2, T, f, List.reverse(&2, T, b)))
51	
52	# ---- operation traces ----
53	
54	def obs_nat(~T: Data, r: Queue<T> & Nat) -> Queue<T> & E.Obs<T>:
55	  (q, n) = r
56	  (q, E.ONat{n})
57	
58	def obs_item(~T: Data, r: Queue<T> & Result<&2, &2, E.Error, T>) -> Queue<T> & E.Obs<T>:
59	  (q, x) = r
60	  (q, E.OItem{x})
61	
62	def obs_list(~T: Data, r: Queue<T> & List<&2, T>) -> Queue<T> & E.Obs<T>:
63	  (q, xs) = r
64	  (q, E.OList{xs})
65	
66	def step(~T: Data, q: Queue<T>, op: E.Op<T>) -> Queue<T> & E.Obs<T>:
67	  match op:
68	    case E.Length{}:
69	      obs_nat(~T, length(~T, q))
70	    case E.Enqueue{+x}:
71	      (enqueue(~T, q, x), E.OUnit{})
72	    case E.Dequeue{}:
73	      obs_item(~T, dequeue(~T, q))
74	    case E.Peek{}:
75	      obs_item(~T, peek(~T, q))
76	    case E.ToList{}:
77	      obs_list(~T, to_list(~T, q))
78	
79	def record(~T: Data, acc: List<&2, E.Obs<T>>, r: Queue<T> & E.Obs<T>) -> Queue<T> & List<&2, E.Obs<T>>:
80	  (q, o) = r
81	  (q, Con{o, acc})
82	
83	def step_acc(~T: Data, op: E.Op<T>, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:
84	  (q, acc) = st
85	  record(~T, acc, step(~T, q, op))
86	
87	def run_acc(~T: Data, ops: List<&2, E.Op<T>>, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:
88	  match ops:
89	    case Nil{}:
90	      st
91	    case Con{op, rest}:
92	      run_acc(~T, rest, step_acc(~T, op, st))
93	
94	def finish(~T: Data, st: Queue<T> & List<&2, E.Obs<T>>) -> Queue<T> & List<&2, E.Obs<T>>:
95	  (q, acc) = st
96	  (q, List.reverse(&2, E.Obs<T>, acc))
97	
98	def run(~T: Data, ops: List<&2, E.Op<T>>, q: Queue<T>) -> Queue<T> & List<&2, E.Obs<T>>:
99	  finish(~T, run_acc(~T, ops, (q, Nil{})))