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-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.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 HT.Nodes (X).Has_Element := False; 764 HT_Ops.Free (HT, X); 765 end Free; 766 767 ---------------------- 768 -- Generic_Allocate -- 769 ---------------------- 770 771 procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is 772 procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element); 773 begin 774 Allocate (HT, Node); 775 HT.Nodes (Node).Has_Element := True; 776 end Generic_Allocate; 777 778 package body Generic_Keys with SPARK_Mode => Off is 779 780 ----------------------- 781 -- Local Subprograms -- 782 ----------------------- 783 784 function Equivalent_Key_Node 785 (Key : Key_Type; 786 Node : Node_Type) return Boolean; 787 pragma Inline (Equivalent_Key_Node); 788 789 -------------------------- 790 -- Local Instantiations -- 791 -------------------------- 792 793 package Key_Keys is new Hash_Tables.Generic_Bounded_Keys 794 (HT_Types => HT_Types, 795 Next => Next, 796 Set_Next => Set_Next, 797 Key_Type => Key_Type, 798 Hash => Hash, 799 Equivalent_Keys => Equivalent_Key_Node); 800 801 -------------- 802 -- Contains -- 803 -------------- 804 805 function Contains 806 (Container : Set; 807 Key : Key_Type) return Boolean 808 is 809 begin 810 return Find (Container, Key) /= No_Element; 811 end Contains; 812 813 ------------ 814 -- Delete -- 815 ------------ 816 817 procedure Delete (Container : in out Set; Key : Key_Type) is 818 X : Count_Type; 819 820 begin 821 Key_Keys.Delete_Key_Sans_Free (Container, Key, X); 822 823 if X = 0 then 824 raise Constraint_Error with "attempt to delete key not in set"; 825 end if; 826 827 Free (Container, X); 828 end Delete; 829 830 ------------- 831 -- Element -- 832 ------------- 833 834 function Element 835 (Container : Set; 836 Key : Key_Type) return Element_Type 837 is 838 Node : constant Count_Type := Find (Container, Key).Node; 839 840 begin 841 if Node = 0 then 842 raise Constraint_Error with "key not in map"; 843 end if; 844 845 return Container.Nodes (Node).Element; 846 end Element; 847 848 ------------------------- 849 -- Equivalent_Key_Node -- 850 ------------------------- 851 852 function Equivalent_Key_Node 853 (Key : Key_Type; 854 Node : Node_Type) return Boolean 855 is 856 begin 857 return Equivalent_Keys (Key, Generic_Keys.Key (Node.Element)); 858 end Equivalent_Key_Node; 859 860 ------------- 861 -- Exclude -- 862 ------------- 863 864 procedure Exclude (Container : in out Set; Key : Key_Type) is 865 X : Count_Type; 866 begin 867 Key_Keys.Delete_Key_Sans_Free (Container, Key, X); 868 Free (Container, X); 869 end Exclude; 870 871 ---------- 872 -- Find -- 873 ---------- 874 875 function Find 876 (Container : Set; 877 Key : Key_Type) return Cursor 878 is 879 Node : constant Count_Type := Key_Keys.Find (Container, Key); 880 begin 881 return (if Node = 0 then No_Element else (Node => Node)); 882 end Find; 883 884 ------------------ 885 -- Formal_Model -- 886 ------------------ 887 888 package body Formal_Model is 889 890 ----------------------- 891 -- M_Included_Except -- 892 ----------------------- 893 894 function M_Included_Except 895 (Left : M.Set; 896 Right : M.Set; 897 Key : Key_Type) return Boolean 898 is 899 begin 900 for E of Left loop 901 if not Contains (Right, E) 902 and not Equivalent_Keys (Generic_Keys.Key (E), Key) 903 then 904 return False; 905 end if; 906 end loop; 907 908 return True; 909 end M_Included_Except; 910 911 end Formal_Model; 912 913 --------- 914 -- Key -- 915 --------- 916 917 function Key (Container : Set; Position : Cursor) return Key_Type is 918 begin 919 if not Has_Element (Container, Position) then 920 raise Constraint_Error with "Position cursor has no element"; 921 end if; 922 923 pragma Assert 924 (Vet (Container, Position), "bad cursor in function Key"); 925 926 declare 927 N : Node_Type renames Container.Nodes (Position.Node); 928 begin 929 return Key (N.Element); 930 end; 931 end Key; 932 933 ------------- 934 -- Replace -- 935 ------------- 936 937 procedure Replace 938 (Container : in out Set; 939 Key : Key_Type; 940 New_Item : Element_Type) 941 is 942 Node : constant Count_Type := Key_Keys.Find (Container, Key); 943 944 begin 945 if Node = 0 then 946 raise Constraint_Error with "attempt to replace key not in set"; 947 end if; 948 949 Replace_Element (Container, Node, New_Item); 950 end Replace; 951 952 end Generic_Keys; 953 954 ----------------- 955 -- Has_Element -- 956 ----------------- 957 958 function Has_Element (Container : Set; Position : Cursor) return Boolean is 959 begin 960 if Position.Node = 0 961 or else not Container.Nodes (Position.Node).Has_Element 962 then 963 return False; 964 end if; 965 966 return True; 967 end Has_Element; 968 969 --------------- 970 -- Hash_Node -- 971 --------------- 972 973 function Hash_Node (Node : Node_Type) return Hash_Type is 974 begin 975 return Hash (Node.Element); 976 end Hash_Node; 977 978 ------------- 979 -- Include -- 980 ------------- 981 982 procedure Include (Container : in out Set; New_Item : Element_Type) is 983 Inserted : Boolean; 984 Position : Cursor; 985 986 begin 987 Insert (Container, New_Item, Position, Inserted); 988 989 if not Inserted then 990 Container.Nodes (Position.Node).Element := New_Item; 991 end if; 992 end Include; 993 994 ------------ 995 -- Insert -- 996 ------------ 997 998 procedure Insert 999 (Container : in out Set; 1000 New_Item : Element_Type; 1001 Position : out Cursor; 1002 Inserted : out Boolean) 1003 is 1004 begin 1005 Insert (Container, New_Item, Position.Node, Inserted); 1006 end Insert; 1007 1008 procedure Insert (Container : in out Set; New_Item : Element_Type) is 1009 Inserted : Boolean; 1010 Position : Cursor; 1011 1012 begin 1013 Insert (Container, New_Item, Position, Inserted); 1014 1015 if not Inserted then 1016 raise Constraint_Error with 1017 "attempt to insert element already in set"; 1018 end if; 1019 end Insert; 1020 1021 procedure Insert 1022 (Container : in out Set; 1023 New_Item : Element_Type; 1024 Node : out Count_Type; 1025 Inserted : out Boolean) 1026 is 1027 procedure Allocate_Set_Element (Node : in out Node_Type); 1028 pragma Inline (Allocate_Set_Element); 1029 1030 function New_Node return Count_Type; 1031 pragma Inline (New_Node); 1032 1033 procedure Local_Insert is 1034 new Element_Keys.Generic_Conditional_Insert (New_Node); 1035 1036 procedure Allocate is 1037 new Generic_Allocate (Allocate_Set_Element); 1038 1039 --------------------------- 1040 -- Allocate_Set_Element -- 1041 --------------------------- 1042 1043 procedure Allocate_Set_Element (Node : in out Node_Type) is 1044 begin 1045 Node.Element := New_Item; 1046 end Allocate_Set_Element; 1047 1048 -------------- 1049 -- New_Node -- 1050 -------------- 1051 1052 function New_Node return Count_Type is 1053 Result : Count_Type; 1054 begin 1055 Allocate (Container, Result); 1056 return Result; 1057 end New_Node; 1058 1059 -- Start of processing for Insert 1060 1061 begin 1062 Local_Insert (Container, New_Item, Node, Inserted); 1063 end Insert; 1064 1065 ------------------ 1066 -- Intersection -- 1067 ------------------ 1068 1069 procedure Intersection (Target : in out Set; Source : Set) is 1070 Tgt_Node : Count_Type; 1071 TN : Nodes_Type renames Target.Nodes; 1072 1073 begin 1074 if Target'Address = Source'Address then 1075 return; 1076 end if; 1077 1078 if Source.Length = 0 then 1079 Clear (Target); 1080 return; 1081 end if; 1082 1083 Tgt_Node := HT_Ops.First (Target); 1084 while Tgt_Node /= 0 loop 1085 if Find (Source, TN (Tgt_Node).Element).Node /= 0 then 1086 Tgt_Node := HT_Ops.Next (Target, Tgt_Node); 1087 1088 else 1089 declare 1090 X : constant Count_Type := Tgt_Node; 1091 begin 1092 Tgt_Node := HT_Ops.Next (Target, Tgt_Node); 1093 HT_Ops.Delete_Node_Sans_Free (Target, X); 1094 Free (Target, X); 1095 end; 1096 end if; 1097 end loop; 1098 end Intersection; 1099 1100 procedure Intersection (Left : Set; Right : Set; Target : in out Set) is 1101 procedure Process (L_Node : Count_Type); 1102 1103 procedure Iterate is 1104 new HT_Ops.Generic_Iteration (Process); 1105 1106 ------------- 1107 -- Process -- 1108 ------------- 1109 1110 procedure Process (L_Node : Count_Type) is 1111 E : Element_Type renames Left.Nodes (L_Node).Element; 1112 X : Count_Type; 1113 B : Boolean; 1114 1115 begin 1116 if Find (Right, E).Node /= 0 then 1117 Insert (Target, E, X, B); 1118 pragma Assert (B); 1119 end if; 1120 end Process; 1121 1122 -- Start of processing for Intersection 1123 1124 begin 1125 Iterate (Left); 1126 end Intersection; 1127 1128 function Intersection (Left : Set; Right : Set) return Set is 1129 C : Count_Type; 1130 H : Hash_Type; 1131 1132 begin 1133 if Left'Address = Right'Address then 1134 return Left.Copy; 1135 end if; 1136 1137 C := Count_Type'Min (Length (Left), Length (Right)); -- ??? 1138 H := Default_Modulus (C); 1139 1140 return S : Set (C, H) do 1141 if Length (Left) /= 0 and Length (Right) /= 0 then 1142 Intersection (Left, Right, Target => S); 1143 end if; 1144 end return; 1145 end Intersection; 1146 1147 -------------- 1148 -- Is_Empty -- 1149 -------------- 1150 1151 function Is_Empty (Container : Set) return Boolean is 1152 begin 1153 return Length (Container) = 0; 1154 end Is_Empty; 1155 1156 ----------- 1157 -- Is_In -- 1158 ----------- 1159 1160 function Is_In (HT : Set; Key : Node_Type) return Boolean is 1161 begin 1162 return Element_Keys.Find (HT, Key.Element) /= 0; 1163 end Is_In; 1164 1165 --------------- 1166 -- Is_Subset -- 1167 --------------- 1168 1169 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is 1170 Subset_Node : Count_Type; 1171 Subset_Nodes : Nodes_Type renames Subset.Nodes; 1172 1173 begin 1174 if Subset'Address = Of_Set'Address then 1175 return True; 1176 end if; 1177 1178 if Length (Subset) > Length (Of_Set) then 1179 return False; 1180 end if; 1181 1182 Subset_Node := First (Subset).Node; 1183 while Subset_Node /= 0 loop 1184 declare 1185 N : Node_Type renames Subset_Nodes (Subset_Node); 1186 E : Element_Type renames N.Element; 1187 1188 begin 1189 if Find (Of_Set, E).Node = 0 then 1190 return False; 1191 end if; 1192 end; 1193 1194 Subset_Node := HT_Ops.Next (Subset, Subset_Node); 1195 end loop; 1196 1197 return True; 1198 end Is_Subset; 1199 1200 ------------ 1201 -- Length -- 1202 ------------ 1203 1204 function Length (Container : Set) return Count_Type is 1205 begin 1206 return Container.Length; 1207 end Length; 1208 1209 ---------- 1210 -- Move -- 1211 ---------- 1212 1213 -- Comments??? 1214 1215 procedure Move (Target : in out Set; Source : in out Set) is 1216 NN : HT_Types.Nodes_Type renames Source.Nodes; 1217 X, Y : Count_Type; 1218 1219 begin 1220 if Target'Address = Source'Address then 1221 return; 1222 end if; 1223 1224 if Target.Capacity < Length (Source) then 1225 raise Constraint_Error with -- ??? 1226 "Source length exceeds Target capacity"; 1227 end if; 1228 1229 Clear (Target); 1230 1231 if Source.Length = 0 then 1232 return; 1233 end if; 1234 1235 X := HT_Ops.First (Source); 1236 while X /= 0 loop 1237 Insert (Target, NN (X).Element); -- optimize??? 1238 1239 Y := HT_Ops.Next (Source, X); 1240 1241 HT_Ops.Delete_Node_Sans_Free (Source, X); 1242 Free (Source, X); 1243 1244 X := Y; 1245 end loop; 1246 end Move; 1247 1248 ---------- 1249 -- Next -- 1250 ---------- 1251 1252 function Next (Node : Node_Type) return Count_Type is 1253 begin 1254 return Node.Next; 1255 end Next; 1256 1257 function Next (Container : Set; Position : Cursor) return Cursor is 1258 begin 1259 if Position.Node = 0 then 1260 return No_Element; 1261 end if; 1262 1263 if not Has_Element (Container, Position) then 1264 raise Constraint_Error with "Position has no element"; 1265 end if; 1266 1267 pragma Assert (Vet (Container, Position), "bad cursor in Next"); 1268 1269 return (Node => HT_Ops.Next (Container, Position.Node)); 1270 end Next; 1271 1272 procedure Next (Container : Set; Position : in out Cursor) is 1273 begin 1274 Position := Next (Container, Position); 1275 end Next; 1276 1277 ------------- 1278 -- Overlap -- 1279 ------------- 1280 1281 function Overlap (Left, Right : Set) return Boolean is 1282 Left_Node : Count_Type; 1283 Left_Nodes : Nodes_Type renames Left.Nodes; 1284 1285 begin 1286 if Length (Right) = 0 or Length (Left) = 0 then 1287 return False; 1288 end if; 1289 1290 if Left'Address = Right'Address then 1291 return True; 1292 end if; 1293 1294 Left_Node := First (Left).Node; 1295 while Left_Node /= 0 loop 1296 declare 1297 N : Node_Type renames Left_Nodes (Left_Node); 1298 E : Element_Type renames N.Element; 1299 begin 1300 if Find (Right, E).Node /= 0 then 1301 return True; 1302 end if; 1303 end; 1304 1305 Left_Node := HT_Ops.Next (Left, Left_Node); 1306 end loop; 1307 1308 return False; 1309 end Overlap; 1310 1311 ------------- 1312 -- Replace -- 1313 ------------- 1314 1315 procedure Replace (Container : in out Set; New_Item : Element_Type) is 1316 Node : constant Count_Type := Element_Keys.Find (Container, New_Item); 1317 1318 begin 1319 if Node = 0 then 1320 raise Constraint_Error with "attempt to replace element not in set"; 1321 end if; 1322 1323 Container.Nodes (Node).Element := New_Item; 1324 end Replace; 1325 1326 --------------------- 1327 -- Replace_Element -- 1328 --------------------- 1329 1330 procedure Replace_Element 1331 (Container : in out Set; 1332 Position : Cursor; 1333 New_Item : Element_Type) 1334 is 1335 begin 1336 if not Has_Element (Container, Position) then 1337 raise Constraint_Error with "Position cursor equals No_Element"; 1338 end if; 1339 1340 pragma Assert 1341 (Vet (Container, Position), "bad cursor in Replace_Element"); 1342 1343 Replace_Element (Container, Position.Node, New_Item); 1344 end Replace_Element; 1345 1346 ---------------------- 1347 -- Reserve_Capacity -- 1348 ---------------------- 1349 1350 procedure Reserve_Capacity 1351 (Container : in out Set; 1352 Capacity : Count_Type) 1353 is 1354 begin 1355 if Capacity > Container.Capacity then 1356 raise Constraint_Error with "requested capacity is too large"; 1357 end if; 1358 end Reserve_Capacity; 1359 1360 ------------------ 1361 -- Set_Element -- 1362 ------------------ 1363 1364 procedure Set_Element (Node : in out Node_Type; Item : Element_Type) is 1365 begin 1366 Node.Element := Item; 1367 end Set_Element; 1368 1369 -------------- 1370 -- Set_Next -- 1371 -------------- 1372 1373 procedure Set_Next (Node : in out Node_Type; Next : Count_Type) is 1374 begin 1375 Node.Next := Next; 1376 end Set_Next; 1377 1378 -------------------------- 1379 -- Symmetric_Difference -- 1380 -------------------------- 1381 1382 procedure Symmetric_Difference (Target : in out Set; Source : Set) is 1383 procedure Process (Source_Node : Count_Type); 1384 pragma Inline (Process); 1385 1386 procedure Iterate is new HT_Ops.Generic_Iteration (Process); 1387 1388 ------------- 1389 -- Process -- 1390 ------------- 1391 1392 procedure Process (Source_Node : Count_Type) is 1393 B : Boolean; 1394 N : Node_Type renames Source.Nodes (Source_Node); 1395 X : Count_Type; 1396 1397 begin 1398 if Is_In (Target, N) then 1399 Delete (Target, N.Element); 1400 else 1401 Insert (Target, N.Element, X, B); 1402 pragma Assert (B); 1403 end if; 1404 end Process; 1405 1406 -- Start of processing for Symmetric_Difference 1407 1408 begin 1409 if Target'Address = Source'Address then 1410 Clear (Target); 1411 return; 1412 end if; 1413 1414 if Length (Target) = 0 then 1415 Assign (Target, Source); 1416 return; 1417 end if; 1418 1419 Iterate (Source); 1420 end Symmetric_Difference; 1421 1422 function Symmetric_Difference (Left : Set; Right : Set) return Set is 1423 C : Count_Type; 1424 H : Hash_Type; 1425 1426 begin 1427 if Left'Address = Right'Address then 1428 return Empty_Set; 1429 end if; 1430 1431 if Length (Right) = 0 then 1432 return Left.Copy; 1433 end if; 1434 1435 if Length (Left) = 0 then 1436 return Right.Copy; 1437 end if; 1438 1439 C := Length (Left) + Length (Right); 1440 H := Default_Modulus (C); 1441 1442 return S : Set (C, H) do 1443 Difference (Left, Right, S); 1444 Difference (Right, Left, S); 1445 end return; 1446 end Symmetric_Difference; 1447 1448 ------------ 1449 -- To_Set -- 1450 ------------ 1451 1452 function To_Set (New_Item : Element_Type) return Set is 1453 X : Count_Type; 1454 B : Boolean; 1455 1456 begin 1457 return S : Set (Capacity => 1, Modulus => 1) do 1458 Insert (S, New_Item, X, B); 1459 pragma Assert (B); 1460 end return; 1461 end To_Set; 1462 1463 ----------- 1464 -- Union -- 1465 ----------- 1466 1467 procedure Union (Target : in out Set; Source : Set) is 1468 procedure Process (Src_Node : Count_Type); 1469 1470 procedure Iterate is 1471 new HT_Ops.Generic_Iteration (Process); 1472 1473 ------------- 1474 -- Process -- 1475 ------------- 1476 1477 procedure Process (Src_Node : Count_Type) is 1478 N : Node_Type renames Source.Nodes (Src_Node); 1479 E : Element_Type renames N.Element; 1480 1481 X : Count_Type; 1482 B : Boolean; 1483 1484 begin 1485 Insert (Target, E, X, B); 1486 end Process; 1487 1488 -- Start of processing for Union 1489 1490 begin 1491 if Target'Address = Source'Address then 1492 return; 1493 end if; 1494 1495 Iterate (Source); 1496 end Union; 1497 1498 function Union (Left : Set; Right : Set) return Set is 1499 C : Count_Type; 1500 H : Hash_Type; 1501 1502 begin 1503 if Left'Address = Right'Address then 1504 return Left.Copy; 1505 end if; 1506 1507 if Length (Right) = 0 then 1508 return Left.Copy; 1509 end if; 1510 1511 if Length (Left) = 0 then 1512 return Right.Copy; 1513 end if; 1514 1515 C := Length (Left) + Length (Right); 1516 H := Default_Modulus (C); 1517 return S : Set (C, H) do 1518 Assign (Target => S, Source => Left); 1519 Union (Target => S, Source => Right); 1520 end return; 1521 end Union; 1522 1523 --------- 1524 -- Vet -- 1525 --------- 1526 1527 function Vet (Container : Set; Position : Cursor) return Boolean is 1528 begin 1529 if Position.Node = 0 then 1530 return True; 1531 end if; 1532 1533 declare 1534 S : Set renames Container; 1535 N : Nodes_Type renames S.Nodes; 1536 X : Count_Type; 1537 1538 begin 1539 if S.Length = 0 then 1540 return False; 1541 end if; 1542 1543 if Position.Node > N'Last then 1544 return False; 1545 end if; 1546 1547 if N (Position.Node).Next = Position.Node then 1548 return False; 1549 end if; 1550 1551 X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element)); 1552 1553 for J in 1 .. S.Length loop 1554 if X = Position.Node then 1555 return True; 1556 end if; 1557 1558 if X = 0 then 1559 return False; 1560 end if; 1561 1562 if X = N (X).Next then -- to prevent unnecessary looping 1563 return False; 1564 end if; 1565 1566 X := N (X).Next; 1567 end loop; 1568 1569 return False; 1570 end; 1571 end Vet; 1572 1573end Ada.Containers.Formal_Hashed_Sets; 1574