1------------------------------------------------------------------------------
2--                                                                          --
3--                         GNAT LIBRARY COMPONENTS                          --
4--                                                                          --
5--                      ADA.CONTAINERS.FUNCTIONAL_SETS                      --
6--                                                                          --
7--                                 B o d y                                  --
8--                                                                          --
9--          Copyright (C) 2016-2018, Free Software Foundation, Inc.         --
10--                                                                          --
11-- This specification is derived from the Ada Reference Manual for use with --
12-- GNAT. The copyright notice above, and the license provisions that follow --
13-- apply solely to the  contents of the part following the private keyword. --
14--                                                                          --
15-- GNAT is free software;  you can  redistribute it  and/or modify it under --
16-- terms of the  GNU General Public License as published  by the Free Soft- --
17-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
18-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
19-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
20-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
21--                                                                          --
22-- As a special exception under Section 7 of GPL version 3, you are granted --
23-- additional permissions described in the GCC Runtime Library Exception,   --
24-- version 3.1, as published by the Free Software Foundation.               --
25--                                                                          --
26-- You should have received a copy of the GNU General Public License and    --
27-- a copy of the GCC Runtime Library Exception along with this program;     --
28-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
29-- <http://www.gnu.org/licenses/>.                                          --
30------------------------------------------------------------------------------
31
32pragma Ada_2012;
33
34package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
35   use Containers;
36
37   ---------
38   -- "=" --
39   ---------
40
41   function "=" (Left : Set; Right : Set) return Boolean is
42     (Left.Content <= Right.Content and Right.Content <= Left.Content);
43
44   ----------
45   -- "<=" --
46   ----------
47
48   function "<=" (Left : Set; Right : Set) return Boolean is
49     (Left.Content <= Right.Content);
50
51   ---------
52   -- Add --
53   ---------
54
55   function Add (Container : Set; Item : Element_Type) return Set is
56     (Content =>
57       Add (Container.Content, Length (Container.Content) + 1, Item));
58
59   --------------
60   -- Contains --
61   --------------
62
63   function Contains (Container : Set; Item : Element_Type) return Boolean is
64     (Find (Container.Content, Item) > 0);
65
66   ---------------------
67   -- Included_Except --
68   ---------------------
69
70   function Included_Except
71     (Left  : Set;
72      Right : Set;
73      Item  : Element_Type) return Boolean
74   is
75     (for all E of Left =>
76       Equivalent_Elements (E, Item) or Contains (Right, E));
77
78   -----------------------
79   -- Included_In_Union --
80   -----------------------
81
82   function Included_In_Union
83     (Container : Set;
84      Left      : Set;
85      Right     : Set) return Boolean
86   is
87     (for all Item of Container =>
88       Contains (Left, Item) or Contains (Right, Item));
89
90   ---------------------------
91   -- Includes_Intersection --
92   ---------------------------
93
94   function Includes_Intersection
95     (Container : Set;
96      Left      : Set;
97      Right     : Set) return Boolean
98   is
99     (for all Item of Left =>
100       (if Contains (Right, Item) then Contains (Container, Item)));
101
102   ------------------
103   -- Intersection --
104   ------------------
105
106   function Intersection (Left : Set; Right : Set) return Set is
107     (Content => Intersection (Left.Content, Right.Content));
108
109   --------------
110   -- Is_Empty --
111   --------------
112
113   function Is_Empty (Container : Set) return Boolean is
114     (Length (Container.Content) = 0);
115
116   ------------------
117   -- Is_Singleton --
118   ------------------
119
120   function Is_Singleton
121     (Container : Set;
122      New_Item  : Element_Type) return Boolean
123   is
124     (Length (Container.Content) = 1
125        and New_Item = Get (Container.Content, 1));
126
127   ------------
128   -- Length --
129   ------------
130
131   function Length (Container : Set) return Count_Type is
132     (Length (Container.Content));
133
134   -----------------
135   -- Not_In_Both --
136   -----------------
137
138   function Not_In_Both
139     (Container : Set;
140      Left      : Set;
141      Right     : Set) return Boolean
142   is
143     (for all Item of Container =>
144       not Contains (Right, Item) or not Contains (Left, Item));
145
146   ----------------
147   -- No_Overlap --
148   ----------------
149
150   function No_Overlap (Left : Set; Right : Set) return Boolean is
151     (Num_Overlaps (Left.Content, Right.Content) = 0);
152
153   ------------------
154   -- Num_Overlaps --
155   ------------------
156
157   function Num_Overlaps (Left : Set; Right : Set) return Count_Type is
158     (Num_Overlaps (Left.Content, Right.Content));
159
160   ------------
161   -- Remove --
162   ------------
163
164   function Remove (Container : Set; Item : Element_Type) return Set is
165     (Content => Remove (Container.Content, Find (Container.Content, Item)));
166
167   -----------
168   -- Union --
169   -----------
170
171   function Union (Left : Set; Right : Set) return Set is
172     (Content => Union (Left.Content, Right.Content));
173
174end Ada.Containers.Functional_Sets;
175