1	import Base
2	import ./list.bend as List
3	
4	# queue.bend: a FIFO queue as two lists, specified by the list it holds.
5	#
6	#   import ./queue.bend as Q
7	#
8	# push conses onto rear; pop takes from front, and when front is empty the
9	# reversed rear becomes the new front. Queue is linear (Type), so each
10	# queue value is used once; then each element is reversed at most once and
11	# every operation costs O(1) on average.
12	#
13	# model(q) is the list q holds. push_model and pop_model state push and
14	# pop in terms of it.
15	
16	type Queue<-A: Data> is Type:
17	  Queue{front: List<&2, A>, rear: List<&2, A>}
18	
19	def empty(-A: Data) -> Queue<A>:
20	  Queue{Nil{}, Nil{}}
21	
22	def model(-A: Data, q: Queue<A>) -> List<&2, A>:
23	  match q:
24	    case Queue{f, r}:
25	      List.append(&2, A, f, List.reverse(&2, A, r))
26	
27	def push(-A: Data, q: Queue<A>, x: A) -> Queue<A>:
28	  match q:
29	    case Queue{f, r}:
30	      Queue{f, x <> r}
31	
32	# front is empty; f is the reversed rear
33	def pop.rot(-A: Data, f: List<&2, A>) -> List.Step<&1, A, Queue<A>>:
34	  match f:
35	    case Nil{}:
36	      List.Stop{}
37	    case h <> t:
38	      List.Next{h, Queue{t, Nil{}}}
39	
40	def pop(-A: Data, q: Queue<A>) -> List.Step<&1, A, Queue<A>>:
41	  match q:
42	    case Queue{Nil{}, r}:
43	      pop.rot(A, List.reverse(&2, A, r))
44	    case Queue{h <> t, r}:
45	      List.Next{h, Queue{t, r}}
46	
47	# pop's result with the remaining queue replaced by its model
48	def pop.model(-A: Data, s: List.Step<&1, A, Queue<A>>) -> List.Step<&2, A, List<&2, A>>:
49	  match s:
50	    case List.Stop{}:
51	      List.Stop{}
52	    case List.Next{x, q}:
53	      List.Next{x, model(A, q)}
54	
55	# push appends x to the model.
56	law push_model:
57	  for -A: Data
58	  for q: Queue<A>
59	  for +x: A
60	  {List.append(&2, A, model(A, q), [x]) == model(A, push(A, q, x)) : List<&2, A>}
61	
62	def push_model(A, q, x):
63	  match q:
64	    case Queue{+f, +r}:
65	      %List.reverse_go(A, r, [x]) : {List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, r)), [x]) == List.append(&2, A, f, _) : List<&2, A>}
66	      Equal.sym(List<&2, A>,
67	        List.append(&2, A, f, List.append(&2, A, List.reverse(&2, A, r), [x])),
68	        List.append(&2, A, List.append(&2, A, f, List.reverse(&2, A, r)), [x]),
69	        List.append_assoc(A, f, List.reverse(&2, A, r), [x]))
70	
71	law pop_model.rot:
72	  for -A: Data
73	  for f: List<&2, A>
74	  {List.uncons(A, f) == pop.model(A, pop.rot(A, f)) : List.Step<&2, A, List<&2, A>>}
75	
76	def pop_model.rot(A, f):
77	  match f:
78	    case Nil{}:
79	      {==}
80	    case h <> t:
81	      %List.append_nil(A, t) : {List.Next{h, t} == List.Next{h, _} : List.Step<&2, A, List<&2, A>>}
82	      {==}
83	
84	# pop returns the model's head and tail.
85	law pop_model:
86	  for -A: Data
87	  for q: Queue<A>
88	  {List.uncons(A, model(A, q)) == pop.model(A, pop(A, q)) : List.Step<&2, A, List<&2, A>>}
89	
90	def pop_model(A, q):
91	  match q:
92	    case Queue{Nil{}, r}:
93	      pop_model.rot(A, List.reverse(&2, A, r))
94	    case Queue{h <> t, r}:
95	      {==}