|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS --
|
|
|
6 -- --
|
|
|
7 -- B o d y --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2010-2019, Free Software Foundation, Inc. --
|
|
111
|
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 -- As a special exception under Section 7 of GPL version 3, you are granted --
|
|
|
19 -- additional permissions described in the GCC Runtime Library Exception, --
|
|
|
20 -- version 3.1, as published by the Free Software Foundation. --
|
|
|
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 with Ada.Containers.Generic_Array_Sort;
|
|
|
29 with Ada.Unchecked_Deallocation;
|
|
|
30
|
|
|
31 with System; use type System.Address;
|
|
|
32
|
|
|
33 package body Ada.Containers.Formal_Indefinite_Vectors with
|
|
|
34 SPARK_Mode => Off
|
|
|
35 is
|
|
|
36 function H (New_Item : Element_Type) return Holder renames To_Holder;
|
|
|
37 function E (Container : Holder) return Element_Type renames Get;
|
|
|
38
|
|
|
39 Growth_Factor : constant := 2;
|
|
|
40 -- When growing a container, multiply current capacity by this. Doubling
|
|
|
41 -- leads to amortized linear-time copying.
|
|
|
42
|
|
|
43 type Int is range System.Min_Int .. System.Max_Int;
|
|
|
44
|
|
|
45 procedure Free is
|
|
|
46 new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
|
|
|
47
|
|
|
48 type Maximal_Array_Ptr is access all Elements_Array (Array_Index)
|
|
|
49 with Storage_Size => 0;
|
|
|
50 type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index)
|
|
|
51 with Storage_Size => 0;
|
|
|
52
|
|
|
53 function Elems (Container : in out Vector) return Maximal_Array_Ptr;
|
|
|
54 function Elemsc
|
|
|
55 (Container : Vector) return Maximal_Array_Ptr_Const;
|
|
|
56 -- Returns a pointer to the Elements array currently in use -- either
|
|
|
57 -- Container.Elements_Ptr or a pointer to Container.Elements. We work with
|
|
|
58 -- pointers to a bogus array subtype that is constrained with the maximum
|
|
|
59 -- possible bounds. This means that the pointer is a thin pointer. This is
|
|
|
60 -- necessary because 'Unrestricted_Access doesn't work when it produces
|
|
|
61 -- access-to-unconstrained and is returned from a function.
|
|
|
62 --
|
|
|
63 -- Note that this is dangerous: make sure calls to this use an indexed
|
|
|
64 -- component or slice that is within the bounds 1 .. Length (Container).
|
|
|
65
|
|
|
66 function Get_Element
|
|
|
67 (Container : Vector;
|
|
|
68 Position : Capacity_Range) return Element_Type;
|
|
|
69
|
|
|
70 function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base;
|
|
|
71
|
|
|
72 function Current_Capacity (Container : Vector) return Capacity_Range;
|
|
|
73
|
|
|
74 procedure Insert_Space
|
|
|
75 (Container : in out Vector;
|
|
|
76 Before : Extended_Index;
|
|
|
77 Count : Count_Type := 1);
|
|
|
78
|
|
|
79 ---------
|
|
|
80 -- "=" --
|
|
|
81 ---------
|
|
|
82
|
|
|
83 function "=" (Left : Vector; Right : Vector) return Boolean is
|
|
|
84 begin
|
|
|
85 if Left'Address = Right'Address then
|
|
|
86 return True;
|
|
|
87 end if;
|
|
|
88
|
|
|
89 if Length (Left) /= Length (Right) then
|
|
|
90 return False;
|
|
|
91 end if;
|
|
|
92
|
|
|
93 for J in 1 .. Length (Left) loop
|
|
|
94 if Get_Element (Left, J) /= Get_Element (Right, J) then
|
|
|
95 return False;
|
|
|
96 end if;
|
|
|
97 end loop;
|
|
|
98
|
|
|
99 return True;
|
|
|
100 end "=";
|
|
|
101
|
|
|
102 ------------
|
|
|
103 -- Append --
|
|
|
104 ------------
|
|
|
105
|
|
|
106 procedure Append (Container : in out Vector; New_Item : Vector) is
|
|
|
107 begin
|
|
|
108 if Is_Empty (New_Item) then
|
|
|
109 return;
|
|
|
110 end if;
|
|
|
111
|
|
|
112 if Container.Last >= Index_Type'Last then
|
|
|
113 raise Constraint_Error with "vector is already at its maximum length";
|
|
|
114 end if;
|
|
|
115
|
|
|
116 Insert (Container, Container.Last + 1, New_Item);
|
|
|
117 end Append;
|
|
|
118
|
|
|
119 procedure Append (Container : in out Vector; New_Item : Element_Type) is
|
|
|
120 begin
|
|
|
121 Append (Container, New_Item, 1);
|
|
|
122 end Append;
|
|
|
123
|
|
|
124 procedure Append
|
|
|
125 (Container : in out Vector;
|
|
|
126 New_Item : Element_Type;
|
|
|
127 Count : Count_Type)
|
|
|
128 is
|
|
|
129 begin
|
|
|
130 if Count = 0 then
|
|
|
131 return;
|
|
|
132 end if;
|
|
|
133
|
|
|
134 if Container.Last >= Index_Type'Last then
|
|
|
135 raise Constraint_Error with "vector is already at its maximum length";
|
|
|
136 end if;
|
|
|
137
|
|
|
138 Insert (Container, Container.Last + 1, New_Item, Count);
|
|
|
139 end Append;
|
|
|
140
|
|
|
141 ------------
|
|
|
142 -- Assign --
|
|
|
143 ------------
|
|
|
144
|
|
|
145 procedure Assign (Target : in out Vector; Source : Vector) is
|
|
|
146 LS : constant Capacity_Range := Length (Source);
|
|
|
147
|
|
|
148 begin
|
|
|
149 if Target'Address = Source'Address then
|
|
|
150 return;
|
|
|
151 end if;
|
|
|
152
|
|
|
153 if Bounded and then Target.Capacity < LS then
|
|
|
154 raise Constraint_Error;
|
|
|
155 end if;
|
|
|
156
|
|
|
157 Clear (Target);
|
|
|
158 Append (Target, Source);
|
|
|
159 end Assign;
|
|
|
160
|
|
|
161 --------------
|
|
|
162 -- Capacity --
|
|
|
163 --------------
|
|
|
164
|
|
|
165 function Capacity (Container : Vector) return Capacity_Range is
|
|
|
166 begin
|
|
|
167 return
|
|
|
168 (if Bounded then
|
|
|
169 Container.Capacity
|
|
|
170 else
|
|
|
171 Capacity_Range'Last);
|
|
|
172 end Capacity;
|
|
|
173
|
|
|
174 -----------
|
|
|
175 -- Clear --
|
|
|
176 -----------
|
|
|
177
|
|
|
178 procedure Clear (Container : in out Vector) is
|
|
|
179 begin
|
|
|
180 Container.Last := No_Index;
|
|
|
181
|
|
|
182 -- Free element, note that this is OK if Elements_Ptr is null
|
|
|
183
|
|
|
184 Free (Container.Elements_Ptr);
|
|
|
185 end Clear;
|
|
|
186
|
|
|
187 --------------
|
|
|
188 -- Contains --
|
|
|
189 --------------
|
|
|
190
|
|
|
191 function Contains
|
|
|
192 (Container : Vector;
|
|
|
193 Item : Element_Type) return Boolean
|
|
|
194 is
|
|
|
195 begin
|
|
|
196 return Find_Index (Container, Item) /= No_Index;
|
|
|
197 end Contains;
|
|
|
198
|
|
|
199 ----------
|
|
|
200 -- Copy --
|
|
|
201 ----------
|
|
|
202
|
|
|
203 function Copy
|
|
|
204 (Source : Vector;
|
|
|
205 Capacity : Capacity_Range := 0) return Vector
|
|
|
206 is
|
|
|
207 LS : constant Capacity_Range := Length (Source);
|
|
|
208 C : Capacity_Range;
|
|
|
209
|
|
|
210 begin
|
|
|
211 if Capacity = 0 then
|
|
|
212 C := LS;
|
|
|
213 elsif Capacity >= LS then
|
|
|
214 C := Capacity;
|
|
|
215 else
|
|
|
216 raise Capacity_Error;
|
|
|
217 end if;
|
|
|
218
|
|
|
219 return Target : Vector (C) do
|
|
|
220 Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS);
|
|
|
221 Target.Last := Source.Last;
|
|
|
222 end return;
|
|
|
223 end Copy;
|
|
|
224
|
|
|
225 ----------------------
|
|
|
226 -- Current_Capacity --
|
|
|
227 ----------------------
|
|
|
228
|
|
|
229 function Current_Capacity (Container : Vector) return Capacity_Range is
|
|
|
230 begin
|
|
|
231 return
|
|
|
232 (if Container.Elements_Ptr = null then
|
|
|
233 Container.Elements'Length
|
|
|
234 else
|
|
|
235 Container.Elements_Ptr.all'Length);
|
|
|
236 end Current_Capacity;
|
|
|
237
|
|
|
238 ------------
|
|
|
239 -- Delete --
|
|
|
240 ------------
|
|
|
241
|
|
|
242 procedure Delete (Container : in out Vector; Index : Extended_Index) is
|
|
|
243 begin
|
|
|
244 Delete (Container, Index, 1);
|
|
|
245 end Delete;
|
|
|
246
|
|
|
247 procedure Delete
|
|
|
248 (Container : in out Vector;
|
|
|
249 Index : Extended_Index;
|
|
|
250 Count : Count_Type)
|
|
|
251 is
|
|
|
252 Old_Last : constant Index_Type'Base := Container.Last;
|
|
|
253 Old_Len : constant Count_Type := Length (Container);
|
|
|
254 New_Last : Index_Type'Base;
|
|
|
255 Count2 : Count_Type'Base; -- count of items from Index to Old_Last
|
|
|
256 Off : Count_Type'Base; -- Index expressed as offset from IT'First
|
|
|
257
|
|
|
258 begin
|
|
|
259 -- Delete removes items from the vector, the number of which is the
|
|
|
260 -- minimum of the specified Count and the items (if any) that exist from
|
|
|
261 -- Index to Container.Last. There are no constraints on the specified
|
|
|
262 -- value of Count (it can be larger than what's available at this
|
|
|
263 -- position in the vector, for example), but there are constraints on
|
|
|
264 -- the allowed values of the Index.
|
|
|
265
|
|
|
266 -- As a precondition on the generic actual Index_Type, the base type
|
|
|
267 -- must include Index_Type'Pred (Index_Type'First); this is the value
|
|
|
268 -- that Container.Last assumes when the vector is empty. However, we do
|
|
|
269 -- not allow that as the value for Index when specifying which items
|
|
|
270 -- should be deleted, so we must manually check. (That the user is
|
|
|
271 -- allowed to specify the value at all here is a consequence of the
|
|
|
272 -- declaration of the Extended_Index subtype, which includes the values
|
|
|
273 -- in the base range that immediately precede and immediately follow the
|
|
|
274 -- values in the Index_Type.)
|
|
|
275
|
|
|
276 if Index < Index_Type'First then
|
|
|
277 raise Constraint_Error with "Index is out of range (too small)";
|
|
|
278 end if;
|
|
|
279
|
|
|
280 -- We do allow a value greater than Container.Last to be specified as
|
|
|
281 -- the Index, but only if it's immediately greater. This allows the
|
|
|
282 -- corner case of deleting no items from the back end of the vector to
|
|
|
283 -- be treated as a no-op. (It is assumed that specifying an index value
|
|
|
284 -- greater than Last + 1 indicates some deeper flaw in the caller's
|
|
|
285 -- algorithm, so that case is treated as a proper error.)
|
|
|
286
|
|
|
287 if Index > Old_Last then
|
|
|
288 if Index > Old_Last + 1 then
|
|
|
289 raise Constraint_Error with "Index is out of range (too large)";
|
|
|
290 end if;
|
|
|
291
|
|
|
292 return;
|
|
|
293 end if;
|
|
|
294
|
|
|
295 if Count = 0 then
|
|
|
296 return;
|
|
|
297 end if;
|
|
|
298
|
|
|
299 -- We first calculate what's available for deletion starting at
|
|
|
300 -- Index. Here and elsewhere we use the wider of Index_Type'Base and
|
|
|
301 -- Count_Type'Base as the type for intermediate values. (See function
|
|
|
302 -- Length for more information.)
|
|
|
303
|
|
|
304 if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then
|
|
|
305 Count2 := Count_Type'Base (Old_Last) - Count_Type'Base (Index) + 1;
|
|
|
306 else
|
|
|
307 Count2 := Count_Type'Base (Old_Last - Index + 1);
|
|
|
308 end if;
|
|
|
309
|
|
|
310 -- If more elements are requested (Count) for deletion than are
|
|
|
311 -- available (Count2) for deletion beginning at Index, then everything
|
|
|
312 -- from Index is deleted. There are no elements to slide down, and so
|
|
|
313 -- all we need to do is set the value of Container.Last.
|
|
|
314
|
|
|
315 if Count >= Count2 then
|
|
|
316 Container.Last := Index - 1;
|
|
|
317 return;
|
|
|
318 end if;
|
|
|
319
|
|
|
320 -- There are some elements that aren't being deleted (the requested
|
|
|
321 -- count was less than the available count), so we must slide them down
|
|
|
322 -- to Index. We first calculate the index values of the respective array
|
|
|
323 -- slices, using the wider of Index_Type'Base and Count_Type'Base as the
|
|
|
324 -- type for intermediate calculations.
|
|
|
325
|
|
|
326 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
|
|
|
327 Off := Count_Type'Base (Index - Index_Type'First);
|
|
|
328 New_Last := Old_Last - Index_Type'Base (Count);
|
|
|
329 else
|
|
|
330 Off := Count_Type'Base (Index) - Count_Type'Base (Index_Type'First);
|
|
|
331 New_Last := Index_Type'Base (Count_Type'Base (Old_Last) - Count);
|
|
|
332 end if;
|
|
|
333
|
|
|
334 -- The array index values for each slice have already been determined,
|
|
|
335 -- so we just slide down to Index the elements that weren't deleted.
|
|
|
336
|
|
|
337 declare
|
|
|
338 EA : Maximal_Array_Ptr renames Elems (Container);
|
|
|
339 Idx : constant Count_Type := EA'First + Off;
|
|
|
340
|
|
|
341 begin
|
|
|
342 EA (Idx .. Old_Len - Count) := EA (Idx + Count .. Old_Len);
|
|
|
343 Container.Last := New_Last;
|
|
|
344 end;
|
|
|
345 end Delete;
|
|
|
346
|
|
|
347 ------------------
|
|
|
348 -- Delete_First --
|
|
|
349 ------------------
|
|
|
350
|
|
|
351 procedure Delete_First (Container : in out Vector) is
|
|
|
352 begin
|
|
|
353 Delete_First (Container, 1);
|
|
|
354 end Delete_First;
|
|
|
355
|
|
|
356 procedure Delete_First (Container : in out Vector; Count : Count_Type) is
|
|
|
357 begin
|
|
|
358 if Count = 0 then
|
|
|
359 return;
|
|
|
360
|
|
|
361 elsif Count >= Length (Container) then
|
|
|
362 Clear (Container);
|
|
|
363 return;
|
|
|
364
|
|
|
365 else
|
|
|
366 Delete (Container, Index_Type'First, Count);
|
|
|
367 end if;
|
|
|
368 end Delete_First;
|
|
|
369
|
|
|
370 -----------------
|
|
|
371 -- Delete_Last --
|
|
|
372 -----------------
|
|
|
373
|
|
|
374 procedure Delete_Last (Container : in out Vector) is
|
|
|
375 begin
|
|
|
376 Delete_Last (Container, 1);
|
|
|
377 end Delete_Last;
|
|
|
378
|
|
|
379 procedure Delete_Last (Container : in out Vector; Count : Count_Type) is
|
|
|
380 begin
|
|
|
381 if Count = 0 then
|
|
|
382 return;
|
|
|
383 end if;
|
|
|
384
|
|
|
385 -- There is no restriction on how large Count can be when deleting
|
|
|
386 -- items. If it is equal or greater than the current length, then this
|
|
|
387 -- is equivalent to clearing the vector. (In particular, there's no need
|
|
|
388 -- for us to actually calculate the new value for Last.)
|
|
|
389
|
|
|
390 -- If the requested count is less than the current length, then we must
|
|
|
391 -- calculate the new value for Last. For the type we use the widest of
|
|
|
392 -- Index_Type'Base and Count_Type'Base for the intermediate values of
|
|
|
393 -- our calculation. (See the comments in Length for more information.)
|
|
|
394
|
|
|
395 if Count >= Length (Container) then
|
|
|
396 Container.Last := No_Index;
|
|
|
397
|
|
|
398 elsif Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
|
|
|
399 Container.Last := Container.Last - Index_Type'Base (Count);
|
|
|
400
|
|
|
401 else
|
|
|
402 Container.Last :=
|
|
|
403 Index_Type'Base (Count_Type'Base (Container.Last) - Count);
|
|
|
404 end if;
|
|
|
405 end Delete_Last;
|
|
|
406
|
|
|
407 -------------
|
|
|
408 -- Element --
|
|
|
409 -------------
|
|
|
410
|
|
|
411 function Element
|
|
|
412 (Container : Vector;
|
|
|
413 Index : Index_Type) return Element_Type
|
|
|
414 is
|
|
|
415 begin
|
|
|
416 if Index > Container.Last then
|
|
|
417 raise Constraint_Error with "Index is out of range";
|
|
|
418 end if;
|
|
|
419
|
|
|
420 declare
|
|
|
421 II : constant Int'Base := Int (Index) - Int (No_Index);
|
|
|
422 I : constant Capacity_Range := Capacity_Range (II);
|
|
|
423
|
|
|
424 begin
|
|
|
425 return Get_Element (Container, I);
|
|
|
426 end;
|
|
|
427 end Element;
|
|
|
428
|
|
131
|
429 -----------
|
|
|
430 -- Elems --
|
|
|
431 -----------
|
|
111
|
432
|
|
|
433 function Elems (Container : in out Vector) return Maximal_Array_Ptr is
|
|
|
434 begin
|
|
|
435 return
|
|
|
436 (if Container.Elements_Ptr = null then
|
|
|
437 Container.Elements'Unrestricted_Access
|
|
|
438 else
|
|
|
439 Container.Elements_Ptr.all'Unrestricted_Access);
|
|
|
440 end Elems;
|
|
|
441
|
|
|
442 function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is
|
|
|
443 begin
|
|
|
444 return
|
|
|
445 (if Container.Elements_Ptr = null then
|
|
|
446 Container.Elements'Unrestricted_Access
|
|
|
447 else
|
|
|
448 Container.Elements_Ptr.all'Unrestricted_Access);
|
|
|
449 end Elemsc;
|
|
|
450
|
|
|
451 ----------------
|
|
|
452 -- Find_Index --
|
|
|
453 ----------------
|
|
|
454
|
|
|
455 function Find_Index
|
|
|
456 (Container : Vector;
|
|
|
457 Item : Element_Type;
|
|
|
458 Index : Index_Type := Index_Type'First) return Extended_Index
|
|
|
459 is
|
|
145
|
460 K : Count_Type;
|
|
|
461 Last : constant Extended_Index := Last_Index (Container);
|
|
111
|
462
|
|
|
463 begin
|
|
|
464 K := Capacity_Range (Int (Index) - Int (No_Index));
|
|
|
465 for Indx in Index .. Last loop
|
|
|
466 if Get_Element (Container, K) = Item then
|
|
|
467 return Indx;
|
|
|
468 end if;
|
|
|
469
|
|
|
470 K := K + 1;
|
|
|
471 end loop;
|
|
|
472
|
|
|
473 return No_Index;
|
|
|
474 end Find_Index;
|
|
|
475
|
|
|
476 -------------------
|
|
|
477 -- First_Element --
|
|
|
478 -------------------
|
|
|
479
|
|
|
480 function First_Element (Container : Vector) return Element_Type is
|
|
|
481 begin
|
|
|
482 if Is_Empty (Container) then
|
|
|
483 raise Constraint_Error with "Container is empty";
|
|
|
484 else
|
|
|
485 return Get_Element (Container, 1);
|
|
|
486 end if;
|
|
|
487 end First_Element;
|
|
|
488
|
|
|
489 -----------------
|
|
|
490 -- First_Index --
|
|
|
491 -----------------
|
|
|
492
|
|
|
493 function First_Index (Container : Vector) return Index_Type is
|
|
|
494 pragma Unreferenced (Container);
|
|
|
495 begin
|
|
|
496 return Index_Type'First;
|
|
|
497 end First_Index;
|
|
|
498
|
|
|
499 ------------------
|
|
|
500 -- Formal_Model --
|
|
|
501 ------------------
|
|
|
502
|
|
|
503 package body Formal_Model is
|
|
|
504
|
|
|
505 -------------------------
|
|
|
506 -- M_Elements_In_Union --
|
|
|
507 -------------------------
|
|
|
508
|
|
|
509 function M_Elements_In_Union
|
|
|
510 (Container : M.Sequence;
|
|
|
511 Left : M.Sequence;
|
|
|
512 Right : M.Sequence) return Boolean
|
|
|
513 is
|
|
|
514 begin
|
|
|
515 for Index in Index_Type'First .. M.Last (Container) loop
|
|
|
516 declare
|
|
|
517 Elem : constant Element_Type := Element (Container, Index);
|
|
|
518 begin
|
|
|
519 if not M.Contains (Left, Index_Type'First, M.Last (Left), Elem)
|
|
|
520 and then
|
|
|
521 not M.Contains
|
|
|
522 (Right, Index_Type'First, M.Last (Right), Elem)
|
|
|
523 then
|
|
|
524 return False;
|
|
|
525 end if;
|
|
|
526 end;
|
|
|
527 end loop;
|
|
|
528
|
|
|
529 return True;
|
|
|
530 end M_Elements_In_Union;
|
|
|
531
|
|
|
532 -------------------------
|
|
|
533 -- M_Elements_Included --
|
|
|
534 -------------------------
|
|
|
535
|
|
|
536 function M_Elements_Included
|
|
|
537 (Left : M.Sequence;
|
|
|
538 L_Fst : Index_Type := Index_Type'First;
|
|
|
539 L_Lst : Extended_Index;
|
|
|
540 Right : M.Sequence;
|
|
|
541 R_Fst : Index_Type := Index_Type'First;
|
|
|
542 R_Lst : Extended_Index) return Boolean
|
|
|
543 is
|
|
|
544 begin
|
|
|
545 for I in L_Fst .. L_Lst loop
|
|
|
546 declare
|
|
|
547 Found : Boolean := False;
|
|
|
548 J : Extended_Index := R_Fst - 1;
|
|
|
549
|
|
|
550 begin
|
|
|
551 while not Found and J < R_Lst loop
|
|
|
552 J := J + 1;
|
|
|
553 if Element (Left, I) = Element (Right, J) then
|
|
|
554 Found := True;
|
|
|
555 end if;
|
|
|
556 end loop;
|
|
|
557
|
|
|
558 if not Found then
|
|
|
559 return False;
|
|
|
560 end if;
|
|
|
561 end;
|
|
|
562 end loop;
|
|
|
563
|
|
|
564 return True;
|
|
|
565 end M_Elements_Included;
|
|
|
566
|
|
|
567 -------------------------
|
|
|
568 -- M_Elements_Reversed --
|
|
|
569 -------------------------
|
|
|
570
|
|
|
571 function M_Elements_Reversed
|
|
|
572 (Left : M.Sequence;
|
|
|
573 Right : M.Sequence) return Boolean
|
|
|
574 is
|
|
|
575 L : constant Index_Type := M.Last (Left);
|
|
|
576
|
|
|
577 begin
|
|
|
578 if L /= M.Last (Right) then
|
|
|
579 return False;
|
|
|
580 end if;
|
|
|
581
|
|
|
582 for I in Index_Type'First .. L loop
|
|
|
583 if Element (Left, I) /= Element (Right, L - I + 1)
|
|
|
584 then
|
|
|
585 return False;
|
|
|
586 end if;
|
|
|
587 end loop;
|
|
|
588
|
|
|
589 return True;
|
|
|
590 end M_Elements_Reversed;
|
|
|
591
|
|
|
592 ------------------------
|
|
131
|
593 -- M_Elements_Swapped --
|
|
111
|
594 ------------------------
|
|
|
595
|
|
|
596 function M_Elements_Swapped
|
|
|
597 (Left : M.Sequence;
|
|
|
598 Right : M.Sequence;
|
|
|
599 X : Index_Type;
|
|
|
600 Y : Index_Type) return Boolean
|
|
|
601 is
|
|
|
602 begin
|
|
|
603 if M.Length (Left) /= M.Length (Right)
|
|
|
604 or else Element (Left, X) /= Element (Right, Y)
|
|
|
605 or else Element (Left, Y) /= Element (Right, X)
|
|
|
606 then
|
|
|
607 return False;
|
|
|
608 end if;
|
|
|
609
|
|
|
610 for I in Index_Type'First .. M.Last (Left) loop
|
|
|
611 if I /= X and then I /= Y
|
|
|
612 and then Element (Left, I) /= Element (Right, I)
|
|
|
613 then
|
|
|
614 return False;
|
|
|
615 end if;
|
|
|
616 end loop;
|
|
|
617
|
|
|
618 return True;
|
|
|
619 end M_Elements_Swapped;
|
|
|
620
|
|
|
621 -----------
|
|
|
622 -- Model --
|
|
|
623 -----------
|
|
|
624
|
|
|
625 function Model (Container : Vector) return M.Sequence is
|
|
|
626 R : M.Sequence;
|
|
|
627
|
|
|
628 begin
|
|
|
629 for Position in 1 .. Length (Container) loop
|
|
|
630 R := M.Add (R, E (Elemsc (Container) (Position)));
|
|
|
631 end loop;
|
|
|
632
|
|
|
633 return R;
|
|
|
634 end Model;
|
|
|
635
|
|
|
636 end Formal_Model;
|
|
|
637
|
|
|
638 ---------------------
|
|
|
639 -- Generic_Sorting --
|
|
|
640 ---------------------
|
|
|
641
|
|
|
642 package body Generic_Sorting with SPARK_Mode => Off is
|
|
|
643
|
|
|
644 ------------------
|
|
|
645 -- Formal_Model --
|
|
|
646 ------------------
|
|
|
647
|
|
|
648 package body Formal_Model is
|
|
|
649
|
|
|
650 -----------------------
|
|
|
651 -- M_Elements_Sorted --
|
|
|
652 -----------------------
|
|
|
653
|
|
|
654 function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
|
|
655 begin
|
|
|
656 if M.Length (Container) = 0 then
|
|
|
657 return True;
|
|
|
658 end if;
|
|
|
659
|
|
|
660 declare
|
|
|
661 E1 : Element_Type := Element (Container, Index_Type'First);
|
|
|
662
|
|
|
663 begin
|
|
|
664 for I in Index_Type'First + 1 .. M.Last (Container) loop
|
|
|
665 declare
|
|
|
666 E2 : constant Element_Type := Element (Container, I);
|
|
|
667
|
|
|
668 begin
|
|
|
669 if E2 < E1 then
|
|
|
670 return False;
|
|
|
671 end if;
|
|
|
672
|
|
|
673 E1 := E2;
|
|
|
674 end;
|
|
|
675 end loop;
|
|
|
676 end;
|
|
|
677
|
|
|
678 return True;
|
|
|
679 end M_Elements_Sorted;
|
|
|
680
|
|
|
681 end Formal_Model;
|
|
|
682
|
|
|
683 ---------------
|
|
|
684 -- Is_Sorted --
|
|
|
685 ---------------
|
|
|
686
|
|
|
687 function Is_Sorted (Container : Vector) return Boolean is
|
|
|
688 L : constant Capacity_Range := Length (Container);
|
|
|
689
|
|
|
690 begin
|
|
|
691 for J in 1 .. L - 1 loop
|
|
|
692 if Get_Element (Container, J + 1) < Get_Element (Container, J) then
|
|
|
693 return False;
|
|
|
694 end if;
|
|
|
695 end loop;
|
|
|
696
|
|
|
697 return True;
|
|
|
698 end Is_Sorted;
|
|
|
699
|
|
|
700 ----------
|
|
|
701 -- Sort --
|
|
|
702 ----------
|
|
|
703
|
|
|
704 procedure Sort (Container : in out Vector) is
|
|
|
705 function "<" (Left : Holder; Right : Holder) return Boolean is
|
|
|
706 (E (Left) < E (Right));
|
|
|
707
|
|
|
708 procedure Sort is new Generic_Array_Sort
|
|
|
709 (Index_Type => Array_Index,
|
|
|
710 Element_Type => Holder,
|
|
|
711 Array_Type => Elements_Array,
|
|
|
712 "<" => "<");
|
|
|
713
|
|
|
714 Len : constant Capacity_Range := Length (Container);
|
|
|
715
|
|
|
716 begin
|
|
|
717 if Container.Last <= Index_Type'First then
|
|
|
718 return;
|
|
|
719 else
|
|
|
720 Sort (Elems (Container) (1 .. Len));
|
|
|
721 end if;
|
|
|
722 end Sort;
|
|
|
723
|
|
|
724 -----------
|
|
|
725 -- Merge --
|
|
|
726 -----------
|
|
|
727
|
|
|
728 procedure Merge (Target : in out Vector; Source : in out Vector) is
|
|
|
729 I : Count_Type;
|
|
|
730 J : Count_Type;
|
|
|
731
|
|
|
732 begin
|
|
|
733 if Target'Address = Source'Address then
|
|
|
734 raise Program_Error with "Target and Source denote same container";
|
|
|
735 end if;
|
|
|
736
|
|
|
737 if Length (Source) = 0 then
|
|
|
738 return;
|
|
|
739 end if;
|
|
|
740
|
|
|
741 if Length (Target) = 0 then
|
|
|
742 Move (Target => Target, Source => Source);
|
|
|
743 return;
|
|
|
744 end if;
|
|
|
745
|
|
|
746 I := Length (Target);
|
|
|
747
|
|
|
748 declare
|
|
|
749 New_Length : constant Count_Type := I + Length (Source);
|
|
|
750
|
|
|
751 begin
|
|
|
752 if not Bounded
|
|
|
753 and then Current_Capacity (Target) < Capacity_Range (New_Length)
|
|
|
754 then
|
|
|
755 Reserve_Capacity
|
|
|
756 (Target,
|
|
|
757 Capacity_Range'Max
|
|
|
758 (Current_Capacity (Target) * Growth_Factor,
|
|
|
759 Capacity_Range (New_Length)));
|
|
|
760 end if;
|
|
|
761
|
|
|
762 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
|
|
|
763 Target.Last := No_Index + Index_Type'Base (New_Length);
|
|
|
764
|
|
|
765 else
|
|
|
766 Target.Last :=
|
|
|
767 Index_Type'Base (Count_Type'Base (No_Index) + New_Length);
|
|
|
768 end if;
|
|
|
769 end;
|
|
|
770
|
|
|
771 declare
|
|
|
772 TA : Maximal_Array_Ptr renames Elems (Target);
|
|
|
773 SA : Maximal_Array_Ptr renames Elems (Source);
|
|
|
774
|
|
|
775 begin
|
|
|
776 J := Length (Target);
|
|
|
777 while Length (Source) /= 0 loop
|
|
|
778 if I = 0 then
|
|
|
779 TA (1 .. J) := SA (1 .. Length (Source));
|
|
|
780 Source.Last := No_Index;
|
|
|
781 exit;
|
|
|
782 end if;
|
|
|
783
|
|
|
784 if E (SA (Length (Source))) < E (TA (I)) then
|
|
|
785 TA (J) := TA (I);
|
|
|
786 I := I - 1;
|
|
|
787
|
|
|
788 else
|
|
|
789 TA (J) := SA (Length (Source));
|
|
|
790 Source.Last := Source.Last - 1;
|
|
|
791 end if;
|
|
|
792
|
|
|
793 J := J - 1;
|
|
|
794 end loop;
|
|
|
795 end;
|
|
|
796 end Merge;
|
|
|
797
|
|
|
798 end Generic_Sorting;
|
|
|
799
|
|
|
800 -----------------
|
|
|
801 -- Get_Element --
|
|
|
802 -----------------
|
|
|
803
|
|
|
804 function Get_Element
|
|
|
805 (Container : Vector;
|
|
|
806 Position : Capacity_Range) return Element_Type
|
|
|
807 is
|
|
|
808 begin
|
|
|
809 return E (Elemsc (Container) (Position));
|
|
|
810 end Get_Element;
|
|
|
811
|
|
|
812 -----------------
|
|
|
813 -- Has_Element --
|
|
|
814 -----------------
|
|
|
815
|
|
|
816 function Has_Element
|
|
|
817 (Container : Vector;
|
|
|
818 Position : Extended_Index) return Boolean
|
|
|
819 is
|
|
|
820 begin
|
|
|
821 return Position in First_Index (Container) .. Last_Index (Container);
|
|
|
822 end Has_Element;
|
|
|
823
|
|
|
824 ------------
|
|
|
825 -- Insert --
|
|
|
826 ------------
|
|
|
827
|
|
|
828 procedure Insert
|
|
|
829 (Container : in out Vector;
|
|
|
830 Before : Extended_Index;
|
|
|
831 New_Item : Element_Type)
|
|
|
832 is
|
|
|
833 begin
|
|
|
834 Insert (Container, Before, New_Item, 1);
|
|
|
835 end Insert;
|
|
|
836
|
|
|
837 procedure Insert
|
|
|
838 (Container : in out Vector;
|
|
|
839 Before : Extended_Index;
|
|
|
840 New_Item : Element_Type;
|
|
|
841 Count : Count_Type)
|
|
|
842 is
|
|
|
843 J : Count_Type'Base; -- scratch
|
|
|
844
|
|
|
845 begin
|
|
|
846 -- Use Insert_Space to create the "hole" (the destination slice)
|
|
|
847
|
|
|
848 Insert_Space (Container, Before, Count);
|
|
|
849
|
|
|
850 J := To_Array_Index (Before);
|
|
|
851
|
|
|
852 Elems (Container) (J .. J - 1 + Count) := (others => H (New_Item));
|
|
|
853 end Insert;
|
|
|
854
|
|
|
855 procedure Insert
|
|
|
856 (Container : in out Vector;
|
|
|
857 Before : Extended_Index;
|
|
|
858 New_Item : Vector)
|
|
|
859 is
|
|
|
860 N : constant Count_Type := Length (New_Item);
|
|
|
861 B : Count_Type; -- index Before converted to Count_Type
|
|
|
862
|
|
|
863 begin
|
|
|
864 if Container'Address = New_Item'Address then
|
|
|
865 raise Program_Error with
|
|
|
866 "Container and New_Item denote same container";
|
|
|
867 end if;
|
|
|
868
|
|
|
869 -- Use Insert_Space to create the "hole" (the destination slice) into
|
|
|
870 -- which we copy the source items.
|
|
|
871
|
|
|
872 Insert_Space (Container, Before, Count => N);
|
|
|
873
|
|
|
874 if N = 0 then
|
|
|
875 -- There's nothing else to do here (vetting of parameters was
|
|
|
876 -- performed already in Insert_Space), so we simply return.
|
|
|
877
|
|
|
878 return;
|
|
|
879 end if;
|
|
|
880
|
|
|
881 B := To_Array_Index (Before);
|
|
|
882
|
|
|
883 Elems (Container) (B .. B + N - 1) := Elemsc (New_Item) (1 .. N);
|
|
|
884 end Insert;
|
|
|
885
|
|
|
886 ------------------
|
|
|
887 -- Insert_Space --
|
|
|
888 ------------------
|
|
|
889
|
|
|
890 procedure Insert_Space
|
|
|
891 (Container : in out Vector;
|
|
|
892 Before : Extended_Index;
|
|
|
893 Count : Count_Type := 1)
|
|
|
894 is
|
|
|
895 Old_Length : constant Count_Type := Length (Container);
|
|
|
896
|
|
|
897 Max_Length : Count_Type'Base; -- determined from range of Index_Type
|
|
|
898 New_Length : Count_Type'Base; -- sum of current length and Count
|
|
|
899
|
|
|
900 Index : Index_Type'Base; -- scratch for intermediate values
|
|
|
901 J : Count_Type'Base; -- scratch
|
|
|
902
|
|
|
903 begin
|
|
|
904 -- As a precondition on the generic actual Index_Type, the base type
|
|
|
905 -- must include Index_Type'Pred (Index_Type'First); this is the value
|
|
|
906 -- that Container.Last assumes when the vector is empty. However, we do
|
|
|
907 -- not allow that as the value for Index when specifying where the new
|
|
|
908 -- items should be inserted, so we must manually check. (That the user
|
|
|
909 -- is allowed to specify the value at all here is a consequence of the
|
|
|
910 -- declaration of the Extended_Index subtype, which includes the values
|
|
|
911 -- in the base range that immediately precede and immediately follow the
|
|
|
912 -- values in the Index_Type.)
|
|
|
913
|
|
|
914 if Before < Index_Type'First then
|
|
|
915 raise Constraint_Error with
|
|
|
916 "Before index is out of range (too small)";
|
|
|
917 end if;
|
|
|
918
|
|
|
919 -- We do allow a value greater than Container.Last to be specified as
|
|
|
920 -- the Index, but only if it's immediately greater. This allows for the
|
|
|
921 -- case of appending items to the back end of the vector. (It is assumed
|
|
|
922 -- that specifying an index value greater than Last + 1 indicates some
|
|
|
923 -- deeper flaw in the caller's algorithm, so that case is treated as a
|
|
|
924 -- proper error.)
|
|
|
925
|
|
|
926 if Before > Container.Last
|
|
|
927 and then Before - 1 > Container.Last
|
|
|
928 then
|
|
|
929 raise Constraint_Error with
|
|
|
930 "Before index is out of range (too large)";
|
|
|
931 end if;
|
|
|
932
|
|
|
933 -- We treat inserting 0 items into the container as a no-op, so we
|
|
|
934 -- simply return.
|
|
|
935
|
|
|
936 if Count = 0 then
|
|
|
937 return;
|
|
|
938 end if;
|
|
|
939
|
|
|
940 -- There are two constraints we need to satisfy. The first constraint is
|
|
|
941 -- that a container cannot have more than Count_Type'Last elements, so
|
|
|
942 -- we must check the sum of the current length and the insertion
|
|
|
943 -- count. Note that we cannot simply add these values, because of the
|
|
|
944 -- possibility of overflow.
|
|
|
945
|
|
|
946 if Old_Length > Count_Type'Last - Count then
|
|
|
947 raise Constraint_Error with "Count is out of range";
|
|
|
948 end if;
|
|
|
949
|
|
|
950 -- It is now safe compute the length of the new vector, without fear of
|
|
|
951 -- overflow.
|
|
|
952
|
|
|
953 New_Length := Old_Length + Count;
|
|
|
954
|
|
|
955 -- The second constraint is that the new Last index value cannot exceed
|
|
|
956 -- Index_Type'Last. In each branch below, we calculate the maximum
|
|
|
957 -- length (computed from the range of values in Index_Type), and then
|
|
|
958 -- compare the new length to the maximum length. If the new length is
|
|
|
959 -- acceptable, then we compute the new last index from that.
|
|
|
960
|
|
|
961 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
|
|
|
962
|
|
|
963 -- We have to handle the case when there might be more values in the
|
|
|
964 -- range of Index_Type than in the range of Count_Type.
|
|
|
965
|
|
|
966 if Index_Type'First <= 0 then
|
|
|
967
|
|
|
968 -- We know that No_Index (the same as Index_Type'First - 1) is
|
|
|
969 -- less than 0, so it is safe to compute the following sum without
|
|
|
970 -- fear of overflow.
|
|
|
971
|
|
|
972 Index := No_Index + Index_Type'Base (Count_Type'Last);
|
|
|
973
|
|
|
974 if Index <= Index_Type'Last then
|
|
|
975
|
|
|
976 -- We have determined that range of Index_Type has at least as
|
|
|
977 -- many values as in Count_Type, so Count_Type'Last is the
|
|
|
978 -- maximum number of items that are allowed.
|
|
|
979
|
|
|
980 Max_Length := Count_Type'Last;
|
|
|
981
|
|
|
982 else
|
|
|
983 -- The range of Index_Type has fewer values than in Count_Type,
|
|
|
984 -- so the maximum number of items is computed from the range of
|
|
|
985 -- the Index_Type.
|
|
|
986
|
|
|
987 Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
|
|
|
988 end if;
|
|
|
989
|
|
|
990 else
|
|
|
991 -- No_Index is equal or greater than 0, so we can safely compute
|
|
|
992 -- the difference without fear of overflow (which we would have to
|
|
|
993 -- worry about if No_Index were less than 0, but that case is
|
|
|
994 -- handled above).
|
|
|
995
|
|
|
996 if Index_Type'Last - No_Index >= Count_Type'Pos (Count_Type'Last)
|
|
|
997 then
|
|
|
998 -- We have determined that range of Index_Type has at least as
|
|
|
999 -- many values as in Count_Type, so Count_Type'Last is the
|
|
|
1000 -- maximum number of items that are allowed.
|
|
|
1001
|
|
|
1002 Max_Length := Count_Type'Last;
|
|
|
1003
|
|
|
1004 else
|
|
|
1005 -- The range of Index_Type has fewer values than in Count_Type,
|
|
|
1006 -- so the maximum number of items is computed from the range of
|
|
|
1007 -- the Index_Type.
|
|
|
1008
|
|
|
1009 Max_Length := Count_Type'Base (Index_Type'Last - No_Index);
|
|
|
1010 end if;
|
|
|
1011 end if;
|
|
|
1012
|
|
|
1013 elsif Index_Type'First <= 0 then
|
|
|
1014
|
|
|
1015 -- We know that No_Index (the same as Index_Type'First - 1) is less
|
|
|
1016 -- than 0, so it is safe to compute the following sum without fear of
|
|
|
1017 -- overflow.
|
|
|
1018
|
|
|
1019 J := Count_Type'Base (No_Index) + Count_Type'Last;
|
|
|
1020
|
|
|
1021 if J <= Count_Type'Base (Index_Type'Last) then
|
|
|
1022
|
|
|
1023 -- We have determined that range of Index_Type has at least as
|
|
|
1024 -- many values as in Count_Type, so Count_Type'Last is the maximum
|
|
|
1025 -- number of items that are allowed.
|
|
|
1026
|
|
|
1027 Max_Length := Count_Type'Last;
|
|
|
1028
|
|
|
1029 else
|
|
|
1030 -- The range of Index_Type has fewer values than Count_Type does,
|
|
|
1031 -- so the maximum number of items is computed from the range of
|
|
|
1032 -- the Index_Type.
|
|
|
1033
|
|
|
1034 Max_Length :=
|
|
|
1035 Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
|
|
|
1036 end if;
|
|
|
1037
|
|
|
1038 else
|
|
|
1039 -- No_Index is equal or greater than 0, so we can safely compute the
|
|
|
1040 -- difference without fear of overflow (which we would have to worry
|
|
|
1041 -- about if No_Index were less than 0, but that case is handled
|
|
|
1042 -- above).
|
|
|
1043
|
|
|
1044 Max_Length :=
|
|
|
1045 Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index);
|
|
|
1046 end if;
|
|
|
1047
|
|
|
1048 -- We have just computed the maximum length (number of items). We must
|
|
|
1049 -- now compare the requested length to the maximum length, as we do not
|
|
|
1050 -- allow a vector expand beyond the maximum (because that would create
|
|
|
1051 -- an internal array with a last index value greater than
|
|
|
1052 -- Index_Type'Last, with no way to index those elements).
|
|
|
1053
|
|
|
1054 if New_Length > Max_Length then
|
|
|
1055 raise Constraint_Error with "Count is out of range";
|
|
|
1056 end if;
|
|
|
1057
|
|
|
1058 J := To_Array_Index (Before);
|
|
|
1059
|
|
|
1060 -- Increase the capacity of container if needed
|
|
|
1061
|
|
|
1062 if not Bounded
|
|
|
1063 and then Current_Capacity (Container) < Capacity_Range (New_Length)
|
|
|
1064 then
|
|
|
1065 Reserve_Capacity
|
|
|
1066 (Container,
|
|
|
1067 Capacity_Range'Max
|
|
|
1068 (Current_Capacity (Container) * Growth_Factor,
|
|
|
1069 Capacity_Range (New_Length)));
|
|
|
1070 end if;
|
|
|
1071
|
|
|
1072 declare
|
|
|
1073 EA : Maximal_Array_Ptr renames Elems (Container);
|
|
|
1074
|
|
|
1075 begin
|
|
|
1076 if Before <= Container.Last then
|
|
|
1077
|
|
|
1078 -- The new items are being inserted before some existing
|
|
|
1079 -- elements, so we must slide the existing elements up to their
|
|
|
1080 -- new home.
|
|
|
1081
|
|
|
1082 EA (J + Count .. New_Length) := EA (J .. Old_Length);
|
|
|
1083 end if;
|
|
|
1084 end;
|
|
|
1085
|
|
|
1086 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
|
|
|
1087 Container.Last := No_Index + Index_Type'Base (New_Length);
|
|
|
1088
|
|
|
1089 else
|
|
|
1090 Container.Last :=
|
|
|
1091 Index_Type'Base (Count_Type'Base (No_Index) + New_Length);
|
|
|
1092 end if;
|
|
|
1093 end Insert_Space;
|
|
|
1094
|
|
|
1095 --------------
|
|
|
1096 -- Is_Empty --
|
|
|
1097 --------------
|
|
|
1098
|
|
|
1099 function Is_Empty (Container : Vector) return Boolean is
|
|
|
1100 begin
|
|
|
1101 return Last_Index (Container) < Index_Type'First;
|
|
|
1102 end Is_Empty;
|
|
|
1103
|
|
|
1104 ------------------
|
|
|
1105 -- Last_Element --
|
|
|
1106 ------------------
|
|
|
1107
|
|
|
1108 function Last_Element (Container : Vector) return Element_Type is
|
|
|
1109 begin
|
|
|
1110 if Is_Empty (Container) then
|
|
|
1111 raise Constraint_Error with "Container is empty";
|
|
|
1112 else
|
|
|
1113 return Get_Element (Container, Length (Container));
|
|
|
1114 end if;
|
|
|
1115 end Last_Element;
|
|
|
1116
|
|
|
1117 ----------------
|
|
|
1118 -- Last_Index --
|
|
|
1119 ----------------
|
|
|
1120
|
|
|
1121 function Last_Index (Container : Vector) return Extended_Index is
|
|
|
1122 begin
|
|
|
1123 return Container.Last;
|
|
|
1124 end Last_Index;
|
|
|
1125
|
|
|
1126 ------------
|
|
|
1127 -- Length --
|
|
|
1128 ------------
|
|
|
1129
|
|
|
1130 function Length (Container : Vector) return Capacity_Range is
|
|
|
1131 L : constant Int := Int (Container.Last);
|
|
|
1132 F : constant Int := Int (Index_Type'First);
|
|
|
1133 N : constant Int'Base := L - F + 1;
|
|
|
1134
|
|
|
1135 begin
|
|
|
1136 return Capacity_Range (N);
|
|
|
1137 end Length;
|
|
|
1138
|
|
|
1139 ----------
|
|
|
1140 -- Move --
|
|
|
1141 ----------
|
|
|
1142
|
|
|
1143 procedure Move (Target : in out Vector; Source : in out Vector) is
|
|
|
1144 LS : constant Capacity_Range := Length (Source);
|
|
|
1145
|
|
|
1146 begin
|
|
|
1147 if Target'Address = Source'Address then
|
|
|
1148 return;
|
|
|
1149 end if;
|
|
|
1150
|
|
|
1151 if Bounded and then Target.Capacity < LS then
|
|
|
1152 raise Constraint_Error;
|
|
|
1153 end if;
|
|
|
1154
|
|
|
1155 Clear (Target);
|
|
|
1156 Append (Target, Source);
|
|
|
1157 Clear (Source);
|
|
|
1158 end Move;
|
|
|
1159
|
|
|
1160 ------------
|
|
|
1161 -- Prepend --
|
|
|
1162 ------------
|
|
|
1163
|
|
|
1164 procedure Prepend (Container : in out Vector; New_Item : Vector) is
|
|
|
1165 begin
|
|
|
1166 Insert (Container, Index_Type'First, New_Item);
|
|
|
1167 end Prepend;
|
|
|
1168
|
|
|
1169 procedure Prepend (Container : in out Vector; New_Item : Element_Type) is
|
|
|
1170 begin
|
|
|
1171 Prepend (Container, New_Item, 1);
|
|
|
1172 end Prepend;
|
|
|
1173
|
|
|
1174 procedure Prepend
|
|
|
1175 (Container : in out Vector;
|
|
|
1176 New_Item : Element_Type;
|
|
|
1177 Count : Count_Type)
|
|
|
1178 is
|
|
|
1179 begin
|
|
|
1180 Insert (Container, Index_Type'First, New_Item, Count);
|
|
|
1181 end Prepend;
|
|
|
1182
|
|
|
1183 ---------------------
|
|
|
1184 -- Replace_Element --
|
|
|
1185 ---------------------
|
|
|
1186
|
|
|
1187 procedure Replace_Element
|
|
|
1188 (Container : in out Vector;
|
|
|
1189 Index : Index_Type;
|
|
|
1190 New_Item : Element_Type)
|
|
|
1191 is
|
|
|
1192 begin
|
|
|
1193 if Index > Container.Last then
|
|
|
1194 raise Constraint_Error with "Index is out of range";
|
|
|
1195 end if;
|
|
|
1196
|
|
|
1197 declare
|
|
|
1198 II : constant Int'Base := Int (Index) - Int (No_Index);
|
|
|
1199 I : constant Capacity_Range := Capacity_Range (II);
|
|
|
1200
|
|
|
1201 begin
|
|
|
1202 Elems (Container) (I) := H (New_Item);
|
|
|
1203 end;
|
|
|
1204 end Replace_Element;
|
|
|
1205
|
|
|
1206 ----------------------
|
|
|
1207 -- Reserve_Capacity --
|
|
|
1208 ----------------------
|
|
|
1209
|
|
|
1210 procedure Reserve_Capacity
|
|
|
1211 (Container : in out Vector;
|
|
|
1212 Capacity : Capacity_Range)
|
|
|
1213 is
|
|
|
1214 begin
|
|
|
1215 if Bounded then
|
|
|
1216 if Capacity > Container.Capacity then
|
|
|
1217 raise Constraint_Error with "Capacity is out of range";
|
|
|
1218 end if;
|
|
|
1219
|
|
|
1220 else
|
|
|
1221 if Capacity > Current_Capacity (Container) then
|
|
|
1222 declare
|
|
|
1223 New_Elements : constant Elements_Array_Ptr :=
|
|
|
1224 new Elements_Array (1 .. Capacity);
|
|
|
1225 L : constant Capacity_Range := Length (Container);
|
|
|
1226
|
|
|
1227 begin
|
|
|
1228 New_Elements (1 .. L) := Elemsc (Container) (1 .. L);
|
|
|
1229 Free (Container.Elements_Ptr);
|
|
|
1230 Container.Elements_Ptr := New_Elements;
|
|
|
1231 end;
|
|
|
1232 end if;
|
|
|
1233 end if;
|
|
|
1234 end Reserve_Capacity;
|
|
|
1235
|
|
|
1236 ----------------------
|
|
|
1237 -- Reverse_Elements --
|
|
|
1238 ----------------------
|
|
|
1239
|
|
|
1240 procedure Reverse_Elements (Container : in out Vector) is
|
|
|
1241 begin
|
|
|
1242 if Length (Container) <= 1 then
|
|
|
1243 return;
|
|
|
1244 end if;
|
|
|
1245
|
|
|
1246 declare
|
|
|
1247 I : Capacity_Range;
|
|
|
1248 J : Capacity_Range;
|
|
|
1249 E : Elements_Array renames
|
|
|
1250 Elems (Container) (1 .. Length (Container));
|
|
|
1251
|
|
|
1252 begin
|
|
|
1253 I := 1;
|
|
|
1254 J := Length (Container);
|
|
|
1255 while I < J loop
|
|
|
1256 declare
|
|
|
1257 EI : constant Holder := E (I);
|
|
|
1258
|
|
|
1259 begin
|
|
|
1260 E (I) := E (J);
|
|
|
1261 E (J) := EI;
|
|
|
1262 end;
|
|
|
1263
|
|
|
1264 I := I + 1;
|
|
|
1265 J := J - 1;
|
|
|
1266 end loop;
|
|
|
1267 end;
|
|
|
1268 end Reverse_Elements;
|
|
|
1269
|
|
|
1270 ------------------------
|
|
|
1271 -- Reverse_Find_Index --
|
|
|
1272 ------------------------
|
|
|
1273
|
|
|
1274 function Reverse_Find_Index
|
|
|
1275 (Container : Vector;
|
|
|
1276 Item : Element_Type;
|
|
|
1277 Index : Index_Type := Index_Type'Last) return Extended_Index
|
|
|
1278 is
|
|
|
1279 Last : Index_Type'Base;
|
|
145
|
1280 K : Count_Type'Base;
|
|
111
|
1281
|
|
|
1282 begin
|
|
|
1283 if Index > Last_Index (Container) then
|
|
|
1284 Last := Last_Index (Container);
|
|
|
1285 else
|
|
|
1286 Last := Index;
|
|
|
1287 end if;
|
|
|
1288
|
|
|
1289 K := Capacity_Range (Int (Last) - Int (No_Index));
|
|
|
1290 for Indx in reverse Index_Type'First .. Last loop
|
|
|
1291 if Get_Element (Container, K) = Item then
|
|
|
1292 return Indx;
|
|
|
1293 end if;
|
|
|
1294
|
|
|
1295 K := K - 1;
|
|
|
1296 end loop;
|
|
|
1297
|
|
|
1298 return No_Index;
|
|
|
1299 end Reverse_Find_Index;
|
|
|
1300
|
|
|
1301 ----------
|
|
|
1302 -- Swap --
|
|
|
1303 ----------
|
|
|
1304
|
|
|
1305 procedure Swap
|
|
|
1306 (Container : in out Vector;
|
|
|
1307 I : Index_Type;
|
|
|
1308 J : Index_Type)
|
|
|
1309 is
|
|
|
1310 begin
|
|
|
1311 if I > Container.Last then
|
|
|
1312 raise Constraint_Error with "I index is out of range";
|
|
|
1313 end if;
|
|
|
1314
|
|
|
1315 if J > Container.Last then
|
|
|
1316 raise Constraint_Error with "J index is out of range";
|
|
|
1317 end if;
|
|
|
1318
|
|
|
1319 if I = J then
|
|
|
1320 return;
|
|
|
1321 end if;
|
|
|
1322
|
|
|
1323 declare
|
|
|
1324 II : constant Int'Base := Int (I) - Int (No_Index);
|
|
|
1325 JJ : constant Int'Base := Int (J) - Int (No_Index);
|
|
|
1326
|
|
|
1327 EI : Holder renames Elems (Container) (Capacity_Range (II));
|
|
|
1328 EJ : Holder renames Elems (Container) (Capacity_Range (JJ));
|
|
|
1329
|
|
|
1330 EI_Copy : constant Holder := EI;
|
|
|
1331
|
|
|
1332 begin
|
|
|
1333 EI := EJ;
|
|
|
1334 EJ := EI_Copy;
|
|
|
1335 end;
|
|
|
1336 end Swap;
|
|
|
1337
|
|
|
1338 --------------------
|
|
|
1339 -- To_Array_Index --
|
|
|
1340 --------------------
|
|
|
1341
|
|
|
1342 function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base is
|
|
|
1343 Offset : Count_Type'Base;
|
|
|
1344
|
|
|
1345 begin
|
|
|
1346 -- We know that
|
|
|
1347 -- Index >= Index_Type'First
|
|
|
1348 -- hence we also know that
|
|
|
1349 -- Index - Index_Type'First >= 0
|
|
|
1350
|
|
|
1351 -- The issue is that even though 0 is guaranteed to be a value in the
|
|
|
1352 -- type Index_Type'Base, there's no guarantee that the difference is a
|
|
|
1353 -- value in that type. To prevent overflow we use the wider of
|
|
|
1354 -- Count_Type'Base and Index_Type'Base to perform intermediate
|
|
|
1355 -- calculations.
|
|
|
1356
|
|
|
1357 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
|
|
|
1358 Offset := Count_Type'Base (Index - Index_Type'First);
|
|
|
1359
|
|
|
1360 else
|
|
|
1361 Offset := Count_Type'Base (Index) -
|
|
|
1362 Count_Type'Base (Index_Type'First);
|
|
|
1363 end if;
|
|
|
1364
|
|
|
1365 -- The array index subtype for all container element arrays always
|
|
|
1366 -- starts with 1.
|
|
|
1367
|
|
|
1368 return 1 + Offset;
|
|
|
1369 end To_Array_Index;
|
|
|
1370
|
|
|
1371 ---------------
|
|
|
1372 -- To_Vector --
|
|
|
1373 ---------------
|
|
|
1374
|
|
|
1375 function To_Vector
|
|
|
1376 (New_Item : Element_Type;
|
|
|
1377 Length : Capacity_Range) return Vector
|
|
|
1378 is
|
|
|
1379 begin
|
|
|
1380 if Length = 0 then
|
|
|
1381 return Empty_Vector;
|
|
|
1382 end if;
|
|
|
1383
|
|
|
1384 declare
|
|
|
1385 First : constant Int := Int (Index_Type'First);
|
|
|
1386 Last_As_Int : constant Int'Base := First + Int (Length) - 1;
|
|
|
1387 Last : Index_Type;
|
|
|
1388
|
|
|
1389 begin
|
|
|
1390 if Last_As_Int > Index_Type'Pos (Index_Type'Last) then
|
|
|
1391 raise Constraint_Error with "Length is out of range"; -- ???
|
|
|
1392 end if;
|
|
|
1393
|
|
|
1394 Last := Index_Type (Last_As_Int);
|
|
|
1395
|
|
|
1396 return
|
|
|
1397 (Capacity => Length,
|
|
|
1398 Last => Last,
|
|
|
1399 Elements_Ptr => <>,
|
|
|
1400 Elements => (others => H (New_Item)));
|
|
|
1401 end;
|
|
|
1402 end To_Vector;
|
|
|
1403
|
|
|
1404 end Ada.Containers.Formal_Indefinite_Vectors;
|
