Add a new unbounded functional sequence. This sequence is indexed by
Big_Positive and so is unbounded from the user and spark points view.
Hower the actually implemented sequence are bounded by Count_Type'Last.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-cfinse.adb, libgnat/a-cfinse.ads: Implementation
files of the sequence.
* Makefile.rtl, impunit.adb: Take into account the add of the
new filesdiff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
--- a/gcc/ada/Makefile.rtl
+++ b/gcc/ada/Makefile.rtl
@@ -114,6 +114,7 @@ GNATRTL_NONTASKING_OBJS= \
a-cfhama$(objext) \
a-cfhase$(objext) \
a-cfinve$(objext) \
+ a-cfinse$(objext) \
a-cforma$(objext) \
a-cforse$(objext) \
a-cgaaso$(objext) \
diff --git a/gcc/ada/impunit.adb b/gcc/ada/impunit.adb
--- a/gcc/ada/impunit.adb
+++ b/gcc/ada/impunit.adb
@@ -605,6 +605,7 @@ package body Impunit is
-- GNAT Defined Additions to Ada 2012 --
----------------------------------------
+ ("a-cfinse", F), -- Ada.Containers.Functional_Infinite_Sequences
("a-cfinve", F), -- Ada.Containers.Formal_Indefinite_Vectors
("a-coboho", F), -- Ada.Containers.Bounded_Holders
("a-cofove", F), -- Ada.Containers.Formal_Vectors
diff --git /dev/null b/gcc/ada/libgnat/a-cfinse.adb
new file mode 100644
--- /dev/null
+++ b/gcc/ada/libgnat/a-cfinse.adb
@@ -0,0 +1,304 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- ADA.CONTAINERS.FUNCTIONAL_INFINITE_SEQUENCE --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2022-2022, Free Software Foundation, Inc. --
+-- --
+-- This specification is derived from the Ada Reference Manual for use with --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the contents of the part following the private keyword. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+pragma Ada_2012;
+
+package body Ada.Containers.Functional_Infinite_Sequences
+with SPARK_Mode => Off
+is
+ use Containers;
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ package Big_From_Count is new Signed_Conversions
+ (Int => Count_Type);
+
+ function Big (C : Count_Type) return Big_Integer renames
+ Big_From_Count.To_Big_Integer;
+
+ -- Store Count_Type'Last as a Big Natural because it is often used
+
+ Count_Type_Big_Last : constant Big_Natural := Big (Count_Type'Last);
+
+ function To_Count (C : Big_Natural) return Count_Type;
+ -- Convert Big_Natural to Count_Type
+
+ ---------
+ -- "<" --
+ ---------
+
+ function "<" (Left : Sequence; Right : Sequence) return Boolean is
+ (Length (Left) < Length (Right)
+ and then (for all N in Left =>
+ Get (Left, N) = Get (Right, N)));
+
+ ----------
+ -- "<=" --
+ ----------
+
+ function "<=" (Left : Sequence; Right : Sequence) return Boolean is
+ (Length (Left) <= Length (Right)
+ and then (for all N in Left =>
+ Get (Left, N) = Get (Right, N)));
+
+ ---------
+ -- "=" --
+ ---------
+
+ function "=" (Left : Sequence; Right : Sequence) return Boolean is
+ (Left.Content = Right.Content);
+
+ ---------
+ -- Add --
+ ---------
+
+ function Add (Container : Sequence; New_Item : Element_Type) return Sequence
+ is
+ (Add (Container, Last (Container) + 1, New_Item));
+
+ function Add
+ (Container : Sequence;
+ Position : Big_Positive;
+ New_Item : Element_Type) return Sequence is
+ (Content => Add (Container.Content, To_Count (Position), New_Item));
+
+ --------------------
+ -- Constant_Range --
+ --------------------
+
+ function Constant_Range
+ (Container : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural;
+ Item : Element_Type) return Boolean
+ is
+ Count_Fst : constant Count_Type := To_Count (Fst);
+ Count_Lst : constant Count_Type := To_Count (Lst);
+
+ begin
+ for J in Count_Fst .. Count_Lst loop
+ if Get (Container.Content, J) /= Item then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Constant_Range;
+
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains
+ (Container : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural;
+ Item : Element_Type) return Boolean
+ is
+ Count_Fst : constant Count_Type := To_Count (Fst);
+ Count_Lst : constant Count_Type := To_Count (Lst);
+
+ begin
+ for J in Count_Fst .. Count_Lst loop
+ if Get (Container.Content, J) = Item then
+ return True;
+ end if;
+ end loop;
+
+ return False;
+ end Contains;
+
+ --------------------
+ -- Empty_Sequence --
+ --------------------
+
+ function Empty_Sequence return Sequence is
+ (Content => <>);
+
+ ------------------
+ -- Equal_Except --
+ ------------------
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ Position : Big_Positive) return Boolean
+ is
+ Count_Pos : constant Count_Type := To_Count (Position);
+ Count_Lst : constant Count_Type := To_Count (Last (Left));
+
+ begin
+ if Length (Left) /= Length (Right) then
+ return False;
+ end if;
+
+ for J in 1 .. Count_Lst loop
+ if J /= Count_Pos
+ and then Get (Left.Content, J) /= Get (Right.Content, J)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Equal_Except;
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ X : Big_Positive;
+ Y : Big_Positive) return Boolean
+ is
+ Count_X : constant Count_Type := To_Count (X);
+ Count_Y : constant Count_Type := To_Count (Y);
+ Count_Lst : constant Count_Type := To_Count (Last (Left));
+
+ begin
+ if Length (Left) /= Length (Right) then
+ return False;
+ end if;
+
+ for J in 1 .. Count_Lst loop
+ if J /= Count_X
+ and then J /= Count_Y
+ and then Get (Left.Content, J) /= Get (Right.Content, J)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Equal_Except;
+
+ ---------
+ -- Get --
+ ---------
+
+ function Get
+ (Container : Sequence;
+ Position : Big_Integer) return Element_Type is
+ (Get (Container.Content, To_Count (Position)));
+
+ ----------
+ -- Last --
+ ----------
+
+ function Last (Container : Sequence) return Big_Natural is
+ (Length (Container));
+
+ ------------
+ -- Length --
+ ------------
+
+ function Length (Container : Sequence) return Big_Natural is
+ (Big (Length (Container.Content)));
+
+ -----------------
+ -- Range_Equal --
+ -----------------
+
+ function Range_Equal
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural) return Boolean
+ is
+ Count_Fst : constant Count_Type := To_Count (Fst);
+ Count_Lst : constant Count_Type := To_Count (Lst);
+
+ begin
+ for J in Count_Fst .. Count_Lst loop
+ if Get (Left.Content, J) /= Get (Right.Content, J) then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Range_Equal;
+
+ -------------------
+ -- Range_Shifted --
+ -------------------
+
+ function Range_Shifted
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural;
+ Offset : Big_Integer) return Boolean
+ is
+ Count_Fst : constant Count_Type := To_Count (Fst);
+ Count_Lst : constant Count_Type := To_Count (Lst);
+
+ begin
+ for J in Count_Fst .. Count_Lst loop
+ if Get (Left.Content, J) /= Get (Right, Big (J) + Offset) then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Range_Shifted;
+
+ ------------
+ -- Remove --
+ ------------
+
+ function Remove
+ (Container : Sequence;
+ Position : Big_Positive) return Sequence is
+ (Content => Remove (Container.Content, To_Count (Position)));
+
+ ---------
+ -- Set --
+ ---------
+
+ function Set
+ (Container : Sequence;
+ Position : Big_Positive;
+ New_Item : Element_Type) return Sequence is
+ (Content => Set (Container.Content, To_Count (Position), New_Item));
+
+ --------------
+ -- To_Count --
+ --------------
+
+ function To_Count (C : Big_Natural) return Count_Type is
+ begin
+ if C > Count_Type_Big_Last then
+ raise Program_Error with "Big_Integer too large for Count_Type";
+ end if;
+ return Big_From_Count.From_Big_Integer (C);
+ end To_Count;
+
+end Ada.Containers.Functional_Infinite_Sequences;
diff --git /dev/null b/gcc/ada/libgnat/a-cfinse.ads
new file mode 100644
--- /dev/null
+++ b/gcc/ada/libgnat/a-cfinse.ads
@@ -0,0 +1,377 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- ADA.CONTAINERS.FUNCTIONAL_INFINITE_SEQUENCE --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2022-2022, Free Software Foundation, Inc. --
+-- --
+-- This specification is derived from the Ada Reference Manual for use with --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the contents of the part following the private keyword. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+pragma Ada_2012;
+private with Ada.Containers.Functional_Base;
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
+
+generic
+ type Element_Type (<>) is private;
+ with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Functional_Infinite_Sequences with SPARK_Mode is
+
+ type Sequence is private
+ with Default_Initial_Condition => Length (Sequence) = 0,
+ Iterable => (First => Iter_First,
+ Has_Element => Iter_Has_Element,
+ Next => Iter_Next,
+ Element => Get);
+ -- Sequences are empty when default initialized.
+ -- Quantification over sequences can be done using the regular
+ -- quantification over its range or directly on its elements with "for of".
+
+ -----------------------
+ -- Basic operations --
+ -----------------------
+
+ -- Sequences are axiomatized using Length and Get, providing respectively
+ -- the length of a sequence and an accessor to its Nth element:
+
+ function Length (Container : Sequence) return Big_Natural with
+ -- Length of a sequence
+
+ Global => null;
+
+ function Get
+ (Container : Sequence;
+ Position : Big_Integer) return Element_Type
+ -- Access the Element at position Position in Container
+
+ with
+ Global => null,
+ Pre => Iter_Has_Element (Container, Position);
+
+ function Last (Container : Sequence) return Big_Natural with
+ -- Last index of a sequence
+
+ Global => null,
+ Post =>
+ Last'Result = Length (Container);
+ pragma Annotate (GNATprove, Inline_For_Proof, Last);
+
+ function First return Big_Positive is (1) with
+ -- First index of a sequence
+
+ Global => null;
+
+ ------------------------
+ -- Property Functions --
+ ------------------------
+
+ function "=" (Left : Sequence; Right : Sequence) return Boolean with
+ -- Extensional equality over sequences
+
+ Global => null,
+ Post =>
+ "="'Result =
+ (Length (Left) = Length (Right)
+ and then (for all N in Left => Get (Left, N) = Get (Right, N)));
+ pragma Annotate (GNATprove, Inline_For_Proof, "=");
+
+ function "<" (Left : Sequence; Right : Sequence) return Boolean with
+ -- Left is a strict subsequence of Right
+
+ Global => null,
+ Post =>
+ "<"'Result =
+ (Length (Left) < Length (Right)
+ and then (for all N in Left => Get (Left, N) = Get (Right, N)));
+ pragma Annotate (GNATprove, Inline_For_Proof, "<");
+
+ function "<=" (Left : Sequence; Right : Sequence) return Boolean with
+ -- Left is a subsequence of Right
+
+ Global => null,
+ Post =>
+ "<="'Result =
+ (Length (Left) <= Length (Right)
+ and then (for all N in Left => Get (Left, N) = Get (Right, N)));
+ pragma Annotate (GNATprove, Inline_For_Proof, "<=");
+
+ function Contains
+ (Container : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural;
+ Item : Element_Type) return Boolean
+ -- Returns True if Item occurs in the range from Fst to Lst of Container
+
+ with
+ Global => null,
+ Pre => Lst <= Last (Container),
+ Post =>
+ Contains'Result =
+ (for some J in Container =>
+ Fst <= J and J <= Lst and Get (Container, J) = Item);
+ pragma Annotate (GNATprove, Inline_For_Proof, Contains);
+
+ function Constant_Range
+ (Container : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural;
+ Item : Element_Type) return Boolean
+ -- Returns True if every element of the range from Fst to Lst of Container
+ -- is equal to Item.
+
+ with
+ Global => null,
+ Pre => Lst <= Last (Container),
+ Post =>
+ Constant_Range'Result =
+ (for all J in Container =>
+ (if Fst <= J and J <= Lst then Get (Container, J) = Item));
+ pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range);
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ Position : Big_Positive) return Boolean
+ -- Returns True is Left and Right are the same except at position Position
+
+ with
+ Global => null,
+ Pre => Position <= Last (Left),
+ Post =>
+ Equal_Except'Result =
+ (Length (Left) = Length (Right)
+ and then (for all J in Left =>
+ (if J /= Position then
+ Get (Left, J) = Get (Right, J))));
+ pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ X : Big_Positive;
+ Y : Big_Positive) return Boolean
+ -- Returns True is Left and Right are the same except at positions X and Y
+
+ with
+ Global => null,
+ Pre => X <= Last (Left) and Y <= Last (Left),
+ Post =>
+ Equal_Except'Result =
+ (Length (Left) = Length (Right)
+ and then (for all J in Left =>
+ (if J /= X and J /= Y then
+ Get (Left, J) = Get (Right, J))));
+ pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
+
+ function Range_Equal
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural) return Boolean
+ -- Returns True if the ranges from Fst to Lst contain the same elements in
+ -- Left and Right.
+
+ with
+ Global => null,
+ Pre => Lst <= Last (Left) and Lst <= Last (Right),
+ Post =>
+ Range_Equal'Result =
+ (for all J in Left =>
+ (if Fst <= J and J <= Lst then Get (Left, J) = Get (Right, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal);
+
+ function Range_Shifted
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Big_Positive;
+ Lst : Big_Natural;
+ Offset : Big_Integer) return Boolean
+ -- Returns True if the range from Fst to Lst in Left contains the same
+ -- elements as the range from Fst + Offset to Lst + Offset in Right.
+
+ with
+ Global => null,
+ Pre =>
+ Lst <= Last (Left)
+ and then
+ (if Fst <= Lst then
+ Offset + Fst >= 1 and Offset + Lst <= Length (Right)),
+ Post =>
+ Range_Shifted'Result =
+ ((for all J in Left =>
+ (if Fst <= J and J <= Lst then
+ Get (Left, J) = Get (Right, J + Offset)))
+ and
+ (for all J in Right =>
+ (if Fst + Offset <= J and J <= Lst + Offset then
+ Get (Left, J - Offset) = Get (Right, J))));
+ pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
+
+ ----------------------------
+ -- Construction Functions --
+ ----------------------------
+
+ -- For better efficiency of both proofs and execution, avoid using
+ -- construction functions in annotations and rather use property functions.
+
+ function Set
+ (Container : Sequence;
+ Position : Big_Positive;
+ New_Item : Element_Type) return Sequence
+ -- Returns a new sequence which contains the same elements as Container
+ -- except for the one at position Position which is replaced by New_Item.
+
+ with
+ Global => null,
+ Pre => Position <= Last (Container),
+ Post =>
+ Get (Set'Result, Position) = New_Item
+ and then Equal_Except (Container, Set'Result, Position);
+
+ function Add (Container : Sequence; New_Item : Element_Type) return Sequence
+ -- Returns a new sequence which contains the same elements as Container
+ -- plus New_Item at the end.
+
+ with
+ Global => null,
+ Post =>
+ Length (Add'Result) = Length (Container) + 1
+ and then Get (Add'Result, Last (Add'Result)) = New_Item
+ and then Container <= Add'Result;
+
+ function Add
+ (Container : Sequence;
+ Position : Big_Positive;
+ New_Item : Element_Type) return Sequence
+ with
+ -- Returns a new sequence which contains the same elements as Container
+ -- except that New_Item has been inserted at position Position.
+
+ Global => null,
+ Pre => Position <= Last (Container) + 1,
+ Post =>
+ Length (Add'Result) = Length (Container) + 1
+ and then Get (Add'Result, Position) = New_Item
+ and then Range_Equal
+ (Left => Container,
+ Right => Add'Result,
+ Fst => 1,
+ Lst => Position - 1)
+ and then Range_Shifted
+ (Left => Container,
+ Right => Add'Result,
+ Fst => Position,
+ Lst => Last (Container),
+ Offset => 1);
+
+ function Remove
+ (Container : Sequence;
+ Position : Big_Positive) return Sequence
+ -- Returns a new sequence which contains the same elements as Container
+ -- except that the element at position Position has been removed.
+
+ with
+ Global => null,
+ Pre => Position <= Last (Container),
+ Post =>
+ Length (Remove'Result) = Length (Container) - 1
+ and then Range_Equal
+ (Left => Container,
+ Right => Remove'Result,
+ Fst => 1,
+ Lst => Position - 1)
+ and then Range_Shifted
+ (Left => Remove'Result,
+ Right => Container,
+ Fst => Position,
+ Lst => Last (Remove'Result),
+ Offset => 1);
+
+ function Copy_Element (Item : Element_Type) return Element_Type is (Item);
+ -- Elements of containers are copied by numerous primitives in this
+ -- package. This function causes GNATprove to verify that such a copy is
+ -- valid (in particular, it does not break the ownership policy of SPARK,
+ -- i.e. it does not contain pointers that could be used to alias mutable
+ -- data).
+
+ function Empty_Sequence return Sequence with
+ -- Return an empty Sequence
+
+ Global => null,
+ Post => Length (Empty_Sequence'Result) = 0;
+
+ ---------------------------
+ -- Iteration Primitives --
+ ---------------------------
+
+ function Iter_First (Container : Sequence) return Big_Integer with
+ Global => null,
+ Post => Iter_First'Result = 1;
+
+ function Iter_Has_Element
+ (Container : Sequence;
+ Position : Big_Integer) return Boolean
+ with
+ Global => null,
+ Post => Iter_Has_Element'Result =
+ In_Range (Position, 1, Length (Container));
+ pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
+
+ function Iter_Next
+ (Container : Sequence;
+ Position : Big_Integer) return Big_Integer
+ with
+ Global => null,
+ Pre => Iter_Has_Element (Container, Position),
+ Post => Iter_Next'Result = Position + 1;
+
+private
+ pragma SPARK_Mode (Off);
+
+ subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+ package Containers is new Ada.Containers.Functional_Base
+ (Index_Type => Positive_Count_Type,
+ Element_Type => Element_Type);
+
+ type Sequence is record
+ Content : Containers.Container;
+ end record;
+
+ function Iter_First (Container : Sequence) return Big_Integer is (1);
+
+ function Iter_Next
+ (Container : Sequence;
+ Position : Big_Integer) return Big_Integer
+ is
+ (Position + 1);
+
+ function Iter_Has_Element
+ (Container : Sequence;
+ Position : Big_Integer) return Boolean
+ is
+ (In_Range (Position, 1, Length (Container)));
+end Ada.Containers.Functional_Infinite_Sequences;
