| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT LIBRARY COMPONENTS -- |
| -- -- |
| -- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS -- |
| -- -- |
| -- B o d y -- |
| -- -- |
| -- Copyright (C) 2010-2022, Free Software Foundation, Inc. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. -- |
| -- -- |
| -- As a special exception under Section 7 of GPL version 3, you are granted -- |
| -- additional permissions described in the GCC Runtime Library Exception, -- |
| -- version 3.1, as published by the Free Software Foundation. -- |
| -- -- |
| -- You should have received a copy of the GNU General Public License and -- |
| -- a copy of the GCC Runtime Library Exception along with this program; -- |
| -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- |
| -- <http://www.gnu.org/licenses/>. -- |
| ------------------------------------------------------------------------------ |
| |
| with Ada.Containers.Generic_Array_Sort; |
| with Ada.Unchecked_Deallocation; |
| |
| with System; use type System.Address; |
| |
| package body Ada.Containers.Formal_Indefinite_Vectors with |
| SPARK_Mode => Off |
| is |
| function H (New_Item : Element_Type) return Holder renames To_Holder; |
| function E (Container : Holder) return Element_Type renames Get; |
| |
| Growth_Factor : constant := 2; |
| -- When growing a container, multiply current capacity by this. Doubling |
| -- leads to amortized linear-time copying. |
| |
| subtype Int is Long_Long_Integer; |
| |
| procedure Free is |
| new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); |
| |
| type Maximal_Array_Ptr is access all Elements_Array (Array_Index) |
| with Storage_Size => 0; |
| type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index) |
| with Storage_Size => 0; |
| |
| function Elems (Container : in out Vector) return Maximal_Array_Ptr; |
| function Elemsc |
| (Container : Vector) return Maximal_Array_Ptr_Const; |
| -- Returns a pointer to the Elements array currently in use -- either |
| -- Container.Elements_Ptr or a pointer to Container.Elements. We work with |
| -- pointers to a bogus array subtype that is constrained with the maximum |
| -- possible bounds. This means that the pointer is a thin pointer. This is |
| -- necessary because 'Unrestricted_Access doesn't work when it produces |
| -- access-to-unconstrained and is returned from a function. |
| -- |
| -- Note that this is dangerous: make sure calls to this use an indexed |
| -- component or slice that is within the bounds 1 .. Length (Container). |
| |
| function Get_Element |
| (Container : Vector; |
| Position : Capacity_Range) return Element_Type; |
| |
| function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base; |
| |
| function Current_Capacity (Container : Vector) return Capacity_Range; |
| |
| procedure Insert_Space |
| (Container : in out Vector; |
| Before : Extended_Index; |
| Count : Count_Type := 1); |
| |
| --------- |
| -- "=" -- |
| --------- |
| |
| function "=" (Left : Vector; Right : Vector) return Boolean is |
| begin |
| if Left'Address = Right'Address then |
| return True; |
| end if; |
| |
| if Length (Left) /= Length (Right) then |
| return False; |
| end if; |
| |
| for J in 1 .. Length (Left) loop |
| if Get_Element (Left, J) /= Get_Element (Right, J) then |
| return False; |
| end if; |
| end loop; |
| |
| return True; |
| end "="; |
| |
| ------------ |
| -- Append -- |
| ------------ |
| |
| procedure Append (Container : in out Vector; New_Item : Vector) is |
| begin |
| if Is_Empty (New_Item) then |
| return; |
| end if; |
| |
| if Container.Last >= Index_Type'Last then |
| raise Constraint_Error with "vector is already at its maximum length"; |
| end if; |
| |
| Insert (Container, Container.Last + 1, New_Item); |
| end Append; |
| |
| procedure Append (Container : in out Vector; New_Item : Element_Type) is |
| begin |
| Append (Container, New_Item, 1); |
| end Append; |
| |
| procedure Append |
| (Container : in out Vector; |
| New_Item : Element_Type; |
| Count : Count_Type) |
| is |
| begin |
| if Count = 0 then |
| return; |
| end if; |
| |
| if Container.Last >= Index_Type'Last then |
| raise Constraint_Error with "vector is already at its maximum length"; |
| end if; |
| |
| Insert (Container, Container.Last + 1, New_Item, Count); |
| end Append; |
| |
| ------------ |
| -- Assign -- |
| ------------ |
| |
| procedure Assign (Target : in out Vector; Source : Vector) is |
| LS : constant Capacity_Range := Length (Source); |
| |
| begin |
| if Target'Address = Source'Address then |
| return; |
| end if; |
| |
| if Bounded and then Target.Capacity < LS then |
| raise Constraint_Error; |
| end if; |
| |
| Clear (Target); |
| Append (Target, Source); |
| end Assign; |
| |
| -------------- |
| -- Capacity -- |
| -------------- |
| |
| function Capacity (Container : Vector) return Capacity_Range is |
| begin |
| return |
| (if Bounded then |
| Container.Capacity |
| else |
| Capacity_Range'Last); |
| end Capacity; |
| |
| ----------- |
| -- Clear -- |
| ----------- |
| |
| procedure Clear (Container : in out Vector) is |
| begin |
| Container.Last := No_Index; |
| |
| -- Free element, note that this is OK if Elements_Ptr is null |
| |
| Free (Container.Elements_Ptr); |
| end Clear; |
| |
| ------------------------ |
| -- Constant_Reference -- |
| ------------------------ |
| |
| function Constant_Reference |
| (Container : aliased Vector; |
| Index : Index_Type) return not null access constant Element_Type |
| is |
| begin |
| if Index > Container.Last then |
| raise Constraint_Error with "Index is out of range"; |
| end if; |
| |
| declare |
| II : constant Int'Base := Int (Index) - Int (No_Index); |
| I : constant Capacity_Range := Capacity_Range (II); |
| |
| begin |
| return Constant_Reference (Elemsc (Container) (I)); |
| end; |
| end Constant_Reference; |
| |
| -------------- |
| -- Contains -- |
| -------------- |
| |
| function Contains |
| (Container : Vector; |
| Item : Element_Type) return Boolean |
| is |
| begin |
| return Find_Index (Container, Item) /= No_Index; |
| end Contains; |
| |
| ---------- |
| -- Copy -- |
| ---------- |
| |
| function Copy |
| (Source : Vector; |
| Capacity : Capacity_Range := 0) return Vector |
| is |
| LS : constant Capacity_Range := Length (Source); |
| C : Capacity_Range; |
| |
| begin |
| if Capacity = 0 then |
| C := LS; |
| elsif Capacity >= LS then |
| C := Capacity; |
| else |
| raise Capacity_Error; |
| end if; |
| |
| return Target : Vector (C) do |
| Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS); |
| Target.Last := Source.Last; |
| end return; |
| end Copy; |
| |
| ---------------------- |
| -- Current_Capacity -- |
| ---------------------- |
| |
| function Current_Capacity (Container : Vector) return Capacity_Range is |
| begin |
| return |
| (if Container.Elements_Ptr = null then |
| Container.Elements'Length |
| else |
| Container.Elements_Ptr.all'Length); |
| end Current_Capacity; |
| |
| ------------ |
| -- Delete -- |
| ------------ |
| |
| procedure Delete (Container : in out Vector; Index : Extended_Index) is |
| begin |
| Delete (Container, Index, 1); |
| end Delete; |
| |
| procedure Delete |
| (Container : in out Vector; |
| Index : Extended_Index; |
| Count : Count_Type) |
| is |
| Old_Last : constant Index_Type'Base := Container.Last; |
| Old_Len : constant Count_Type := Length (Container); |
| New_Last : Index_Type'Base; |
| Count2 : Count_Type'Base; -- count of items from Index to Old_Last |
| Off : Count_Type'Base; -- Index expressed as offset from IT'First |
| |
| begin |
| -- Delete removes items from the vector, the number of which is the |
| -- minimum of the specified Count and the items (if any) that exist from |
| -- Index to Container.Last. There are no constraints on the specified |
| -- value of Count (it can be larger than what's available at this |
| -- position in the vector, for example), but there are constraints on |
| -- the allowed values of the Index. |
| |
| -- As a precondition on the generic actual Index_Type, the base type |
| -- must include Index_Type'Pred (Index_Type'First); this is the value |
| -- that Container.Last assumes when the vector is empty. However, we do |
| -- not allow that as the value for Index when specifying which items |
| -- should be deleted, so we must manually check. (That the user is |
| -- allowed to specify the value at all here is a consequence of the |
| -- declaration of the Extended_Index subtype, which includes the values |
| -- in the base range that immediately precede and immediately follow the |
| -- values in the Index_Type.) |
| |
| if Index < Index_Type'First then |
| raise Constraint_Error with "Index is out of range (too small)"; |
| end if; |
| |
| -- We do allow a value greater than Container.Last to be specified as |
| -- the Index, but only if it's immediately greater. This allows the |
| -- corner case of deleting no items from the back end of the vector to |
| -- be treated as a no-op. (It is assumed that specifying an index value |
| -- greater than Last + 1 indicates some deeper flaw in the caller's |
| -- algorithm, so that case is treated as a proper error.) |
| |
| if Index > Old_Last then |
| if Index > Old_Last + 1 then |
| raise Constraint_Error with "Index is out of range (too large)"; |
| end if; |
| |
| return; |
| end if; |
| |
| if Count = 0 then |
| return; |
| end if; |
| |
| -- We first calculate what's available for deletion starting at |
| -- Index. Here and elsewhere we use the wider of Index_Type'Base and |
| -- Count_Type'Base as the type for intermediate values. (See function |
| -- Length for more information.) |
| |
| if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then |
| Count2 := Count_Type'Base (Old_Last) - Count_Type'Base (Index) + 1; |
| else |
| Count2 := Count_Type'Base (Old_Last - Index + 1); |
| end if; |
| |
| -- If more elements are requested (Count) for deletion than are |
| -- available (Count2) for deletion beginning at Index, then everything |
| -- from Index is deleted. There are no elements to slide down, and so |
| -- all we need to do is set the value of Container.Last. |
| |
| if Count >= Count2 then |
| Container.Last := Index - 1; |
| return; |
| end if; |
| |
| -- There are some elements that aren't being deleted (the requested |
| -- count was less than the available count), so we must slide them down |
| -- to Index. We first calculate the index values of the respective array |
| -- slices, using the wider of Index_Type'Base and Count_Type'Base as the |
| -- type for intermediate calculations. |
| |
| if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then |
| Off := Count_Type'Base (Index - Index_Type'First); |
| New_Last := Old_Last - Index_Type'Base (Count); |
| else |
| Off := Count_Type'Base (Index) - Count_Type'Base (Index_Type'First); |
| New_Last := Index_Type'Base (Count_Type'Base (Old_Last) - Count); |
| end if; |
| |
| -- The array index values for each slice have already been determined, |
| -- so we just slide down to Index the elements that weren't deleted. |
| |
| declare |
| EA : Maximal_Array_Ptr renames Elems (Container); |
| Idx : constant Count_Type := EA'First + Off; |
| |
| begin |
| EA (Idx .. Old_Len - Count) := EA (Idx + Count .. Old_Len); |
| Container.Last := New_Last; |
| end; |
| end Delete; |
| |
| ------------------ |
| -- Delete_First -- |
| ------------------ |
| |
| procedure Delete_First (Container : in out Vector) is |
| begin |
| Delete_First (Container, 1); |
| end Delete_First; |
| |
| procedure Delete_First (Container : in out Vector; Count : Count_Type) is |
| begin |
| if Count = 0 then |
| return; |
| |
| elsif Count >= Length (Container) then |
| Clear (Container); |
| return; |
| |
| else |
| Delete (Container, Index_Type'First, Count); |
| end if; |
| end Delete_First; |
| |
| ----------------- |
| -- Delete_Last -- |
| ----------------- |
| |
| procedure Delete_Last (Container : in out Vector) is |
| begin |
| Delete_Last (Container, 1); |
| end Delete_Last; |
| |
| procedure Delete_Last (Container : in out Vector; Count : Count_Type) is |
| begin |
| if Count = 0 then |
| return; |
| end if; |
| |
| -- There is no restriction on how large Count can be when deleting |
| -- items. If it is equal or greater than the current length, then this |
| -- is equivalent to clearing the vector. (In particular, there's no need |
| -- for us to actually calculate the new value for Last.) |
| |
| -- If the requested count is less than the current length, then we must |
| -- calculate the new value for Last. For the type we use the widest of |
| -- Index_Type'Base and Count_Type'Base for the intermediate values of |
| -- our calculation. (See the comments in Length for more information.) |
| |
| if Count >= Length (Container) then |
| Container.Last := No_Index; |
| |
| elsif Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then |
| Container.Last := Container.Last - Index_Type'Base (Count); |
| |
| else |
| Container.Last := |
| Index_Type'Base (Count_Type'Base (Container.Last) - Count); |
| end if; |
| end Delete_Last; |
| |
| ------------- |
| -- Element -- |
| ------------- |
| |
| function Element |
| (Container : Vector; |
| Index : Index_Type) return Element_Type |
| is |
| begin |
| if Index > Container.Last then |
| raise Constraint_Error with "Index is out of range"; |
| end if; |
| |
| declare |
| II : constant Int'Base := Int (Index) - Int (No_Index); |
| I : constant Capacity_Range := Capacity_Range (II); |
| |
| begin |
| return Get_Element (Container, I); |
| end; |
| end Element; |
| |
| ----------- |
| -- Elems -- |
| ----------- |
| |
| function Elems (Container : in out Vector) return Maximal_Array_Ptr is |
| begin |
| return |
| (if Container.Elements_Ptr = null then |
| Container.Elements'Unrestricted_Access |
| else |
| Container.Elements_Ptr.all'Unrestricted_Access); |
| end Elems; |
| |
| function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is |
| begin |
| return |
| (if Container.Elements_Ptr = null then |
| Container.Elements'Unrestricted_Access |
| else |
| Container.Elements_Ptr.all'Unrestricted_Access); |
| end Elemsc; |
| |
| ---------------- |
| -- Find_Index -- |
| ---------------- |
| |
| function Find_Index |
| (Container : Vector; |
| Item : Element_Type; |
| Index : Index_Type := Index_Type'First) return Extended_Index |
| is |
| K : Count_Type; |
| Last : constant Extended_Index := Last_Index (Container); |
| |
| begin |
| K := Capacity_Range (Int (Index) - Int (No_Index)); |
| for Indx in Index .. Last loop |
| if Get_Element (Container, K) = Item then |
| return Indx; |
| end if; |
| |
| K := K + 1; |
| end loop; |
| |
| return No_Index; |
| end Find_Index; |
| |
| ------------------- |
| -- First_Element -- |
| ------------------- |
| |
| function First_Element (Container : Vector) return Element_Type is |
| begin |
| if Is_Empty (Container) then |
| raise Constraint_Error with "Container is empty"; |
| else |
| return Get_Element (Container, 1); |
| end if; |
| end First_Element; |
| |
| ----------------- |
| -- First_Index -- |
| ----------------- |
| |
| function First_Index (Container : Vector) return Index_Type is |
| pragma Unreferenced (Container); |
| begin |
| return Index_Type'First; |
| end First_Index; |
| |
| ------------------ |
| -- Formal_Model -- |
| ------------------ |
| |
| package body Formal_Model is |
| |
| ------------------------- |
| -- M_Elements_In_Union -- |
| ------------------------- |
| |
| function M_Elements_In_Union |
| (Container : M.Sequence; |
| Left : M.Sequence; |
| Right : M.Sequence) return Boolean |
| is |
| begin |
| for Index in Index_Type'First .. M.Last (Container) loop |
| declare |
| Elem : constant Element_Type := Element (Container, Index); |
| begin |
| if not M.Contains (Left, Index_Type'First, M.Last (Left), Elem) |
| and then |
| not M.Contains |
| (Right, Index_Type'First, M.Last (Right), Elem) |
| then |
| return False; |
| end if; |
| end; |
| end loop; |
| |
| return True; |
| end M_Elements_In_Union; |
| |
| ------------------------- |
| -- M_Elements_Included -- |
| ------------------------- |
| |
| function M_Elements_Included |
| (Left : M.Sequence; |
| L_Fst : Index_Type := Index_Type'First; |
| L_Lst : Extended_Index; |
| Right : M.Sequence; |
| R_Fst : Index_Type := Index_Type'First; |
| R_Lst : Extended_Index) return Boolean |
| is |
| begin |
| for I in L_Fst .. L_Lst loop |
| declare |
| Found : Boolean := False; |
| J : Extended_Index := R_Fst - 1; |
| |
| begin |
| while not Found and J < R_Lst loop |
| J := J + 1; |
| if Element (Left, I) = Element (Right, J) then |
| Found := True; |
| end if; |
| end loop; |
| |
| if not Found then |
| return False; |
| end if; |
| end; |
| end loop; |
| |
| return True; |
| end M_Elements_Included; |
| |
| ------------------------- |
| -- M_Elements_Reversed -- |
| ------------------------- |
| |
| function M_Elements_Reversed |
| (Left : M.Sequence; |
| Right : M.Sequence) return Boolean |
| is |
| L : constant Index_Type := M.Last (Left); |
| |
| begin |
| if L /= M.Last (Right) then |
| return False; |
| end if; |
| |
| for I in Index_Type'First .. L loop |
| if Element (Left, I) /= Element (Right, L - I + 1) |
| then |
| return False; |
| end if; |
| end loop; |
| |
| return True; |
| end M_Elements_Reversed; |
| |
| ------------------------ |
| -- M_Elements_Swapped -- |
| ------------------------ |
| |
| function M_Elements_Swapped |
| (Left : M.Sequence; |
| Right : M.Sequence; |
| X : Index_Type; |
| Y : Index_Type) return Boolean |
| is |
| begin |
| if M.Length (Left) /= M.Length (Right) |
| or else Element (Left, X) /= Element (Right, Y) |
| or else Element (Left, Y) /= Element (Right, X) |
| then |
| return False; |
| end if; |
| |
| for I in Index_Type'First .. M.Last (Left) loop |
| if I /= X and then I /= Y |
| and then Element (Left, I) /= Element (Right, I) |
| then |
| return False; |
| end if; |
| end loop; |
| |
| return True; |
| end M_Elements_Swapped; |
| |
| ----------- |
| -- Model -- |
| ----------- |
| |
| function Model (Container : Vector) return M.Sequence is |
| R : M.Sequence; |
| |
| begin |
| for Position in 1 .. Length (Container) loop |
| R := M.Add (R, E (Elemsc (Container) (Position))); |
| end loop; |
| |
| return R; |
| end Model; |
| |
| end Formal_Model; |
| |
| --------------------- |
| -- Generic_Sorting -- |
| --------------------- |
| |
| package body Generic_Sorting with SPARK_Mode => Off is |
| |
| ------------------ |
| -- Formal_Model -- |
| ------------------ |
| |
| package body Formal_Model is |
| |
| ----------------------- |
| -- M_Elements_Sorted -- |
| ----------------------- |
| |
| function M_Elements_Sorted (Container : M.Sequence) return Boolean is |
| begin |
| if M.Length (Container) = 0 then |
| return True; |
| end if; |
| |
| declare |
| E1 : Element_Type := Element (Container, Index_Type'First); |
| |
| begin |
| for I in Index_Type'First + 1 .. M.Last (Container) loop |
| declare |
| E2 : constant Element_Type := Element (Container, I); |
| |
| begin |
| if E2 < E1 then |
| return False; |
| end if; |
| |
| E1 := E2; |
| end; |
| end loop; |
| end; |
| |
| return True; |
| end M_Elements_Sorted; |
| |
| end Formal_Model; |
| |
| --------------- |
| -- Is_Sorted -- |
| --------------- |
| |
| function Is_Sorted (Container : Vector) return Boolean is |
| L : constant Capacity_Range := Length (Container); |
| |
| begin |
| for J in 1 .. L - 1 loop |
| if Get_Element (Container, J + 1) < Get_Element (Container, J) then |
| return False; |
| end if; |
| end loop; |
| |
| return True; |
| end Is_Sorted; |
| |
| ---------- |
| -- Sort -- |
| ---------- |
| |
| procedure Sort (Container : in out Vector) is |
| function "<" (Left : Holder; Right : Holder) return Boolean is |
| (E (Left) < E (Right)); |
| |
| procedure Sort is new Generic_Array_Sort |
| (Index_Type => Array_Index, |
| Element_Type => Holder, |
| Array_Type => Elements_Array, |
| "<" => "<"); |
| |
| Len : constant Capacity_Range := Length (Container); |
| |
| begin |
| if Container.Last <= Index_Type'First then |
| return; |
| else |
| Sort (Elems (Container) (1 .. Len)); |
| end if; |
| end Sort; |
| |
| ----------- |
| -- Merge -- |
| ----------- |
| |
| procedure Merge (Target : in out Vector; Source : in out Vector) is |
| I : Count_Type; |
| J : Count_Type; |
| |
| begin |
| if Target'Address = Source'Address then |
| raise Program_Error with "Target and Source denote same container"; |
| end if; |
| |
| if Length (Source) = 0 then |
| return; |
| end if; |
| |
| if Length (Target) = 0 then |
| Move (Target => Target, Source => Source); |
| return; |
| end if; |
| |
| I := Length (Target); |
| |
| declare |
| New_Length : constant Count_Type := I + Length (Source); |
| |
| begin |
| if not Bounded |
| and then Current_Capacity (Target) < Capacity_Range (New_Length) |
| then |
| Reserve_Capacity |
| (Target, |
| Capacity_Range'Max |
| (Current_Capacity (Target) * Growth_Factor, |
| Capacity_Range (New_Length))); |
| end if; |
| |
| if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then |
| Target.Last := No_Index + Index_Type'Base (New_Length); |
| |
| else |
| Target.Last := |
| Index_Type'Base (Count_Type'Base (No_Index) + New_Length); |
| end if; |
| end; |
| |
| declare |
| TA : Maximal_Array_Ptr renames Elems (Target); |
| SA : Maximal_Array_Ptr renames Elems (Source); |
| |
| begin |
| J := Length (Target); |
| while Length (Source) /= 0 loop |
| if I = 0 then |
| TA (1 .. J) := SA (1 .. Length (Source)); |
| Source.Last := No_Index; |
| exit; |
| end if; |
| |
| if E (SA (Length (Source))) < E (TA (I)) then |
| TA (J) := TA (I); |
| I := I - 1; |
| |
| else |
| TA (J) := SA (Length (Source)); |
| Source.Last := Source.Last - 1; |
| end if; |
| |
| J := J - 1; |
| end loop; |
| end; |
| end Merge; |
| |
| end Generic_Sorting; |
| |
| ----------------- |
| -- Get_Element -- |
| ----------------- |
| |
| function Get_Element |
| (Container : Vector; |
| Position : Capacity_Range) return Element_Type |
| is |
| begin |
| return E (Elemsc (Container) (Position)); |
| end Get_Element; |
| |
| ----------------- |
| -- Has_Element -- |
| ----------------- |
| |
| function Has_Element |
| (Container : Vector; |
| Position : Extended_Index) return Boolean |
| is |
| begin |
| return Position in First_Index (Container) .. Last_Index (Container); |
| end Has_Element; |
| |
| ------------ |
| -- Insert -- |
| ------------ |
| |
| procedure Insert |
| (Container : in out Vector; |
| Before : Extended_Index; |
| New_Item : Element_Type) |
| is |
| begin |
| Insert (Container, Before, New_Item, 1); |
| end Insert; |
| |
| procedure Insert |
| (Container : in out Vector; |
| Before : Extended_Index; |
| New_Item : Element_Type; |
| Count : Count_Type) |
| is |
| J : Count_Type'Base; -- scratch |
| |
| begin |
| -- Use Insert_Space to create the "hole" (the destination slice) |
| |
| Insert_Space (Container, Before, Count); |
| |
| J := To_Array_Index (Before); |
| |
| Elems (Container) (J .. J - 1 + Count) := [others => H (New_Item)]; |
| end Insert; |
| |
| procedure Insert |
| (Container : in out Vector; |
| Before : Extended_Index; |
| New_Item : Vector) |
| is |
| N : constant Count_Type := Length (New_Item); |
| B : Count_Type; -- index Before converted to Count_Type |
| |
| begin |
| if Container'Address = New_Item'Address then |
| raise Program_Error with |
| "Container and New_Item denote same container"; |
| end if; |
| |
| -- Use Insert_Space to create the "hole" (the destination slice) into |
| -- which we copy the source items. |
| |
| Insert_Space (Container, Before, Count => N); |
| |
| if N = 0 then |
| -- There's nothing else to do here (vetting of parameters was |
| -- performed already in Insert_Space), so we simply return. |
| |
| return; |
| end if; |
| |
| B := To_Array_Index (Before); |
| |
| Elems (Container) (B .. B + N - 1) := Elemsc (New_Item) (1 .. N); |
| end Insert; |
| |
| ------------------ |
| -- Insert_Space -- |
| ------------------ |
| |
| procedure Insert_Space |
| (Container : in out Vector; |
| Before : Extended_Index; |
| Count : Count_Type := 1) |
| is |
| Old_Length : constant Count_Type := Length (Container); |
| |
| Max_Length : Count_Type'Base; -- determined from range of Index_Type |
| New_Length : Count_Type'Base; -- sum of current length and Count |
| |
| Index : Index_Type'Base; -- scratch for intermediate values |
| J : Count_Type'Base; -- scratch |
| |
| begin |
| -- As a precondition on the generic actual Index_Type, the base type |
| -- must include Index_Type'Pred (Index_Type'First); this is the value |
| -- that Container.Last assumes when the vector is empty. However, we do |
| -- not allow that as the value for Index when specifying where the new |
| -- items should be inserted, so we must manually check. (That the user |
| -- is allowed to specify the value at all here is a consequence of the |
| -- declaration of the Extended_Index subtype, which includes the values |
| -- in the base range that immediately precede and immediately follow the |
| -- values in the Index_Type.) |
| |
| if Before < Index_Type'First then |
| raise Constraint_Error with |
| "Before index is out of range (too small)"; |
| end if; |
| |
| -- We do allow a value greater than Container.Last to be specified as |
| -- the Index, but only if it's immediately greater. This allows for the |
| -- case of appending items to the back end of the vector. (It is assumed |
| -- that specifying an index value greater than Last + 1 indicates some |
| -- deeper flaw in the caller's algorithm, so that case is treated as a |
| -- proper error.) |
| |
| if Before > Container.Last |
| and then Before - 1 > Container.Last |
| then |
| raise Constraint_Error with |
| "Before index is out of range (too large)"; |
| end if; |
| |
| -- We treat inserting 0 items into the container as a no-op, so we |
| -- simply return. |
| |
| if Count = 0 then |
| return; |
| end if; |
| |
| -- There are two constraints we need to satisfy. The first constraint is |
| -- that a container cannot have more than Count_Type'Last elements, so |
| -- we must check the sum of the current length and the insertion |
| -- count. Note that we cannot simply add these values, because of the |
| -- possibility of overflow. |
| |
| if Old_Length > Count_Type'Last - Count then |
| raise Constraint_Error with "Count is out of range"; |
| end if; |
| |
| -- It is now safe compute the length of the new vector, without fear of |
| -- overflow. |
| |
| New_Length := Old_Length + Count; |
| |
| -- The second constraint is that the new Last index value cannot exceed |
| -- Index_Type'Last. In each branch below, we calculate the maximum |
| -- length (computed from the range of values in Index_Type), and then |
| -- compare the new length to the maximum length. If the new length is |
| -- acceptable, then we compute the new last index from that. |
| |
| if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then |
| |
| -- We have to handle the case when there might be more values in the |
| -- range of Index_Type than in the range of Count_Type. |
| |
| if Index_Type'First <= 0 then |
| |
| -- We know that No_Index (the same as Index_Type'First - 1) is |
| -- less than 0, so it is safe to compute the following sum without |
| -- fear of overflow. |
| |
| Index := No_Index + Index_Type'Base (Count_Type'Last); |
| |
| if Index <= Index_Type'Last then |
| |
| -- We have determined that range of Index_Type has at least as |
| -- many values as in Count_Type, so Count_Type'Last is the |
| -- maximum number of items that are allowed. |
| |
| Max_Length := Count_Type'Last; |
| |
| else |
| -- The range of Index_Type has fewer values than in Count_Type, |
| -- so the maximum number of items is computed from the range of |
| -- the Index_Type. |
| |
| Max_Length := Count_Type'Base (Index_Type'Last - No_Index); |
| end if; |
| |
| else |
| -- No_Index is equal or greater than 0, so we can safely compute |
| -- the difference without fear of overflow (which we would have to |
| -- worry about if No_Index were less than 0, but that case is |
| -- handled above). |
| |
| if Index_Type'Last - No_Index >= Count_Type'Pos (Count_Type'Last) |
| then |
| -- We have determined that range of Index_Type has at least as |
| -- many values as in Count_Type, so Count_Type'Last is the |
| -- maximum number of items that are allowed. |
| |
| Max_Length := Count_Type'Last; |
| |
| else |
| -- The range of Index_Type has fewer values than in Count_Type, |
| -- so the maximum number of items is computed from the range of |
| -- the Index_Type. |
| |
| Max_Length := Count_Type'Base (Index_Type'Last - No_Index); |
| end if; |
| end if; |
| |
| elsif Index_Type'First <= 0 then |
| |
| -- We know that No_Index (the same as Index_Type'First - 1) is less |
| -- than 0, so it is safe to compute the following sum without fear of |
| -- overflow. |
| |
| J := Count_Type'Base (No_Index) + Count_Type'Last; |
| |
| if J <= Count_Type'Base (Index_Type'Last) then |
| |
| -- We have determined that range of Index_Type has at least as |
| -- many values as in Count_Type, so Count_Type'Last is the maximum |
| -- number of items that are allowed. |
| |
| Max_Length := Count_Type'Last; |
| |
| else |
| -- The range of Index_Type has fewer values than Count_Type does, |
| -- so the maximum number of items is computed from the range of |
| -- the Index_Type. |
| |
| Max_Length := |
| Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); |
| end if; |
| |
| else |
| -- No_Index is equal or greater than 0, so we can safely compute the |
| -- difference without fear of overflow (which we would have to worry |
| -- about if No_Index were less than 0, but that case is handled |
| -- above). |
| |
| Max_Length := |
| Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); |
| end if; |
| |
| -- We have just computed the maximum length (number of items). We must |
| -- now compare the requested length to the maximum length, as we do not |
| -- allow a vector expand beyond the maximum (because that would create |
| -- an internal array with a last index value greater than |
| -- Index_Type'Last, with no way to index those elements). |
| |
| if New_Length > Max_Length then |
| raise Constraint_Error with "Count is out of range"; |
| end if; |
| |
| J := To_Array_Index (Before); |
| |
| -- Increase the capacity of container if needed |
| |
| if not Bounded |
| and then Current_Capacity (Container) < Capacity_Range (New_Length) |
| then |
| Reserve_Capacity |
| (Container, |
| Capacity_Range'Max |
| (Current_Capacity (Container) * Growth_Factor, |
| Capacity_Range (New_Length))); |
| end if; |
| |
| declare |
| EA : Maximal_Array_Ptr renames Elems (Container); |
| |
| begin |
| if Before <= Container.Last then |
| |
| -- The new items are being inserted before some existing |
| -- elements, so we must slide the existing elements up to their |
| -- new home. |
| |
| EA (J + Count .. New_Length) := EA (J .. Old_Length); |
| end if; |
| end; |
| |
| if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then |
| Container.Last := No_Index + Index_Type'Base (New_Length); |
| |
| else |
| Container.Last := |
| Index_Type'Base (Count_Type'Base (No_Index) + New_Length); |
| end if; |
| end Insert_Space; |
| |
| -------------- |
| -- Is_Empty -- |
| -------------- |
| |
| function Is_Empty (Container : Vector) return Boolean is |
| begin |
| return Last_Index (Container) < Index_Type'First; |
| end Is_Empty; |
| |
| ------------------ |
| -- Last_Element -- |
| ------------------ |
| |
| function Last_Element (Container : Vector) return Element_Type is |
| begin |
| if Is_Empty (Container) then |
| raise Constraint_Error with "Container is empty"; |
| else |
| return Get_Element (Container, Length (Container)); |
| end if; |
| end Last_Element; |
| |
| ---------------- |
| -- Last_Index -- |
| ---------------- |
| |
| function Last_Index (Container : Vector) return Extended_Index is |
| begin |
| return Container.Last; |
| end Last_Index; |
| |
| ------------ |
| -- Length -- |
| ------------ |
| |
| function Length (Container : Vector) return Capacity_Range is |
| L : constant Int := Int (Container.Last); |
| F : constant Int := Int (Index_Type'First); |
| N : constant Int'Base := L - F + 1; |
| |
| begin |
| return Capacity_Range (N); |
| end Length; |
| |
| ---------- |
| -- Move -- |
| ---------- |
| |
| procedure Move (Target : in out Vector; Source : in out Vector) is |
| LS : constant Capacity_Range := Length (Source); |
| |
| begin |
| if Target'Address = Source'Address then |
| return; |
| end if; |
| |
| if Bounded and then Target.Capacity < LS then |
| raise Constraint_Error; |
| end if; |
| |
| Clear (Target); |
| Append (Target, Source); |
| Clear (Source); |
| end Move; |
| |
| ------------ |
| -- Prepend -- |
| ------------ |
| |
| procedure Prepend (Container : in out Vector; New_Item : Vector) is |
| begin |
| Insert (Container, Index_Type'First, New_Item); |
| end Prepend; |
| |
| procedure Prepend (Container : in out Vector; New_Item : Element_Type) is |
| begin |
| Prepend (Container, New_Item, 1); |
| end Prepend; |
| |
| procedure Prepend |
| (Container : in out Vector; |
| New_Item : Element_Type; |
| Count : Count_Type) |
| is |
| begin |
| Insert (Container, Index_Type'First, New_Item, Count); |
| end Prepend; |
| |
| --------------- |
| -- Reference -- |
| --------------- |
| |
| function Reference |
| (Container : not null access Vector; |
| Index : Index_Type) return not null access Element_Type |
| is |
| begin |
| if Index > Container.Last then |
| raise Constraint_Error with "Index is out of range"; |
| end if; |
| |
| declare |
| II : constant Int'Base := Int (Index) - Int (No_Index); |
| I : constant Capacity_Range := Capacity_Range (II); |
| |
| begin |
| if Container.Elements_Ptr = null then |
| return Reference (Container.Elements (I)'Access); |
| else |
| return Reference (Container.Elements_Ptr (I)'Access); |
| end if; |
| end; |
| end Reference; |
| |
| --------------------- |
| -- Replace_Element -- |
| --------------------- |
| |
| procedure Replace_Element |
| (Container : in out Vector; |
| Index : Index_Type; |
| New_Item : Element_Type) |
| is |
| begin |
| if Index > Container.Last then |
| raise Constraint_Error with "Index is out of range"; |
| end if; |
| |
| declare |
| II : constant Int'Base := Int (Index) - Int (No_Index); |
| I : constant Capacity_Range := Capacity_Range (II); |
| |
| begin |
| Elems (Container) (I) := H (New_Item); |
| end; |
| end Replace_Element; |
| |
| ---------------------- |
| -- Reserve_Capacity -- |
| ---------------------- |
| |
| procedure Reserve_Capacity |
| (Container : in out Vector; |
| Capacity : Capacity_Range) |
| is |
| begin |
| if Bounded then |
| if Capacity > Container.Capacity then |
| raise Constraint_Error with "Capacity is out of range"; |
| end if; |
| |
| else |
| if Capacity > Current_Capacity (Container) then |
| declare |
| New_Elements : constant Elements_Array_Ptr := |
| new Elements_Array (1 .. Capacity); |
| L : constant Capacity_Range := Length (Container); |
| |
| begin |
| New_Elements (1 .. L) := Elemsc (Container) (1 .. L); |
| Free (Container.Elements_Ptr); |
| Container.Elements_Ptr := New_Elements; |
| end; |
| end if; |
| end if; |
| end Reserve_Capacity; |
| |
| ---------------------- |
| -- Reverse_Elements -- |
| ---------------------- |
| |
| procedure Reverse_Elements (Container : in out Vector) is |
| begin |
| if Length (Container) <= 1 then |
| return; |
| end if; |
| |
| declare |
| I : Capacity_Range; |
| J : Capacity_Range; |
| E : Elements_Array renames |
| Elems (Container) (1 .. Length (Container)); |
| |
| begin |
| I := 1; |
| J := Length (Container); |
| while I < J loop |
| declare |
| EI : constant Holder := E (I); |
| |
| begin |
| E (I) := E (J); |
| E (J) := EI; |
| end; |
| |
| I := I + 1; |
| J := J - 1; |
| end loop; |
| end; |
| end Reverse_Elements; |
| |
| ------------------------ |
| -- Reverse_Find_Index -- |
| ------------------------ |
| |
| function Reverse_Find_Index |
| (Container : Vector; |
| Item : Element_Type; |
| Index : Index_Type := Index_Type'Last) return Extended_Index |
| is |
| Last : Index_Type'Base; |
| K : Count_Type'Base; |
| |
| begin |
| if Index > Last_Index (Container) then |
| Last := Last_Index (Container); |
| else |
| Last := Index; |
| end if; |
| |
| K := Capacity_Range (Int (Last) - Int (No_Index)); |
| for Indx in reverse Index_Type'First .. Last loop |
| if Get_Element (Container, K) = Item then |
| return Indx; |
| end if; |
| |
| K := K - 1; |
| end loop; |
| |
| return No_Index; |
| end Reverse_Find_Index; |
| |
| ---------- |
| -- Swap -- |
| ---------- |
| |
| procedure Swap |
| (Container : in out Vector; |
| I : Index_Type; |
| J : Index_Type) |
| is |
| begin |
| if I > Container.Last then |
| raise Constraint_Error with "I index is out of range"; |
| end if; |
| |
| if J > Container.Last then |
| raise Constraint_Error with "J index is out of range"; |
| end if; |
| |
| if I = J then |
| return; |
| end if; |
| |
| declare |
| II : constant Int'Base := Int (I) - Int (No_Index); |
| JJ : constant Int'Base := Int (J) - Int (No_Index); |
| |
| EI : Holder renames Elems (Container) (Capacity_Range (II)); |
| EJ : Holder renames Elems (Container) (Capacity_Range (JJ)); |
| |
| EI_Copy : constant Holder := EI; |
| |
| begin |
| EI := EJ; |
| EJ := EI_Copy; |
| end; |
| end Swap; |
| |
| -------------------- |
| -- To_Array_Index -- |
| -------------------- |
| |
| function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base is |
| Offset : Count_Type'Base; |
| |
| begin |
| -- We know that |
| -- Index >= Index_Type'First |
| -- hence we also know that |
| -- Index - Index_Type'First >= 0 |
| |
| -- The issue is that even though 0 is guaranteed to be a value in the |
| -- type Index_Type'Base, there's no guarantee that the difference is a |
| -- value in that type. To prevent overflow we use the wider of |
| -- Count_Type'Base and Index_Type'Base to perform intermediate |
| -- calculations. |
| |
| if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then |
| Offset := Count_Type'Base (Index - Index_Type'First); |
| |
| else |
| Offset := Count_Type'Base (Index) - |
| Count_Type'Base (Index_Type'First); |
| end if; |
| |
| -- The array index subtype for all container element arrays always |
| -- starts with 1. |
| |
| return 1 + Offset; |
| end To_Array_Index; |
| |
| --------------- |
| -- To_Vector -- |
| --------------- |
| |
| function To_Vector |
| (New_Item : Element_Type; |
| Length : Capacity_Range) return Vector |
| is |
| begin |
| if Length = 0 then |
| return Empty_Vector; |
| end if; |
| |
| declare |
| First : constant Int := Int (Index_Type'First); |
| Last_As_Int : constant Int'Base := First + Int (Length) - 1; |
| Last : Index_Type; |
| |
| begin |
| if Last_As_Int > Index_Type'Pos (Index_Type'Last) then |
| raise Constraint_Error with "Length is out of range"; -- ??? |
| end if; |
| |
| Last := Index_Type (Last_As_Int); |
| |
| return |
| (Capacity => Length, |
| Last => Last, |
| Elements_Ptr => <>, |
| Elements => [others => H (New_Item)]); |
| end; |
| end To_Vector; |
| |
| end Ada.Containers.Formal_Indefinite_Vectors; |
