public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-824] [Ada] Add empty constructors to the functional containers
@ 2022-05-30 8:29 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-30 8:29 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:efaee961d935f8f4fb640d8445603fe52a9e247c
commit r13-824-gefaee961d935f8f4fb640d8445603fe52a9e247c
Author: Julien Bortolussi <bortolussi@adacore.com>
Date: Thu Apr 14 16:09:30 2022 +0200
[Ada] Add empty constructors to the functional containers
This patch adds empty constructors to the functional containers so that
we can use them in expression functions.
gcc/ada/
* libgnat/a-cofuma.ads, libgnat/a-cofuma.adb,
libgnat/a-cofuse.ads, libgnat/a-cofuse.adb,
libgnat/a-cofuve.ads, libgnat/a-cofuve.adb: Add empty
constructors.
Diff:
---
gcc/ada/libgnat/a-cofuma.adb | 7 +++++++
gcc/ada/libgnat/a-cofuma.ads | 8 ++++++++
gcc/ada/libgnat/a-cofuse.adb | 7 +++++++
gcc/ada/libgnat/a-cofuse.ads | 6 ++++++
gcc/ada/libgnat/a-cofuve.adb | 7 +++++++
gcc/ada/libgnat/a-cofuve.ads | 6 ++++++
6 files changed, 41 insertions(+)
diff --git a/gcc/ada/libgnat/a-cofuma.adb b/gcc/ada/libgnat/a-cofuma.adb
index 080229db285..0fcdbdc0e97 100644
--- a/gcc/ada/libgnat/a-cofuma.adb
+++ b/gcc/ada/libgnat/a-cofuma.adb
@@ -130,6 +130,13 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
return True;
end Elements_Equal_Except;
+ ---------------
+ -- Empty_Map --
+ ---------------
+
+ function Empty_Map return Map is
+ ((others => <>));
+
---------
-- Get --
---------
diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads
index 3f61b63c2d9..f240e1e41ef 100644
--- a/gcc/ada/libgnat/a-cofuma.ads
+++ b/gcc/ada/libgnat/a-cofuma.ads
@@ -243,6 +243,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
and Container <= Add'Result
and Keys_Included_Except (Add'Result, Container, New_Key);
+ function Empty_Map return Map with
+ -- Return an empty Map
+
+ Global => null,
+ Post =>
+ Length (Empty_Map'Result) = 0
+ and Is_Empty (Empty_Map'Result);
+
function Remove
(Container : Map;
Key : Key_Type) return Map
diff --git a/gcc/ada/libgnat/a-cofuse.adb b/gcc/ada/libgnat/a-cofuse.adb
index 0157988d808..77adb1d6414 100644
--- a/gcc/ada/libgnat/a-cofuse.adb
+++ b/gcc/ada/libgnat/a-cofuse.adb
@@ -63,6 +63,13 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
function Contains (Container : Set; Item : Element_Type) return Boolean is
(Find (Container.Content, Item) > 0);
+ ---------------
+ -- Empty_Set --
+ ---------------
+
+ function Empty_Set return Set is
+ ((others => <>));
+
---------------------
-- Included_Except --
---------------------
diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads
index db88b9a4e1e..ce961aa28a8 100644
--- a/gcc/ada/libgnat/a-cofuse.ads
+++ b/gcc/ada/libgnat/a-cofuse.ads
@@ -215,6 +215,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
and Container <= Add'Result
and Included_Except (Add'Result, Container, Item);
+ function Empty_Set return Set with
+ -- Return an new empty set
+
+ Global => null,
+ Post => Is_Empty (Empty_Set'Result);
+
function Remove (Container : Set; Item : Element_Type) return Set with
-- Return a new set containing all the elements of Container except E
diff --git a/gcc/ada/libgnat/a-cofuve.adb b/gcc/ada/libgnat/a-cofuve.adb
index 06075b14423..0d91da5015e 100644
--- a/gcc/ada/libgnat/a-cofuve.adb
+++ b/gcc/ada/libgnat/a-cofuve.adb
@@ -118,6 +118,13 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
return False;
end Contains;
+ --------------------
+ -- Empty_Sequence --
+ --------------------
+
+ function Empty_Sequence return Sequence is
+ ((others => <>));
+
------------------
-- Equal_Except --
------------------
diff --git a/gcc/ada/libgnat/a-cofuve.ads b/gcc/ada/libgnat/a-cofuve.ads
index ce3a3a449dd..f926a963737 100644
--- a/gcc/ada/libgnat/a-cofuve.ads
+++ b/gcc/ada/libgnat/a-cofuve.ads
@@ -343,6 +343,12 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
-- i.e. it does not contain pointers that could be used to alias mutable
-- data).
+ function Empty_Sequence return Sequence with
+ -- Return an empty Sequence
+
+ Global => null,
+ Post => Length (Empty_Sequence'Result) = 0;
+
---------------------------
-- Iteration Primitives --
---------------------------
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-30 8:29 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-30 8:29 [gcc r13-824] [Ada] Add empty constructors to the functional containers Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).