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