[Ada] Make the functional Maps and Sets unbounded

Before this patch, the Functional Sets ans Maps were bounded both from
the user and the implementation points of view.  To make them closer to
mathematical Sets ans Maps, this patch removes the bounds from the
contracts. Note that, in practice, they are still bounded by
Count_Type'Last, even if the user is not aware of it anymore.

This patch removed constraints on length of sets and maps from the
preconditions of functions. The function Length and Num_Overlaps now
return a Big_Natural.

gcc/ada/

	* libgnat/a-cofuse.ads, libgnat/a-cofuse.adb,
	libgnat/a-cofuma.ads, libgnat/a-cofuma.adb: Make Length and
	Num_Overlaps return Big_Natural.
	* libgnat/a-cforse.ads, libgnat/a-cforse.adb,
	libgnat/a-cforma.adb, libgnat/a-cfhase.ads,
	libgnat/a-cfhase.adb, libgnat/a-cfhama.adb,
	libgnat/a-cfdlli.adb: Adapt code to handle Big_Integers instead
	of Count_Type.

diff --git a/gcc/ada/libgnat/a-cfdlli.adb b/gcc/ada/libgnat/a-cfdlli.adb
index 7b23ad7..bbb8fd4 100644 (file)
--- a/gcc/ada/libgnat/a-cfdlli.adb
+++ b/gcc/ada/libgnat/a-cfdlli.adb
@@ -29,9 +29,17 @@ with Ada.Containers.Stable_Sorting; use Ada.Containers.Stable_Sorting;
 
 with System; use type System.Address;
 
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
+
 package body Ada.Containers.Formal_Doubly_Linked_Lists with
   SPARK_Mode => Off
 is
+   --  Convert Count_Type to Big_Interger
+
+   package Conversions is new Signed_Conversions (Int => Count_Type);
+   use Conversions;
+
    -----------------------
    -- Local Subprograms --
    -----------------------
@@ -809,7 +817,7 @@ is
 
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
-            pragma Assert (P.Length (R) = I);
+            pragma Assert (P.Length (R) = To_Big_Integer (I));
             Position := Container.Nodes (Position).Next;
             I := I + 1;
          end loop;

diff --git a/gcc/ada/libgnat/a-cfhama.adb b/gcc/ada/libgnat/a-cfhama.adb
index 0b60a01..bdf2c61 100644 (file)
--- a/gcc/ada/libgnat/a-cfhama.adb
+++ b/gcc/ada/libgnat/a-cfhama.adb
@@ -33,6 +33,9 @@ pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Formal_Keys);
 
 with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
 
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
+
 with System; use type System.Address;
 
 package body Ada.Containers.Formal_Hashed_Maps with
@@ -71,6 +74,13 @@ is
    function Vet (Container : Map; Position : Cursor) return Boolean
      with Inline;
 
+   --  Convert Count_Type to Big_Interger
+
+   package Conversions is new Signed_Conversions (Int => Count_Type);
+
+   function Big (J : Count_Type) return Big_Integer renames
+     Conversions.To_Big_Integer;
+
    --------------------------
    -- Local Instantiations --
    --------------------------
@@ -526,7 +536,7 @@ is
 
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
-            pragma Assert (P.Length (R) = I);
+            pragma Assert (P.Length (R) = Big (I));
             Position := HT_Ops.Next (Container.Content, Position);
             I := I + 1;
          end loop;

diff --git a/gcc/ada/libgnat/a-cfhase.adb b/gcc/ada/libgnat/a-cfhase.adb
index 544ad2b..34afa55 100644 (file)
--- a/gcc/ada/libgnat/a-cfhase.adb
+++ b/gcc/ada/libgnat/a-cfhase.adb
@@ -753,7 +753,7 @@ is
 
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
-            pragma Assert (P.Length (R) = I);
+            pragma Assert (P.Length (R) = Big (I));
             Position := HT_Ops.Next (Container.Content, Position);
             I := I + 1;
          end loop;

diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads
index 1a40118..80ce948 100644 (file)
--- a/gcc/ada/libgnat/a-cfhase.ads
+++ b/gcc/ada/libgnat/a-cfhase.ads
@@ -48,6 +48,8 @@
 with Ada.Containers.Functional_Maps;
 with Ada.Containers.Functional_Sets;
 with Ada.Containers.Functional_Vectors;
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
 private with Ada.Containers.Hash_Tables;
 
 generic
@@ -70,6 +72,13 @@ is
    pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
+   --  Convert Count_Type to Big_Interger.
+
+   package Conversions is new Signed_Conversions (Int => Count_Type);
+
+   function Big (J : Count_Type) return Big_Integer renames
+     Conversions.To_Big_Integer;
+
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
      Iterable => (First       => First,
                   Next        => Next,
@@ -261,7 +270,7 @@ is
 
         Ghost,
         Global => null,
-        Post   => M.Length (Model'Result) = Length (Container);
+        Post   => M.Length (Model'Result) = Big (Length (Container));
 
       function Elements (Container : Set) return E.Sequence with
       --  The Elements sequence represents the underlying list structure of
@@ -859,9 +868,9 @@ is
        Length (Source) - Length (Target and Source) <=
          Target.Capacity - Length (Target),
      Post   =>
-       Length (Target) = Length (Target)'Old
+       Big (Length (Target)) = Big (Length (Target)'Old)
          - M.Num_Overlaps (Model (Target)'Old, Model (Source))
-         + Length (Source)
+         + Big (Length (Source))
 
          --  Elements already in Target are still in Target
 
@@ -907,9 +916,9 @@ is
      Global => null,
      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
      Post   =>
-       Length (Union'Result) = Length (Left)
+       Big (Length (Union'Result)) = Big (Length (Left))
          - M.Num_Overlaps (Model (Left), Model (Right))
-         + Length (Right)
+         + Big (Length (Right))
 
          --  Elements of Left and Right are in the result of Union
 
@@ -946,7 +955,7 @@ is
    procedure Intersection (Target : in out Set; Source : Set) with
      Global => null,
      Post   =>
-       Length (Target) =
+       Big (Length (Target)) =
          M.Num_Overlaps (Model (Target)'Old, Model (Source))
 
          --  Elements of Target were already in Target
@@ -982,7 +991,7 @@ is
    function Intersection (Left, Right : Set) return Set with
      Global => null,
      Post   =>
-       Length (Intersection'Result) =
+       Big (Length (Intersection'Result)) =
          M.Num_Overlaps (Model (Left), Model (Right))
 
          --  Elements in the result of Intersection are in Left and Right
@@ -1012,7 +1021,7 @@ is
    procedure Difference (Target : in out Set; Source : Set) with
      Global => null,
      Post   =>
-       Length (Target) = Length (Target)'Old -
+       Big (Length (Target)) = Big (Length (Target)'Old) -
          M.Num_Overlaps (Model (Target)'Old, Model (Source))
 
          --  Elements of Target were already in Target
@@ -1048,7 +1057,7 @@ is
    function Difference (Left, Right : Set) return Set with
      Global => null,
      Post   =>
-       Length (Difference'Result) = Length (Left) -
+       Big (Length (Difference'Result)) = Big (Length (Left)) -
          M.Num_Overlaps (Model (Left), Model (Right))
 
          --  Elements of the result of Difference are in Left
@@ -1085,9 +1094,9 @@ is
        Length (Source) - Length (Target and Source) <=
          Target.Capacity - Length (Target) + Length (Target and Source),
      Post   =>
-       Length (Target) = Length (Target)'Old -
+       Big (Length (Target)) = Big (Length (Target)'Old) -
          2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
-         Length (Source)
+         Big (Length (Source))
 
          --  Elements of the difference were not both in Source and in Target
 
@@ -1125,9 +1134,9 @@ is
      Global => null,
      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
      Post   =>
-       Length (Symmetric_Difference'Result) = Length (Left) -
+       Big (Length (Symmetric_Difference'Result)) = Big (Length (Left)) -
          2 * M.Num_Overlaps (Model (Left), Model (Right)) +
-         Length (Right)
+         Big (Length (Right))
 
          --  Elements of the difference were not both in Left and Right
 

diff --git a/gcc/ada/libgnat/a-cforma.adb b/gcc/ada/libgnat/a-cforma.adb
index 79f25f8..38d15e7 100644 (file)
--- a/gcc/ada/libgnat/a-cforma.adb
+++ b/gcc/ada/libgnat/a-cforma.adb
@@ -32,12 +32,22 @@ pragma Elaborate_All
 with Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys;
 pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys);
 
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
+
 with System; use type System.Address;
 
 package body Ada.Containers.Formal_Ordered_Maps with
   SPARK_Mode => Off
 is
 
+   --  Convert Count_Type to Big_Interger
+
+   package Conversions is new Signed_Conversions (Int => Count_Type);
+
+   function Big (J : Count_Type) return Big_Integer renames
+     Conversions.To_Big_Integer;
+
    -----------------------------
    -- Node Access Subprograms --
    -----------------------------
@@ -745,7 +755,7 @@ is
 
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
-            pragma Assert (P.Length (R) = I);
+            pragma Assert (P.Length (R) = Big (I));
             Position := Tree_Operations.Next (Container.Content, Position);
             I := I + 1;
          end loop;

diff --git a/gcc/ada/libgnat/a-cforse.adb b/gcc/ada/libgnat/a-cforse.adb
index 3b64511..e5cddde 100644 (file)
--- a/gcc/ada/libgnat/a-cforse.adb
+++ b/gcc/ada/libgnat/a-cforse.adb
@@ -943,7 +943,7 @@ is
 
          while Position /= 0 loop
             R := P.Add (R, (Node => Position), I);
-            pragma Assert (P.Length (R) = I);
+            pragma Assert (P.Length (R) = Big (I));
             Position := Tree_Operations.Next (Container.Content, Position);
             I := I + 1;
          end loop;

diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
index a736b48..f6a033f 100644 (file)
--- a/gcc/ada/libgnat/a-cforse.ads
+++ b/gcc/ada/libgnat/a-cforse.ads
@@ -49,6 +49,8 @@
 with Ada.Containers.Functional_Maps;
 with Ada.Containers.Functional_Sets;
 with Ada.Containers.Functional_Vectors;
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
 private with Ada.Containers.Red_Black_Trees;
 
 generic
@@ -67,6 +69,13 @@ is
    pragma Assertion_Policy (Contract_Cases => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
+   --  Convert Count_Type to Big_Interger
+
+   package Conversions is new Signed_Conversions (Int => Count_Type);
+
+   function Big (J : Count_Type) return Big_Integer renames
+     Conversions.To_Big_Integer;
+
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean
    with
      Global => null,
@@ -341,7 +350,7 @@ is
 
         Ghost,
         Global => null,
-        Post   => M.Length (Model'Result) = Length (Container);
+        Post   => M.Length (Model'Result) = Big (Length (Container));
 
       function Elements (Container : Set) return E.Sequence with
       --  The Elements sequence represents the underlying list structure of
@@ -990,9 +999,9 @@ is
        Length (Source) - Length (Target and Source) <=
          Target.Capacity - Length (Target),
      Post   =>
-       Length (Target) = Length (Target)'Old
+       Big (Length (Target)) = Big (Length (Target)'Old)
          - M.Num_Overlaps (Model (Target)'Old, Model (Source))
-         + Length (Source)
+         + Big (Length (Source))
 
          --  Elements already in Target are still in Target
 
@@ -1038,9 +1047,9 @@ is
      Global => null,
      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
      Post   =>
-       Length (Union'Result) = Length (Left)
+       Big (Length (Union'Result)) = Big (Length (Left))
          - M.Num_Overlaps (Model (Left), Model (Right))
-         + Length (Right)
+         + Big (Length (Right))
 
          --  Elements of Left and Right are in the result of Union
 
@@ -1076,7 +1085,7 @@ is
    procedure Intersection (Target : in out Set; Source : Set) with
      Global => null,
      Post   =>
-       Length (Target) =
+       Big (Length (Target)) =
          M.Num_Overlaps (Model (Target)'Old, Model (Source))
 
          --  Elements of Target were already in Target
@@ -1111,7 +1120,7 @@ is
    function Intersection (Left, Right : Set) return Set with
      Global => null,
      Post   =>
-       Length (Intersection'Result) =
+       Big (Length (Intersection'Result)) =
          M.Num_Overlaps (Model (Left), Model (Right))
 
          --  Elements in the result of Intersection are in Left and Right
@@ -1139,7 +1148,7 @@ is
    procedure Difference (Target : in out Set; Source : Set) with
      Global => null,
      Post   =>
-       Length (Target) = Length (Target)'Old -
+       Big (Length (Target)) = Big (Length (Target)'Old) -
          M.Num_Overlaps (Model (Target)'Old, Model (Source))
 
          --  Elements of Target were already in Target
@@ -1174,7 +1183,7 @@ is
    function Difference (Left, Right : Set) return Set with
      Global => null,
      Post   =>
-       Length (Difference'Result) = Length (Left) -
+       Big (Length (Difference'Result)) = Big (Length (Left)) -
          M.Num_Overlaps (Model (Left), Model (Right))
 
          --  Elements of the result of Difference are in Left
@@ -1209,9 +1218,9 @@ is
        Length (Source) - Length (Target and Source) <=
          Target.Capacity - Length (Target) + Length (Target and Source),
      Post   =>
-       Length (Target) = Length (Target)'Old -
+       Big (Length (Target)) = Big (Length (Target)'Old) -
          2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
-         Length (Source)
+         Big (Length (Source))
 
          --  Elements of the difference were not both in Source and in Target
 
@@ -1248,9 +1257,9 @@ is
      Global => null,
      Pre    => Length (Left) <= Count_Type'Last - Length (Right),
      Post   =>
-       Length (Symmetric_Difference'Result) = Length (Left) -
+       Big (Length (Symmetric_Difference'Result)) = Big (Length (Left)) -
          2 * M.Num_Overlaps (Model (Left), Model (Right)) +
-         Length (Right)
+         Big (Length (Right))
 
          --  Elements of the difference were not both in Left and Right
 

diff --git a/gcc/ada/libgnat/a-cofuma.adb b/gcc/ada/libgnat/a-cofuma.adb
index 0fcdbdc..f83b4d8 100644 (file)
--- a/gcc/ada/libgnat/a-cofuma.adb
+++ b/gcc/ada/libgnat/a-cofuma.adb
@@ -34,6 +34,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
    use Key_Containers;
    use Element_Containers;
 
+   package Conversions is new Signed_Conversions (Int => Count_Type);
+   use Conversions;
+
    ---------
    -- "=" --
    ---------
@@ -245,9 +248,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
    -- Length --
    ------------
 
-   function Length (Container : Map) return Count_Type is
+   function Length (Container : Map) return Big_Natural is
    begin
-      return Length (Container.Elements);
+      return To_Big_Integer (Length (Container.Elements));
    end Length;
 
    ------------

diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads
index f240e1e..d01c4b4 100644 (file)
--- a/gcc/ada/libgnat/a-cofuma.ads
+++ b/gcc/ada/libgnat/a-cofuma.ads
@@ -32,6 +32,9 @@
 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 Key_Type (<>) is private;
    type Element_Type (<>)  is private;
@@ -97,7 +100,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
                   (Equivalent_Keys (K, Key) =
                     (Witness (Container, Key) = Witness (Container, K)))));
 
-   function Length (Container : Map) return Count_Type with
+   function Length (Container : Map) return Big_Natural with
      Global => null;
    --  Return the number of mappings in Container
 
@@ -233,9 +236,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
 
    with
      Global => null,
-     Pre    =>
-       not Has_Key (Container, New_Key)
-         and Length (Container) < Count_Type'Last,
+     Pre    => not Has_Key (Container, New_Key),
      Post   =>
        Length (Container) + 1 = Length (Add'Result)
          and Has_Key (Add'Result, New_Key)

diff --git a/gcc/ada/libgnat/a-cofuse.adb b/gcc/ada/libgnat/a-cofuse.adb
index 77adb1d..bbb3f7e 100644 (file)
--- a/gcc/ada/libgnat/a-cofuse.adb
+++ b/gcc/ada/libgnat/a-cofuse.adb
@@ -34,6 +34,9 @@ pragma Ada_2012;
 package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
    use Containers;
 
+   package Conversions is new Signed_Conversions (Int => Count_Type);
+   use Conversions;
+
    ---------
    -- "=" --
    ---------
@@ -135,8 +138,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
    -- Length --
    ------------
 
-   function Length (Container : Set) return Count_Type is
-     (Length (Container.Content));
+   function Length (Container : Set) return Big_Natural is
+     (To_Big_Integer (Length (Container.Content)));
 
    -----------------
    -- Not_In_Both --
@@ -161,8 +164,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
    -- Num_Overlaps --
    ------------------
 
-   function Num_Overlaps (Left : Set; Right : Set) return Count_Type is
-     (Num_Overlaps (Left.Content, Right.Content));
+   function Num_Overlaps (Left : Set; Right : Set) return Big_Natural is
+     (To_Big_Integer (Num_Overlaps (Left.Content, Right.Content)));
 
    ------------
    -- Remove --

diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads
index 6cd340b..29f1e9f 100644 (file)
--- a/gcc/ada/libgnat/a-cofuse.ads
+++ b/gcc/ada/libgnat/a-cofuse.ads
@@ -32,6 +32,9 @@
 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;
 
@@ -79,7 +82,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
           (if (for some E of Container => Equivalent_Elements (E, Item)) then
               Contains'Result));
 
-   function Length (Container : Set) return Count_Type with
+   function Length (Container : Set) return Big_Natural with
      Global => null;
    --  Return the number of elements in Container
 
@@ -183,7 +186,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
        No_Overlap'Result =
          (for all Item of Left => not Contains (Right, Item));
 
-   function Num_Overlaps (Left : Set; Right : Set) return Count_Type with
+   function Num_Overlaps (Left : Set; Right : Set) return Big_Natural with
    --  Number of elements that are both in Left and Right
 
      Global => null,
@@ -206,9 +209,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
    --  Return a new set containing all the elements of Container plus E
 
      Global => null,
-     Pre    =>
-       not Contains (Container, Item)
-       and Length (Container) < Count_Type'Last,
+     Pre    => not Contains (Container, Item),
      Post   =>
        Length (Add'Result) = Length (Container) + 1
          and Contains (Add'Result, Item)
@@ -245,9 +246,6 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
    --  Returns the union of Left and Right
 
      Global => null,
-     Pre    =>
-       Length (Left) - Num_Overlaps (Left, Right) <=
-         Count_Type'Last - Length (Right),
      Post   =>
        Length (Union'Result) =
          Length (Left) - Num_Overlaps (Left, Right) + Length (Right)