1	import Base
2	import ../lib/order.bend as SO
3	import ./binary_heap.bend as HS
4	
5	# ---- contract (SPARK formal containers) ----
6	# Each `<Subprogram>.<clause>` definition below states one Post clause of
7	# that SPARK subprogram, as a proposition on this model; the table names the
8	# clauses. proofs/containers/priority_queue/ proves every clause under its clause name,
9	# and its `impl` lemma carries them to the implementation.
10	#
11	# The priority queue is the binary heap behind another interface; every one
12	# of its operations is the heap's (for every element type and order), so it
13	# has the heap's SPARK-style multiset contracts,
14	# spec/containers/binary_heap.bend (restated below):
15	#
16	#   contract                 priority_queue   binary_heap      contract lemmas (HC.)
17	#   Empty_Set                new              new              new_empty
18	#   Length                   qsize            length           length_result, length_frame
19	#   Insert (multiplicity)    put              push             push_length, push_bag, push_sorted
20	#   First_Element (minimum)  peek             peek             peek_min, peek_frame, peek_empty
21	#   Delete_First (minimum)   get              pop              pop_length, pop_result, pop_min,
22	#                                                              pop_bag, pop_empty
23	#   To_Set                   from_list        from_list        from_list_model, from_list_length,
24	#                                                              from_list_sorted
25	#   Elements (ordered)       to_sorted_list   to_sorted_list   to_sorted_result, to_sorted_frame
26	#   implementation                                             HC.impl, HC.model_sorted
27	
28	# The model is the binary_heap's (HS.step) and so is every clause:
29	
30	def Length.length_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
31	  HS.Length.length_result(~A, ~cmp, xs)
32	
33	def Length.length_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
34	  HS.Length.length_frame(~A, ~cmp, xs)
35	
36	def Insert.push_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +x: A) -> Type:
37	  HS.Insert.push_length(~A, ~cmp, xs, x)
38	
39	def Insert.push_bag(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +x: A) -> Type:
40	  HS.Insert.push_bag(~A, ~cmp, ~o, xs, x)
41	
42	def Insert.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}) -> Type:
43	  HS.Insert.push_sorted(~A, ~cmp, ~o, xs, x, hs)
44	
45	def First_Element.peek_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
46	  HS.First_Element.peek_min(~A, ~cmp, h, t, hs)
47	
48	def First_Element.peek_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
49	  HS.First_Element.peek_frame(~A, ~cmp, xs)
50	
51	def First_Element.peek_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
52	  HS.First_Element.peek_empty(~A, ~cmp)
53	
54	def Delete_First.pop_length(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:
55	  HS.Delete_First.pop_length(~A, ~cmp, h, t)
56	
57	def Delete_First.pop_result(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>) -> Type:
58	  HS.Delete_First.pop_result(~A, ~cmp, h, t)
59	
60	def Delete_First.pop_min(~A: Data, ~cmp: A -> A -> Cmp, +h: A, +t: List<&2, A>, +hs: {HS.sorted(~A, ~cmp, Con{h, t}) == True{} : Bool}) -> Type:
61	  HS.Delete_First.pop_min(~A, ~cmp, h, t, hs)
62	
63	def Delete_First.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}) -> Type:
64	  HS.Delete_First.pop_bag(~A, ~cmp, ~o, h, t, hs)
65	
66	def Delete_First.pop_empty(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
67	  HS.Delete_First.pop_empty(~A, ~cmp)
68	
69	def To_Set.from_list_model(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
70	  HS.To_Set.from_list_model(~A, ~cmp, xs, ys)
71	
72	def To_Set.from_list_length(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
73	  HS.To_Set.from_list_length(~A, ~cmp, xs, ys)
74	
75	def To_Set.from_list_sorted(~A: Data, ~cmp: A -> A -> Cmp, ~o: SO.Order(~A, ~cmp), +xs: List<&2, A>, +ys: List<&2, A>) -> Type:
76	  HS.To_Set.from_list_sorted(~A, ~cmp, ~o, xs, ys)
77	
78	def Elements.to_sorted_result(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
79	  HS.Elements.to_sorted_result(~A, ~cmp, xs)
80	
81	def Elements.to_sorted_frame(~A: Data, ~cmp: A -> A -> Cmp, +xs: List<&2, A>) -> Type:
82	  HS.Elements.to_sorted_frame(~A, ~cmp, xs)
83