File : a-cfinve.adb
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT LIBRARY COMPONENTS --
4 -- --
5 -- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
10 -- --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. --
17 -- --
18 -- --
19 -- --
20 -- --
21 -- --
22 -- You should have received a copy of the GNU General Public License and --
23 -- a copy of the GCC Runtime Library Exception along with this program; --
24 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
25 -- <http://www.gnu.org/licenses/>. --
26 ------------------------------------------------------------------------------
27
28 package body Ada.Containers.Formal_Indefinite_Vectors with
29 SPARK_Mode => Off
30 is
31
32 function H (New_Item : Element_Type) return Holder renames To_Holder;
33 function E (Container : Holder) return Element_Type renames Get;
34
35 ---------
36 -- "=" --
37 ---------
38
39 function "=" (Left, Right : Vector) return Boolean is
40 (Left.V = Right.V);
41
42 ------------
43 -- Append --
44 ------------
45
46 procedure Append (Container : in out Vector; New_Item : Vector) is
47 begin
48 Append (Container.V, New_Item.V);
49 end Append;
50
51 procedure Append
52 (Container : in out Vector;
53 New_Item : Element_Type)
54 is
55 begin
56 Append (Container.V, H (New_Item));
57 end Append;
58
59 ------------
60 -- Assign --
61 ------------
62
63 procedure Assign (Target : in out Vector; Source : Vector) is
64 begin
65 Assign (Target.V, Source.V);
66 end Assign;
67
68 --------------
69 -- Capacity --
70 --------------
71
72 function Capacity (Container : Vector) return Capacity_Range is
73 (Capacity (Container.V));
74
75 -----------
76 -- Clear --
77 -----------
78
79 procedure Clear (Container : in out Vector) is
80 begin
81 Clear (Container.V);
82 end Clear;
83
84 --------------
85 -- Contains --
86 --------------
87
88 function Contains
89 (Container : Vector;
90 Item : Element_Type) return Boolean
91 is
92 (Contains (Container.V, H (Item)));
93
94 ----------
95 -- Copy --
96 ----------
97
98 function Copy
99 (Source : Vector;
100 Capacity : Capacity_Range := 0) return Vector
101 is
102 ((if Capacity = 0 then Length (Source) else Capacity),
103 V => Copy (Source.V, Capacity));
104
105 ---------------------
106 -- Current_To_Last --
107 ---------------------
108
109 function Current_To_Last
110 (Container : Vector;
111 Current : Index_Type) return Vector is
112 begin
113 return (Length (Container), Current_To_Last (Container.V, Current));
114 end Current_To_Last;
115
116 -----------------
117 -- Delete_Last --
118 -----------------
119
120 procedure Delete_Last
121 (Container : in out Vector)
122 is
123 begin
124 Delete_Last (Container.V);
125 end Delete_Last;
126
127 -------------
128 -- Element --
129 -------------
130
131 function Element
132 (Container : Vector;
133 Index : Index_Type) return Element_Type is
134 (E (Element (Container.V, Index)));
135
136 ----------------
137 -- Find_Index --
138 ----------------
139
140 function Find_Index
141 (Container : Vector;
142 Item : Element_Type;
143 Index : Index_Type := Index_Type'First) return Extended_Index
144 is
145 (Find_Index (Container.V, H (Item), Index));
146
147 -------------------
148 -- First_Element --
149 -------------------
150
151 function First_Element (Container : Vector) return Element_Type is
152 (E (First_Element (Container.V)));
153
154 -----------------
155 -- First_Index --
156 -----------------
157
158 function First_Index (Container : Vector) return Index_Type is
159 (First_Index (Container.V));
160
161 -----------------------
162 -- First_To_Previous --
163 -----------------------
164
165 function First_To_Previous
166 (Container : Vector;
167 Current : Index_Type) return Vector is
168 begin
169 return (Length (Container), First_To_Previous (Container.V, Current));
170 end First_To_Previous;
171
172 ---------------------
173 -- Generic_Sorting --
174 ---------------------
175
176 package body Generic_Sorting with SPARK_Mode => Off is
177
178 function "<" (X, Y : Holder) return Boolean is (E (X) < E (Y));
179 package Def_Sorting is new Def.Generic_Sorting ("<");
180 use Def_Sorting;
181
182 ---------------
183 -- Is_Sorted --
184 ---------------
185
186 function Is_Sorted (Container : Vector) return Boolean is
187 (Is_Sorted (Container.V));
188
189 ----------
190 -- Sort --
191 ----------
192
193 procedure Sort (Container : in out Vector) is
194 begin
195 Sort (Container.V);
196 end Sort;
197
198 end Generic_Sorting;
199
200 -----------------
201 -- Has_Element --
202 -----------------
203
204 function Has_Element
205 (Container : Vector;
206 Position : Extended_Index) return Boolean
207 is
208 (Has_Element (Container.V, Position));
209
210 --------------
211 -- Is_Empty --
212 --------------
213
214 function Is_Empty (Container : Vector) return Boolean is
215 (Is_Empty (Container.V));
216
217 ------------------
218 -- Last_Element --
219 ------------------
220
221 function Last_Element (Container : Vector) return Element_Type is
222 (E (Last_Element (Container.V)));
223
224 ----------------
225 -- Last_Index --
226 ----------------
227
228 function Last_Index (Container : Vector) return Extended_Index is
229 (Last_Index (Container.V));
230
231 ------------
232 -- Length --
233 ------------
234
235 function Length (Container : Vector) return Capacity_Range is
236 (Length (Container.V));
237
238 ---------------------
239 -- Replace_Element --
240 ---------------------
241
242 procedure Replace_Element
243 (Container : in out Vector;
244 Index : Index_Type;
245 New_Item : Element_Type)
246 is
247 begin
248 Replace_Element (Container.V, Index, H (New_Item));
249 end Replace_Element;
250
251 ----------------------
252 -- Reserve_Capacity --
253 ----------------------
254
255 procedure Reserve_Capacity
256 (Container : in out Vector;
257 Capacity : Capacity_Range)
258 is
259 begin
260 Reserve_Capacity (Container.V, Capacity);
261 end Reserve_Capacity;
262
263 ----------------------
264 -- Reverse_Elements --
265 ----------------------
266
267 procedure Reverse_Elements (Container : in out Vector) is
268 begin
269 Reverse_Elements (Container.V);
270 end Reverse_Elements;
271
272 ------------------------
273 -- Reverse_Find_Index --
274 ------------------------
275
276 function Reverse_Find_Index
277 (Container : Vector;
278 Item : Element_Type;
279 Index : Index_Type := Index_Type'Last) return Extended_Index
280 is
281 (Reverse_Find_Index (Container.V, H (Item), Index));
282
283 ----------
284 -- Swap --
285 ----------
286
287 procedure Swap (Container : in out Vector; I, J : Index_Type) is
288 begin
289 Swap (Container.V, I, J);
290 end Swap;
291
292 ---------------
293 -- To_Vector --
294 ---------------
295
296 function To_Vector
297 (New_Item : Element_Type;
298 Length : Capacity_Range) return Vector
299 is
300 begin
301 return (Length, To_Vector (H (New_Item), Length));
302 end To_Vector;
303
304 end Ada.Containers.Formal_Indefinite_Vectors;