1	import Base
2	import ../lib/common.bend as C
3	import ../../src/containers/types/deque.bend as E
4	import ../lib/sequence.bend as V
5	
6	# Independent model: a deque is the finite sequence of its elements, front
7	# first. Nothing here refers to the two-list representation.
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.EmptyDeque{}}
13	    case Some{v}:
14	      Done{v}
15	
16	def pop_front(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>:
17	  match xs:
18	    case Nil{}:
19	      (Nil{}, E.OItem{Fail{E.EmptyDeque{}}})
20	    case Con{h, t}:
21	      (t, E.OItem{Done{h}})
22	
23	def pop_back(-T: Data, xs: List<&2, T>) -> List<&2, T> & E.Obs<T>:
24	  match xs:
25	    case Nil{}:
26	      (Nil{}, E.OItem{Fail{E.EmptyDeque{}}})
27	    case Con{+h, +t}:
28	      (C.init(T, Con{h, t}), E.OItem{item(T, C.last(T, Con{h, t}))})
29	
30	def step(-T: Data, +xs: List<&2, T>, op: E.Op<T>) -> List<&2, T> & E.Obs<T>:
31	  match op:
32	    case E.Length{}:
33	      (xs, E.ONat{C.length(T, xs)})
34	    case E.PushFront{x}:
35	      (Con{x, xs}, E.OUnit{})
36	    case E.PushBack{x}:
37	      (C.snoc(T, xs, x), E.OUnit{})
38	    case E.PopFront{}:
39	      pop_front(T, xs)
40	    case E.PopBack{}:
41	      pop_back(T, xs)
42	    case E.PeekFront{}:
43	      (xs, E.OItem{item(T, C.head(T, xs))})
44	    case E.PeekBack{}:
45	      (xs, E.OItem{item(T, C.last(T, xs))})
46	    case E.ToList{}:
47	      (xs, E.OList{xs})
48	
49	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>>:
50	  (m, os) = r
51	  (m, Con{o, os})
52	
53	def run(-T: Data, ops: List<&2, E.Op<T>>, +xs: List<&2, T>) -> List<&2, T> & List<&2, E.Obs<T>>:
54	  match ops:
55	    case Nil{}:
56	      (xs, Nil{})
57	    case Con{+op, rest}:
58	      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))))
59	
60	# ---- contract (SPARK formal containers) ----
61	# Each `<Subprogram>.<clause>` definition below states one Post clause of
62	# that SPARK subprogram, as a proposition on this model; the table names the
63	# clauses. proofs/containers/deque/ proves every clause under its clause name,
64	# and its `impl` lemma carries them to the implementation.
65	#
66	# Contracts of the deque in the style of SPARK's formal vectors
67	# (SPARKlib src/spark-containers-formal-vectors.ads, AdaCore/SPARKlib
68	# 46ec319; model predicates in spec/lib/sequence.bend). The model is the
69	# sequence front first. Each lemma is one Post clause of step; `impl`
70	# (via P.step_ok) carries every clause to the implementation: DQ.step on
71	# the deque of a shadow lands on the deque of a shadow whose model
72	# satisfies it.
73	#
74	#   SPARK subprogram (.ads line)   ours        clauses
75	#   Length (284)                   length      length_result, length_frame
76	#   Empty_Vector (292)             new         new_empty, new_impl
77	#   Prepend (624)                  push_front  push_front_length, push_front_first, push_front_shifted
78	#   Append (706)                   push_back   push_back_length, push_back_prefix, push_back_element
79	#   Delete_First (825)             pop_front   pop_front_length, pop_front_shifted,
80	#                                              pop_front_result, pop_front_empty
81	#   Delete_Last (866)              pop_back    pop_back_length, pop_back_prefix,
82	#                                              pop_back_result, pop_back_empty
83	#   First_Element (913)            peek_front  peek_front_first, peek_front_frame, peek_front_empty
84	#   Last_Element (923)             peek_back   peek_back_last, peek_back_frame, peek_back_empty
85	#   iteration (Iter_Model, 1193)   to_list     to_list_model, to_list_frame
86	#   implementation                 DQ.step     impl
87	# Not in this API: Capacity/Reserve_Capacity (unbounded), Is_Empty, Clear,
88	# "=", To_Vector, Assign/Copy/Move, Element at an index, Replace_Element,
89	# Reference, Insert*, Prepend/Append with Count or a vector, Delete (at an
90	# index or a count), Reverse_Elements, Swap, Find_Index, Reverse_Find_Index,
91	# Contains, Has_Element. SPARK's Pre (not Is_Empty) is a defensive check:
92	# on an empty deque pops and peeks return EmptyDeque and change nothing.
93	
94	def nx(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> List<&2, T>:
95	  Pair.fst(List<&2, T>, E.Obs<T>, step(T, xs, op))
96	
97	def ob(-T: Data, +xs: List<&2, T>, +op: E.Op<T>) -> E.Obs<T>:
98	  Pair.snd(List<&2, T>, E.Obs<T>, step(T, xs, op))
99	
100	# Length (284)
101	def Length.length_result(-T: Data, +xs: List<&2, T>) -> Type:
102	  {ob(T, xs, E.Length{}) == E.ONat{C.length(T, xs)} : E.Obs<T>}
103	
104	# Length (284)
105	def Length.length_frame(-T: Data, +xs: List<&2, T>) -> Type:
106	  {nx(T, xs, E.Length{}) == xs : List<&2, T>}
107	
108	# iteration (Iter_Model, 1193)
109	def Iteration.to_list_model(-T: Data, +xs: List<&2, T>) -> Type:
110	  {ob(T, xs, E.ToList{}) == E.OList{xs} : E.Obs<T>}
111	
112	# iteration (Iter_Model, 1193)
113	def Iteration.to_list_frame(-T: Data, +xs: List<&2, T>) -> Type:
114	  {nx(T, xs, E.ToList{}) == xs : List<&2, T>}
115	
116	# Prepend (624)
117	def Prepend.push_front_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
118	  {C.length(T, nx(T, xs, E.PushFront{v})) == 1n+C.length(T, xs) : Nat}
119	
120	# Prepend (624)
121	def Prepend.push_front_first(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
122	  {C.nth(T, nx(T, xs, E.PushFront{v}), 0n) == Some{v} : Maybe<&2, T>}
123	
124	# Prepend (624)
125	def Prepend.push_front_shifted(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
126	  V.RangeShifted(T, xs, nx(T, xs, E.PushFront{v}), 0n, C.length(T, xs), 1n)
127	
128	# Append (706)
129	def Append.push_back_length(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
130	  {C.length(T, nx(T, xs, E.PushBack{v})) == 1n+C.length(T, xs) : Nat}
131	
132	# Append (706)
133	def Append.push_back_prefix(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
134	  V.EqualPrefix(T, xs, nx(T, xs, E.PushBack{v}))
135	
136	# Append (706)
137	def Append.push_back_element(-T: Data, +xs: List<&2, T>, +v: T) -> Type:
138	  {C.nth(T, nx(T, xs, E.PushBack{v}), C.length(T, xs)) == Some{v} : Maybe<&2, T>}
139	
140	# Delete_First (825)
141	def Delete_First.pop_front_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
142	  {1n+C.length(T, nx(T, Con{h, t}, E.PopFront{})) == C.length(T, Con{h, t}) : Nat}
143	
144	# Delete_First (825)
145	def Delete_First.pop_front_shifted(-T: Data, +h: T, +t: List<&2, T>) -> Type:
146	  V.RangeShifted(T, nx(T, Con{h, t}, E.PopFront{}), Con{h, t}, 0n, C.length(T, nx(T, Con{h, t}, E.PopFront{})), 1n)
147	
148	# Delete_First (825)
149	def Delete_First.pop_front_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
150	  {ob(T, Con{h, t}, E.PopFront{}) == E.OItem{Done{h}} : E.Obs<T>}
151	
152	# Delete_First (825)
153	def Delete_First.pop_front_empty(-T: Data) -> Type:
154	  {step(T, Nil{}, E.PopFront{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}
155	
156	# Delete_Last (866)
157	def Delete_Last.pop_back_length(-T: Data, +h: T, +t: List<&2, T>) -> Type:
158	  {C.length(T, nx(T, Con{h, t}, E.PopBack{})) == C.length(T, t) : Nat}
159	
160	# Delete_Last (866)
161	def Delete_Last.pop_back_prefix(-T: Data, +h: T, +t: List<&2, T>) -> Type:
162	  V.EqualPrefix(T, nx(T, Con{h, t}, E.PopBack{}), Con{h, t})
163	
164	# Delete_Last (866)
165	def Delete_Last.pop_back_result(-T: Data, +h: T, +t: List<&2, T>) -> Type:
166	  {ob(T, Con{h, t}, E.PopBack{}) == E.OItem{item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
167	
168	# Delete_Last (866)
169	def Delete_Last.pop_back_empty(-T: Data) -> Type:
170	  {step(T, Nil{}, E.PopBack{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}
171	
172	# First_Element (913)
173	def First_Element.peek_front_first(-T: Data, +h: T, +t: List<&2, T>) -> Type:
174	  {ob(T, Con{h, t}, E.PeekFront{}) == E.OItem{Done{h}} : E.Obs<T>} & {C.nth(T, Con{h, t}, 0n) == Some{h} : Maybe<&2, T>}
175	
176	# First_Element (913)
177	def First_Element.peek_front_frame(-T: Data, +xs: List<&2, T>) -> Type:
178	  {nx(T, xs, E.PeekFront{}) == xs : List<&2, T>}
179	
180	# First_Element (913)
181	def First_Element.peek_front_empty(-T: Data) -> Type:
182	  {step(T, Nil{}, E.PeekFront{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}
183	
184	# Last_Element (923)
185	def Last_Element.peek_back_last(-T: Data, +h: T, +t: List<&2, T>) -> Type:
186	  {ob(T, Con{h, t}, E.PeekBack{}) == E.OItem{item(T, V.last_elem(T, Con{h, t}))} : E.Obs<T>}
187	
188	# Last_Element (923)
189	def Last_Element.peek_back_frame(-T: Data, +xs: List<&2, T>) -> Type:
190	  {nx(T, xs, E.PeekBack{}) == xs : List<&2, T>}
191	
192	# Last_Element (923)
193	def Last_Element.peek_back_empty(-T: Data) -> Type:
194	  {step(T, Nil{}, E.PeekBack{}) == (Nil{}, E.OItem{Fail{E.EmptyDeque{}}}) : List<&2, T> & E.Obs<T>}