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