[Ada] Add Remove primitive on functional maps

A primitive for removing a mapping from a functional map has been added.

2019-09-17  Claire Dross  <dross@adacore.com>

gcc/ada/

	* libgnat/a-cofuma.ads, libgnat/a-cofuma.adb (Remove): New
	function which returns a copy of the input container without a
	given mapping.

From-SVN: r275797

gcc/ada/ChangeLog

@@ -1,3 +1,9 @@
+2019-09-17  Claire Dross  <dross@adacore.com>
+
+	* libgnat/a-cofuma.ads, libgnat/a-cofuma.adb (Remove): New
+	function which returns a copy of the input container without a
+	given mapping.
+
 2019-09-17  Yannick Moy  <moy@adacore.com>
 
 	* libgnat/s-arit64.adb (Double_Divide): Correctly handle the

gcc/ada/libgnat/a-cofuma.adb

@@ -243,6 +243,18 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
       return Length (Container.Elements);
    end Length;
 
+   ------------
+   -- Remove --
+   ------------
+
+   function Remove (Container : Map; Key : Key_Type) return Map is
+      I : constant Extended_Index := Find (Container.Keys, Key);
+   begin
+      return
+        (Keys     => Remove (Container.Keys, I),
+         Elements => Remove (Container.Elements, I));
+   end Remove;
+
    ---------------
    -- Same_Keys --
    ---------------

gcc/ada/libgnat/a-cofuma.ads

@@ -243,6 +243,20 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
          and Container <= Add'Result
          and Keys_Included_Except (Add'Result, Container, New_Key);
 
+   function Remove
+     (Container : Map;
+      Key       : Key_Type) return Map
+   --  Returns Container without any mapping for Key
+
+   with
+     Global => null,
+     Pre    => Has_Key (Container, Key),
+     Post   =>
+       Length (Container) = Length (Remove'Result) + 1
+         and not Has_Key (Remove'Result, Key)
+         and Remove'Result <= Container
+         and Keys_Included_Except (Container, Remove'Result, Key);
+
    function Set
      (Container : Map;
       Key       : Key_Type;