1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT LIBRARY COMPONENTS                          --
4--                                                                          --
5--                 ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS                 --
6--                                                                          --
7--                                 B o d y                                  --
8--                                                                          --
9--          Copyright (C) 2010-2019, 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-- 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
28with Ada.Containers.Generic_Array_Sort;
29with Ada.Unchecked_Deallocation;
30
31with System; use type System.Address;
32
33package body Ada.Containers.Formal_Indefinite_Vectors with
34  SPARK_Mode => Off
35is
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
429   -----------
430   -- Elems --
431   -----------
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
460      K    : Capacity_Range;
461      Last : constant Index_Type := Last_Index (Container);
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      ------------------------
593      -- M_Elements_Swapped --
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;
1280      K    : Capacity_Range;
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
1404end Ada.Containers.Formal_Indefinite_Vectors;
1405