|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- A D A . C O N T A I N E R S . F O R M A L _ O R D E R E D _ S E T S --
|
|
|
6 -- --
|
|
|
7 -- B o d y --
|
|
|
8 -- --
|
|
|
9 -- Copyright (C) 2010-2017, Free Software Foundation, Inc. --
|
|
|
10 -- --
|
|
|
11 -- GNAT is free software; you can redistribute it and/or modify it under --
|
|
|
12 -- terms of the GNU General Public License as published by the Free Soft- --
|
|
|
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
|
|
|
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
|
|
|
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
|
|
|
16 -- or FITNESS FOR A PARTICULAR PURPOSE. --
|
|
|
17 -- --
|
|
|
18 -- As a special exception under Section 7 of GPL version 3, you are granted --
|
|
|
19 -- additional permissions described in the GCC Runtime Library Exception, --
|
|
|
20 -- version 3.1, as published by the Free Software Foundation. --
|
|
|
21 -- --
|
|
|
22 -- You should have received a copy of the GNU General Public License and --
|
|
|
23 -- a copy of the GCC Runtime Library Exception along with this program; --
|
|
|
24 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
|
|
|
25 -- <http://www.gnu.org/licenses/>. --
|
|
|
26 ------------------------------------------------------------------------------
|
|
|
27
|
|
|
28 with Ada.Containers.Red_Black_Trees.Generic_Bounded_Operations;
|
|
|
29 pragma Elaborate_All
|
|
|
30 (Ada.Containers.Red_Black_Trees.Generic_Bounded_Operations);
|
|
|
31
|
|
|
32 with Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys;
|
|
|
33 pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys);
|
|
|
34
|
|
|
35 with Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations;
|
|
|
36 pragma Elaborate_All
|
|
|
37 (Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations);
|
|
|
38
|
|
|
39 with System; use type System.Address;
|
|
|
40
|
|
|
41 package body Ada.Containers.Formal_Ordered_Sets with
|
|
|
42 SPARK_Mode => Off
|
|
|
43 is
|
|
|
44
|
|
|
45 ------------------------------
|
|
|
46 -- Access to Fields of Node --
|
|
|
47 ------------------------------
|
|
|
48
|
|
|
49 -- These subprograms provide functional notation for access to fields
|
|
|
50 -- of a node, and procedural notation for modifiying these fields.
|
|
|
51
|
|
|
52 function Color (Node : Node_Type) return Red_Black_Trees.Color_Type;
|
|
|
53 pragma Inline (Color);
|
|
|
54
|
|
|
55 function Left_Son (Node : Node_Type) return Count_Type;
|
|
|
56 pragma Inline (Left_Son);
|
|
|
57
|
|
|
58 function Parent (Node : Node_Type) return Count_Type;
|
|
|
59 pragma Inline (Parent);
|
|
|
60
|
|
|
61 function Right_Son (Node : Node_Type) return Count_Type;
|
|
|
62 pragma Inline (Right_Son);
|
|
|
63
|
|
|
64 procedure Set_Color
|
|
|
65 (Node : in out Node_Type;
|
|
|
66 Color : Red_Black_Trees.Color_Type);
|
|
|
67 pragma Inline (Set_Color);
|
|
|
68
|
|
|
69 procedure Set_Left (Node : in out Node_Type; Left : Count_Type);
|
|
|
70 pragma Inline (Set_Left);
|
|
|
71
|
|
|
72 procedure Set_Right (Node : in out Node_Type; Right : Count_Type);
|
|
|
73 pragma Inline (Set_Right);
|
|
|
74
|
|
|
75 procedure Set_Parent (Node : in out Node_Type; Parent : Count_Type);
|
|
|
76 pragma Inline (Set_Parent);
|
|
|
77
|
|
|
78 -----------------------
|
|
|
79 -- Local Subprograms --
|
|
|
80 -----------------------
|
|
|
81
|
|
|
82 -- Comments needed???
|
|
|
83
|
|
|
84 generic
|
|
|
85 with procedure Set_Element (Node : in out Node_Type);
|
|
|
86 procedure Generic_Allocate
|
|
|
87 (Tree : in out Tree_Types.Tree_Type'Class;
|
|
|
88 Node : out Count_Type);
|
|
|
89
|
|
|
90 procedure Free (Tree : in out Set; X : Count_Type);
|
|
|
91
|
|
|
92 procedure Insert_Sans_Hint
|
|
|
93 (Container : in out Set;
|
|
|
94 New_Item : Element_Type;
|
|
|
95 Node : out Count_Type;
|
|
|
96 Inserted : out Boolean);
|
|
|
97
|
|
|
98 procedure Insert_With_Hint
|
|
|
99 (Dst_Set : in out Set;
|
|
|
100 Dst_Hint : Count_Type;
|
|
|
101 Src_Node : Node_Type;
|
|
|
102 Dst_Node : out Count_Type);
|
|
|
103
|
|
|
104 function Is_Greater_Element_Node
|
|
|
105 (Left : Element_Type;
|
|
|
106 Right : Node_Type) return Boolean;
|
|
|
107 pragma Inline (Is_Greater_Element_Node);
|
|
|
108
|
|
|
109 function Is_Less_Element_Node
|
|
|
110 (Left : Element_Type;
|
|
|
111 Right : Node_Type) return Boolean;
|
|
|
112 pragma Inline (Is_Less_Element_Node);
|
|
|
113
|
|
|
114 function Is_Less_Node_Node (L, R : Node_Type) return Boolean;
|
|
|
115 pragma Inline (Is_Less_Node_Node);
|
|
|
116
|
|
|
117 procedure Replace_Element
|
|
|
118 (Tree : in out Set;
|
|
|
119 Node : Count_Type;
|
|
|
120 Item : Element_Type);
|
|
|
121
|
|
|
122 --------------------------
|
|
|
123 -- Local Instantiations --
|
|
|
124 --------------------------
|
|
|
125
|
|
|
126 package Tree_Operations is
|
|
|
127 new Red_Black_Trees.Generic_Bounded_Operations
|
|
|
128 (Tree_Types,
|
|
|
129 Left => Left_Son,
|
|
|
130 Right => Right_Son);
|
|
|
131
|
|
|
132 use Tree_Operations;
|
|
|
133
|
|
|
134 package Element_Keys is
|
|
|
135 new Red_Black_Trees.Generic_Bounded_Keys
|
|
|
136 (Tree_Operations => Tree_Operations,
|
|
|
137 Key_Type => Element_Type,
|
|
|
138 Is_Less_Key_Node => Is_Less_Element_Node,
|
|
|
139 Is_Greater_Key_Node => Is_Greater_Element_Node);
|
|
|
140
|
|
|
141 package Set_Ops is
|
|
|
142 new Red_Black_Trees.Generic_Bounded_Set_Operations
|
|
|
143 (Tree_Operations => Tree_Operations,
|
|
|
144 Set_Type => Set,
|
|
|
145 Assign => Assign,
|
|
|
146 Insert_With_Hint => Insert_With_Hint,
|
|
|
147 Is_Less => Is_Less_Node_Node);
|
|
|
148
|
|
|
149 ---------
|
|
|
150 -- "=" --
|
|
|
151 ---------
|
|
|
152
|
|
|
153 function "=" (Left, Right : Set) return Boolean is
|
|
|
154 Lst : Count_Type;
|
|
|
155 Node : Count_Type;
|
|
|
156 ENode : Count_Type;
|
|
|
157
|
|
|
158 begin
|
|
|
159 if Length (Left) /= Length (Right) then
|
|
|
160 return False;
|
|
|
161 end if;
|
|
|
162
|
|
|
163 if Is_Empty (Left) then
|
|
|
164 return True;
|
|
|
165 end if;
|
|
|
166
|
|
|
167 Lst := Next (Left, Last (Left).Node);
|
|
|
168
|
|
|
169 Node := First (Left).Node;
|
|
|
170 while Node /= Lst loop
|
|
|
171 ENode := Find (Right, Left.Nodes (Node).Element).Node;
|
|
|
172 if ENode = 0
|
|
|
173 or else Left.Nodes (Node).Element /= Right.Nodes (ENode).Element
|
|
|
174 then
|
|
|
175 return False;
|
|
|
176 end if;
|
|
|
177
|
|
|
178 Node := Next (Left, Node);
|
|
|
179 end loop;
|
|
|
180
|
|
|
181 return True;
|
|
|
182 end "=";
|
|
|
183
|
|
|
184 ------------
|
|
|
185 -- Assign --
|
|
|
186 ------------
|
|
|
187
|
|
|
188 procedure Assign (Target : in out Set; Source : Set) is
|
|
|
189 procedure Append_Element (Source_Node : Count_Type);
|
|
|
190
|
|
|
191 procedure Append_Elements is
|
|
|
192 new Tree_Operations.Generic_Iteration (Append_Element);
|
|
|
193
|
|
|
194 --------------------
|
|
|
195 -- Append_Element --
|
|
|
196 --------------------
|
|
|
197
|
|
|
198 procedure Append_Element (Source_Node : Count_Type) is
|
|
|
199 SN : Node_Type renames Source.Nodes (Source_Node);
|
|
|
200
|
|
|
201 procedure Set_Element (Node : in out Node_Type);
|
|
|
202 pragma Inline (Set_Element);
|
|
|
203
|
|
|
204 function New_Node return Count_Type;
|
|
|
205 pragma Inline (New_Node);
|
|
|
206
|
|
|
207 procedure Insert_Post is
|
|
|
208 new Element_Keys.Generic_Insert_Post (New_Node);
|
|
|
209
|
|
|
210 procedure Unconditional_Insert_Sans_Hint is
|
|
|
211 new Element_Keys.Generic_Unconditional_Insert (Insert_Post);
|
|
|
212
|
|
|
213 procedure Unconditional_Insert_Avec_Hint is
|
|
|
214 new Element_Keys.Generic_Unconditional_Insert_With_Hint
|
|
|
215 (Insert_Post,
|
|
|
216 Unconditional_Insert_Sans_Hint);
|
|
|
217
|
|
|
218 procedure Allocate is new Generic_Allocate (Set_Element);
|
|
|
219
|
|
|
220 --------------
|
|
|
221 -- New_Node --
|
|
|
222 --------------
|
|
|
223
|
|
|
224 function New_Node return Count_Type is
|
|
|
225 Result : Count_Type;
|
|
|
226 begin
|
|
|
227 Allocate (Target, Result);
|
|
|
228 return Result;
|
|
|
229 end New_Node;
|
|
|
230
|
|
|
231 -----------------
|
|
|
232 -- Set_Element --
|
|
|
233 -----------------
|
|
|
234
|
|
|
235 procedure Set_Element (Node : in out Node_Type) is
|
|
|
236 begin
|
|
|
237 Node.Element := SN.Element;
|
|
|
238 end Set_Element;
|
|
|
239
|
|
|
240 -- Local variables
|
|
|
241
|
|
|
242 Target_Node : Count_Type;
|
|
|
243
|
|
|
244 -- Start of processing for Append_Element
|
|
|
245
|
|
|
246 begin
|
|
|
247 Unconditional_Insert_Avec_Hint
|
|
|
248 (Tree => Target,
|
|
|
249 Hint => 0,
|
|
|
250 Key => SN.Element,
|
|
|
251 Node => Target_Node);
|
|
|
252 end Append_Element;
|
|
|
253
|
|
|
254 -- Start of processing for Assign
|
|
|
255
|
|
|
256 begin
|
|
|
257 if Target'Address = Source'Address then
|
|
|
258 return;
|
|
|
259 end if;
|
|
|
260
|
|
|
261 if Target.Capacity < Source.Length then
|
|
|
262 raise Constraint_Error
|
|
|
263 with "Target capacity is less than Source length";
|
|
|
264 end if;
|
|
|
265
|
|
|
266 Tree_Operations.Clear_Tree (Target);
|
|
|
267 Append_Elements (Source);
|
|
|
268 end Assign;
|
|
|
269
|
|
|
270 -------------
|
|
|
271 -- Ceiling --
|
|
|
272 -------------
|
|
|
273
|
|
|
274 function Ceiling (Container : Set; Item : Element_Type) return Cursor is
|
|
|
275 Node : constant Count_Type := Element_Keys.Ceiling (Container, Item);
|
|
|
276
|
|
|
277 begin
|
|
|
278 if Node = 0 then
|
|
|
279 return No_Element;
|
|
|
280 end if;
|
|
|
281
|
|
|
282 return (Node => Node);
|
|
|
283 end Ceiling;
|
|
|
284
|
|
|
285 -----------
|
|
|
286 -- Clear --
|
|
|
287 -----------
|
|
|
288
|
|
|
289 procedure Clear (Container : in out Set) is
|
|
|
290 begin
|
|
|
291 Tree_Operations.Clear_Tree (Container);
|
|
|
292 end Clear;
|
|
|
293
|
|
|
294 -----------
|
|
|
295 -- Color --
|
|
|
296 -----------
|
|
|
297
|
|
|
298 function Color (Node : Node_Type) return Red_Black_Trees.Color_Type is
|
|
|
299 begin
|
|
|
300 return Node.Color;
|
|
|
301 end Color;
|
|
|
302
|
|
|
303 --------------
|
|
|
304 -- Contains --
|
|
|
305 --------------
|
|
|
306
|
|
|
307 function Contains
|
|
|
308 (Container : Set;
|
|
|
309 Item : Element_Type) return Boolean
|
|
|
310 is
|
|
|
311 begin
|
|
|
312 return Find (Container, Item) /= No_Element;
|
|
|
313 end Contains;
|
|
|
314
|
|
|
315 ----------
|
|
|
316 -- Copy --
|
|
|
317 ----------
|
|
|
318
|
|
|
319 function Copy (Source : Set; Capacity : Count_Type := 0) return Set is
|
|
|
320 Node : Count_Type;
|
|
|
321 N : Count_Type;
|
|
|
322 Target : Set (Count_Type'Max (Source.Capacity, Capacity));
|
|
|
323
|
|
|
324 begin
|
|
|
325 if 0 < Capacity and then Capacity < Source.Capacity then
|
|
|
326 raise Capacity_Error;
|
|
|
327 end if;
|
|
|
328
|
|
|
329 if Length (Source) > 0 then
|
|
|
330 Target.Length := Source.Length;
|
|
|
331 Target.Root := Source.Root;
|
|
|
332 Target.First := Source.First;
|
|
|
333 Target.Last := Source.Last;
|
|
|
334 Target.Free := Source.Free;
|
|
|
335
|
|
|
336 Node := 1;
|
|
|
337 while Node <= Source.Capacity loop
|
|
|
338 Target.Nodes (Node).Element :=
|
|
|
339 Source.Nodes (Node).Element;
|
|
|
340 Target.Nodes (Node).Parent :=
|
|
|
341 Source.Nodes (Node).Parent;
|
|
|
342 Target.Nodes (Node).Left :=
|
|
|
343 Source.Nodes (Node).Left;
|
|
|
344 Target.Nodes (Node).Right :=
|
|
|
345 Source.Nodes (Node).Right;
|
|
|
346 Target.Nodes (Node).Color :=
|
|
|
347 Source.Nodes (Node).Color;
|
|
|
348 Target.Nodes (Node).Has_Element :=
|
|
|
349 Source.Nodes (Node).Has_Element;
|
|
|
350 Node := Node + 1;
|
|
|
351 end loop;
|
|
|
352
|
|
|
353 while Node <= Target.Capacity loop
|
|
|
354 N := Node;
|
|
|
355 Formal_Ordered_Sets.Free (Tree => Target, X => N);
|
|
|
356 Node := Node + 1;
|
|
|
357 end loop;
|
|
|
358 end if;
|
|
|
359
|
|
|
360 return Target;
|
|
|
361 end Copy;
|
|
|
362
|
|
|
363 ------------
|
|
|
364 -- Delete --
|
|
|
365 ------------
|
|
|
366
|
|
|
367 procedure Delete (Container : in out Set; Position : in out Cursor) is
|
|
|
368 begin
|
|
|
369 if not Has_Element (Container, Position) then
|
|
|
370 raise Constraint_Error with "Position cursor has no element";
|
|
|
371 end if;
|
|
|
372
|
|
|
373 pragma Assert (Vet (Container, Position.Node),
|
|
|
374 "bad cursor in Delete");
|
|
|
375
|
|
|
376 Tree_Operations.Delete_Node_Sans_Free (Container,
|
|
|
377 Position.Node);
|
|
|
378 Formal_Ordered_Sets.Free (Container, Position.Node);
|
|
|
379 Position := No_Element;
|
|
|
380 end Delete;
|
|
|
381
|
|
|
382 procedure Delete (Container : in out Set; Item : Element_Type) is
|
|
|
383 X : constant Count_Type := Element_Keys.Find (Container, Item);
|
|
|
384
|
|
|
385 begin
|
|
|
386 if X = 0 then
|
|
|
387 raise Constraint_Error with "attempt to delete element not in set";
|
|
|
388 end if;
|
|
|
389
|
|
|
390 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
391 Formal_Ordered_Sets.Free (Container, X);
|
|
|
392 end Delete;
|
|
|
393
|
|
|
394 ------------------
|
|
|
395 -- Delete_First --
|
|
|
396 ------------------
|
|
|
397
|
|
|
398 procedure Delete_First (Container : in out Set) is
|
|
|
399 X : constant Count_Type := Container.First;
|
|
|
400 begin
|
|
|
401 if X /= 0 then
|
|
|
402 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
403 Formal_Ordered_Sets.Free (Container, X);
|
|
|
404 end if;
|
|
|
405 end Delete_First;
|
|
|
406
|
|
|
407 -----------------
|
|
|
408 -- Delete_Last --
|
|
|
409 -----------------
|
|
|
410
|
|
|
411 procedure Delete_Last (Container : in out Set) is
|
|
|
412 X : constant Count_Type := Container.Last;
|
|
|
413 begin
|
|
|
414 if X /= 0 then
|
|
|
415 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
416 Formal_Ordered_Sets.Free (Container, X);
|
|
|
417 end if;
|
|
|
418 end Delete_Last;
|
|
|
419
|
|
|
420 ----------------
|
|
|
421 -- Difference --
|
|
|
422 ----------------
|
|
|
423
|
|
|
424 procedure Difference (Target : in out Set; Source : Set) is
|
|
|
425 begin
|
|
|
426 Set_Ops.Set_Difference (Target, Source);
|
|
|
427 end Difference;
|
|
|
428
|
|
|
429 function Difference (Left, Right : Set) return Set is
|
|
|
430 begin
|
|
|
431 if Left'Address = Right'Address then
|
|
|
432 return Empty_Set;
|
|
|
433 end if;
|
|
|
434
|
|
|
435 if Length (Left) = 0 then
|
|
|
436 return Empty_Set;
|
|
|
437 end if;
|
|
|
438
|
|
|
439 if Length (Right) = 0 then
|
|
|
440 return Left.Copy;
|
|
|
441 end if;
|
|
|
442
|
|
|
443 return S : Set (Length (Left)) do
|
|
|
444 Assign (S, Set_Ops.Set_Difference (Left, Right));
|
|
|
445 end return;
|
|
|
446 end Difference;
|
|
|
447
|
|
|
448 -------------
|
|
|
449 -- Element --
|
|
|
450 -------------
|
|
|
451
|
|
|
452 function Element (Container : Set; Position : Cursor) return Element_Type is
|
|
|
453 begin
|
|
|
454 if not Has_Element (Container, Position) then
|
|
|
455 raise Constraint_Error with "Position cursor has no element";
|
|
|
456 end if;
|
|
|
457
|
|
|
458 pragma Assert (Vet (Container, Position.Node),
|
|
|
459 "bad cursor in Element");
|
|
|
460
|
|
|
461 return Container.Nodes (Position.Node).Element;
|
|
|
462 end Element;
|
|
|
463
|
|
|
464 -------------------------
|
|
|
465 -- Equivalent_Elements --
|
|
|
466 -------------------------
|
|
|
467
|
|
|
468 function Equivalent_Elements (Left, Right : Element_Type) return Boolean is
|
|
|
469 begin
|
|
|
470 if Left < Right
|
|
|
471 or else Right < Left
|
|
|
472 then
|
|
|
473 return False;
|
|
|
474 else
|
|
|
475 return True;
|
|
|
476 end if;
|
|
|
477 end Equivalent_Elements;
|
|
|
478
|
|
|
479 ---------------------
|
|
|
480 -- Equivalent_Sets --
|
|
|
481 ---------------------
|
|
|
482
|
|
|
483 function Equivalent_Sets (Left, Right : Set) return Boolean is
|
|
|
484 function Is_Equivalent_Node_Node
|
|
|
485 (L, R : Node_Type) return Boolean;
|
|
|
486 pragma Inline (Is_Equivalent_Node_Node);
|
|
|
487
|
|
|
488 function Is_Equivalent is
|
|
|
489 new Tree_Operations.Generic_Equal (Is_Equivalent_Node_Node);
|
|
|
490
|
|
|
491 -----------------------------
|
|
|
492 -- Is_Equivalent_Node_Node --
|
|
|
493 -----------------------------
|
|
|
494
|
|
|
495 function Is_Equivalent_Node_Node (L, R : Node_Type) return Boolean is
|
|
|
496 begin
|
|
|
497 if L.Element < R.Element then
|
|
|
498 return False;
|
|
|
499 elsif R.Element < L.Element then
|
|
|
500 return False;
|
|
|
501 else
|
|
|
502 return True;
|
|
|
503 end if;
|
|
|
504 end Is_Equivalent_Node_Node;
|
|
|
505
|
|
|
506 -- Start of processing for Equivalent_Sets
|
|
|
507
|
|
|
508 begin
|
|
|
509 return Is_Equivalent (Left, Right);
|
|
|
510 end Equivalent_Sets;
|
|
|
511
|
|
|
512 -------------
|
|
|
513 -- Exclude --
|
|
|
514 -------------
|
|
|
515
|
|
|
516 procedure Exclude (Container : in out Set; Item : Element_Type) is
|
|
|
517 X : constant Count_Type := Element_Keys.Find (Container, Item);
|
|
|
518 begin
|
|
|
519 if X /= 0 then
|
|
|
520 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
521 Formal_Ordered_Sets.Free (Container, X);
|
|
|
522 end if;
|
|
|
523 end Exclude;
|
|
|
524
|
|
|
525 ----------
|
|
|
526 -- Find --
|
|
|
527 ----------
|
|
|
528
|
|
|
529 function Find (Container : Set; Item : Element_Type) return Cursor is
|
|
|
530 Node : constant Count_Type := Element_Keys.Find (Container, Item);
|
|
|
531
|
|
|
532 begin
|
|
|
533 if Node = 0 then
|
|
|
534 return No_Element;
|
|
|
535 end if;
|
|
|
536
|
|
|
537 return (Node => Node);
|
|
|
538 end Find;
|
|
|
539
|
|
|
540 -----------
|
|
|
541 -- First --
|
|
|
542 -----------
|
|
|
543
|
|
|
544 function First (Container : Set) return Cursor is
|
|
|
545 begin
|
|
|
546 if Length (Container) = 0 then
|
|
|
547 return No_Element;
|
|
|
548 end if;
|
|
|
549
|
|
|
550 return (Node => Container.First);
|
|
|
551 end First;
|
|
|
552
|
|
|
553 -------------------
|
|
|
554 -- First_Element --
|
|
|
555 -------------------
|
|
|
556
|
|
|
557 function First_Element (Container : Set) return Element_Type is
|
|
|
558 Fst : constant Count_Type := First (Container).Node;
|
|
|
559 begin
|
|
|
560 if Fst = 0 then
|
|
|
561 raise Constraint_Error with "set is empty";
|
|
|
562 end if;
|
|
|
563
|
|
|
564 declare
|
|
|
565 N : Tree_Types.Nodes_Type renames Container.Nodes;
|
|
|
566 begin
|
|
|
567 return N (Fst).Element;
|
|
|
568 end;
|
|
|
569 end First_Element;
|
|
|
570
|
|
|
571 -----------
|
|
|
572 -- Floor --
|
|
|
573 -----------
|
|
|
574
|
|
|
575 function Floor (Container : Set; Item : Element_Type) return Cursor is
|
|
|
576 begin
|
|
|
577 declare
|
|
|
578 Node : constant Count_Type := Element_Keys.Floor (Container, Item);
|
|
|
579
|
|
|
580 begin
|
|
|
581 if Node = 0 then
|
|
|
582 return No_Element;
|
|
|
583 end if;
|
|
|
584
|
|
|
585 return (Node => Node);
|
|
|
586 end;
|
|
|
587 end Floor;
|
|
|
588
|
|
|
589 ------------------
|
|
|
590 -- Formal_Model --
|
|
|
591 ------------------
|
|
|
592
|
|
|
593 package body Formal_Model is
|
|
|
594
|
|
|
595 -------------------------
|
|
|
596 -- E_Bigger_Than_Range --
|
|
|
597 -------------------------
|
|
|
598
|
|
|
599 function E_Bigger_Than_Range
|
|
|
600 (Container : E.Sequence;
|
|
|
601 Fst : Positive_Count_Type;
|
|
|
602 Lst : Count_Type;
|
|
|
603 Item : Element_Type) return Boolean
|
|
|
604 is
|
|
|
605 begin
|
|
|
606 for I in Fst .. Lst loop
|
|
|
607 if not (E.Get (Container, I) < Item) then
|
|
|
608 return False;
|
|
|
609 end if;
|
|
|
610 end loop;
|
|
|
611
|
|
|
612 return True;
|
|
|
613 end E_Bigger_Than_Range;
|
|
|
614
|
|
|
615 -------------------------
|
|
|
616 -- E_Elements_Included --
|
|
|
617 -------------------------
|
|
|
618
|
|
|
619 function E_Elements_Included
|
|
|
620 (Left : E.Sequence;
|
|
|
621 Right : E.Sequence) return Boolean
|
|
|
622 is
|
|
|
623 begin
|
|
|
624 for I in 1 .. E.Length (Left) loop
|
|
|
625 if not E.Contains (Right, 1, E.Length (Right), E.Get (Left, I))
|
|
|
626 then
|
|
|
627 return False;
|
|
|
628 end if;
|
|
|
629 end loop;
|
|
|
630
|
|
|
631 return True;
|
|
|
632 end E_Elements_Included;
|
|
|
633
|
|
|
634 function E_Elements_Included
|
|
|
635 (Left : E.Sequence;
|
|
|
636 Model : M.Set;
|
|
|
637 Right : E.Sequence) return Boolean
|
|
|
638 is
|
|
|
639 begin
|
|
|
640 for I in 1 .. E.Length (Left) loop
|
|
|
641 declare
|
|
|
642 Item : constant Element_Type := E.Get (Left, I);
|
|
|
643 begin
|
|
|
644 if M.Contains (Model, Item) then
|
|
|
645 if not E.Contains (Right, 1, E.Length (Right), Item) then
|
|
|
646 return False;
|
|
|
647 end if;
|
|
|
648 end if;
|
|
|
649 end;
|
|
|
650 end loop;
|
|
|
651
|
|
|
652 return True;
|
|
|
653 end E_Elements_Included;
|
|
|
654
|
|
|
655 function E_Elements_Included
|
|
|
656 (Container : E.Sequence;
|
|
|
657 Model : M.Set;
|
|
|
658 Left : E.Sequence;
|
|
|
659 Right : E.Sequence) return Boolean
|
|
|
660 is
|
|
|
661 begin
|
|
|
662 for I in 1 .. E.Length (Container) loop
|
|
|
663 declare
|
|
|
664 Item : constant Element_Type := E.Get (Container, I);
|
|
|
665 begin
|
|
|
666 if M.Contains (Model, Item) then
|
|
|
667 if not E.Contains (Left, 1, E.Length (Left), Item) then
|
|
|
668 return False;
|
|
|
669 end if;
|
|
|
670 else
|
|
|
671 if not E.Contains (Right, 1, E.Length (Right), Item) then
|
|
|
672 return False;
|
|
|
673 end if;
|
|
|
674 end if;
|
|
|
675 end;
|
|
|
676 end loop;
|
|
|
677
|
|
|
678 return True;
|
|
|
679 end E_Elements_Included;
|
|
|
680
|
|
|
681 ---------------
|
|
|
682 -- E_Is_Find --
|
|
|
683 ---------------
|
|
|
684
|
|
|
685 function E_Is_Find
|
|
|
686 (Container : E.Sequence;
|
|
|
687 Item : Element_Type;
|
|
|
688 Position : Count_Type) return Boolean
|
|
|
689 is
|
|
|
690 begin
|
|
|
691 for I in 1 .. Position - 1 loop
|
|
|
692 if Item < E.Get (Container, I) then
|
|
|
693 return False;
|
|
|
694 end if;
|
|
|
695 end loop;
|
|
|
696
|
|
|
697 if Position < E.Length (Container) then
|
|
|
698 for I in Position + 1 .. E.Length (Container) loop
|
|
|
699 if E.Get (Container, I) < Item then
|
|
|
700 return False;
|
|
|
701 end if;
|
|
|
702 end loop;
|
|
|
703 end if;
|
|
|
704
|
|
|
705 return True;
|
|
|
706 end E_Is_Find;
|
|
|
707
|
|
|
708 --------------------------
|
|
|
709 -- E_Smaller_Than_Range --
|
|
|
710 --------------------------
|
|
|
711
|
|
|
712 function E_Smaller_Than_Range
|
|
|
713 (Container : E.Sequence;
|
|
|
714 Fst : Positive_Count_Type;
|
|
|
715 Lst : Count_Type;
|
|
|
716 Item : Element_Type) return Boolean
|
|
|
717 is
|
|
|
718 begin
|
|
|
719 for I in Fst .. Lst loop
|
|
|
720 if not (Item < E.Get (Container, I)) then
|
|
|
721 return False;
|
|
|
722 end if;
|
|
|
723 end loop;
|
|
|
724
|
|
|
725 return True;
|
|
|
726 end E_Smaller_Than_Range;
|
|
|
727
|
|
|
728 ----------
|
|
|
729 -- Find --
|
|
|
730 ----------
|
|
|
731
|
|
|
732 function Find
|
|
|
733 (Container : E.Sequence;
|
|
|
734 Item : Element_Type) return Count_Type
|
|
|
735 is
|
|
|
736 begin
|
|
|
737 for I in 1 .. E.Length (Container) loop
|
|
|
738 if Equivalent_Elements (Item, E.Get (Container, I)) then
|
|
|
739 return I;
|
|
|
740 end if;
|
|
|
741 end loop;
|
|
|
742
|
|
|
743 return 0;
|
|
|
744 end Find;
|
|
|
745
|
|
|
746 --------------
|
|
|
747 -- Elements --
|
|
|
748 --------------
|
|
|
749
|
|
|
750 function Elements (Container : Set) return E.Sequence is
|
|
|
751 Position : Count_Type := Container.First;
|
|
|
752 R : E.Sequence;
|
|
|
753
|
|
|
754 begin
|
|
|
755 -- Can't use First, Next or Element here, since they depend on models
|
|
|
756 -- for their postconditions.
|
|
|
757
|
|
|
758 while Position /= 0 loop
|
|
|
759 R := E.Add (R, Container.Nodes (Position).Element);
|
|
|
760 Position := Tree_Operations.Next (Container, Position);
|
|
|
761 end loop;
|
|
|
762
|
|
|
763 return R;
|
|
|
764 end Elements;
|
|
|
765
|
|
|
766 ----------------------------
|
|
|
767 -- Lift_Abstraction_Level --
|
|
|
768 ----------------------------
|
|
|
769
|
|
|
770 procedure Lift_Abstraction_Level (Container : Set) is null;
|
|
|
771
|
|
|
772 -----------------------
|
|
|
773 -- Mapping_Preserved --
|
|
|
774 -----------------------
|
|
|
775
|
|
|
776 function Mapping_Preserved
|
|
|
777 (E_Left : E.Sequence;
|
|
|
778 E_Right : E.Sequence;
|
|
|
779 P_Left : P.Map;
|
|
|
780 P_Right : P.Map) return Boolean
|
|
|
781 is
|
|
|
782 begin
|
|
|
783 for C of P_Left loop
|
|
|
784 if not P.Has_Key (P_Right, C)
|
|
|
785 or else P.Get (P_Left, C) > E.Length (E_Left)
|
|
|
786 or else P.Get (P_Right, C) > E.Length (E_Right)
|
|
|
787 or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
|
|
788 E.Get (E_Right, P.Get (P_Right, C))
|
|
|
789 then
|
|
|
790 return False;
|
|
|
791 end if;
|
|
|
792 end loop;
|
|
|
793
|
|
|
794 return True;
|
|
|
795 end Mapping_Preserved;
|
|
|
796
|
|
|
797 ------------------------------
|
|
|
798 -- Mapping_Preserved_Except --
|
|
|
799 ------------------------------
|
|
|
800
|
|
|
801 function Mapping_Preserved_Except
|
|
|
802 (E_Left : E.Sequence;
|
|
|
803 E_Right : E.Sequence;
|
|
|
804 P_Left : P.Map;
|
|
|
805 P_Right : P.Map;
|
|
|
806 Position : Cursor) return Boolean
|
|
|
807 is
|
|
|
808 begin
|
|
|
809 for C of P_Left loop
|
|
|
810 if C /= Position
|
|
|
811 and (not P.Has_Key (P_Right, C)
|
|
|
812 or else P.Get (P_Left, C) > E.Length (E_Left)
|
|
|
813 or else P.Get (P_Right, C) > E.Length (E_Right)
|
|
|
814 or else E.Get (E_Left, P.Get (P_Left, C)) /=
|
|
|
815 E.Get (E_Right, P.Get (P_Right, C)))
|
|
|
816 then
|
|
|
817 return False;
|
|
|
818 end if;
|
|
|
819 end loop;
|
|
|
820
|
|
|
821 return True;
|
|
|
822 end Mapping_Preserved_Except;
|
|
|
823
|
|
|
824 -------------------------
|
|
|
825 -- P_Positions_Shifted --
|
|
|
826 -------------------------
|
|
|
827
|
|
|
828 function P_Positions_Shifted
|
|
|
829 (Small : P.Map;
|
|
|
830 Big : P.Map;
|
|
|
831 Cut : Positive_Count_Type;
|
|
|
832 Count : Count_Type := 1) return Boolean
|
|
|
833 is
|
|
|
834 begin
|
|
|
835 for Cu of Small loop
|
|
|
836 if not P.Has_Key (Big, Cu) then
|
|
|
837 return False;
|
|
|
838 end if;
|
|
|
839 end loop;
|
|
|
840
|
|
|
841 for Cu of Big loop
|
|
|
842 declare
|
|
|
843 Pos : constant Positive_Count_Type := P.Get (Big, Cu);
|
|
|
844
|
|
|
845 begin
|
|
|
846 if Pos < Cut then
|
|
|
847 if not P.Has_Key (Small, Cu)
|
|
|
848 or else Pos /= P.Get (Small, Cu)
|
|
|
849 then
|
|
|
850 return False;
|
|
|
851 end if;
|
|
|
852
|
|
|
853 elsif Pos >= Cut + Count then
|
|
|
854 if not P.Has_Key (Small, Cu)
|
|
|
855 or else Pos /= P.Get (Small, Cu) + Count
|
|
|
856 then
|
|
|
857 return False;
|
|
|
858 end if;
|
|
|
859
|
|
|
860 else
|
|
|
861 if P.Has_Key (Small, Cu) then
|
|
|
862 return False;
|
|
|
863 end if;
|
|
|
864 end if;
|
|
|
865 end;
|
|
|
866 end loop;
|
|
|
867
|
|
|
868 return True;
|
|
|
869 end P_Positions_Shifted;
|
|
|
870
|
|
|
871 -----------
|
|
|
872 -- Model --
|
|
|
873 -----------
|
|
|
874
|
|
|
875 function Model (Container : Set) return M.Set is
|
|
|
876 Position : Count_Type := Container.First;
|
|
|
877 R : M.Set;
|
|
|
878
|
|
|
879 begin
|
|
|
880 -- Can't use First, Next or Element here, since they depend on models
|
|
|
881 -- for their postconditions.
|
|
|
882
|
|
|
883 while Position /= 0 loop
|
|
|
884 R :=
|
|
|
885 M.Add
|
|
|
886 (Container => R,
|
|
|
887 Item => Container.Nodes (Position).Element);
|
|
|
888
|
|
|
889 Position := Tree_Operations.Next (Container, Position);
|
|
|
890 end loop;
|
|
|
891
|
|
|
892 return R;
|
|
|
893 end Model;
|
|
|
894
|
|
|
895 ---------------
|
|
|
896 -- Positions --
|
|
|
897 ---------------
|
|
|
898
|
|
|
899 function Positions (Container : Set) return P.Map is
|
|
|
900 I : Count_Type := 1;
|
|
|
901 Position : Count_Type := Container.First;
|
|
|
902 R : P.Map;
|
|
|
903
|
|
|
904 begin
|
|
|
905 -- Can't use First, Next or Element here, since they depend on models
|
|
|
906 -- for their postconditions.
|
|
|
907
|
|
|
908 while Position /= 0 loop
|
|
|
909 R := P.Add (R, (Node => Position), I);
|
|
|
910 pragma Assert (P.Length (R) = I);
|
|
|
911 Position := Tree_Operations.Next (Container, Position);
|
|
|
912 I := I + 1;
|
|
|
913 end loop;
|
|
|
914
|
|
|
915 return R;
|
|
|
916 end Positions;
|
|
|
917
|
|
|
918 end Formal_Model;
|
|
|
919
|
|
|
920 ----------
|
|
|
921 -- Free --
|
|
|
922 ----------
|
|
|
923
|
|
|
924 procedure Free (Tree : in out Set; X : Count_Type) is
|
|
|
925 begin
|
|
|
926 Tree.Nodes (X).Has_Element := False;
|
|
|
927 Tree_Operations.Free (Tree, X);
|
|
|
928 end Free;
|
|
|
929
|
|
|
930 ----------------------
|
|
|
931 -- Generic_Allocate --
|
|
|
932 ----------------------
|
|
|
933
|
|
|
934 procedure Generic_Allocate
|
|
|
935 (Tree : in out Tree_Types.Tree_Type'Class;
|
|
|
936 Node : out Count_Type)
|
|
|
937 is
|
|
|
938 procedure Allocate is
|
|
|
939 new Tree_Operations.Generic_Allocate (Set_Element);
|
|
|
940 begin
|
|
|
941 Allocate (Tree, Node);
|
|
|
942 Tree.Nodes (Node).Has_Element := True;
|
|
|
943 end Generic_Allocate;
|
|
|
944
|
|
|
945 ------------------
|
|
|
946 -- Generic_Keys --
|
|
|
947 ------------------
|
|
|
948
|
|
|
949 package body Generic_Keys with SPARK_Mode => Off is
|
|
|
950
|
|
|
951 -----------------------
|
|
|
952 -- Local Subprograms --
|
|
|
953 -----------------------
|
|
|
954
|
|
|
955 function Is_Greater_Key_Node
|
|
|
956 (Left : Key_Type;
|
|
|
957 Right : Node_Type) return Boolean;
|
|
|
958 pragma Inline (Is_Greater_Key_Node);
|
|
|
959
|
|
|
960 function Is_Less_Key_Node
|
|
|
961 (Left : Key_Type;
|
|
|
962 Right : Node_Type) return Boolean;
|
|
|
963 pragma Inline (Is_Less_Key_Node);
|
|
|
964
|
|
|
965 --------------------------
|
|
|
966 -- Local Instantiations --
|
|
|
967 --------------------------
|
|
|
968
|
|
|
969 package Key_Keys is
|
|
|
970 new Red_Black_Trees.Generic_Bounded_Keys
|
|
|
971 (Tree_Operations => Tree_Operations,
|
|
|
972 Key_Type => Key_Type,
|
|
|
973 Is_Less_Key_Node => Is_Less_Key_Node,
|
|
|
974 Is_Greater_Key_Node => Is_Greater_Key_Node);
|
|
|
975
|
|
|
976 -------------
|
|
|
977 -- Ceiling --
|
|
|
978 -------------
|
|
|
979
|
|
|
980 function Ceiling (Container : Set; Key : Key_Type) return Cursor is
|
|
|
981 Node : constant Count_Type := Key_Keys.Ceiling (Container, Key);
|
|
|
982
|
|
|
983 begin
|
|
|
984 if Node = 0 then
|
|
|
985 return No_Element;
|
|
|
986 end if;
|
|
|
987
|
|
|
988 return (Node => Node);
|
|
|
989 end Ceiling;
|
|
|
990
|
|
|
991 --------------
|
|
|
992 -- Contains --
|
|
|
993 --------------
|
|
|
994
|
|
|
995 function Contains (Container : Set; Key : Key_Type) return Boolean is
|
|
|
996 begin
|
|
|
997 return Find (Container, Key) /= No_Element;
|
|
|
998 end Contains;
|
|
|
999
|
|
|
1000 ------------
|
|
|
1001 -- Delete --
|
|
|
1002 ------------
|
|
|
1003
|
|
|
1004 procedure Delete (Container : in out Set; Key : Key_Type) is
|
|
|
1005 X : constant Count_Type := Key_Keys.Find (Container, Key);
|
|
|
1006
|
|
|
1007 begin
|
|
|
1008 if X = 0 then
|
|
|
1009 raise Constraint_Error with "attempt to delete key not in set";
|
|
|
1010 end if;
|
|
|
1011
|
|
|
1012 Delete_Node_Sans_Free (Container, X);
|
|
|
1013 Formal_Ordered_Sets.Free (Container, X);
|
|
|
1014 end Delete;
|
|
|
1015
|
|
|
1016 -------------
|
|
|
1017 -- Element --
|
|
|
1018 -------------
|
|
|
1019
|
|
|
1020 function Element (Container : Set; Key : Key_Type) return Element_Type is
|
|
|
1021 Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
|
|
1022
|
|
|
1023 begin
|
|
|
1024 if Node = 0 then
|
|
|
1025 raise Constraint_Error with "key not in set";
|
|
|
1026 end if;
|
|
|
1027
|
|
|
1028 declare
|
|
|
1029 N : Tree_Types.Nodes_Type renames Container.Nodes;
|
|
|
1030 begin
|
|
|
1031 return N (Node).Element;
|
|
|
1032 end;
|
|
|
1033 end Element;
|
|
|
1034
|
|
|
1035 ---------------------
|
|
|
1036 -- Equivalent_Keys --
|
|
|
1037 ---------------------
|
|
|
1038
|
|
|
1039 function Equivalent_Keys (Left, Right : Key_Type) return Boolean is
|
|
|
1040 begin
|
|
|
1041 if Left < Right
|
|
|
1042 or else Right < Left
|
|
|
1043 then
|
|
|
1044 return False;
|
|
|
1045 else
|
|
|
1046 return True;
|
|
|
1047 end if;
|
|
|
1048 end Equivalent_Keys;
|
|
|
1049
|
|
|
1050 -------------
|
|
|
1051 -- Exclude --
|
|
|
1052 -------------
|
|
|
1053
|
|
|
1054 procedure Exclude (Container : in out Set; Key : Key_Type) is
|
|
|
1055 X : constant Count_Type := Key_Keys.Find (Container, Key);
|
|
|
1056 begin
|
|
|
1057 if X /= 0 then
|
|
|
1058 Delete_Node_Sans_Free (Container, X);
|
|
|
1059 Formal_Ordered_Sets.Free (Container, X);
|
|
|
1060 end if;
|
|
|
1061 end Exclude;
|
|
|
1062
|
|
|
1063 ----------
|
|
|
1064 -- Find --
|
|
|
1065 ----------
|
|
|
1066
|
|
|
1067 function Find (Container : Set; Key : Key_Type) return Cursor is
|
|
|
1068 Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
|
|
1069 begin
|
|
|
1070 return (if Node = 0 then No_Element else (Node => Node));
|
|
|
1071 end Find;
|
|
|
1072
|
|
|
1073 -----------
|
|
|
1074 -- Floor --
|
|
|
1075 -----------
|
|
|
1076
|
|
|
1077 function Floor (Container : Set; Key : Key_Type) return Cursor is
|
|
|
1078 Node : constant Count_Type := Key_Keys.Floor (Container, Key);
|
|
|
1079 begin
|
|
|
1080 return (if Node = 0 then No_Element else (Node => Node));
|
|
|
1081 end Floor;
|
|
|
1082
|
|
|
1083 ------------------
|
|
|
1084 -- Formal_Model --
|
|
|
1085 ------------------
|
|
|
1086
|
|
|
1087 package body Formal_Model is
|
|
|
1088
|
|
|
1089 -------------------------
|
|
|
1090 -- E_Bigger_Than_Range --
|
|
|
1091 -------------------------
|
|
|
1092
|
|
|
1093 function E_Bigger_Than_Range
|
|
|
1094 (Container : E.Sequence;
|
|
|
1095 Fst : Positive_Count_Type;
|
|
|
1096 Lst : Count_Type;
|
|
|
1097 Key : Key_Type) return Boolean
|
|
|
1098 is
|
|
|
1099 begin
|
|
|
1100 for I in Fst .. Lst loop
|
|
|
1101 if not (Generic_Keys.Key (E.Get (Container, I)) < Key) then
|
|
|
1102 return False;
|
|
|
1103 end if;
|
|
|
1104 end loop;
|
|
|
1105 return True;
|
|
|
1106 end E_Bigger_Than_Range;
|
|
|
1107
|
|
|
1108 ---------------
|
|
|
1109 -- E_Is_Find --
|
|
|
1110 ---------------
|
|
|
1111
|
|
|
1112 function E_Is_Find
|
|
|
1113 (Container : E.Sequence;
|
|
|
1114 Key : Key_Type;
|
|
|
1115 Position : Count_Type) return Boolean
|
|
|
1116 is
|
|
|
1117 begin
|
|
|
1118 for I in 1 .. Position - 1 loop
|
|
|
1119 if Key < Generic_Keys.Key (E.Get (Container, I)) then
|
|
|
1120 return False;
|
|
|
1121 end if;
|
|
|
1122 end loop;
|
|
|
1123
|
|
|
1124 if Position < E.Length (Container) then
|
|
|
1125 for I in Position + 1 .. E.Length (Container) loop
|
|
|
1126 if Generic_Keys.Key (E.Get (Container, I)) < Key then
|
|
|
1127 return False;
|
|
|
1128 end if;
|
|
|
1129 end loop;
|
|
|
1130 end if;
|
|
|
1131 return True;
|
|
|
1132 end E_Is_Find;
|
|
|
1133
|
|
|
1134 --------------------------
|
|
|
1135 -- E_Smaller_Than_Range --
|
|
|
1136 --------------------------
|
|
|
1137
|
|
|
1138 function E_Smaller_Than_Range
|
|
|
1139 (Container : E.Sequence;
|
|
|
1140 Fst : Positive_Count_Type;
|
|
|
1141 Lst : Count_Type;
|
|
|
1142 Key : Key_Type) return Boolean
|
|
|
1143 is
|
|
|
1144 begin
|
|
|
1145 for I in Fst .. Lst loop
|
|
|
1146 if not (Key < Generic_Keys.Key (E.Get (Container, I))) then
|
|
|
1147 return False;
|
|
|
1148 end if;
|
|
|
1149 end loop;
|
|
|
1150 return True;
|
|
|
1151 end E_Smaller_Than_Range;
|
|
|
1152
|
|
|
1153 ----------
|
|
|
1154 -- Find --
|
|
|
1155 ----------
|
|
|
1156
|
|
|
1157 function Find
|
|
|
1158 (Container : E.Sequence;
|
|
|
1159 Key : Key_Type) return Count_Type
|
|
|
1160 is
|
|
|
1161 begin
|
|
|
1162 for I in 1 .. E.Length (Container) loop
|
|
|
1163 if Equivalent_Keys
|
|
|
1164 (Key, Generic_Keys.Key (E.Get (Container, I)))
|
|
|
1165 then
|
|
|
1166 return I;
|
|
|
1167 end if;
|
|
|
1168 end loop;
|
|
|
1169 return 0;
|
|
|
1170 end Find;
|
|
|
1171
|
|
|
1172 -----------------------
|
|
|
1173 -- M_Included_Except --
|
|
|
1174 -----------------------
|
|
|
1175
|
|
|
1176 function M_Included_Except
|
|
|
1177 (Left : M.Set;
|
|
|
1178 Right : M.Set;
|
|
|
1179 Key : Key_Type) return Boolean
|
|
|
1180 is
|
|
|
1181 begin
|
|
|
1182 for E of Left loop
|
|
|
1183 if not Contains (Right, E)
|
|
|
1184 and not Equivalent_Keys (Generic_Keys.Key (E), Key)
|
|
|
1185 then
|
|
|
1186 return False;
|
|
|
1187 end if;
|
|
|
1188 end loop;
|
|
|
1189 return True;
|
|
|
1190 end M_Included_Except;
|
|
|
1191 end Formal_Model;
|
|
|
1192
|
|
|
1193 -------------------------
|
|
|
1194 -- Is_Greater_Key_Node --
|
|
|
1195 -------------------------
|
|
|
1196
|
|
|
1197 function Is_Greater_Key_Node
|
|
|
1198 (Left : Key_Type;
|
|
|
1199 Right : Node_Type) return Boolean
|
|
|
1200 is
|
|
|
1201 begin
|
|
|
1202 return Key (Right.Element) < Left;
|
|
|
1203 end Is_Greater_Key_Node;
|
|
|
1204
|
|
|
1205 ----------------------
|
|
|
1206 -- Is_Less_Key_Node --
|
|
|
1207 ----------------------
|
|
|
1208
|
|
|
1209 function Is_Less_Key_Node
|
|
|
1210 (Left : Key_Type;
|
|
|
1211 Right : Node_Type) return Boolean
|
|
|
1212 is
|
|
|
1213 begin
|
|
|
1214 return Left < Key (Right.Element);
|
|
|
1215 end Is_Less_Key_Node;
|
|
|
1216
|
|
|
1217 ---------
|
|
|
1218 -- Key --
|
|
|
1219 ---------
|
|
|
1220
|
|
|
1221 function Key (Container : Set; Position : Cursor) return Key_Type is
|
|
|
1222 begin
|
|
|
1223 if not Has_Element (Container, Position) then
|
|
|
1224 raise Constraint_Error with
|
|
|
1225 "Position cursor has no element";
|
|
|
1226 end if;
|
|
|
1227
|
|
|
1228 pragma Assert (Vet (Container, Position.Node),
|
|
|
1229 "bad cursor in Key");
|
|
|
1230
|
|
|
1231 declare
|
|
|
1232 N : Tree_Types.Nodes_Type renames Container.Nodes;
|
|
|
1233 begin
|
|
|
1234 return Key (N (Position.Node).Element);
|
|
|
1235 end;
|
|
|
1236 end Key;
|
|
|
1237
|
|
|
1238 -------------
|
|
|
1239 -- Replace --
|
|
|
1240 -------------
|
|
|
1241
|
|
|
1242 procedure Replace
|
|
|
1243 (Container : in out Set;
|
|
|
1244 Key : Key_Type;
|
|
|
1245 New_Item : Element_Type)
|
|
|
1246 is
|
|
|
1247 Node : constant Count_Type := Key_Keys.Find (Container, Key);
|
|
|
1248 begin
|
|
|
1249 if not Has_Element (Container, (Node => Node)) then
|
|
|
1250 raise Constraint_Error with
|
|
|
1251 "attempt to replace key not in set";
|
|
|
1252 else
|
|
|
1253 Replace_Element (Container, Node, New_Item);
|
|
|
1254 end if;
|
|
|
1255 end Replace;
|
|
|
1256
|
|
|
1257 end Generic_Keys;
|
|
|
1258
|
|
|
1259 -----------------
|
|
|
1260 -- Has_Element --
|
|
|
1261 -----------------
|
|
|
1262
|
|
|
1263 function Has_Element (Container : Set; Position : Cursor) return Boolean is
|
|
|
1264 begin
|
|
|
1265 if Position.Node = 0 then
|
|
|
1266 return False;
|
|
|
1267 else
|
|
|
1268 return Container.Nodes (Position.Node).Has_Element;
|
|
|
1269 end if;
|
|
|
1270 end Has_Element;
|
|
|
1271
|
|
|
1272 -------------
|
|
|
1273 -- Include --
|
|
|
1274 -------------
|
|
|
1275
|
|
|
1276 procedure Include (Container : in out Set; New_Item : Element_Type) is
|
|
|
1277 Position : Cursor;
|
|
|
1278 Inserted : Boolean;
|
|
|
1279
|
|
|
1280 begin
|
|
|
1281 Insert (Container, New_Item, Position, Inserted);
|
|
|
1282
|
|
|
1283 if not Inserted then
|
|
|
1284 declare
|
|
|
1285 N : Tree_Types.Nodes_Type renames Container.Nodes;
|
|
|
1286 begin
|
|
|
1287 N (Position.Node).Element := New_Item;
|
|
|
1288 end;
|
|
|
1289 end if;
|
|
|
1290 end Include;
|
|
|
1291
|
|
|
1292 ------------
|
|
|
1293 -- Insert --
|
|
|
1294 ------------
|
|
|
1295
|
|
|
1296 procedure Insert
|
|
|
1297 (Container : in out Set;
|
|
|
1298 New_Item : Element_Type;
|
|
|
1299 Position : out Cursor;
|
|
|
1300 Inserted : out Boolean)
|
|
|
1301 is
|
|
|
1302 begin
|
|
|
1303 Insert_Sans_Hint (Container, New_Item, Position.Node, Inserted);
|
|
|
1304 end Insert;
|
|
|
1305
|
|
|
1306 procedure Insert
|
|
|
1307 (Container : in out Set;
|
|
|
1308 New_Item : Element_Type)
|
|
|
1309 is
|
|
|
1310 Position : Cursor;
|
|
|
1311 Inserted : Boolean;
|
|
|
1312
|
|
|
1313 begin
|
|
|
1314 Insert (Container, New_Item, Position, Inserted);
|
|
|
1315
|
|
|
1316 if not Inserted then
|
|
|
1317 raise Constraint_Error with
|
|
|
1318 "attempt to insert element already in set";
|
|
|
1319 end if;
|
|
|
1320 end Insert;
|
|
|
1321
|
|
|
1322 ----------------------
|
|
|
1323 -- Insert_Sans_Hint --
|
|
|
1324 ----------------------
|
|
|
1325
|
|
|
1326 procedure Insert_Sans_Hint
|
|
|
1327 (Container : in out Set;
|
|
|
1328 New_Item : Element_Type;
|
|
|
1329 Node : out Count_Type;
|
|
|
1330 Inserted : out Boolean)
|
|
|
1331 is
|
|
|
1332 procedure Set_Element (Node : in out Node_Type);
|
|
|
1333
|
|
|
1334 function New_Node return Count_Type;
|
|
|
1335 pragma Inline (New_Node);
|
|
|
1336
|
|
|
1337 procedure Insert_Post is
|
|
|
1338 new Element_Keys.Generic_Insert_Post (New_Node);
|
|
|
1339
|
|
|
1340 procedure Conditional_Insert_Sans_Hint is
|
|
|
1341 new Element_Keys.Generic_Conditional_Insert (Insert_Post);
|
|
|
1342
|
|
|
1343 procedure Allocate is new Generic_Allocate (Set_Element);
|
|
|
1344
|
|
|
1345 --------------
|
|
|
1346 -- New_Node --
|
|
|
1347 --------------
|
|
|
1348
|
|
|
1349 function New_Node return Count_Type is
|
|
|
1350 Result : Count_Type;
|
|
|
1351 begin
|
|
|
1352 Allocate (Container, Result);
|
|
|
1353 return Result;
|
|
|
1354 end New_Node;
|
|
|
1355
|
|
|
1356 -----------------
|
|
|
1357 -- Set_Element --
|
|
|
1358 -----------------
|
|
|
1359
|
|
|
1360 procedure Set_Element (Node : in out Node_Type) is
|
|
|
1361 begin
|
|
|
1362 Node.Element := New_Item;
|
|
|
1363 end Set_Element;
|
|
|
1364
|
|
|
1365 -- Start of processing for Insert_Sans_Hint
|
|
|
1366
|
|
|
1367 begin
|
|
|
1368 Conditional_Insert_Sans_Hint
|
|
|
1369 (Container,
|
|
|
1370 New_Item,
|
|
|
1371 Node,
|
|
|
1372 Inserted);
|
|
|
1373 end Insert_Sans_Hint;
|
|
|
1374
|
|
|
1375 ----------------------
|
|
|
1376 -- Insert_With_Hint --
|
|
|
1377 ----------------------
|
|
|
1378
|
|
|
1379 procedure Insert_With_Hint
|
|
|
1380 (Dst_Set : in out Set;
|
|
|
1381 Dst_Hint : Count_Type;
|
|
|
1382 Src_Node : Node_Type;
|
|
|
1383 Dst_Node : out Count_Type)
|
|
|
1384 is
|
|
|
1385 Success : Boolean;
|
|
|
1386 pragma Unreferenced (Success);
|
|
|
1387
|
|
|
1388 procedure Set_Element (Node : in out Node_Type);
|
|
|
1389
|
|
|
1390 function New_Node return Count_Type;
|
|
|
1391 pragma Inline (New_Node);
|
|
|
1392
|
|
|
1393 procedure Insert_Post is
|
|
|
1394 new Element_Keys.Generic_Insert_Post (New_Node);
|
|
|
1395
|
|
|
1396 procedure Insert_Sans_Hint is
|
|
|
1397 new Element_Keys.Generic_Conditional_Insert (Insert_Post);
|
|
|
1398
|
|
|
1399 procedure Local_Insert_With_Hint is
|
|
|
1400 new Element_Keys.Generic_Conditional_Insert_With_Hint
|
|
|
1401 (Insert_Post, Insert_Sans_Hint);
|
|
|
1402
|
|
|
1403 procedure Allocate is new Generic_Allocate (Set_Element);
|
|
|
1404
|
|
|
1405 --------------
|
|
|
1406 -- New_Node --
|
|
|
1407 --------------
|
|
|
1408
|
|
|
1409 function New_Node return Count_Type is
|
|
|
1410 Result : Count_Type;
|
|
|
1411 begin
|
|
|
1412 Allocate (Dst_Set, Result);
|
|
|
1413 return Result;
|
|
|
1414 end New_Node;
|
|
|
1415
|
|
|
1416 -----------------
|
|
|
1417 -- Set_Element --
|
|
|
1418 -----------------
|
|
|
1419
|
|
|
1420 procedure Set_Element (Node : in out Node_Type) is
|
|
|
1421 begin
|
|
|
1422 Node.Element := Src_Node.Element;
|
|
|
1423 end Set_Element;
|
|
|
1424
|
|
|
1425 -- Start of processing for Insert_With_Hint
|
|
|
1426
|
|
|
1427 begin
|
|
|
1428 Local_Insert_With_Hint
|
|
|
1429 (Dst_Set,
|
|
|
1430 Dst_Hint,
|
|
|
1431 Src_Node.Element,
|
|
|
1432 Dst_Node,
|
|
|
1433 Success);
|
|
|
1434 end Insert_With_Hint;
|
|
|
1435
|
|
|
1436 ------------------
|
|
|
1437 -- Intersection --
|
|
|
1438 ------------------
|
|
|
1439
|
|
|
1440 procedure Intersection (Target : in out Set; Source : Set) is
|
|
|
1441 begin
|
|
|
1442 Set_Ops.Set_Intersection (Target, Source);
|
|
|
1443 end Intersection;
|
|
|
1444
|
|
|
1445 function Intersection (Left, Right : Set) return Set is
|
|
|
1446 begin
|
|
|
1447 if Left'Address = Right'Address then
|
|
|
1448 return Left.Copy;
|
|
|
1449 end if;
|
|
|
1450
|
|
|
1451 return S : Set (Count_Type'Min (Length (Left), Length (Right))) do
|
|
|
1452 Assign (S, Set_Ops.Set_Intersection (Left, Right));
|
|
|
1453 end return;
|
|
|
1454 end Intersection;
|
|
|
1455
|
|
|
1456 --------------
|
|
|
1457 -- Is_Empty --
|
|
|
1458 --------------
|
|
|
1459
|
|
|
1460 function Is_Empty (Container : Set) return Boolean is
|
|
|
1461 begin
|
|
|
1462 return Length (Container) = 0;
|
|
|
1463 end Is_Empty;
|
|
|
1464
|
|
|
1465 -----------------------------
|
|
|
1466 -- Is_Greater_Element_Node --
|
|
|
1467 -----------------------------
|
|
|
1468
|
|
|
1469 function Is_Greater_Element_Node
|
|
|
1470 (Left : Element_Type;
|
|
|
1471 Right : Node_Type) return Boolean
|
|
|
1472 is
|
|
|
1473 begin
|
|
|
1474 -- Compute e > node same as node < e
|
|
|
1475
|
|
|
1476 return Right.Element < Left;
|
|
|
1477 end Is_Greater_Element_Node;
|
|
|
1478
|
|
|
1479 --------------------------
|
|
|
1480 -- Is_Less_Element_Node --
|
|
|
1481 --------------------------
|
|
|
1482
|
|
|
1483 function Is_Less_Element_Node
|
|
|
1484 (Left : Element_Type;
|
|
|
1485 Right : Node_Type) return Boolean
|
|
|
1486 is
|
|
|
1487 begin
|
|
|
1488 return Left < Right.Element;
|
|
|
1489 end Is_Less_Element_Node;
|
|
|
1490
|
|
|
1491 -----------------------
|
|
|
1492 -- Is_Less_Node_Node --
|
|
|
1493 -----------------------
|
|
|
1494
|
|
|
1495 function Is_Less_Node_Node (L, R : Node_Type) return Boolean is
|
|
|
1496 begin
|
|
|
1497 return L.Element < R.Element;
|
|
|
1498 end Is_Less_Node_Node;
|
|
|
1499
|
|
|
1500 ---------------
|
|
|
1501 -- Is_Subset --
|
|
|
1502 ---------------
|
|
|
1503
|
|
|
1504 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
|
|
|
1505 begin
|
|
|
1506 return Set_Ops.Set_Subset (Subset, Of_Set => Of_Set);
|
|
|
1507 end Is_Subset;
|
|
|
1508
|
|
|
1509 ----------
|
|
|
1510 -- Last --
|
|
|
1511 ----------
|
|
|
1512
|
|
|
1513 function Last (Container : Set) return Cursor is
|
|
|
1514 begin
|
|
|
1515 return (if Length (Container) = 0
|
|
|
1516 then No_Element
|
|
|
1517 else (Node => Container.Last));
|
|
|
1518 end Last;
|
|
|
1519
|
|
|
1520 ------------------
|
|
|
1521 -- Last_Element --
|
|
|
1522 ------------------
|
|
|
1523
|
|
|
1524 function Last_Element (Container : Set) return Element_Type is
|
|
|
1525 begin
|
|
|
1526 if Last (Container).Node = 0 then
|
|
|
1527 raise Constraint_Error with "set is empty";
|
|
|
1528 end if;
|
|
|
1529
|
|
|
1530 declare
|
|
|
1531 N : Tree_Types.Nodes_Type renames Container.Nodes;
|
|
|
1532 begin
|
|
|
1533 return N (Last (Container).Node).Element;
|
|
|
1534 end;
|
|
|
1535 end Last_Element;
|
|
|
1536
|
|
|
1537 --------------
|
|
|
1538 -- Left_Son --
|
|
|
1539 --------------
|
|
|
1540
|
|
|
1541 function Left_Son (Node : Node_Type) return Count_Type is
|
|
|
1542 begin
|
|
|
1543 return Node.Left;
|
|
|
1544 end Left_Son;
|
|
|
1545
|
|
|
1546 ------------
|
|
|
1547 -- Length --
|
|
|
1548 ------------
|
|
|
1549
|
|
|
1550 function Length (Container : Set) return Count_Type is
|
|
|
1551 begin
|
|
|
1552 return Container.Length;
|
|
|
1553 end Length;
|
|
|
1554
|
|
|
1555 ----------
|
|
|
1556 -- Move --
|
|
|
1557 ----------
|
|
|
1558
|
|
|
1559 procedure Move (Target : in out Set; Source : in out Set) is
|
|
|
1560 N : Tree_Types.Nodes_Type renames Source.Nodes;
|
|
|
1561 X : Count_Type;
|
|
|
1562
|
|
|
1563 begin
|
|
|
1564 if Target'Address = Source'Address then
|
|
|
1565 return;
|
|
|
1566 end if;
|
|
|
1567
|
|
|
1568 if Target.Capacity < Length (Source) then
|
|
|
1569 raise Constraint_Error with -- ???
|
|
|
1570 "Source length exceeds Target capacity";
|
|
|
1571 end if;
|
|
|
1572
|
|
|
1573 Clear (Target);
|
|
|
1574
|
|
|
1575 loop
|
|
|
1576 X := Source.First;
|
|
|
1577 exit when X = 0;
|
|
|
1578
|
|
|
1579 Insert (Target, N (X).Element); -- optimize???
|
|
|
1580
|
|
|
1581 Tree_Operations.Delete_Node_Sans_Free (Source, X);
|
|
|
1582 Formal_Ordered_Sets.Free (Source, X);
|
|
|
1583 end loop;
|
|
|
1584 end Move;
|
|
|
1585
|
|
|
1586 ----------
|
|
|
1587 -- Next --
|
|
|
1588 ----------
|
|
|
1589
|
|
|
1590 function Next (Container : Set; Position : Cursor) return Cursor is
|
|
|
1591 begin
|
|
|
1592 if Position = No_Element then
|
|
|
1593 return No_Element;
|
|
|
1594 end if;
|
|
|
1595
|
|
|
1596 if not Has_Element (Container, Position) then
|
|
|
1597 raise Constraint_Error;
|
|
|
1598 end if;
|
|
|
1599
|
|
|
1600 pragma Assert (Vet (Container, Position.Node),
|
|
|
1601 "bad cursor in Next");
|
|
|
1602 return (Node => Tree_Operations.Next (Container, Position.Node));
|
|
|
1603 end Next;
|
|
|
1604
|
|
|
1605 procedure Next (Container : Set; Position : in out Cursor) is
|
|
|
1606 begin
|
|
|
1607 Position := Next (Container, Position);
|
|
|
1608 end Next;
|
|
|
1609
|
|
|
1610 -------------
|
|
|
1611 -- Overlap --
|
|
|
1612 -------------
|
|
|
1613
|
|
|
1614 function Overlap (Left, Right : Set) return Boolean is
|
|
|
1615 begin
|
|
|
1616 return Set_Ops.Set_Overlap (Left, Right);
|
|
|
1617 end Overlap;
|
|
|
1618
|
|
|
1619 ------------
|
|
|
1620 -- Parent --
|
|
|
1621 ------------
|
|
|
1622
|
|
|
1623 function Parent (Node : Node_Type) return Count_Type is
|
|
|
1624 begin
|
|
|
1625 return Node.Parent;
|
|
|
1626 end Parent;
|
|
|
1627
|
|
|
1628 --------------
|
|
|
1629 -- Previous --
|
|
|
1630 --------------
|
|
|
1631
|
|
|
1632 function Previous (Container : Set; Position : Cursor) return Cursor is
|
|
|
1633 begin
|
|
|
1634 if Position = No_Element then
|
|
|
1635 return No_Element;
|
|
|
1636 end if;
|
|
|
1637
|
|
|
1638 if not Has_Element (Container, Position) then
|
|
|
1639 raise Constraint_Error;
|
|
|
1640 end if;
|
|
|
1641
|
|
|
1642 pragma Assert (Vet (Container, Position.Node),
|
|
|
1643 "bad cursor in Previous");
|
|
|
1644
|
|
|
1645 declare
|
|
|
1646 Node : constant Count_Type :=
|
|
|
1647 Tree_Operations.Previous (Container, Position.Node);
|
|
|
1648 begin
|
|
|
1649 return (if Node = 0 then No_Element else (Node => Node));
|
|
|
1650 end;
|
|
|
1651 end Previous;
|
|
|
1652
|
|
|
1653 procedure Previous (Container : Set; Position : in out Cursor) is
|
|
|
1654 begin
|
|
|
1655 Position := Previous (Container, Position);
|
|
|
1656 end Previous;
|
|
|
1657
|
|
|
1658 -------------
|
|
|
1659 -- Replace --
|
|
|
1660 -------------
|
|
|
1661
|
|
|
1662 procedure Replace (Container : in out Set; New_Item : Element_Type) is
|
|
|
1663 Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
|
|
|
1664
|
|
|
1665 begin
|
|
|
1666 if Node = 0 then
|
|
|
1667 raise Constraint_Error with
|
|
|
1668 "attempt to replace element not in set";
|
|
|
1669 end if;
|
|
|
1670
|
|
|
1671 Container.Nodes (Node).Element := New_Item;
|
|
|
1672 end Replace;
|
|
|
1673
|
|
|
1674 ---------------------
|
|
|
1675 -- Replace_Element --
|
|
|
1676 ---------------------
|
|
|
1677
|
|
|
1678 procedure Replace_Element
|
|
|
1679 (Tree : in out Set;
|
|
|
1680 Node : Count_Type;
|
|
|
1681 Item : Element_Type)
|
|
|
1682 is
|
|
|
1683 pragma Assert (Node /= 0);
|
|
|
1684
|
|
|
1685 function New_Node return Count_Type;
|
|
|
1686 pragma Inline (New_Node);
|
|
|
1687
|
|
|
1688 procedure Local_Insert_Post is
|
|
|
1689 new Element_Keys.Generic_Insert_Post (New_Node);
|
|
|
1690
|
|
|
1691 procedure Local_Insert_Sans_Hint is
|
|
|
1692 new Element_Keys.Generic_Conditional_Insert (Local_Insert_Post);
|
|
|
1693
|
|
|
1694 procedure Local_Insert_With_Hint is
|
|
|
1695 new Element_Keys.Generic_Conditional_Insert_With_Hint
|
|
|
1696 (Local_Insert_Post,
|
|
|
1697 Local_Insert_Sans_Hint);
|
|
|
1698
|
|
|
1699 NN : Tree_Types.Nodes_Type renames Tree.Nodes;
|
|
|
1700
|
|
|
1701 --------------
|
|
|
1702 -- New_Node --
|
|
|
1703 --------------
|
|
|
1704
|
|
|
1705 function New_Node return Count_Type is
|
|
|
1706 N : Node_Type renames NN (Node);
|
|
|
1707 begin
|
|
|
1708 N.Element := Item;
|
|
|
1709 N.Color := Red;
|
|
|
1710 N.Parent := 0;
|
|
|
1711 N.Right := 0;
|
|
|
1712 N.Left := 0;
|
|
|
1713 return Node;
|
|
|
1714 end New_Node;
|
|
|
1715
|
|
|
1716 Hint : Count_Type;
|
|
|
1717 Result : Count_Type;
|
|
|
1718 Inserted : Boolean;
|
|
|
1719
|
|
|
1720 -- Start of processing for Insert
|
|
|
1721
|
|
|
1722 begin
|
|
|
1723 if Item < NN (Node).Element
|
|
|
1724 or else NN (Node).Element < Item
|
|
|
1725 then
|
|
|
1726 null;
|
|
|
1727
|
|
|
1728 else
|
|
|
1729 NN (Node).Element := Item;
|
|
|
1730 return;
|
|
|
1731 end if;
|
|
|
1732
|
|
|
1733 Hint := Element_Keys.Ceiling (Tree, Item);
|
|
|
1734
|
|
|
1735 if Hint = 0 then
|
|
|
1736 null;
|
|
|
1737
|
|
|
1738 elsif Item < NN (Hint).Element then
|
|
|
1739 if Hint = Node then
|
|
|
1740 NN (Node).Element := Item;
|
|
|
1741 return;
|
|
|
1742 end if;
|
|
|
1743
|
|
|
1744 else
|
|
|
1745 pragma Assert (not (NN (Hint).Element < Item));
|
|
|
1746 raise Program_Error with "attempt to replace existing element";
|
|
|
1747 end if;
|
|
|
1748
|
|
|
1749 Tree_Operations.Delete_Node_Sans_Free (Tree, Node);
|
|
|
1750
|
|
|
1751 Local_Insert_With_Hint
|
|
|
1752 (Tree => Tree,
|
|
|
1753 Position => Hint,
|
|
|
1754 Key => Item,
|
|
|
1755 Node => Result,
|
|
|
1756 Inserted => Inserted);
|
|
|
1757
|
|
|
1758 pragma Assert (Inserted);
|
|
|
1759 pragma Assert (Result = Node);
|
|
|
1760 end Replace_Element;
|
|
|
1761
|
|
|
1762 procedure Replace_Element
|
|
|
1763 (Container : in out Set;
|
|
|
1764 Position : Cursor;
|
|
|
1765 New_Item : Element_Type)
|
|
|
1766 is
|
|
|
1767 begin
|
|
|
1768 if not Has_Element (Container, Position) then
|
|
|
1769 raise Constraint_Error with
|
|
|
1770 "Position cursor has no element";
|
|
|
1771 end if;
|
|
|
1772
|
|
|
1773 pragma Assert (Vet (Container, Position.Node),
|
|
|
1774 "bad cursor in Replace_Element");
|
|
|
1775
|
|
|
1776 Replace_Element (Container, Position.Node, New_Item);
|
|
|
1777 end Replace_Element;
|
|
|
1778
|
|
|
1779 ---------------
|
|
|
1780 -- Right_Son --
|
|
|
1781 ---------------
|
|
|
1782
|
|
|
1783 function Right_Son (Node : Node_Type) return Count_Type is
|
|
|
1784 begin
|
|
|
1785 return Node.Right;
|
|
|
1786 end Right_Son;
|
|
|
1787
|
|
|
1788 ---------------
|
|
|
1789 -- Set_Color --
|
|
|
1790 ---------------
|
|
|
1791
|
|
|
1792 procedure Set_Color
|
|
|
1793 (Node : in out Node_Type;
|
|
|
1794 Color : Red_Black_Trees.Color_Type)
|
|
|
1795 is
|
|
|
1796 begin
|
|
|
1797 Node.Color := Color;
|
|
|
1798 end Set_Color;
|
|
|
1799
|
|
|
1800 --------------
|
|
|
1801 -- Set_Left --
|
|
|
1802 --------------
|
|
|
1803
|
|
|
1804 procedure Set_Left (Node : in out Node_Type; Left : Count_Type) is
|
|
|
1805 begin
|
|
|
1806 Node.Left := Left;
|
|
|
1807 end Set_Left;
|
|
|
1808
|
|
|
1809 ----------------
|
|
|
1810 -- Set_Parent --
|
|
|
1811 ----------------
|
|
|
1812
|
|
|
1813 procedure Set_Parent (Node : in out Node_Type; Parent : Count_Type) is
|
|
|
1814 begin
|
|
|
1815 Node.Parent := Parent;
|
|
|
1816 end Set_Parent;
|
|
|
1817
|
|
|
1818 ---------------
|
|
|
1819 -- Set_Right --
|
|
|
1820 ---------------
|
|
|
1821
|
|
|
1822 procedure Set_Right (Node : in out Node_Type; Right : Count_Type) is
|
|
|
1823 begin
|
|
|
1824 Node.Right := Right;
|
|
|
1825 end Set_Right;
|
|
|
1826
|
|
|
1827 --------------------------
|
|
|
1828 -- Symmetric_Difference --
|
|
|
1829 --------------------------
|
|
|
1830
|
|
|
1831 procedure Symmetric_Difference (Target : in out Set; Source : Set) is
|
|
|
1832 begin
|
|
|
1833 Set_Ops.Set_Symmetric_Difference (Target, Source);
|
|
|
1834 end Symmetric_Difference;
|
|
|
1835
|
|
|
1836 function Symmetric_Difference (Left, Right : Set) return Set is
|
|
|
1837 begin
|
|
|
1838 if Left'Address = Right'Address then
|
|
|
1839 return Empty_Set;
|
|
|
1840 end if;
|
|
|
1841
|
|
|
1842 if Length (Right) = 0 then
|
|
|
1843 return Left.Copy;
|
|
|
1844 end if;
|
|
|
1845
|
|
|
1846 if Length (Left) = 0 then
|
|
|
1847 return Right.Copy;
|
|
|
1848 end if;
|
|
|
1849
|
|
|
1850 return S : Set (Length (Left) + Length (Right)) do
|
|
|
1851 Assign (S, Set_Ops.Set_Symmetric_Difference (Left, Right));
|
|
|
1852 end return;
|
|
|
1853 end Symmetric_Difference;
|
|
|
1854
|
|
|
1855 ------------
|
|
|
1856 -- To_Set --
|
|
|
1857 ------------
|
|
|
1858
|
|
|
1859 function To_Set (New_Item : Element_Type) return Set is
|
|
|
1860 Node : Count_Type;
|
|
|
1861 Inserted : Boolean;
|
|
|
1862 begin
|
|
|
1863 return S : Set (Capacity => 1) do
|
|
|
1864 Insert_Sans_Hint (S, New_Item, Node, Inserted);
|
|
|
1865 pragma Assert (Inserted);
|
|
|
1866 end return;
|
|
|
1867 end To_Set;
|
|
|
1868
|
|
|
1869 -----------
|
|
|
1870 -- Union --
|
|
|
1871 -----------
|
|
|
1872
|
|
|
1873 procedure Union (Target : in out Set; Source : Set) is
|
|
|
1874 begin
|
|
|
1875 Set_Ops.Set_Union (Target, Source);
|
|
|
1876 end Union;
|
|
|
1877
|
|
|
1878 function Union (Left, Right : Set) return Set is
|
|
|
1879 begin
|
|
|
1880 if Left'Address = Right'Address then
|
|
|
1881 return Left.Copy;
|
|
|
1882 end if;
|
|
|
1883
|
|
|
1884 if Length (Left) = 0 then
|
|
|
1885 return Right.Copy;
|
|
|
1886 end if;
|
|
|
1887
|
|
|
1888 if Length (Right) = 0 then
|
|
|
1889 return Left.Copy;
|
|
|
1890 end if;
|
|
|
1891
|
|
|
1892 return S : Set (Length (Left) + Length (Right)) do
|
|
|
1893 Assign (S, Source => Left);
|
|
|
1894 Union (S, Right);
|
|
|
1895 end return;
|
|
|
1896 end Union;
|
|
|
1897
|
|
|
1898 end Ada.Containers.Formal_Ordered_Sets;
|
