1	import Base
2	import ../lib/common.bend as C
3	import ../../src/containers/types/queue.bend as E
4	import ../lib/sequence.bend as V
5	
6	# Independent model: a FIFO queue is the sequence of its elements, oldest
7	# first. Enqueue appends at the end; dequeue removes the first element.
8	
9	def item(-T: Data, x: Maybe<&2, T>) -> Result<&2, &2, E.Error, T>:
10	  match x:
11	    case None{}:
12	      Fail{E.EmptyQueue{}}
13	    case Some{v}:
14	      Done{v}
15	
16	def dequeue(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>:
17	  match xs:
18	    case Nil{}:
19	      (Nil{}, E.OItem{Fail{E.EmptyQueue{}}})
20	    case Con{h, t}:
21	      (t, E.OItem{Done{h}})
22	
23	def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>:
24	  match op:
25	    case E.Length{}:
26	      (xs, E.ONat{C.length(T, xs)})
27	    case E.Enqueue{x}:
28	      (C.snoc(T, xs, x), E.OUnit{})
29	    case E.Dequeue{}:
30	      dequeue(T, xs)
31	    case E.Peek{}:
32	      (xs, E.OItem{item(T, C.head(T, xs))})
33	    case E.ToList{}:
34	      (xs, E.OList{xs})
35	
36	def cons_obs(-T: Data, o: E.Obs<T>, r: List<&2, T> & List<&2, E.Obs<T>>) -> List<&2, T> & List<&2, E.Obs<T>>:
37	  (m, os) = r
38	  (m, Con{o, os})
39	
40	def run(-T: Data, ops: List<&2, E.Op<T>>, +xs: List<&2, T>) -> List<&2, T> & List<&2, E.Obs<T>>:
41	  match ops:
42	    case Nil{}:
43	      (xs, Nil{})
44	    case Con{+op, rest}:
45	      cons_obs(T, Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op)), run(T, rest, Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))))
46	
47	# ---- contract (SPARK formal containers) ----
48	# Each `<Subprogram>.<clause>` definition below states one Post clause of
49	# that SPARK subprogram, as a proposition on this model; the table names the
50	# clauses. proofs/containers/queue/ proves every clause under its clause name,
51	# and its `impl` lemma carries them to the implementation.
52	#
53	# Contracts of the FIFO queue in the style of SPARK's formal vectors
54	# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
55	# 46ec319; model predicates in spec/lib/sequence.bend). The model is the
56	# sequence oldest first: enqueue is Append, dequeue is Delete_First, peek
57	# is First_Element. Each lemma is one Post clause of step; `impl` (via
58	# PS.step_ok) carries every clause to the implementation: Q.step on the
59	# queue of a shadow lands on the queue of a shadow whose model satisfies it.
60	#
61	#   SPARK subprogram (.ads line)   ours      clauses
62	#   Length (284)                   length    length_result, length_frame
63	#   Empty_Vector (292)             new       new_empty, new_impl
64	#   Append (706)                   enqueue   enqueue_length, enqueue_prefix, enqueue_element
65	#   Delete_First (825)             dequeue   dequeue_length, dequeue_shifted,
66	#                                            dequeue_result, dequeue_empty
67	#   First_Element (913)            peek      peek_first, peek_frame, peek_empty
68	#   iteration (Iter_Model, 1193)   to_list   to_list_model, to_list_frame
69	#   implementation                 Q.step    impl
70	# Not in this API: Capacity/Reserve_Capacity (unbounded), Is_Empty, Clear,
71	# "=", To_Vector, Assign/Copy/Move, Element at an index, Replace_Element,
72	# Reference, Insert*, Prepend*, Append_Vector/Count, Delete (at an index),
73	# Delete_Last, Last_Element, Reverse_Elements, Swap, Find_Index,
74	# Reverse_Find_Index, Contains, Has_Element. SPARK's Pre (not Is_Empty) is
75	# a defensive check: on an empty queue dequeue and peek return EmptyQueue
76	# and change nothing.
77	
78	def nx(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> List<&2, T>:
79	  Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))
80	
81	def ob(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> E.Obs<T>:
82	  Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op))
83	
84	# Length (284)
85	def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
86	  {ob(T, xs, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}
87	
88	# Length (284)
89	def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
90	  {nx(T, xs, E.Length{}) == xs : List<&2, T>}
91	
92	# iteration (Iter_Model, 1193)
93	def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
94	  {ob(T, xs, E.ToList{}) == E.OList{xs} : E.Obs<T>}
95	
96	# iteration (Iter_Model, 1193)
97	def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
98	  {nx(T, xs, E.ToList{}) == xs : List<&2, T>}
99	
100	# Append (706)
101	def Append.enqueue_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
102	  {C.length(T, nx(T, xs, E.Enqueue{v})) == 1n+C.length(T, xs) : Nat}
103	
104	# Append (706)
105	def Append.enqueue_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
106	  V.EqualPrefix(T, xs, nx(T, xs, E.Enqueue{v}))
107	
108	# Append (706)
109	def Append.enqueue_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
110	  {C.nth(T, nx(T, xs, E.Enqueue{v}), C.length(T, xs)) == Some{v} : Maybe<&2, T>}
111	
112	# Delete_First (825)
113	def Delete_First.dequeue_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
114	  {1n+C.length(T, nx(T, Con{h, t}, E.Dequeue{})) == C.length(T, Con{h, t}) : Nat}
115	
116	# Delete_First (825)
117	def Delete_First.dequeue_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
118	  V.RangeShifted(T, nx(T, Con{h, t}, E.Dequeue{}), Con{h, t}, 0n, C.length(T, nx(T, Con{h, t}, E.Dequeue{})), 1n)
119	
120	# Delete_First (825)
121	def Delete_First.dequeue_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
122	  {ob(T, Con{h, t}, E.Dequeue{}) == E.OItem{Done{h}} : E.Obs<T>}
123	
124	# Delete_First (825)
125	def Delete_First.dequeue_empty(-T: Data) -> Type:
126	  {step(T, Nil{}, E.Dequeue{}) == (Nil{}, E.OItem{Fail{E.EmptyQueue{}}}) : List<&2, T> & E.Obs<T>}
127	
128	# First_Element (913)
129	def First_Element.peek_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
130	  {ob(T, Con{h, t}, E.Peek{}) == E.OItem{Done{h}} : E.Obs<T>} & {C.nth(T, Con{h, t}, 0n) == Some{h} : Maybe<&2, T>}
131	
132	# First_Element (913)
133	def First_Element.peek_frame(-T: Data, +xs: List<&2, T>) -> Type:
134	  {nx(T, xs, E.Peek{}) == xs : List<&2, T>}
135	
136	# First_Element (913)
137	def First_Element.peek_empty(-T: Data) -> Type:
138	  {step(T, Nil{}, E.Peek{}) == (Nil{}, E.OItem{Fail{E.EmptyQueue{}}}) : List<&2, T> & E.Obs<T>}