From 994e33d27a6d0de5a3fdb646c93aaea72d003c6f Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Tue, 17 Sep 2019 08:03:02 +0000 Subject: [PATCH] [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 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 | 6 ++++++ gcc/ada/libgnat/a-cofuma.adb | 12 ++++++++++++ gcc/ada/libgnat/a-cofuma.ads | 14 ++++++++++++++ 3 files changed, 32 insertions(+) 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 + + * 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 * 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; -- 2.30.2