1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT LIBRARY COMPONENTS                          --
4--                                                                          --
5--                 ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS                 --
6--                                                                          --
7--                                 S p e c                                  --
8--                                                                          --
9--          Copyright (C) 2014-2015, 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   --  Maximum size of Vector elements in bytes. This has the same meaning as
45   --  in Ada.Containers.Bounded_Holders, with the same restrictions. Note that
46   --  setting this too small can lead to erroneous execution; see comments in
47   --  Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the
48   --  responsibility of clients to calculate the maximum size of all types in
49   --  the class.
50
51   with function "=" (Left, Right : Element_Type) return Boolean is <>;
52
53   Bounded : Boolean := True;
54   --  If True, the containers are bounded; the initial capacity is the maximum
55   --  size, and heap allocation will be avoided. If False, the containers can
56   --  grow via heap allocation.
57
58package Ada.Containers.Formal_Indefinite_Vectors with
59  SPARK_Mode => On
60is
61   pragma Annotate (GNATprove, External_Axiomatization);
62   pragma Annotate (CodePeer, Skip_Analysis);
63
64   subtype Extended_Index is Index_Type'Base
65   range Index_Type'First - 1 ..
66     Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
67
68   No_Index : constant Extended_Index := Extended_Index'First;
69
70   subtype Capacity_Range is
71     Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
72
73   type Vector (Capacity : Capacity_Range) is limited private with
74     Default_Initial_Condition;
75
76   function Empty_Vector return Vector;
77
78   function "=" (Left, Right : Vector) return Boolean with
79     Global => null;
80
81   function To_Vector
82     (New_Item : Element_Type;
83      Length   : Capacity_Range) return Vector
84   with
85     Global => null;
86
87   function Capacity (Container : Vector) return Capacity_Range with
88     Global => null,
89     Post   => Capacity'Result >= Container.Capacity;
90
91   procedure Reserve_Capacity
92     (Container : in out Vector;
93      Capacity  : Capacity_Range)
94   with
95     Global => null,
96     Pre    => (if Bounded then Capacity <= Container.Capacity);
97
98   function Length (Container : Vector) return Capacity_Range with
99     Global => null;
100
101   function Is_Empty (Container : Vector) return Boolean with
102     Global => null;
103
104   procedure Clear (Container : in out Vector) with
105     Global => null;
106   --  Note that this reclaims storage in the unbounded case. You need to call
107   --  this before a container goes out of scope in order to avoid storage
108   --  leaks.
109
110   procedure Assign (Target : in out Vector; Source : Vector) with
111     Global => null,
112     Pre    => (if Bounded then Length (Source) <= Target.Capacity);
113
114   function Copy
115     (Source   : Vector;
116      Capacity : Capacity_Range := 0) return Vector
117   with
118     Global => null,
119     Pre    => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity));
120
121   function Element
122     (Container : Vector;
123      Index     : Index_Type) return Element_Type
124   with
125     Global => null,
126     Pre    => Index in First_Index (Container) .. Last_Index (Container);
127
128   procedure Replace_Element
129     (Container : in out Vector;
130      Index     : Index_Type;
131      New_Item  : Element_Type)
132   with
133     Global => null,
134     Pre    => Index in First_Index (Container) .. Last_Index (Container);
135
136   procedure Append
137     (Container : in out Vector;
138      New_Item  : Vector)
139   with
140     Global => null,
141     Pre    => (if Bounded
142                then Length (Container) + Length (New_Item) <=
143                                                       Container.Capacity);
144
145   procedure Append
146     (Container : in out Vector;
147      New_Item  : Element_Type)
148   with
149     Global => null,
150     Pre    => (if Bounded
151                then Length (Container) < Container.Capacity);
152
153   procedure Delete_Last
154     (Container : in out Vector)
155   with
156     Global => null;
157
158   procedure Reverse_Elements (Container : in out Vector) with
159     Global => null;
160
161   procedure Swap (Container : in out Vector; I, J : Index_Type) with
162     Global => null,
163     Pre    => I in First_Index (Container) .. Last_Index (Container)
164      and then J in First_Index (Container) .. Last_Index (Container);
165
166   function First_Index (Container : Vector) return Index_Type with
167     Global => null;
168
169   function First_Element (Container : Vector) return Element_Type with
170     Global => null,
171     Pre    => not Is_Empty (Container);
172
173   function Last_Index (Container : Vector) return Extended_Index with
174     Global => null;
175
176   function Last_Element (Container : Vector) return Element_Type with
177     Global => null,
178     Pre    => not Is_Empty (Container);
179
180   function Find_Index
181     (Container : Vector;
182      Item      : Element_Type;
183      Index     : Index_Type := Index_Type'First) return Extended_Index
184   with
185     Global => null;
186
187   function Reverse_Find_Index
188     (Container : Vector;
189      Item      : Element_Type;
190      Index     : Index_Type := Index_Type'Last) return Extended_Index
191   with
192     Global => null;
193
194   function Contains
195     (Container : Vector;
196      Item      : Element_Type) return Boolean
197   with
198     Global => null;
199
200   function Has_Element
201     (Container : Vector; Position : Extended_Index) return Boolean with
202     Global => null;
203
204   generic
205      with function "<" (Left, Right : Element_Type) return Boolean is <>;
206   package Generic_Sorting with SPARK_Mode is
207
208      function Is_Sorted (Container : Vector) return Boolean with
209        Global => null;
210
211      procedure Sort (Container : in out Vector) with
212        Global => null;
213
214   end Generic_Sorting;
215
216   function First_To_Previous
217     (Container : Vector;
218      Current : Index_Type) return Vector
219   with
220     Ghost,
221     Global => null;
222
223   function Current_To_Last
224     (Container : Vector;
225      Current : Index_Type) return Vector
226   with
227     Ghost,
228     Global => null;
229
230private
231   pragma SPARK_Mode (Off);
232
233   pragma Inline (First_Index);
234   pragma Inline (Last_Index);
235   pragma Inline (Element);
236   pragma Inline (First_Element);
237   pragma Inline (Last_Element);
238   pragma Inline (Replace_Element);
239   pragma Inline (Contains);
240
241   --  The implementation method is to instantiate Bounded_Holders to get a
242   --  definite type for Element_Type, and then use that Holder type to
243   --  instantiate Formal_Vectors. All the operations are just wrappers.
244
245   package Holders is new Bounded_Holders
246     (Element_Type, Max_Size_In_Storage_Elements, "=");
247   use Holders;
248
249   package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded);
250   use Def;
251
252   --  ????Assert that Def subtypes have the same range
253
254   type Vector (Capacity : Capacity_Range) is limited record
255      V : Def.Vector (Capacity);
256   end record;
257
258   function Empty_Vector return Vector is
259     ((Capacity => 0, V => Def.Empty_Vector));
260
261end Ada.Containers.Formal_Indefinite_Vectors;
262