[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6c4eaf762ef602f08f27ebc81bc2d7b38bc84617..b327857a8fee6078ab516316a10c3da3bd449662 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/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

diff --git a/gcc/ada/libgnat/a-cofuma.adb b/gcc/ada/libgnat/a-cofuma.adb
index 1652efeeaa8a532df081517afbab8caa5b1a1dbb..d963f6e623b6018489ba4a3a53fffaf9ef61a1e8 100644 (file)
--- a/gcc/ada/libgnat/a-cofuma.adb
+++ b/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 --
    ---------------

diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads
index bf6e5a8171060bf217ccfad7641b106bb6fcc256..e458b06e77378c65737510b45f5929eb03a5657d 100644 (file)
--- a/gcc/ada/libgnat/a-cofuma.ads
+++ b/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;