Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-cforse.adb @ 111:04ced10e8804

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcc 7
author kono
date Fri, 27 Oct 2017 22:46:09 +0900
parents
children 84e7813d76e9
comparison
equal deleted inserted replaced
68:561a7518be6b 111:04ced10e8804
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;