This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.

Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Add formal function parameter equality to SPARK containers

This patch adds a formal function parameter "=" (L, R : Element_Type) to
SPARK containers. The equality that is used by default for Element_Type
after this patch is the primitive equality and not the predefined any
more. It also allows to use any function with the appropriate signature
for the equality function.

Tested on x86_64-pc-linux-gnu, committed on trunk

2019-08-19  Joffrey Huguet  <huguet@adacore.com>

gcc/ada/

	* libgnat/a-cfdlli.ads, libgnat/a-cfhama.ads,
	libgnat/a-cfinve.ads, libgnat/a-cforma.ads,
	libgnat/a-cofove.ads, libgnat/a-cofuma.ads,
	libgnat/a-cofuve.ads: Add formal function parameter "=" (L, R :
	Element_Type) to the generic packages.
--- gcc/ada/libgnat/a-cfdlli.ads
+++ gcc/ada/libgnat/a-cfdlli.ads
@@ -34,6 +34,7 @@ with Ada.Containers.Functional_Maps;
 
 generic
    type Element_Type is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Doubly_Linked_Lists with
   SPARK_Mode

--- gcc/ada/libgnat/a-cfhama.ads
+++ gcc/ada/libgnat/a-cfhama.ads
@@ -59,6 +59,7 @@ generic
    with function Equivalent_Keys
      (Left  : Key_Type;
       Right : Key_Type) return Boolean is "=";
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Hashed_Maps with
   SPARK_Mode

--- gcc/ada/libgnat/a-cfinve.ads
+++ gcc/ada/libgnat/a-cfinve.ads
@@ -38,6 +38,7 @@ with Ada.Containers.Functional_Vectors;
 generic
    type Index_Type is range <>;
    type Element_Type (<>) is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
    Max_Size_In_Storage_Elements : Natural;
    --  Maximum size of Vector elements in bytes. This has the same meaning as
    --  in Ada.Containers.Bounded_Holders, with the same restrictions. Note that

--- gcc/ada/libgnat/a-cforma.ads
+++ gcc/ada/libgnat/a-cforma.ads
@@ -58,6 +58,7 @@ generic
    type Element_Type is private;
 
    with function "<" (Left, Right : Key_Type) return Boolean is <>;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Ordered_Maps with
   SPARK_Mode

--- gcc/ada/libgnat/a-cofove.ads
+++ gcc/ada/libgnat/a-cofove.ads
@@ -40,6 +40,8 @@ with Ada.Containers.Functional_Vectors;
 generic
    type Index_Type is range <>;
    type Element_Type is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
 package Ada.Containers.Formal_Vectors with
   SPARK_Mode
 is

--- gcc/ada/libgnat/a-cofuma.ads
+++ gcc/ada/libgnat/a-cofuma.ads
@@ -39,6 +39,7 @@ generic
    with function Equivalent_Keys
      (Left  : Key_Type;
       Right : Key_Type) return Boolean is "=";
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
    Enable_Handling_Of_Equivalence : Boolean := True;
    --  This constant should only be set to False when no particular handling

--- gcc/ada/libgnat/a-cofuve.ads
+++ gcc/ada/libgnat/a-cofuve.ads
@@ -38,6 +38,7 @@ generic
    --  should have at least one more element at the low end than Index_Type.
 
    type Element_Type (<>) is private;
+   with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Functional_Vectors with SPARK_Mode is
Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]