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