gcc/ada/a-cofove.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --         A D A . C O N T A I N E R S . F O R M A L _ V E C T O R S        --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2004-2011, 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 --  This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada
  33 --  2012 RM. The modifications are to facilitate formal proofs by making it
  34 --  easier to express properties.
  35
  36 --  The modifications are:
  37
  38 --    A parameter for the container is added to every function reading the
  39 --    content of a container: Element, Next, Query_Element, Previous, Iterate,
  40 --    Has_Element, Reverse_Iterate. This change is motivated by the need
  41 --    to have cursors which are valid on different containers (typically a
  42 --    container C and its previous version C'Old) for expressing properties,
  43 --    which is not possible if cursors encapsulate an access to the underlying
  44 --    container.
  45
  46 --    There are two new functions:
  47
  48 --      function Left  (Container : Vector; Position : Cursor) return Vector;
  49 --      function Right (Container : Vector; Position : Cursor) return Vector;
  50
  51 --      Left returns a container containing all elements preceding Position
  52 --      (excluded) in Container. Right returns a container containing all
  53 --      elements following Position (included) in Container. These two new
  54 --      functions are useful to express invariant properties in loops which
  55 --      iterate over containers. Left returns the part of the container already
  56 --      scanned and Right the part not scanned yet.
  57
  58 private with Ada.Streams;
  59 with Ada.Containers;
  60 use Ada.Containers;
  61
  62 generic
  63    type Index_Type is range <>;
  64    type Element_Type is private;
  65
  66    with function "=" (Left, Right : Element_Type) return Boolean is <>;
  67
  68 package Ada.Containers.Formal_Vectors is
  69    pragma Pure;
  70
  71    subtype Extended_Index is Index_Type'Base
  72    range Index_Type'First - 1 ..
  73      Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
  74
  75    --  ??? i don't think we can do this...
  76    --  TODO: we need the ARG to either figure out how to declare this subtype,
  77    --  or eliminate the requirement that it be present.
  78    --  subtype Capacity_Subtype is Count_Type -- correct name???
  79    --  range 0 .. Count_Type'Max (0,
  80    --                             Index_Type'Pos (Index_Type'Last) -
  81    --                             Index_Type'Pos (Index_Type'First) + 1);
  82    --
  83    --  so for now:
  84    subtype Capacity_Subtype is Count_Type;
  85
  86    No_Index : constant Extended_Index := Extended_Index'First;
  87
  88    type Vector (Capacity : Capacity_Subtype) is tagged private;
  89    --  pragma Preelaborable_Initialization (Vector);
  90
  91    type Cursor is private;
  92    pragma Preelaborable_Initialization (Cursor);
  93
  94    Empty_Vector : constant Vector;
  95
  96    No_Element : constant Cursor;
  97
  98    function "=" (Left, Right : Vector) return Boolean;
  99
 100    function To_Vector (Length : Capacity_Subtype) return Vector;
 101
 102    function To_Vector
 103      (New_Item : Element_Type;
 104       Length   : Capacity_Subtype) return Vector;
 105
 106    function "&" (Left, Right : Vector) return Vector;
 107
 108    function "&" (Left : Vector; Right : Element_Type) return Vector;
 109
 110    function "&" (Left : Element_Type; Right : Vector) return Vector;
 111
 112    function "&" (Left, Right : Element_Type) return Vector;
 113
 114    function Capacity (Container : Vector) return Capacity_Subtype;
 115
 116    procedure Reserve_Capacity
 117      (Container : in out Vector;
 118       Capacity  : Capacity_Subtype);
 119
 120    function Length (Container : Vector) return Capacity_Subtype;
 121
 122    procedure Set_Length
 123      (Container : in out Vector;
 124       Length    : Capacity_Subtype);
 125
 126    function Is_Empty (Container : Vector) return Boolean;
 127
 128    procedure Clear (Container : in out Vector);
 129
 130    procedure Assign (Target : in out Vector; Source : Vector);
 131
 132    function Copy
 133      (Source   : Vector;
 134       Capacity : Capacity_Subtype := 0) return Vector;
 135
 136    function To_Cursor
 137      (Container : Vector;
 138       Index     : Extended_Index) return Cursor;
 139
 140    function To_Index (Position : Cursor) return Extended_Index;
 141
 142    function Element
 143      (Container : Vector;
 144       Index     : Index_Type) return Element_Type;
 145
 146    function Element
 147      (Container : Vector;
 148       Position  : Cursor) return Element_Type;
 149
 150    procedure Replace_Element
 151      (Container : in out Vector;
 152       Index     : Index_Type;
 153       New_Item  : Element_Type);
 154
 155    procedure Replace_Element
 156      (Container : in out Vector;
 157       Position  : Cursor;
 158       New_Item  : Element_Type);
 159
 160    procedure Query_Element
 161      (Container : Vector;
 162       Index     : Index_Type;
 163       Process   : not null access procedure (Element : Element_Type));
 164
 165    procedure Query_Element
 166      (Container : Vector;
 167       Position  : Cursor;
 168       Process   : not null access procedure (Element : Element_Type));
 169
 170    procedure Update_Element
 171      (Container : in out Vector;
 172       Index     : Index_Type;
 173       Process   : not null access procedure (Element : in out Element_Type));
 174
 175    procedure Update_Element
 176      (Container : in out Vector;
 177       Position  : Cursor;
 178       Process   : not null access procedure (Element : in out Element_Type));
 179
 180    procedure Move (Target : in out Vector; Source : in out Vector);
 181
 182    procedure Insert
 183      (Container : in out Vector;
 184       Before    : Extended_Index;
 185       New_Item  : Vector);
 186
 187    procedure Insert
 188      (Container : in out Vector;
 189       Before    : Cursor;
 190       New_Item  : Vector);
 191
 192    procedure Insert
 193      (Container : in out Vector;
 194       Before    : Cursor;
 195       New_Item  : Vector;
 196       Position  : out Cursor);
 197
 198    procedure Insert
 199      (Container : in out Vector;
 200       Before    : Extended_Index;
 201       New_Item  : Element_Type;
 202       Count     : Count_Type := 1);
 203
 204    procedure Insert
 205      (Container : in out Vector;
 206       Before    : Cursor;
 207       New_Item  : Element_Type;
 208       Count     : Count_Type := 1);
 209
 210    procedure Insert
 211      (Container : in out Vector;
 212       Before    : Cursor;
 213       New_Item  : Element_Type;
 214       Position  : out Cursor;
 215       Count     : Count_Type := 1);
 216
 217    procedure Insert
 218      (Container : in out Vector;
 219       Before    : Extended_Index;
 220       Count     : Count_Type := 1);
 221
 222    procedure Insert
 223      (Container : in out Vector;
 224       Before    : Cursor;
 225       Position  : out Cursor;
 226       Count     : Count_Type := 1);
 227
 228    procedure Prepend
 229      (Container : in out Vector;
 230       New_Item  : Vector);
 231
 232    procedure Prepend
 233      (Container : in out Vector;
 234       New_Item  : Element_Type;
 235       Count     : Count_Type := 1);
 236
 237    procedure Append
 238      (Container : in out Vector;
 239       New_Item  : Vector);
 240
 241    procedure Append
 242      (Container : in out Vector;
 243       New_Item  : Element_Type;
 244       Count     : Count_Type := 1);
 245
 246    procedure Insert_Space
 247      (Container : in out Vector;
 248       Before    : Extended_Index;
 249       Count     : Count_Type := 1);
 250
 251    procedure Insert_Space
 252      (Container : in out Vector;
 253       Before    : Cursor;
 254       Position  : out Cursor;
 255       Count     : Count_Type := 1);
 256
 257    procedure Delete
 258      (Container : in out Vector;
 259       Index     : Extended_Index;
 260       Count     : Count_Type := 1);
 261
 262    procedure Delete
 263      (Container : in out Vector;
 264       Position  : in out Cursor;
 265       Count     : Count_Type := 1);
 266
 267    procedure Delete_First
 268      (Container : in out Vector;
 269       Count     : Count_Type := 1);
 270
 271    procedure Delete_Last
 272      (Container : in out Vector;
 273       Count     : Count_Type := 1);
 274
 275    procedure Reverse_Elements (Container : in out Vector);
 276
 277    procedure Swap (Container : in out Vector; I, J : Index_Type);
 278
 279    procedure Swap (Container : in out Vector; I, J : Cursor);
 280
 281    function First_Index (Container : Vector) return Index_Type;
 282
 283    function First (Container : Vector) return Cursor;
 284
 285    function First_Element (Container : Vector) return Element_Type;
 286
 287    function Last_Index (Container : Vector) return Extended_Index;
 288
 289    function Last (Container : Vector) return Cursor;
 290
 291    function Last_Element (Container : Vector) return Element_Type;
 292
 293    function Next (Container : Vector; Position : Cursor) return Cursor;
 294
 295    procedure Next (Container : Vector; Position : in out Cursor);
 296
 297    function Previous (Container : Vector; Position : Cursor) return Cursor;
 298
 299    procedure Previous (Container : Vector; Position : in out Cursor);
 300
 301    function Find_Index
 302      (Container : Vector;
 303       Item      : Element_Type;
 304       Index     : Index_Type := Index_Type'First) return Extended_Index;
 305
 306    function Find
 307      (Container : Vector;
 308       Item      : Element_Type;
 309       Position  : Cursor := No_Element) return Cursor;
 310
 311    function Reverse_Find_Index
 312      (Container : Vector;
 313       Item      : Element_Type;
 314       Index     : Index_Type := Index_Type'Last) return Extended_Index;
 315
 316    function Reverse_Find
 317      (Container : Vector;
 318       Item      : Element_Type;
 319       Position  : Cursor := No_Element) return Cursor;
 320
 321    function Contains
 322      (Container : Vector;
 323       Item      : Element_Type) return Boolean;
 324
 325    function Has_Element (Container : Vector; Position : Cursor) return Boolean;
 326
 327    procedure Iterate
 328      (Container : Vector;
 329       Process   : not null access
 330                     procedure (Container : Vector; Position : Cursor));
 331
 332    procedure Reverse_Iterate
 333      (Container : Vector;
 334       Process   : not null access
 335                     procedure (Container : Vector; Position : Cursor));
 336
 337    generic
 338       with function "<" (Left, Right : Element_Type) return Boolean is <>;
 339    package Generic_Sorting is
 340
 341       function Is_Sorted (Container : Vector) return Boolean;
 342
 343       procedure Sort (Container : in out Vector);
 344
 345       procedure Merge (Target : in out Vector; Source : in out Vector);
 346
 347    end Generic_Sorting;
 348
 349    function Left (Container : Vector; Position : Cursor) return Vector;
 350
 351    function Right (Container : Vector; Position : Cursor) return Vector;
 352
 353 private
 354
 355    pragma Inline (First_Index);
 356    pragma Inline (Last_Index);
 357    pragma Inline (Element);
 358    pragma Inline (First_Element);
 359    pragma Inline (Last_Element);
 360    pragma Inline (Query_Element);
 361    pragma Inline (Update_Element);
 362    pragma Inline (Replace_Element);
 363    pragma Inline (Contains);
 364    pragma Inline (Next);
 365    pragma Inline (Previous);
 366
 367    type Elements_Array is array (Count_Type range <>) of Element_Type;
 368    function "=" (L, R : Elements_Array) return Boolean is abstract;
 369
 370    type Vector (Capacity : Capacity_Subtype) is tagged record
 371       Elements : Elements_Array (1 .. Capacity);
 372       Last     : Extended_Index := No_Index;
 373       Busy     : Natural := 0;
 374       Lock     : Natural := 0;
 375    end record;
 376
 377    use Ada.Streams;
 378
 379    procedure Write
 380      (Stream    : not null access Root_Stream_Type'Class;
 381       Container : Vector);
 382
 383    for Vector'Write use Write;
 384
 385    procedure Read
 386      (Stream    : not null access Root_Stream_Type'Class;
 387       Container : out Vector);
 388
 389    for Vector'Read use Read;
 390
 391    type Cursor is record
 392       Valid : Boolean    := True;
 393       Index : Index_Type := Index_Type'First;
 394    end record;
 395
 396    procedure Write
 397      (Stream   : not null access Root_Stream_Type'Class;
 398       Position : Cursor);
 399
 400    for Cursor'Write use Write;
 401
 402    procedure Read
 403      (Stream   : not null access Root_Stream_Type'Class;
 404       Position : out Cursor);
 405
 406    for Cursor'Read use Read;
 407
 408    Empty_Vector : constant Vector := (Capacity => 0, others => <>);
 409
 410    No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
 411
 412 end Ada.Containers.Formal_Vectors;