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-2018, 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 28with Ada.Containers.Red_Black_Trees.Generic_Bounded_Operations; 29pragma Elaborate_All 30 (Ada.Containers.Red_Black_Trees.Generic_Bounded_Operations); 31 32with Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys; 33pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys); 34 35with Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations; 36pragma Elaborate_All 37 (Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations); 38 39with System; use type System.Address; 40 41package body Ada.Containers.Formal_Ordered_Sets with 42 SPARK_Mode => Off 43is 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 1898end Ada.Containers.Formal_Ordered_Sets; 1899