1	import Base
2	import ../../../src/containers/simple_queue.bend as P1
3	import ../../../src/containers/queue.bend as K1
4	import ../../../src/containers/types/queue.bend as E1
5	import ../../../spec/containers/simple_queue.bend as S
6	import ../queue/proof.bend as UP
7	
8	# src/containers/simple_queue.bend: a FIFO queue behind the queue interface (put = enqueue, get = dequeue, qsize = length).
9	
10	def simple_queue_put(q: K1.Queue<U32>, +v: U32) -> {P1.put(~U32, q, v) == K1.enqueue(~U32, q, v) : K1.Queue<U32>}:
11	  {==}
12	
13	def simple_queue_get(q: K1.Queue<U32>) -> {P1.get(~U32, q) == K1.dequeue(~U32, q) : K1.Queue<U32> & Result<&2, &2, E1.Error, U32>}:
14	  {==}
15	
16	def simple_queue_qsize(q: K1.Queue<U32>) -> {P1.qsize(~U32, q) == K1.length(~U32, q) : K1.Queue<U32> & Nat}:
17	  {==}
18	
19	# ==== the contract of simple_queue (stated in spec/containers/simple_queue.bend) ====================
20	
21	def new_is(~T: Data) -> {P1.new(~T) == K1.new(~T) : K1.Queue<T>}:
22	  {==}
23	
24	def qsize_is(~T: Data, q: K1.Queue<T>) -> {P1.qsize(~T, q) == K1.length(~T, q) : K1.Queue<T> & Nat}:
25	  {==}
26	
27	def put_is(~T: Data, q: K1.Queue<T>, x: T) -> {P1.put(~T, q, x) == K1.enqueue(~T, q, x) : K1.Queue<T>}:
28	  {==}
29	
30	def get_is(~T: Data, q: K1.Queue<T>) -> {P1.get(~T, q) == K1.dequeue(~T, q) : K1.Queue<T> & Result<&2, &2, E1.Error, T>}:
31	  {==}
32	
33	def peek_is(~T: Data, q: K1.Queue<T>) -> {P1.peek(~T, q) == K1.peek(~T, q) : K1.Queue<T> & Result<&2, &2, E1.Error, T>}:
34	  {==}
35	
36	def to_list_is(~T: Data, q: K1.Queue<T>) -> {P1.to_list(~T, q) == K1.to_list(~T, q) : K1.Queue<T> & List<&2, T>}:
37	  {==}
38	
39	# ---- the queue's contract, carried: every clause is proved by the queue ----
40	
41	def length_result(-T: Data, +xs: List<&2, T>) -> S.Length.length_result(T, xs):
42	  UP.length_result(T, xs)
43	
44	def length_frame(-T: Data, +xs: List<&2, T>) -> S.Length.length_frame(T, xs):
45	  UP.length_frame(T, xs)
46	
47	def to_list_model(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_model(T, xs):
48	  UP.to_list_model(T, xs)
49	
50	def to_list_frame(-T: Data, +xs: List<&2, T>) -> S.Iteration.to_list_frame(T, xs):
51	  UP.to_list_frame(T, xs)
52	
53	def enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_length(T, xs, v):
54	  UP.enqueue_length(T, xs, v)
55	
56	def enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_prefix(T, xs, v):
57	  UP.enqueue_prefix(T, xs, v)
58	
59	def enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> S.Append.enqueue_element(T, xs, v):
60	  UP.enqueue_element(T, xs, v)
61	
62	def dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_length(T, h, t):
63	  UP.dequeue_length(T, h, t)
64	
65	def dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_shifted(T, h, t):
66	  UP.dequeue_shifted(T, h, t)
67	
68	def dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> S.Delete_First.dequeue_result(T, h, t):
69	  UP.dequeue_result(T, h, t)
70	
71	def dequeue_empty(-T: Data) -> S.Delete_First.dequeue_empty(T):
72	  UP.dequeue_empty(T)
73	
74	def peek_first(-T: Data, +h: T, +t: List<&2, T>) -> S.First_Element.peek_first(T, h, t):
75	  UP.peek_first(T, h, t)
76	
77	def peek_frame(-T: Data, +xs: List<&2, T>) -> S.First_Element.peek_frame(T, xs):
78	  UP.peek_frame(T, xs)
79	
80	def peek_empty(-T: Data) -> S.First_Element.peek_empty(T):
81	  UP.peek_empty(T)
82