[Ada] Add empty constructors to the functional containers

[Ada] Add empty constructors to the functional containers

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 336 bytes --]

This patch adds empty constructors to the functional containers so that
we can use them in expression functions.

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

gcc/ada/

	* libgnat/a-cofuma.ads, libgnat/a-cofuma.adb,
	libgnat/a-cofuse.ads, libgnat/a-cofuse.adb,
	libgnat/a-cofuve.ads, libgnat/a-cofuve.adb: Add empty
	constructors.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 3325 bytes --]

diff --git a/gcc/ada/libgnat/a-cofuma.adb b/gcc/ada/libgnat/a-cofuma.adb
--- a/gcc/ada/libgnat/a-cofuma.adb
+++ b/gcc/ada/libgnat/a-cofuma.adb
@@ -130,6 +130,13 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
       return True;
    end Elements_Equal_Except;
 
+   ---------------
+   -- Empty_Map --
+   ---------------
+
+   function Empty_Map return Map is
+      ((others =>  <>));
+
    ---------
    -- Get --
    ---------


diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads
--- a/gcc/ada/libgnat/a-cofuma.ads
+++ b/gcc/ada/libgnat/a-cofuma.ads
@@ -243,6 +243,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
          and Container <= Add'Result
          and Keys_Included_Except (Add'Result, Container, New_Key);
 
+   function Empty_Map return Map with
+   --  Return an empty Map
+
+     Global => null,
+     Post   =>
+       Length (Empty_Map'Result) = 0
+         and Is_Empty (Empty_Map'Result);
+
    function Remove
      (Container : Map;
       Key       : Key_Type) return Map


diff --git a/gcc/ada/libgnat/a-cofuse.adb b/gcc/ada/libgnat/a-cofuse.adb
--- a/gcc/ada/libgnat/a-cofuse.adb
+++ b/gcc/ada/libgnat/a-cofuse.adb
@@ -63,6 +63,13 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
    function Contains (Container : Set; Item : Element_Type) return Boolean is
      (Find (Container.Content, Item) > 0);
 
+   ---------------
+   -- Empty_Set --
+   ---------------
+
+   function Empty_Set return Set is
+      ((others => <>));
+
    ---------------------
    -- Included_Except --
    ---------------------


diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads
--- a/gcc/ada/libgnat/a-cofuse.ads
+++ b/gcc/ada/libgnat/a-cofuse.ads
@@ -215,6 +215,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
          and Container <= Add'Result
          and Included_Except (Add'Result, Container, Item);
 
+   function Empty_Set return Set with
+   --  Return an new empty set
+
+     Global => null,
+     Post   => Is_Empty (Empty_Set'Result);
+
    function Remove (Container : Set; Item : Element_Type) return Set with
    --  Return a new set containing all the elements of Container except E
 


diff --git a/gcc/ada/libgnat/a-cofuve.adb b/gcc/ada/libgnat/a-cofuve.adb
--- a/gcc/ada/libgnat/a-cofuve.adb
+++ b/gcc/ada/libgnat/a-cofuve.adb
@@ -118,6 +118,13 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
       return False;
    end Contains;
 
+   --------------------
+   -- Empty_Sequence --
+   --------------------
+
+   function Empty_Sequence return Sequence is
+      ((others => <>));
+
    ------------------
    -- Equal_Except --
    ------------------


diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
--- a/gcc/ada/libgnat/a-cofuve.ads
+++ b/gcc/ada/libgnat/a-cofuve.ads
@@ -343,6 +343,12 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
    --  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 --
    ---------------------------