gcc/ada/libgnat/a-cfhase.adb

   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
  28 with Ada.Containers.Hash_Tables.Generic_Bounded_Operations;
  29 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Operations);
  30
  31 with Ada.Containers.Hash_Tables.Generic_Bounded_Keys;
  32 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys);
  33
  34 with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
  35
  36 with System; use type System.Address;
  37
  38 package body Ada.Containers.Formal_Hashed_Sets with
  39   SPARK_Mode => Off
  40 is
  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
1573 end Ada.Containers.Formal_Hashed_Sets;