1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT LIBRARY COMPONENTS                          --
4--                                                                          --
5--                 ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS                 --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9--             Copyright (C) 2014, Free Software Foundation, Inc.           --
10--                                                                          --
11-- This specification is derived from the Ada Reference Manual for use with --
12-- GNAT. The copyright notice above, and the license provisions that follow --
13-- apply solely to the  contents of the part following the private keyword. --
14--                                                                          --
15-- GNAT is free software;  you can  redistribute it  and/or modify it under --
16-- terms of the  GNU General Public License as published  by the Free Soft- --
17-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
18-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
19-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
20-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
21--                                                                          --
22-- As a special exception under Section 7 of GPL version 3, you are granted --
23-- additional permissions described in the GCC Runtime Library Exception,   --
24-- version 3.1, as published by the Free Software Foundation.               --
25--                                                                          --
26-- You should have received a copy of the GNU General Public License and    --
27-- a copy of the GCC Runtime Library Exception along with this program;     --
28-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
29-- <http://www.gnu.org/licenses/>.                                          --
30------------------------------------------------------------------------------
31
32--  Similar to Ada.Containers.Formal_Vectors. The main difference is that
33--  Element_Type may be indefinite (but not an unconstrained array). In
34--  addition, this is simplified by removing less-used functionality.
35
36with Ada.Containers.Bounded_Holders;
37with Ada.Containers.Formal_Vectors;
38
39generic
40   type Index_Type is range <>;
41   type Element_Type (<>) is private;
42   Max_Size_In_Storage_Elements : Natural :=
43                                    Element_Type'Max_Size_In_Storage_Elements;
44   --  This has the same meaning as in Ada.Containers.Bounded_Holders, with the
45   --  same restrictions.
46
47   with function "=" (Left, Right : Element_Type) return Boolean is <>;
48
49   Bounded : Boolean := True;
50   --  If True, the containers are bounded; the initial capacity is the maximum
51   --  size, and heap allocation will be avoided. If False, the containers can
52   --  grow via heap allocation.
53
54package Ada.Containers.Formal_Indefinite_Vectors with
55  SPARK_Mode => On
56is
57   pragma Annotate (GNATprove, External_Axiomatization);
58
59   subtype Extended_Index is Index_Type'Base
60   range Index_Type'First - 1 ..
61     Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
62
63   No_Index : constant Extended_Index := Extended_Index'First;
64
65   subtype Capacity_Range is
66     Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
67
68   type Vector (Capacity : Capacity_Range) is limited private with
69     Default_Initial_Condition;
70
71   function Empty_Vector return Vector;
72
73   function "=" (Left, Right : Vector) return Boolean with
74     Global => null;
75
76   function To_Vector
77     (New_Item : Element_Type;
78      Length   : Capacity_Range) return Vector
79   with
80     Global => null;
81
82   function Capacity (Container : Vector) return Capacity_Range with
83     Global => null,
84     Post   => Capacity'Result >= Container.Capacity;
85
86   procedure Reserve_Capacity
87     (Container : in out Vector;
88      Capacity  : Capacity_Range)
89   with
90     Global => null,
91     Pre    => (if Bounded then Capacity <= Container.Capacity);
92
93   function Length (Container : Vector) return Capacity_Range with
94     Global => null;
95
96   function Is_Empty (Container : Vector) return Boolean with
97     Global => null;
98
99   procedure Clear (Container : in out Vector) with
100     Global => null;
101   --  Note that this reclaims storage in the unbounded case. You need to call
102   --  this before a container goes out of scope in order to avoid storage
103   --  leaks.
104
105   procedure Assign (Target : in out Vector; Source : Vector) with
106     Global => null,
107     Pre    => (if Bounded then Length (Source) <= Target.Capacity);
108
109   function Copy
110     (Source   : Vector;
111      Capacity : Capacity_Range := 0) return Vector
112   with
113     Global => null,
114     Pre    => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity));
115
116   function Element
117     (Container : Vector;
118      Index     : Index_Type) return Element_Type
119   with
120     Global => null,
121     Pre    => Index in First_Index (Container) .. Last_Index (Container);
122
123   procedure Replace_Element
124     (Container : in out Vector;
125      Index     : Index_Type;
126      New_Item  : Element_Type)
127   with
128     Global => null,
129     Pre    => Index in First_Index (Container) .. Last_Index (Container);
130
131   procedure Append
132     (Container : in out Vector;
133      New_Item  : Vector)
134   with
135     Global => null,
136     Pre    => (if Bounded
137                then Length (Container) + Length (New_Item) <=
138                                                       Container.Capacity);
139
140   procedure Append
141     (Container : in out Vector;
142      New_Item  : Element_Type)
143   with
144     Global => null,
145     Pre    => (if Bounded
146                then Length (Container) < Container.Capacity);
147
148   procedure Delete_Last
149     (Container : in out Vector)
150   with
151     Global => null;
152
153   procedure Reverse_Elements (Container : in out Vector) with
154     Global => null;
155
156   procedure Swap (Container : in out Vector; I, J : Index_Type) with
157     Global => null,
158     Pre    => I in First_Index (Container) .. Last_Index (Container)
159      and then J in First_Index (Container) .. Last_Index (Container);
160
161   function First_Index (Container : Vector) return Index_Type with
162     Global => null;
163
164   function First_Element (Container : Vector) return Element_Type with
165     Global => null,
166     Pre    => not Is_Empty (Container);
167
168   function Last_Index (Container : Vector) return Extended_Index with
169     Global => null;
170
171   function Last_Element (Container : Vector) return Element_Type with
172     Global => null,
173     Pre    => not Is_Empty (Container);
174
175   function Find_Index
176     (Container : Vector;
177      Item      : Element_Type;
178      Index     : Index_Type := Index_Type'First) return Extended_Index
179   with
180     Global => null;
181
182   function Reverse_Find_Index
183     (Container : Vector;
184      Item      : Element_Type;
185      Index     : Index_Type := Index_Type'Last) return Extended_Index
186   with
187     Global => null;
188
189   function Contains
190     (Container : Vector;
191      Item      : Element_Type) return Boolean
192   with
193     Global => null;
194
195   function Has_Element
196     (Container : Vector; Position : Extended_Index) return Boolean with
197     Global => null;
198
199   generic
200      with function "<" (Left, Right : Element_Type) return Boolean is <>;
201   package Generic_Sorting is
202
203      function Is_Sorted (Container : Vector) return Boolean with
204        Global => null;
205
206      procedure Sort (Container : in out Vector) with
207        Global => null;
208
209   end Generic_Sorting;
210
211   function First_To_Previous
212     (Container : Vector;
213      Current : Index_Type) return Vector
214   with
215     Ghost,
216     Global => null;
217
218   function Current_To_Last
219     (Container : Vector;
220      Current : Index_Type) return Vector
221   with
222     Ghost,
223     Global => null;
224
225private
226   pragma SPARK_Mode (Off);
227
228   pragma Inline (First_Index);
229   pragma Inline (Last_Index);
230   pragma Inline (Element);
231   pragma Inline (First_Element);
232   pragma Inline (Last_Element);
233   pragma Inline (Replace_Element);
234   pragma Inline (Contains);
235
236   --  The implementation method is to instantiate Bounded_Holders to get a
237   --  definite type for Element_Type, and then use that Holder type to
238   --  instantiate Formal_Vectors. All the operations are just wrappers.
239
240   package Holders is new Bounded_Holders
241     (Element_Type, Max_Size_In_Storage_Elements, "=");
242   use Holders;
243
244   package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded);
245   use Def;
246
247   --  ????Assert that Def subtypes have the same range
248
249   type Vector (Capacity : Capacity_Range) is limited record
250      V : Def.Vector (Capacity);
251   end record;
252
253   function Empty_Vector return Vector is
254     ((Capacity => 0, V => Def.Empty_Vector));
255
256end Ada.Containers.Formal_Indefinite_Vectors;
257