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-2020, Free Software Foundation, Inc. -- 10-- -- 11-- GNAT is free software; you can redistribute it and/or modify it under -- 12-- terms of the GNU General Public License as published by the Free Soft- -- 13-- ware Foundation; either version 3, or (at your option) any later ver- -- 14-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 15-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 16-- or FITNESS FOR A PARTICULAR PURPOSE. -- 17-- -- 18-- As a special exception under Section 7 of GPL version 3, you are granted -- 19-- additional permissions described in the GCC Runtime Library Exception, -- 20-- version 3.1, as published by the Free Software Foundation. -- 21-- -- 22-- You should have received a copy of the GNU General Public License and -- 23-- a copy of the GCC Runtime Library Exception along with this program; -- 24-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 25-- <http://www.gnu.org/licenses/>. -- 26------------------------------------------------------------------------------ 27 28with System; use type System.Address; 29 30package body Ada.Containers.Formal_Doubly_Linked_Lists with 31 SPARK_Mode => Off 32is 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_Swapped -- 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 1894end Ada.Containers.Formal_Doubly_Linked_Lists; 1895