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