diff options
| author | Claire Dross <dross@adacore.com> | 2019-09-17 08:03:02 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-09-17 08:03:02 +0000 |
| commit | 994e33d27a6d0de5a3fdb646c93aaea72d003c6f (patch) | |
| tree | f4cb6dfbc1e9d2b6229a07d17af5224a9aae99a3 /gcc | |
| parent | e34716b8dd8836a565b4cf0c26f7244161f194f1 (diff) | |
| download | gcc-994e33d27a6d0de5a3fdb646c93aaea72d003c6f.zip gcc-994e33d27a6d0de5a3fdb646c93aaea72d003c6f.tar.gz gcc-994e33d27a6d0de5a3fdb646c93aaea72d003c6f.tar.bz2 | |
[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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 6 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-cofuma.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-cofuma.ads | 14 |
3 files changed, 32 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6c4eaf7..b327857 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 1652efe..d963f6e 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 bf6e5a8..e458b06 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; |