1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2014-2015, 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 28package body Ada.Containers.Formal_Indefinite_Vectors with 29 SPARK_Mode => Off 30is 31 32 function H (New_Item : Element_Type) return Holder renames To_Holder; 33 function E (Container : Holder) return Element_Type renames Get; 34 35 --------- 36 -- "=" -- 37 --------- 38 39 function "=" (Left, Right : Vector) return Boolean is 40 (Left.V = Right.V); 41 42 ------------ 43 -- Append -- 44 ------------ 45 46 procedure Append (Container : in out Vector; New_Item : Vector) is 47 begin 48 Append (Container.V, New_Item.V); 49 end Append; 50 51 procedure Append 52 (Container : in out Vector; 53 New_Item : Element_Type) 54 is 55 begin 56 Append (Container.V, H (New_Item)); 57 end Append; 58 59 ------------ 60 -- Assign -- 61 ------------ 62 63 procedure Assign (Target : in out Vector; Source : Vector) is 64 begin 65 Assign (Target.V, Source.V); 66 end Assign; 67 68 -------------- 69 -- Capacity -- 70 -------------- 71 72 function Capacity (Container : Vector) return Capacity_Range is 73 (Capacity (Container.V)); 74 75 ----------- 76 -- Clear -- 77 ----------- 78 79 procedure Clear (Container : in out Vector) is 80 begin 81 Clear (Container.V); 82 end Clear; 83 84 -------------- 85 -- Contains -- 86 -------------- 87 88 function Contains 89 (Container : Vector; 90 Item : Element_Type) return Boolean 91 is 92 (Contains (Container.V, H (Item))); 93 94 ---------- 95 -- Copy -- 96 ---------- 97 98 function Copy 99 (Source : Vector; 100 Capacity : Capacity_Range := 0) return Vector 101 is 102 ((if Capacity = 0 then Length (Source) else Capacity), 103 V => Copy (Source.V, Capacity)); 104 105 --------------------- 106 -- Current_To_Last -- 107 --------------------- 108 109 function Current_To_Last 110 (Container : Vector; 111 Current : Index_Type) return Vector is 112 begin 113 return (Length (Container), Current_To_Last (Container.V, Current)); 114 end Current_To_Last; 115 116 ----------------- 117 -- Delete_Last -- 118 ----------------- 119 120 procedure Delete_Last 121 (Container : in out Vector) 122 is 123 begin 124 Delete_Last (Container.V); 125 end Delete_Last; 126 127 ------------- 128 -- Element -- 129 ------------- 130 131 function Element 132 (Container : Vector; 133 Index : Index_Type) return Element_Type is 134 (E (Element (Container.V, Index))); 135 136 ---------------- 137 -- Find_Index -- 138 ---------------- 139 140 function Find_Index 141 (Container : Vector; 142 Item : Element_Type; 143 Index : Index_Type := Index_Type'First) return Extended_Index 144 is 145 (Find_Index (Container.V, H (Item), Index)); 146 147 ------------------- 148 -- First_Element -- 149 ------------------- 150 151 function First_Element (Container : Vector) return Element_Type is 152 (E (First_Element (Container.V))); 153 154 ----------------- 155 -- First_Index -- 156 ----------------- 157 158 function First_Index (Container : Vector) return Index_Type is 159 (First_Index (Container.V)); 160 161 ----------------------- 162 -- First_To_Previous -- 163 ----------------------- 164 165 function First_To_Previous 166 (Container : Vector; 167 Current : Index_Type) return Vector is 168 begin 169 return (Length (Container), First_To_Previous (Container.V, Current)); 170 end First_To_Previous; 171 172 --------------------- 173 -- Generic_Sorting -- 174 --------------------- 175 176 package body Generic_Sorting with SPARK_Mode => Off is 177 178 function "<" (X, Y : Holder) return Boolean is (E (X) < E (Y)); 179 package Def_Sorting is new Def.Generic_Sorting ("<"); 180 use Def_Sorting; 181 182 --------------- 183 -- Is_Sorted -- 184 --------------- 185 186 function Is_Sorted (Container : Vector) return Boolean is 187 (Is_Sorted (Container.V)); 188 189 ---------- 190 -- Sort -- 191 ---------- 192 193 procedure Sort (Container : in out Vector) is 194 begin 195 Sort (Container.V); 196 end Sort; 197 198 end Generic_Sorting; 199 200 ----------------- 201 -- Has_Element -- 202 ----------------- 203 204 function Has_Element 205 (Container : Vector; 206 Position : Extended_Index) return Boolean 207 is 208 (Has_Element (Container.V, Position)); 209 210 -------------- 211 -- Is_Empty -- 212 -------------- 213 214 function Is_Empty (Container : Vector) return Boolean is 215 (Is_Empty (Container.V)); 216 217 ------------------ 218 -- Last_Element -- 219 ------------------ 220 221 function Last_Element (Container : Vector) return Element_Type is 222 (E (Last_Element (Container.V))); 223 224 ---------------- 225 -- Last_Index -- 226 ---------------- 227 228 function Last_Index (Container : Vector) return Extended_Index is 229 (Last_Index (Container.V)); 230 231 ------------ 232 -- Length -- 233 ------------ 234 235 function Length (Container : Vector) return Capacity_Range is 236 (Length (Container.V)); 237 238 --------------------- 239 -- Replace_Element -- 240 --------------------- 241 242 procedure Replace_Element 243 (Container : in out Vector; 244 Index : Index_Type; 245 New_Item : Element_Type) 246 is 247 begin 248 Replace_Element (Container.V, Index, H (New_Item)); 249 end Replace_Element; 250 251 ---------------------- 252 -- Reserve_Capacity -- 253 ---------------------- 254 255 procedure Reserve_Capacity 256 (Container : in out Vector; 257 Capacity : Capacity_Range) 258 is 259 begin 260 Reserve_Capacity (Container.V, Capacity); 261 end Reserve_Capacity; 262 263 ---------------------- 264 -- Reverse_Elements -- 265 ---------------------- 266 267 procedure Reverse_Elements (Container : in out Vector) is 268 begin 269 Reverse_Elements (Container.V); 270 end Reverse_Elements; 271 272 ------------------------ 273 -- Reverse_Find_Index -- 274 ------------------------ 275 276 function Reverse_Find_Index 277 (Container : Vector; 278 Item : Element_Type; 279 Index : Index_Type := Index_Type'Last) return Extended_Index 280 is 281 (Reverse_Find_Index (Container.V, H (Item), Index)); 282 283 ---------- 284 -- Swap -- 285 ---------- 286 287 procedure Swap (Container : in out Vector; I, J : Index_Type) is 288 begin 289 Swap (Container.V, I, J); 290 end Swap; 291 292 --------------- 293 -- To_Vector -- 294 --------------- 295 296 function To_Vector 297 (New_Item : Element_Type; 298 Length : Capacity_Range) return Vector 299 is 300 begin 301 return (Length, To_Vector (H (New_Item), Length)); 302 end To_Vector; 303 304end Ada.Containers.Formal_Indefinite_Vectors; 305