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