[Ada] Add Remove primitive on functional maps

[Pierre-Marie de Rodat]

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

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

2019-09-17  Claire Dross  <dr...@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.
--- gcc/ada/libgnat/a-cofuma.adb
+++ 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
+++ 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;