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