From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ej1-x62e.google.com (mail-ej1-x62e.google.com [IPv6:2a00:1450:4864:20::62e]) by sourceware.org (Postfix) with ESMTPS id 7F025385BACC for ; Mon, 4 Jul 2022 07:50:02 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 7F025385BACC Received: by mail-ej1-x62e.google.com with SMTP id g26so15243273ejb.5 for ; Mon, 04 Jul 2022 00:50:02 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=57tiptkjCzxayyiGMtin6W0dk7yNEUDJKDR3p7a9zGk=; b=IkRgud41RBreechlfQCRn0xposwMuOeKeVN91jTGf/4D965tg/wsXqXNDu6G8Umwb0 gbgJm13GLGTTzFs8Ra3tEzHwChlyVJ7XbHK8q+iFcR1WWUB/F4Ogt/+UoyuaDIOqq7K2 IIZbA3trgnRX/ZG/z8V3Axipe4KJKdLI0ZOe+kjz6L1sd2+UivDwEuSXg+9Dgs56hq8P 2qYZzkidvgNPUlcUE7dfpqaKCHm1f34hPm1VYVhuh24JtUGNrnM9kY9l1AgdaFcL11BN J805qsq0rsIPIil5+sN4RmCGcgCSOAgp+dKxfmSPD21FlELVVIsceCMAlY8HnhGyLGJs tzaA== X-Gm-Message-State: AJIora8oxE8SFi3AFDoQvoIYoK6jp1NfZ9AiyXYoWFhd+ebQplNKDNDs qUruz5hnVawt90WgKrLuPqwAnsLs36QoEA== X-Google-Smtp-Source: AGRyM1tzDGrgVFdC5cjj2jILwQMh88uWu0GgWpNeHSJGYRDWqbrvl7vOxfWNNvcJ+RIFHaoL0XXXRQ== X-Received: by 2002:a17:906:938a:b0:726:942a:54e8 with SMTP id l10-20020a170906938a00b00726942a54e8mr27546025ejx.225.1656921001269; Mon, 04 Jul 2022 00:50:01 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id s7-20020a1709066c8700b0070c4abe4706sm13921766ejr.158.2022.07.04.00.50.00 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 04 Jul 2022 00:50:00 -0700 (PDT) Date: Mon, 4 Jul 2022 07:50:00 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Julien Bortolussi Subject: [Ada] Create new unbounded functional sequence Message-ID: <20220704075000.GA98883@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="y0ulUmNC+osPPQO6" Content-Disposition: inline X-Spam-Status: No, score=-12.7 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, KAM_SHORT, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 04 Jul 2022 07:50:06 -0000 --y0ulUmNC+osPPQO6 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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 files --y0ulUmNC+osPPQO6 Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --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 -- +-- . -- +------------------------------------------------------------------------------ + +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 -- +-- . -- +------------------------------------------------------------------------------ + +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; --y0ulUmNC+osPPQO6--