1	import Base
2	import ../../../src/containers/priority_queue.bend as P2
3	import ../../../src/containers/binary_heap.bend as K2
4	import ../../../src/containers/types/binary_heap.bend as E2
5	import ../../../spec/containers/priority_queue.bend as S
6	import ../../../spec/containers/binary_heap.bend as HS
7	import ../../../spec/lib/order.bend as SO
8	import ../binary_heap/proof.bend as UP
9	
10	# src/containers/priority_queue.bend: a binary heap behind the queue interface (put = push, get = pop, qsize = length).
11	
12	def priority_queue_put(q: K2.Heap<U32>, +v: U32) -> {P2.put(~U32, ~U32.cmp, q, v) == K2.push(~U32, ~U32.cmp, q, v) : K2.Heap<U32>}:
13	  {==}
14	
15	def priority_queue_get(q: K2.Heap<U32>) -> {P2.get(~U32, ~U32.cmp, q) == K2.pop(~U32, ~U32.cmp, q) : K2.Heap<U32> & Result<&2, &2, E2.Error, U32>}:
16	  {==}
17	
18	def priority_queue_qsize(q: K2.Heap<U32>) -> {P2.qsize(~U32, q) == K2.length(~U32, q) : K2.Heap<U32> & Nat}:
19	  {==}
20	
21	# ==== the contract of priority_queue (stated in spec/containers/priority_queue.bend) ====================
22	
23	def new_is(~A: Data) -> {P2.new(~A) == K2.new(~A) : K2.Heap<A>}:
24	  {==}
25	
26	def qsize_is(~A: Data, h: K2.Heap<A>) -> {P2.qsize(~A, h) == K2.length(~A, h) : K2.Heap<A> & Nat}:
27	  {==}
28	
29	def put_is(~A: Data, ~cmp: A -> A -> Cmp, h: K2.Heap<A>, x: A) -> {P2.put(~A, ~cmp, h, x) == K2.push(~A, ~cmp, h, x) : K2.Heap<A>}:
30	  {==}
31	
32	def peek_is(~A: Data, h: K2.Heap<A>) -> {P2.peek(~A, h) == K2.peek(~A, h) : K2.Heap<A> & Result<&2, &2, E2.Error, A>}:
33	  {==}
34	
35	def get_is(~A: Data, ~cmp: A -> A -> Cmp, h: K2.Heap<A>) -> {P2.get(~A, ~cmp, h) == K2.pop(~A, ~cmp, h) : K2.Heap<A> & Result<&2, &2, E2.Error, A>}:
36	  {==}
37	
38	def from_list_is(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> {P2.from_list(~A, ~cmp, xs) == K2.from_list(~A, ~cmp, xs) : K2.Heap<A>}:
39	  {==}
40	
41	def to_sorted_list_is(~A: Data, ~cmp: A -> A -> Cmp, h: K2.Heap<A>) -> {P2.to_sorted_list(~A, ~cmp, h) == K2.to_sorted_list(~A, ~cmp, h) : K2.Heap<A> & List<&2, A>}:
42	  {==}
43	
44	# ---- the binary_heap's contract, carried: every clause is proved by the binary_heap ----
45	
46	def length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_result(~A, ~cmp, xs):
47	  UP.length_result(~A, ~cmp, xs)
48	
49	def length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Length.length_frame(~A, ~cmp, xs):
50	  UP.length_frame(~A, ~cmp, xs)
51	
52	def push_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +x: A) -> S.Insert.push_length(~A, ~cmp, xs, x):
53	  UP.push_length(~A, ~cmp, xs, x)
54	
55	def push_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A) -> S.Insert.push_bag(~A, ~cmp, ~o, xs, x):
56	  UP.push_bag(~A, ~cmp, ~o, xs, x)
57	
58	def push_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A, +hs: {HS.sorted(~A, ~cmp, xs) == True{} : Bool}) -> S.Insert.push_sorted(~A, ~cmp, ~o, xs, x, hs):
59	  UP.push_sorted(~A, ~cmp, ~o, xs, x, hs)
60	
61	def peek_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.First_Element.peek_min(~A, ~cmp, h, t, hs):
62	  UP.peek_min(~A, ~cmp, h, t, hs)
63	
64	def peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.First_Element.peek_frame(~A, ~cmp, xs):
65	  UP.peek_frame(~A, ~cmp, xs)
66	
67	def peek_empty(~A: Data, ~cmp: A -> A -> Cmp) -> S.First_Element.peek_empty(~A, ~cmp):
68	  UP.peek_empty(~A, ~cmp)
69	
70	def pop_length(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> S.Delete_First.pop_length(~A, ~cmp, h, t):
71	  UP.pop_length(~A, ~cmp, h, t)
72	
73	def pop_result(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> S.Delete_First.pop_result(~A, ~cmp, h, t):
74	  UP.pop_result(~A, ~cmp, h, t)
75	
76	def pop_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.Delete_First.pop_min(~A, ~cmp, h, t, hs):
77	  UP.pop_min(~A, ~cmp, h, t, hs)
78	
79	def pop_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> S.Delete_First.pop_bag(~A, ~cmp, ~o, h, t, hs):
80	  UP.pop_bag(~A, ~cmp, ~o, h, t, hs)
81	
82	def pop_empty(~A: Data, ~cmp: A -> A -> Cmp) -> S.Delete_First.pop_empty(~A, ~cmp):
83	  UP.pop_empty(~A, ~cmp)
84	
85	def from_list_model(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> S.To_Set.from_list_model(~A, ~cmp, xs, ys):
86	  UP.from_list_model(~A, ~cmp, xs, ys)
87	
88	def from_list_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> S.To_Set.from_list_length(~A, ~cmp, xs, ys):
89	  UP.from_list_length(~A, ~cmp, xs, ys)
90	
91	def from_list_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +ys: List<&2, A>) -> S.To_Set.from_list_sorted(~A, ~cmp, ~o, xs, ys):
92	  UP.from_list_sorted(~A, ~cmp, ~o, xs, ys)
93	
94	def to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_result(~A, ~cmp, xs):
95	  UP.to_sorted_result(~A, ~cmp, xs)
96	
97	def to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> S.Elements.to_sorted_frame(~A, ~cmp, xs):
98	  UP.to_sorted_frame(~A, ~cmp, xs)
99