gcc/ada/a-cfdlli.adb

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