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 _ H A S H E D _ S E T S -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2010-2020, 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.Hash_Tables.Generic_Bounded_Operations; 29pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Operations); 30 31with Ada.Containers.Hash_Tables.Generic_Bounded_Keys; 32pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys); 33 34with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers; 35 36with System; use type System.Address; 37 38package body Ada.Containers.Formal_Hashed_Sets with 39 SPARK_Mode => Off 40is 41 ----------------------- 42 -- Local Subprograms -- 43 ----------------------- 44 45 -- All need comments ??? 46 47 procedure Difference (Left : Set; Right : Set; Target : in out Set); 48 49 function Equivalent_Keys 50 (Key : Element_Type; 51 Node : Node_Type) return Boolean; 52 pragma Inline (Equivalent_Keys); 53 54 procedure Free 55 (HT : in out Set; 56 X : Count_Type); 57 58 generic 59 with procedure Set_Element (Node : in out Node_Type); 60 procedure Generic_Allocate 61 (HT : in out Set; 62 Node : out Count_Type); 63 64 function Hash_Node (Node : Node_Type) return Hash_Type; 65 pragma Inline (Hash_Node); 66 67 procedure Insert 68 (Container : in out Set; 69 New_Item : Element_Type; 70 Node : out Count_Type; 71 Inserted : out Boolean); 72 73 procedure Intersection 74 (Left : Set; 75 Right : Set; 76 Target : in out Set); 77 78 function Is_In 79 (HT : Set; 80 Key : Node_Type) return Boolean; 81 pragma Inline (Is_In); 82 83 procedure Set_Element (Node : in out Node_Type; Item : Element_Type); 84 pragma Inline (Set_Element); 85 86 function Next (Node : Node_Type) return Count_Type; 87 pragma Inline (Next); 88 89 procedure Set_Next (Node : in out Node_Type; Next : Count_Type); 90 pragma Inline (Set_Next); 91 92 function Vet (Container : Set; Position : Cursor) return Boolean; 93 94 -------------------------- 95 -- Local Instantiations -- 96 -------------------------- 97 98 package HT_Ops is new Hash_Tables.Generic_Bounded_Operations 99 (HT_Types => HT_Types, 100 Hash_Node => Hash_Node, 101 Next => Next, 102 Set_Next => Set_Next); 103 104 package Element_Keys is new Hash_Tables.Generic_Bounded_Keys 105 (HT_Types => HT_Types, 106 Next => Next, 107 Set_Next => Set_Next, 108 Key_Type => Element_Type, 109 Hash => Hash, 110 Equivalent_Keys => Equivalent_Keys); 111 112 procedure Replace_Element is 113 new Element_Keys.Generic_Replace_Element (Hash_Node, Set_Element); 114 115 --------- 116 -- "=" -- 117 --------- 118 119 function "=" (Left, Right : Set) return Boolean is 120 begin 121 if Length (Left) /= Length (Right) then 122 return False; 123 end if; 124 125 if Length (Left) = 0 then 126 return True; 127 end if; 128 129 declare 130 Node : Count_Type; 131 ENode : Count_Type; 132 133 begin 134 Node := First (Left).Node; 135 while Node /= 0 loop 136 ENode := 137 Find 138 (Container => Right, 139 Item => Left.Nodes (Node).Element).Node; 140 141 if ENode = 0 142 or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element 143 then 144 return False; 145 end if; 146 147 Node := HT_Ops.Next (Left, Node); 148 end loop; 149 150 return True; 151 end; 152 end "="; 153 154 ------------ 155 -- Assign -- 156 ------------ 157 158 procedure Assign (Target : in out Set; Source : Set) is 159 procedure Insert_Element (Source_Node : Count_Type); 160 161 procedure Insert_Elements is 162 new HT_Ops.Generic_Iteration (Insert_Element); 163 164 -------------------- 165 -- Insert_Element -- 166 -------------------- 167 168 procedure Insert_Element (Source_Node : Count_Type) is 169 N : Node_Type renames Source.Nodes (Source_Node); 170 X : Count_Type; 171 B : Boolean; 172 173 begin 174 Insert (Target, N.Element, X, B); 175 pragma Assert (B); 176 end Insert_Element; 177 178 -- Start of processing for Assign 179 180 begin 181 if Target'Address = Source'Address then 182 return; 183 end if; 184 185 if Target.Capacity < Length (Source) then 186 raise Storage_Error with "not enough capacity"; -- SE or CE? ??? 187 end if; 188 189 HT_Ops.Clear (Target); 190 Insert_Elements (Source); 191 end Assign; 192 193 -------------- 194 -- Capacity -- 195 -------------- 196 197 function Capacity (Container : Set) return Count_Type is 198 begin 199 return Container.Nodes'Length; 200 end Capacity; 201 202 ----------- 203 -- Clear -- 204 ----------- 205 206 procedure Clear (Container : in out Set) is 207 begin 208 HT_Ops.Clear (Container); 209 end Clear; 210 211 -------------- 212 -- Contains -- 213 -------------- 214 215 function Contains (Container : Set; Item : Element_Type) return Boolean is 216 begin 217 return Find (Container, Item) /= No_Element; 218 end Contains; 219 220 ---------- 221 -- Copy -- 222 ---------- 223 224 function Copy 225 (Source : Set; 226 Capacity : Count_Type := 0) return Set 227 is 228 C : constant Count_Type := 229 Count_Type'Max (Capacity, Source.Capacity); 230 Cu : Cursor; 231 H : Hash_Type; 232 N : Count_Type; 233 Target : Set (C, Source.Modulus); 234 235 begin 236 if 0 < Capacity and then Capacity < Source.Capacity then 237 raise Capacity_Error; 238 end if; 239 240 Target.Length := Source.Length; 241 Target.Free := Source.Free; 242 243 H := 1; 244 while H <= Source.Modulus loop 245 Target.Buckets (H) := Source.Buckets (H); 246 H := H + 1; 247 end loop; 248 249 N := 1; 250 while N <= Source.Capacity loop 251 Target.Nodes (N) := Source.Nodes (N); 252 N := N + 1; 253 end loop; 254 255 while N <= C loop 256 Cu := (Node => N); 257 Free (Target, Cu.Node); 258 N := N + 1; 259 end loop; 260 261 return Target; 262 end Copy; 263 264 --------------------- 265 -- Default_Modulus -- 266 --------------------- 267 268 function Default_Modulus (Capacity : Count_Type) return Hash_Type is 269 begin 270 return To_Prime (Capacity); 271 end Default_Modulus; 272 273 ------------ 274 -- Delete -- 275 ------------ 276 277 procedure Delete (Container : in out Set; Item : Element_Type) is 278 X : Count_Type; 279 280 begin 281 Element_Keys.Delete_Key_Sans_Free (Container, Item, X); 282 283 if X = 0 then 284 raise Constraint_Error with "attempt to delete element not in set"; 285 end if; 286 287 Free (Container, X); 288 end Delete; 289 290 procedure Delete (Container : in out Set; Position : in out Cursor) is 291 begin 292 if not Has_Element (Container, Position) then 293 raise Constraint_Error with "Position cursor has no element"; 294 end if; 295 296 pragma Assert (Vet (Container, Position), "bad cursor in Delete"); 297 298 HT_Ops.Delete_Node_Sans_Free (Container, Position.Node); 299 Free (Container, Position.Node); 300 301 Position := No_Element; 302 end Delete; 303 304 ---------------- 305 -- Difference -- 306 ---------------- 307 308 procedure Difference (Target : in out Set; Source : Set) is 309 Src_Last : Count_Type; 310 Src_Length : Count_Type; 311 Src_Node : Count_Type; 312 Tgt_Node : Count_Type; 313 314 TN : Nodes_Type renames Target.Nodes; 315 SN : Nodes_Type renames Source.Nodes; 316 317 begin 318 if Target'Address = Source'Address then 319 Clear (Target); 320 return; 321 end if; 322 323 Src_Length := Source.Length; 324 325 if Src_Length = 0 then 326 return; 327 end if; 328 329 if Src_Length >= Target.Length then 330 Tgt_Node := HT_Ops.First (Target); 331 while Tgt_Node /= 0 loop 332 if Element_Keys.Find (Source, TN (Tgt_Node).Element) /= 0 then 333 declare 334 X : constant Count_Type := Tgt_Node; 335 begin 336 Tgt_Node := HT_Ops.Next (Target, Tgt_Node); 337 HT_Ops.Delete_Node_Sans_Free (Target, X); 338 Free (Target, X); 339 end; 340 341 else 342 Tgt_Node := HT_Ops.Next (Target, Tgt_Node); 343 end if; 344 end loop; 345 346 return; 347 else 348 Src_Node := HT_Ops.First (Source); 349 Src_Last := 0; 350 end if; 351 352 while Src_Node /= Src_Last loop 353 Tgt_Node := Element_Keys.Find (Target, SN (Src_Node).Element); 354 355 if Tgt_Node /= 0 then 356 HT_Ops.Delete_Node_Sans_Free (Target, Tgt_Node); 357 Free (Target, Tgt_Node); 358 end if; 359 360 Src_Node := HT_Ops.Next (Source, Src_Node); 361 end loop; 362 end Difference; 363 364 procedure Difference (Left : Set; Right : Set; Target : in out Set) is 365 procedure Process (L_Node : Count_Type); 366 367 procedure Iterate is 368 new HT_Ops.Generic_Iteration (Process); 369 370 ------------- 371 -- Process -- 372 ------------- 373 374 procedure Process (L_Node : Count_Type) is 375 B : Boolean; 376 E : Element_Type renames Left.Nodes (L_Node).Element; 377 X : Count_Type; 378 379 begin 380 if Find (Right, E).Node = 0 then 381 Insert (Target, E, X, B); 382 pragma Assert (B); 383 end if; 384 end Process; 385 386 -- Start of processing for Difference 387 388 begin 389 Iterate (Left); 390 end Difference; 391 392 function Difference (Left : Set; Right : Set) return Set is 393 C : Count_Type; 394 H : Hash_Type; 395 396 begin 397 if Left'Address = Right'Address then 398 return Empty_Set; 399 end if; 400 401 if Length (Left) = 0 then 402 return Empty_Set; 403 end if; 404 405 if Length (Right) = 0 then 406 return Left.Copy; 407 end if; 408 409 C := Length (Left); 410 H := Default_Modulus (C); 411 412 return S : Set (C, H) do 413 Difference (Left, Right, Target => S); 414 end return; 415 end Difference; 416 417 ------------- 418 -- Element -- 419 ------------- 420 421 function Element 422 (Container : Set; 423 Position : Cursor) return Element_Type 424 is 425 begin 426 if not Has_Element (Container, Position) then 427 raise Constraint_Error with "Position cursor equals No_Element"; 428 end if; 429 430 pragma Assert 431 (Vet (Container, Position), "bad cursor in function Element"); 432 433 return Container.Nodes (Position.Node).Element; 434 end Element; 435 436 --------------------- 437 -- Equivalent_Sets -- 438 --------------------- 439 440 function Equivalent_Sets (Left, Right : Set) return Boolean is 441 442 function Find_Equivalent_Key 443 (R_HT : Hash_Table_Type'Class; 444 L_Node : Node_Type) return Boolean; 445 pragma Inline (Find_Equivalent_Key); 446 447 function Is_Equivalent is 448 new HT_Ops.Generic_Equal (Find_Equivalent_Key); 449 450 ------------------------- 451 -- Find_Equivalent_Key -- 452 ------------------------- 453 454 function Find_Equivalent_Key 455 (R_HT : Hash_Table_Type'Class; 456 L_Node : Node_Type) return Boolean 457 is 458 R_Index : constant Hash_Type := 459 Element_Keys.Index (R_HT, L_Node.Element); 460 R_Node : Count_Type := R_HT.Buckets (R_Index); 461 RN : Nodes_Type renames R_HT.Nodes; 462 463 begin 464 loop 465 if R_Node = 0 then 466 return False; 467 end if; 468 469 if Equivalent_Elements 470 (L_Node.Element, RN (R_Node).Element) 471 then 472 return True; 473 end if; 474 475 R_Node := HT_Ops.Next (R_HT, R_Node); 476 end loop; 477 end Find_Equivalent_Key; 478 479 -- Start of processing for Equivalent_Sets 480 481 begin 482 return Is_Equivalent (Left, Right); 483 end Equivalent_Sets; 484 485 --------------------- 486 -- Equivalent_Keys -- 487 --------------------- 488 489 function Equivalent_Keys 490 (Key : Element_Type; 491 Node : Node_Type) return Boolean 492 is 493 begin 494 return Equivalent_Elements (Key, Node.Element); 495 end Equivalent_Keys; 496 497 ------------- 498 -- Exclude -- 499 ------------- 500 501 procedure Exclude (Container : in out Set; Item : Element_Type) is 502 X : Count_Type; 503 begin 504 Element_Keys.Delete_Key_Sans_Free (Container, Item, X); 505 Free (Container, X); 506 end Exclude; 507 508 ---------- 509 -- Find -- 510 ---------- 511 512 function Find 513 (Container : Set; 514 Item : Element_Type) return Cursor 515 is 516 Node : constant Count_Type := Element_Keys.Find (Container, Item); 517 518 begin 519 if Node = 0 then 520 return No_Element; 521 end if; 522 523 return (Node => Node); 524 end Find; 525 526 ----------- 527 -- First -- 528 ----------- 529 530 function First (Container : Set) return Cursor is 531 Node : constant Count_Type := HT_Ops.First (Container); 532 533 begin 534 if Node = 0 then 535 return No_Element; 536 end if; 537 538 return (Node => Node); 539 end First; 540 541 ------------------ 542 -- Formal_Model -- 543 ------------------ 544 545 package body Formal_Model is 546 547 ------------------------- 548 -- E_Elements_Included -- 549 ------------------------- 550 551 function E_Elements_Included 552 (Left : E.Sequence; 553 Right : E.Sequence) return Boolean 554 is 555 begin 556 for I in 1 .. E.Length (Left) loop 557 if not E.Contains (Right, 1, E.Length (Right), E.Get (Left, I)) 558 then 559 return False; 560 end if; 561 end loop; 562 563 return True; 564 end E_Elements_Included; 565 566 function E_Elements_Included 567 (Left : E.Sequence; 568 Model : M.Set; 569 Right : E.Sequence) return Boolean 570 is 571 begin 572 for I in 1 .. E.Length (Left) loop 573 declare 574 Item : constant Element_Type := E.Get (Left, I); 575 begin 576 if M.Contains (Model, Item) then 577 if not E.Contains (Right, 1, E.Length (Right), Item) then 578 return False; 579 end if; 580 end if; 581 end; 582 end loop; 583 584 return True; 585 end E_Elements_Included; 586 587 function E_Elements_Included 588 (Container : E.Sequence; 589 Model : M.Set; 590 Left : E.Sequence; 591 Right : E.Sequence) return Boolean 592 is 593 begin 594 for I in 1 .. E.Length (Container) loop 595 declare 596 Item : constant Element_Type := E.Get (Container, I); 597 begin 598 if M.Contains (Model, Item) then 599 if not E.Contains (Left, 1, E.Length (Left), Item) then 600 return False; 601 end if; 602 else 603 if not E.Contains (Right, 1, E.Length (Right), Item) then 604 return False; 605 end if; 606 end if; 607 end; 608 end loop; 609 610 return True; 611 end E_Elements_Included; 612 613 ---------- 614 -- Find -- 615 ---------- 616 617 function Find 618 (Container : E.Sequence; 619 Item : Element_Type) return Count_Type 620 is 621 begin 622 for I in 1 .. E.Length (Container) loop 623 if Equivalent_Elements (Item, E.Get (Container, I)) then 624 return I; 625 end if; 626 end loop; 627 return 0; 628 end Find; 629 630 -------------- 631 -- Elements -- 632 -------------- 633 634 function Elements (Container : Set) return E.Sequence is 635 Position : Count_Type := HT_Ops.First (Container); 636 R : E.Sequence; 637 638 begin 639 -- Can't use First, Next or Element here, since they depend on models 640 -- for their postconditions. 641 642 while Position /= 0 loop 643 R := E.Add (R, Container.Nodes (Position).Element); 644 Position := HT_Ops.Next (Container, Position); 645 end loop; 646 647 return R; 648 end Elements; 649 650 ---------------------------- 651 -- Lift_Abstraction_Level -- 652 ---------------------------- 653 654 procedure Lift_Abstraction_Level (Container : Set) is null; 655 656 ----------------------- 657 -- Mapping_Preserved -- 658 ----------------------- 659 660 function Mapping_Preserved 661 (E_Left : E.Sequence; 662 E_Right : E.Sequence; 663 P_Left : P.Map; 664 P_Right : P.Map) return Boolean 665 is 666 begin 667 for C of P_Left loop 668 if not P.Has_Key (P_Right, C) 669 or else P.Get (P_Left, C) > E.Length (E_Left) 670 or else P.Get (P_Right, C) > E.Length (E_Right) 671 or else E.Get (E_Left, P.Get (P_Left, C)) /= 672 E.Get (E_Right, P.Get (P_Right, C)) 673 then 674 return False; 675 end if; 676 end loop; 677 678 return True; 679 end Mapping_Preserved; 680 681 ------------------------------ 682 -- Mapping_Preserved_Except -- 683 ------------------------------ 684 685 function Mapping_Preserved_Except 686 (E_Left : E.Sequence; 687 E_Right : E.Sequence; 688 P_Left : P.Map; 689 P_Right : P.Map; 690 Position : Cursor) return Boolean 691 is 692 begin 693 for C of P_Left loop 694 if C /= Position 695 and (not P.Has_Key (P_Right, C) 696 or else P.Get (P_Left, C) > E.Length (E_Left) 697 or else P.Get (P_Right, C) > E.Length (E_Right) 698 or else E.Get (E_Left, P.Get (P_Left, C)) /= 699 E.Get (E_Right, P.Get (P_Right, C))) 700 then 701 return False; 702 end if; 703 end loop; 704 705 return True; 706 end Mapping_Preserved_Except; 707 708 ----------- 709 -- Model -- 710 ----------- 711 712 function Model (Container : Set) return M.Set is 713 Position : Count_Type := HT_Ops.First (Container); 714 R : M.Set; 715 716 begin 717 -- Can't use First, Next or Element here, since they depend on models 718 -- for their postconditions. 719 720 while Position /= 0 loop 721 R := 722 M.Add 723 (Container => R, 724 Item => Container.Nodes (Position).Element); 725 726 Position := HT_Ops.Next (Container, Position); 727 end loop; 728 729 return R; 730 end Model; 731 732 --------------- 733 -- Positions -- 734 --------------- 735 736 function Positions (Container : Set) return P.Map is 737 I : Count_Type := 1; 738 Position : Count_Type := HT_Ops.First (Container); 739 R : P.Map; 740 741 begin 742 -- Can't use First, Next or Element here, since they depend on models 743 -- for their postconditions. 744 745 while Position /= 0 loop 746 R := P.Add (R, (Node => Position), I); 747 pragma Assert (P.Length (R) = I); 748 Position := HT_Ops.Next (Container, Position); 749 I := I + 1; 750 end loop; 751 752 return R; 753 end Positions; 754 755 end Formal_Model; 756 757 ---------- 758 -- Free -- 759 ---------- 760 761 procedure Free (HT : in out Set; X : Count_Type) is 762 begin 763 if X /= 0 then 764 pragma Assert (X <= HT.Capacity); 765 HT.Nodes (X).Has_Element := False; 766 HT_Ops.Free (HT, X); 767 end if; 768 end Free; 769 770 ---------------------- 771 -- Generic_Allocate -- 772 ---------------------- 773 774 procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is 775 procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element); 776 begin 777 Allocate (HT, Node); 778 HT.Nodes (Node).Has_Element := True; 779 end Generic_Allocate; 780 781 package body Generic_Keys with SPARK_Mode => Off is 782 783 ----------------------- 784 -- Local Subprograms -- 785 ----------------------- 786 787 function Equivalent_Key_Node 788 (Key : Key_Type; 789 Node : Node_Type) return Boolean; 790 pragma Inline (Equivalent_Key_Node); 791 792 -------------------------- 793 -- Local Instantiations -- 794 -------------------------- 795 796 package Key_Keys is new Hash_Tables.Generic_Bounded_Keys 797 (HT_Types => HT_Types, 798 Next => Next, 799 Set_Next => Set_Next, 800 Key_Type => Key_Type, 801 Hash => Hash, 802 Equivalent_Keys => Equivalent_Key_Node); 803 804 -------------- 805 -- Contains -- 806 -------------- 807 808 function Contains 809 (Container : Set; 810 Key : Key_Type) return Boolean 811 is 812 begin 813 return Find (Container, Key) /= No_Element; 814 end Contains; 815 816 ------------ 817 -- Delete -- 818 ------------ 819 820 procedure Delete (Container : in out Set; Key : Key_Type) is 821 X : Count_Type; 822 823 begin 824 Key_Keys.Delete_Key_Sans_Free (Container, Key, X); 825 826 if X = 0 then 827 raise Constraint_Error with "attempt to delete key not in set"; 828 end if; 829 830 Free (Container, X); 831 end Delete; 832 833 ------------- 834 -- Element -- 835 ------------- 836 837 function Element 838 (Container : Set; 839 Key : Key_Type) return Element_Type 840 is 841 Node : constant Count_Type := Find (Container, Key).Node; 842 843 begin 844 if Node = 0 then 845 raise Constraint_Error with "key not in map"; 846 end if; 847 848 return Container.Nodes (Node).Element; 849 end Element; 850 851 ------------------------- 852 -- Equivalent_Key_Node -- 853 ------------------------- 854 855 function Equivalent_Key_Node 856 (Key : Key_Type; 857 Node : Node_Type) return Boolean 858 is 859 begin 860 return Equivalent_Keys (Key, Generic_Keys.Key (Node.Element)); 861 end Equivalent_Key_Node; 862 863 ------------- 864 -- Exclude -- 865 ------------- 866 867 procedure Exclude (Container : in out Set; Key : Key_Type) is 868 X : Count_Type; 869 begin 870 Key_Keys.Delete_Key_Sans_Free (Container, Key, X); 871 Free (Container, X); 872 end Exclude; 873 874 ---------- 875 -- Find -- 876 ---------- 877 878 function Find 879 (Container : Set; 880 Key : Key_Type) return Cursor 881 is 882 Node : constant Count_Type := Key_Keys.Find (Container, Key); 883 begin 884 return (if Node = 0 then No_Element else (Node => Node)); 885 end Find; 886 887 ------------------ 888 -- Formal_Model -- 889 ------------------ 890 891 package body Formal_Model is 892 893 ----------------------- 894 -- M_Included_Except -- 895 ----------------------- 896 897 function M_Included_Except 898 (Left : M.Set; 899 Right : M.Set; 900 Key : Key_Type) return Boolean 901 is 902 begin 903 for E of Left loop 904 if not Contains (Right, E) 905 and not Equivalent_Keys (Generic_Keys.Key (E), Key) 906 then 907 return False; 908 end if; 909 end loop; 910 911 return True; 912 end M_Included_Except; 913 914 end Formal_Model; 915 916 --------- 917 -- Key -- 918 --------- 919 920 function Key (Container : Set; Position : Cursor) return Key_Type is 921 begin 922 if not Has_Element (Container, Position) then 923 raise Constraint_Error with "Position cursor has no element"; 924 end if; 925 926 pragma Assert 927 (Vet (Container, Position), "bad cursor in function Key"); 928 929 declare 930 N : Node_Type renames Container.Nodes (Position.Node); 931 begin 932 return Key (N.Element); 933 end; 934 end Key; 935 936 ------------- 937 -- Replace -- 938 ------------- 939 940 procedure Replace 941 (Container : in out Set; 942 Key : Key_Type; 943 New_Item : Element_Type) 944 is 945 Node : constant Count_Type := Key_Keys.Find (Container, Key); 946 947 begin 948 if Node = 0 then 949 raise Constraint_Error with "attempt to replace key not in set"; 950 end if; 951 952 Replace_Element (Container, Node, New_Item); 953 end Replace; 954 955 end Generic_Keys; 956 957 ----------------- 958 -- Has_Element -- 959 ----------------- 960 961 function Has_Element (Container : Set; Position : Cursor) return Boolean is 962 begin 963 if Position.Node = 0 964 or else not Container.Nodes (Position.Node).Has_Element 965 then 966 return False; 967 end if; 968 969 return True; 970 end Has_Element; 971 972 --------------- 973 -- Hash_Node -- 974 --------------- 975 976 function Hash_Node (Node : Node_Type) return Hash_Type is 977 begin 978 return Hash (Node.Element); 979 end Hash_Node; 980 981 ------------- 982 -- Include -- 983 ------------- 984 985 procedure Include (Container : in out Set; New_Item : Element_Type) is 986 Inserted : Boolean; 987 Position : Cursor; 988 989 begin 990 Insert (Container, New_Item, Position, Inserted); 991 992 if not Inserted then 993 Container.Nodes (Position.Node).Element := New_Item; 994 end if; 995 end Include; 996 997 ------------ 998 -- Insert -- 999 ------------ 1000 1001 procedure Insert 1002 (Container : in out Set; 1003 New_Item : Element_Type; 1004 Position : out Cursor; 1005 Inserted : out Boolean) 1006 is 1007 begin 1008 Insert (Container, New_Item, Position.Node, Inserted); 1009 end Insert; 1010 1011 procedure Insert (Container : in out Set; New_Item : Element_Type) is 1012 Inserted : Boolean; 1013 Position : Cursor; 1014 1015 begin 1016 Insert (Container, New_Item, Position, Inserted); 1017 1018 if not Inserted then 1019 raise Constraint_Error with 1020 "attempt to insert element already in set"; 1021 end if; 1022 end Insert; 1023 1024 procedure Insert 1025 (Container : in out Set; 1026 New_Item : Element_Type; 1027 Node : out Count_Type; 1028 Inserted : out Boolean) 1029 is 1030 procedure Allocate_Set_Element (Node : in out Node_Type); 1031 pragma Inline (Allocate_Set_Element); 1032 1033 function New_Node return Count_Type; 1034 pragma Inline (New_Node); 1035 1036 procedure Local_Insert is 1037 new Element_Keys.Generic_Conditional_Insert (New_Node); 1038 1039 procedure Allocate is 1040 new Generic_Allocate (Allocate_Set_Element); 1041 1042 --------------------------- 1043 -- Allocate_Set_Element -- 1044 --------------------------- 1045 1046 procedure Allocate_Set_Element (Node : in out Node_Type) is 1047 begin 1048 Node.Element := New_Item; 1049 end Allocate_Set_Element; 1050 1051 -------------- 1052 -- New_Node -- 1053 -------------- 1054 1055 function New_Node return Count_Type is 1056 Result : Count_Type; 1057 begin 1058 Allocate (Container, Result); 1059 return Result; 1060 end New_Node; 1061 1062 -- Start of processing for Insert 1063 1064 begin 1065 Local_Insert (Container, New_Item, Node, Inserted); 1066 end Insert; 1067 1068 ------------------ 1069 -- Intersection -- 1070 ------------------ 1071 1072 procedure Intersection (Target : in out Set; Source : Set) is 1073 Tgt_Node : Count_Type; 1074 TN : Nodes_Type renames Target.Nodes; 1075 1076 begin 1077 if Target'Address = Source'Address then 1078 return; 1079 end if; 1080 1081 if Source.Length = 0 then 1082 Clear (Target); 1083 return; 1084 end if; 1085 1086 Tgt_Node := HT_Ops.First (Target); 1087 while Tgt_Node /= 0 loop 1088 if Find (Source, TN (Tgt_Node).Element).Node /= 0 then 1089 Tgt_Node := HT_Ops.Next (Target, Tgt_Node); 1090 1091 else 1092 declare 1093 X : constant Count_Type := Tgt_Node; 1094 begin 1095 Tgt_Node := HT_Ops.Next (Target, Tgt_Node); 1096 HT_Ops.Delete_Node_Sans_Free (Target, X); 1097 Free (Target, X); 1098 end; 1099 end if; 1100 end loop; 1101 end Intersection; 1102 1103 procedure Intersection (Left : Set; Right : Set; Target : in out Set) is 1104 procedure Process (L_Node : Count_Type); 1105 1106 procedure Iterate is 1107 new HT_Ops.Generic_Iteration (Process); 1108 1109 ------------- 1110 -- Process -- 1111 ------------- 1112 1113 procedure Process (L_Node : Count_Type) is 1114 E : Element_Type renames Left.Nodes (L_Node).Element; 1115 X : Count_Type; 1116 B : Boolean; 1117 1118 begin 1119 if Find (Right, E).Node /= 0 then 1120 Insert (Target, E, X, B); 1121 pragma Assert (B); 1122 end if; 1123 end Process; 1124 1125 -- Start of processing for Intersection 1126 1127 begin 1128 Iterate (Left); 1129 end Intersection; 1130 1131 function Intersection (Left : Set; Right : Set) return Set is 1132 C : Count_Type; 1133 H : Hash_Type; 1134 1135 begin 1136 if Left'Address = Right'Address then 1137 return Left.Copy; 1138 end if; 1139 1140 C := Count_Type'Min (Length (Left), Length (Right)); -- ??? 1141 H := Default_Modulus (C); 1142 1143 return S : Set (C, H) do 1144 if Length (Left) /= 0 and Length (Right) /= 0 then 1145 Intersection (Left, Right, Target => S); 1146 end if; 1147 end return; 1148 end Intersection; 1149 1150 -------------- 1151 -- Is_Empty -- 1152 -------------- 1153 1154 function Is_Empty (Container : Set) return Boolean is 1155 begin 1156 return Length (Container) = 0; 1157 end Is_Empty; 1158 1159 ----------- 1160 -- Is_In -- 1161 ----------- 1162 1163 function Is_In (HT : Set; Key : Node_Type) return Boolean is 1164 begin 1165 return Element_Keys.Find (HT, Key.Element) /= 0; 1166 end Is_In; 1167 1168 --------------- 1169 -- Is_Subset -- 1170 --------------- 1171 1172 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is 1173 Subset_Node : Count_Type; 1174 Subset_Nodes : Nodes_Type renames Subset.Nodes; 1175 1176 begin 1177 if Subset'Address = Of_Set'Address then 1178 return True; 1179 end if; 1180 1181 if Length (Subset) > Length (Of_Set) then 1182 return False; 1183 end if; 1184 1185 Subset_Node := First (Subset).Node; 1186 while Subset_Node /= 0 loop 1187 declare 1188 N : Node_Type renames Subset_Nodes (Subset_Node); 1189 E : Element_Type renames N.Element; 1190 1191 begin 1192 if Find (Of_Set, E).Node = 0 then 1193 return False; 1194 end if; 1195 end; 1196 1197 Subset_Node := HT_Ops.Next (Subset, Subset_Node); 1198 end loop; 1199 1200 return True; 1201 end Is_Subset; 1202 1203 ------------ 1204 -- Length -- 1205 ------------ 1206 1207 function Length (Container : Set) return Count_Type is 1208 begin 1209 return Container.Length; 1210 end Length; 1211 1212 ---------- 1213 -- Move -- 1214 ---------- 1215 1216 -- Comments??? 1217 1218 procedure Move (Target : in out Set; Source : in out Set) is 1219 NN : HT_Types.Nodes_Type renames Source.Nodes; 1220 X, Y : Count_Type; 1221 1222 begin 1223 if Target'Address = Source'Address then 1224 return; 1225 end if; 1226 1227 if Target.Capacity < Length (Source) then 1228 raise Constraint_Error with -- ??? 1229 "Source length exceeds Target capacity"; 1230 end if; 1231 1232 Clear (Target); 1233 1234 if Source.Length = 0 then 1235 return; 1236 end if; 1237 1238 X := HT_Ops.First (Source); 1239 while X /= 0 loop 1240 Insert (Target, NN (X).Element); -- optimize??? 1241 1242 Y := HT_Ops.Next (Source, X); 1243 1244 HT_Ops.Delete_Node_Sans_Free (Source, X); 1245 Free (Source, X); 1246 1247 X := Y; 1248 end loop; 1249 end Move; 1250 1251 ---------- 1252 -- Next -- 1253 ---------- 1254 1255 function Next (Node : Node_Type) return Count_Type is 1256 begin 1257 return Node.Next; 1258 end Next; 1259 1260 function Next (Container : Set; Position : Cursor) return Cursor is 1261 begin 1262 if Position.Node = 0 then 1263 return No_Element; 1264 end if; 1265 1266 if not Has_Element (Container, Position) then 1267 raise Constraint_Error with "Position has no element"; 1268 end if; 1269 1270 pragma Assert (Vet (Container, Position), "bad cursor in Next"); 1271 1272 return (Node => HT_Ops.Next (Container, Position.Node)); 1273 end Next; 1274 1275 procedure Next (Container : Set; Position : in out Cursor) is 1276 begin 1277 Position := Next (Container, Position); 1278 end Next; 1279 1280 ------------- 1281 -- Overlap -- 1282 ------------- 1283 1284 function Overlap (Left, Right : Set) return Boolean is 1285 Left_Node : Count_Type; 1286 Left_Nodes : Nodes_Type renames Left.Nodes; 1287 1288 begin 1289 if Length (Right) = 0 or Length (Left) = 0 then 1290 return False; 1291 end if; 1292 1293 if Left'Address = Right'Address then 1294 return True; 1295 end if; 1296 1297 Left_Node := First (Left).Node; 1298 while Left_Node /= 0 loop 1299 declare 1300 N : Node_Type renames Left_Nodes (Left_Node); 1301 E : Element_Type renames N.Element; 1302 begin 1303 if Find (Right, E).Node /= 0 then 1304 return True; 1305 end if; 1306 end; 1307 1308 Left_Node := HT_Ops.Next (Left, Left_Node); 1309 end loop; 1310 1311 return False; 1312 end Overlap; 1313 1314 ------------- 1315 -- Replace -- 1316 ------------- 1317 1318 procedure Replace (Container : in out Set; New_Item : Element_Type) is 1319 Node : constant Count_Type := Element_Keys.Find (Container, New_Item); 1320 1321 begin 1322 if Node = 0 then 1323 raise Constraint_Error with "attempt to replace element not in set"; 1324 end if; 1325 1326 Container.Nodes (Node).Element := New_Item; 1327 end Replace; 1328 1329 --------------------- 1330 -- Replace_Element -- 1331 --------------------- 1332 1333 procedure Replace_Element 1334 (Container : in out Set; 1335 Position : Cursor; 1336 New_Item : Element_Type) 1337 is 1338 begin 1339 if not Has_Element (Container, Position) then 1340 raise Constraint_Error with "Position cursor equals No_Element"; 1341 end if; 1342 1343 pragma Assert 1344 (Vet (Container, Position), "bad cursor in Replace_Element"); 1345 1346 Replace_Element (Container, Position.Node, New_Item); 1347 end Replace_Element; 1348 1349 ---------------------- 1350 -- Reserve_Capacity -- 1351 ---------------------- 1352 1353 procedure Reserve_Capacity 1354 (Container : in out Set; 1355 Capacity : Count_Type) 1356 is 1357 begin 1358 if Capacity > Container.Capacity then 1359 raise Constraint_Error with "requested capacity is too large"; 1360 end if; 1361 end Reserve_Capacity; 1362 1363 ------------------ 1364 -- Set_Element -- 1365 ------------------ 1366 1367 procedure Set_Element (Node : in out Node_Type; Item : Element_Type) is 1368 begin 1369 Node.Element := Item; 1370 end Set_Element; 1371 1372 -------------- 1373 -- Set_Next -- 1374 -------------- 1375 1376 procedure Set_Next (Node : in out Node_Type; Next : Count_Type) is 1377 begin 1378 Node.Next := Next; 1379 end Set_Next; 1380 1381 -------------------------- 1382 -- Symmetric_Difference -- 1383 -------------------------- 1384 1385 procedure Symmetric_Difference (Target : in out Set; Source : Set) is 1386 procedure Process (Source_Node : Count_Type); 1387 pragma Inline (Process); 1388 1389 procedure Iterate is new HT_Ops.Generic_Iteration (Process); 1390 1391 ------------- 1392 -- Process -- 1393 ------------- 1394 1395 procedure Process (Source_Node : Count_Type) is 1396 B : Boolean; 1397 N : Node_Type renames Source.Nodes (Source_Node); 1398 X : Count_Type; 1399 1400 begin 1401 if Is_In (Target, N) then 1402 Delete (Target, N.Element); 1403 else 1404 Insert (Target, N.Element, X, B); 1405 pragma Assert (B); 1406 end if; 1407 end Process; 1408 1409 -- Start of processing for Symmetric_Difference 1410 1411 begin 1412 if Target'Address = Source'Address then 1413 Clear (Target); 1414 return; 1415 end if; 1416 1417 if Length (Target) = 0 then 1418 Assign (Target, Source); 1419 return; 1420 end if; 1421 1422 Iterate (Source); 1423 end Symmetric_Difference; 1424 1425 function Symmetric_Difference (Left : Set; Right : Set) return Set is 1426 C : Count_Type; 1427 H : Hash_Type; 1428 1429 begin 1430 if Left'Address = Right'Address then 1431 return Empty_Set; 1432 end if; 1433 1434 if Length (Right) = 0 then 1435 return Left.Copy; 1436 end if; 1437 1438 if Length (Left) = 0 then 1439 return Right.Copy; 1440 end if; 1441 1442 C := Length (Left) + Length (Right); 1443 H := Default_Modulus (C); 1444 1445 return S : Set (C, H) do 1446 Difference (Left, Right, S); 1447 Difference (Right, Left, S); 1448 end return; 1449 end Symmetric_Difference; 1450 1451 ------------ 1452 -- To_Set -- 1453 ------------ 1454 1455 function To_Set (New_Item : Element_Type) return Set is 1456 X : Count_Type; 1457 B : Boolean; 1458 1459 begin 1460 return S : Set (Capacity => 1, Modulus => 1) do 1461 Insert (S, New_Item, X, B); 1462 pragma Assert (B); 1463 end return; 1464 end To_Set; 1465 1466 ----------- 1467 -- Union -- 1468 ----------- 1469 1470 procedure Union (Target : in out Set; Source : Set) is 1471 procedure Process (Src_Node : Count_Type); 1472 1473 procedure Iterate is 1474 new HT_Ops.Generic_Iteration (Process); 1475 1476 ------------- 1477 -- Process -- 1478 ------------- 1479 1480 procedure Process (Src_Node : Count_Type) is 1481 N : Node_Type renames Source.Nodes (Src_Node); 1482 E : Element_Type renames N.Element; 1483 1484 X : Count_Type; 1485 B : Boolean; 1486 1487 begin 1488 Insert (Target, E, X, B); 1489 end Process; 1490 1491 -- Start of processing for Union 1492 1493 begin 1494 if Target'Address = Source'Address then 1495 return; 1496 end if; 1497 1498 Iterate (Source); 1499 end Union; 1500 1501 function Union (Left : Set; Right : Set) return Set is 1502 C : Count_Type; 1503 H : Hash_Type; 1504 1505 begin 1506 if Left'Address = Right'Address then 1507 return Left.Copy; 1508 end if; 1509 1510 if Length (Right) = 0 then 1511 return Left.Copy; 1512 end if; 1513 1514 if Length (Left) = 0 then 1515 return Right.Copy; 1516 end if; 1517 1518 C := Length (Left) + Length (Right); 1519 H := Default_Modulus (C); 1520 return S : Set (C, H) do 1521 Assign (Target => S, Source => Left); 1522 Union (Target => S, Source => Right); 1523 end return; 1524 end Union; 1525 1526 --------- 1527 -- Vet -- 1528 --------- 1529 1530 function Vet (Container : Set; Position : Cursor) return Boolean is 1531 begin 1532 if Position.Node = 0 then 1533 return True; 1534 end if; 1535 1536 declare 1537 S : Set renames Container; 1538 N : Nodes_Type renames S.Nodes; 1539 X : Count_Type; 1540 1541 begin 1542 if S.Length = 0 then 1543 return False; 1544 end if; 1545 1546 if Position.Node > N'Last then 1547 return False; 1548 end if; 1549 1550 if N (Position.Node).Next = Position.Node then 1551 return False; 1552 end if; 1553 1554 X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element)); 1555 1556 for J in 1 .. S.Length loop 1557 if X = Position.Node then 1558 return True; 1559 end if; 1560 1561 if X = 0 then 1562 return False; 1563 end if; 1564 1565 if X = N (X).Next then -- to prevent unnecessary looping 1566 return False; 1567 end if; 1568 1569 X := N (X).Next; 1570 end loop; 1571 1572 return False; 1573 end; 1574 end Vet; 1575 1576end Ada.Containers.Formal_Hashed_Sets; 1577