gcc/ada/a-cofuve.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --                    ADA.CONTAINERS.FUNCTIONAL_VECTORS                     --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2016-2017, 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 pragma Ada_2012;
  33 private with Ada.Containers.Functional_Base;
  34
  35 generic
  36    type Index_Type is (<>);
  37    --  To avoid Constraint_Error being raised at run time, Index_Type'Base
  38    --  should have at least one more element at the low end than Index_Type.
  39
  40    type Element_Type (<>) is private;
  41 package Ada.Containers.Functional_Vectors with SPARK_Mode is
  42
  43    subtype Extended_Index is Index_Type'Base range
  44      Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
  45    --  Index_Type with one more element at the low end of the range.
  46    --  This type is never used but it forces GNATprove to check that there is
  47    --  room for one more element at the low end of Index_Type.
  48
  49    type Sequence is private
  50      with Default_Initial_Condition => Length (Sequence) = 0,
  51      Iterable => (First       => Iter_First,
  52                   Has_Element => Iter_Has_Element,
  53                   Next        => Iter_Next,
  54                   Element     => Get);
  55    --  Sequences are empty when default initialized.
  56    --  Quantification over sequences can be done using the regular
  57    --  quantification over its range or directly on its elements with "for of".
  58
  59    -----------------------
  60    --  Basic operations --
  61    -----------------------
  62
  63    --  Sequences are axiomatized using Length and Get, providing respectively
  64    --  the length of a sequence and an accessor to its Nth element:
  65
  66    function Length (Container : Sequence) return Count_Type with
  67    --  Length of a sequence
  68
  69      Global => null,
  70      Post   =>
  71        (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
  72           Index_Type'Pos (Index_Type'Last);
  73
  74    function Get
  75      (Container : Sequence;
  76       Position  : Extended_Index) return Element_Type
  77    --  Access the Element at position Position in Container
  78
  79    with
  80      Global => null,
  81      Pre    => Position in Index_Type'First .. Last (Container);
  82
  83    function Last (Container : Sequence) return Extended_Index with
  84    --  Last index of a sequence
  85
  86      Global => null,
  87      Post =>
  88        Last'Result =
  89          Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1)
  90                          + Length (Container));
  91    pragma Annotate (GNATprove, Inline_For_Proof, Last);
  92
  93    function First return Extended_Index is (Index_Type'First);
  94    --  First index of a sequence
  95
  96    ------------------------
  97    -- Property Functions --
  98    ------------------------
  99
 100    function "=" (Left : Sequence; Right : Sequence) return Boolean with
 101    --  Extensional equality over sequences
 102
 103      Global => null,
 104      Post   =>
 105        "="'Result =
 106          (Length (Left) = Length (Right)
 107           and then (for all N in Index_Type'First .. Last (Left) =>
 108               Get (Left, N) = Get (Right, N)));
 109    pragma Annotate (GNATprove, Inline_For_Proof, "=");
 110
 111    function "<" (Left : Sequence; Right : Sequence) return Boolean with
 112    --  Left is a strict subsequence of Right
 113
 114      Global => null,
 115      Post   =>
 116        "<"'Result =
 117          (Length (Left) < Length (Right)
 118           and then (for all N in Index_Type'First .. Last (Left) =>
 119               Get (Left, N) = Get (Right, N)));
 120    pragma Annotate (GNATprove, Inline_For_Proof, "<");
 121
 122    function "<=" (Left : Sequence; Right : Sequence) return Boolean with
 123    --  Left is a subsequence of Right
 124
 125      Global => null,
 126      Post   =>
 127        "<="'Result =
 128          (Length (Left) <= Length (Right)
 129           and then (for all N in Index_Type'First .. Last (Left) =>
 130               Get (Left, N) = Get (Right, N)));
 131    pragma Annotate (GNATprove, Inline_For_Proof, "<=");
 132
 133    function Contains
 134      (Container : Sequence;
 135       Fst       : Index_Type;
 136       Lst       : Extended_Index;
 137       Item      : Element_Type)
 138          return Boolean
 139    --  Returns True if Item occurs in the range from Fst to Lst of Container
 140
 141    with
 142      Global => null,
 143      Pre    => Lst <= Last (Container),
 144      Post   =>
 145        Contains'Result =
 146          (for some I in Fst .. Lst => Get (Container, I) = Item);
 147    pragma Annotate (GNATprove, Inline_For_Proof, Contains);
 148
 149    function Constant_Range
 150      (Container : Sequence;
 151       Fst       : Index_Type;
 152       Lst       : Extended_Index;
 153       Item      : Element_Type)
 154          return Boolean
 155    --  Returns True if every element of the range from Fst to Lst of Container
 156    --  is equal to Item.
 157
 158    with
 159      Global => null,
 160      Pre    => Lst <= Last (Container),
 161      Post   =>
 162        Constant_Range'Result =
 163          (for all I in Fst .. Lst => Get (Container, I) = Item);
 164    pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range);
 165
 166    function Equal_Except
 167      (Left     : Sequence;
 168       Right    : Sequence;
 169       Position : Index_Type) return Boolean
 170    --  Returns True is Left and Right are the same except at position Position
 171
 172    with
 173      Global => null,
 174      Pre    => Position <= Last (Left),
 175      Post   =>
 176        Equal_Except'Result =
 177          (Length (Left) = Length (Right)
 178           and then (for all I in Index_Type'First .. Last (Left) =>
 179               (if I /= Position then Get (Left, I) = Get (Right, I))));
 180    pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
 181
 182    function Equal_Except
 183      (Left  : Sequence;
 184       Right : Sequence;
 185       X, Y  : Index_Type) return Boolean
 186    --  Returns True is Left and Right are the same except at positions X and Y
 187
 188    with
 189      Global => null,
 190      Pre    => X <= Last (Left) and Y <= Last (Left),
 191      Post   =>
 192        Equal_Except'Result =
 193          (Length (Left) = Length (Right)
 194           and then (for all I in Index_Type'First .. Last (Left) =>
 195               (if I /= X and I /= Y then Get (Left, I) = Get (Right, I))));
 196    pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
 197
 198    function Range_Equal
 199      (Left  : Sequence;
 200       Right : Sequence;
 201       Fst   : Index_Type;
 202       Lst   : Extended_Index) return Boolean
 203    --  Returns True if the ranges from Fst to Lst contain the same elements in
 204    --  Left and Right.
 205
 206    with
 207      Global => null,
 208      Pre    => Lst <= Last (Left) and Lst <= Last (Right),
 209      Post   =>
 210        Range_Equal'Result =
 211          (for all I in Fst .. Lst => Get (Left, I) = Get (Right, I));
 212    pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal);
 213
 214    function Range_Shifted
 215      (Left   : Sequence;
 216       Right  : Sequence;
 217       Fst    : Index_Type;
 218       Lst    : Extended_Index;
 219       Offset : Count_Type'Base) return Boolean
 220    --  Returns True if the range from Fst to Lst in Left contains the same
 221    --  elements as the range from Fst + Offset to Lst + Offset in Right.
 222
 223    with
 224      Global => null,
 225      Pre    => Lst <= Last (Left)
 226            and Offset in
 227               Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
 228                    (Index_Type'Pos (Index_Type'First) - 1)
 229                   + Length (Right) - Index_Type'Pos (Lst),
 230      Post   =>
 231        Range_Shifted'Result =
 232          ((for all I in Fst .. Lst =>
 233                    Get (Left, I)
 234            = Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)))
 235           and
 236             (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) ..
 237                Index_Type'Val (Index_Type'Pos (Lst) + Offset) =>
 238                  Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset))
 239              = Get (Right, I)));
 240    pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
 241
 242    ----------------------------
 243    -- Construction Functions --
 244    ----------------------------
 245
 246    --  For better efficiency of both proofs and execution, avoid using
 247    --  construction functions in annotations and rather use property functions.
 248
 249    function Set
 250      (Container : Sequence;
 251       Position  : Index_Type;
 252       New_Item  : Element_Type) return Sequence
 253    --  Returns a new sequence which contains the same elements as Container
 254    --  except for the one at position Position which is replaced by New_Item.
 255
 256    with
 257      Global => null,
 258      Pre    => Position in Index_Type'First .. Last (Container),
 259      Post   => Get (Set'Result, Position) = New_Item
 260      and then Equal_Except (Container, Set'Result, Position);
 261
 262    function Add (Container : Sequence; New_Item : Element_Type) return Sequence
 263    --  Returns a new sequence which contains the same elements as Container
 264    --  plus New_Item at the end.
 265
 266    with
 267      Global => null,
 268      Pre    =>
 269        Length (Container) < Count_Type'Last
 270          and then Last (Container) < Index_Type'Last,
 271      Post   =>
 272        Length (Add'Result) = Length (Container) + 1
 273          and then Get (Add'Result, Last (Add'Result)) = New_Item
 274          and then Container <= Add'Result;
 275
 276    function Add
 277      (Container : Sequence;
 278       Position  : Index_Type;
 279       New_Item  : Element_Type) return Sequence
 280    with
 281    --  Returns a new sequence which contains the same elements as Container
 282    --  except that New_Item has been inserted at position Position.
 283
 284      Global => null,
 285      Pre    =>
 286        Length (Container) < Count_Type'Last
 287          and then Last (Container) < Index_Type'Last
 288          and then Position <= Extended_Index'Succ (Last (Container)),
 289      Post   =>
 290        Length (Add'Result) = Length (Container) + 1
 291          and then Get (Add'Result, Position) = New_Item
 292          and then
 293             Range_Equal (Left  => Container,
 294                          Right =>  Add'Result,
 295                          Fst   => Index_Type'First,
 296                          Lst   => Index_Type'Pred (Position))
 297          and then
 298             Range_Shifted (Left   => Container,
 299                            Right  => Add'Result,
 300                            Fst    => Position,
 301                            Lst    => Last (Container),
 302                            Offset => 1);
 303
 304    function Remove
 305      (Container : Sequence;
 306       Position : Index_Type) return Sequence
 307    --  Returns a new sequence which contains the same elements as Container
 308    --  except that the element at position Position has been removed.
 309
 310    with
 311      Global => null,
 312      Pre    =>
 313        Length (Container) < Count_Type'Last
 314          and Last (Container) < Index_Type'Last
 315          and Position in Index_Type'First .. Last (Container),
 316      Post   =>
 317        Length (Remove'Result) = Length (Container) - 1
 318          and then
 319             Range_Equal (Left  => Container,
 320                          Right => Remove'Result,
 321                          Fst   => Index_Type'First,
 322                          Lst   => Index_Type'Pred (Position))
 323          and then
 324             Range_Shifted (Left   => Remove'Result,
 325                            Right  => Container,
 326                            Fst    => Position,
 327                            Lst    => Last (Remove'Result),
 328                            Offset => 1);
 329
 330    ---------------------------
 331    --  Iteration Primitives --
 332    ---------------------------
 333
 334    function Iter_First (Container : Sequence) return Extended_Index with
 335      Global => null;
 336
 337    function Iter_Has_Element
 338      (Container : Sequence;
 339       Position  : Extended_Index) return Boolean
 340    with
 341      Global => null,
 342      Post   => Iter_Has_Element'Result =
 343          (Position in Index_Type'First .. Last (Container));
 344    pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
 345
 346    function Iter_Next
 347      (Container : Sequence;
 348       Position  : Extended_Index) return Extended_Index
 349    with
 350      Global => null,
 351      Pre    => Iter_Has_Element (Container, Position);
 352
 353 private
 354
 355    pragma SPARK_Mode (Off);
 356
 357    package Containers is new Ada.Containers.Functional_Base
 358      (Index_Type   => Index_Type,
 359       Element_Type => Element_Type);
 360
 361    type Sequence is record
 362       Content : Containers.Container;
 363    end record;
 364
 365    function Iter_First (Container : Sequence) return Extended_Index is
 366      (Index_Type'First);
 367    function Iter_Next
 368      (Container : Sequence;
 369       Position  : Extended_Index) return Extended_Index
 370    is
 371      (if Position = Extended_Index'Last then Extended_Index'First
 372       else Extended_Index'Succ (Position));
 373
 374    function Iter_Has_Element
 375      (Container : Sequence;
 376       Position  : Extended_Index) return Boolean
 377    is
 378      (Position in Index_Type'First ..
 379         (Index_Type'Val
 380            ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container))));
 381
 382 end Ada.Containers.Functional_Vectors;