From: Claire Dross <dross@adacore.com>
Date: Tue, 17 Sep 2019 08:03:02 +0000 (+0000)
Subject: [Ada] Add Remove primitive on functional maps
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=994e33d27a6d0de5a3fdb646c93aaea72d003c6f;p=gcc.git

[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 6c4eaf762ef..b327857a8fe 100644
--- 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 1652efeeaa8..d963f6e623b 100644
--- 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 bf6e5a81710..e458b06e773 100644
--- 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;