1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- A D A . C O N T A I N E R S . F O R M A L _ V E C T O R S -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2010-2018, Free Software Foundation, Inc. -- 10-- -- 11-- GNAT is free software; you can redistribute it and/or modify it under -- 12-- terms of the GNU General Public License as published by the Free Soft- -- 13-- ware Foundation; either version 3, or (at your option) any later ver- -- 14-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 15-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 16-- or FITNESS FOR A PARTICULAR PURPOSE. -- 17-- -- 18-- As a special exception under Section 7 of GPL version 3, you are granted -- 19-- additional permissions described in the GCC Runtime Library Exception, -- 20-- version 3.1, as published by the Free Software Foundation. -- 21-- -- 22-- You should have received a copy of the GNU General Public License and -- 23-- a copy of the GCC Runtime Library Exception along with this program; -- 24-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 25-- <http://www.gnu.org/licenses/>. -- 26------------------------------------------------------------------------------ 27 28with Ada.Containers.Generic_Array_Sort; 29with Ada.Unchecked_Deallocation; 30 31with System; use type System.Address; 32 33package body Ada.Containers.Formal_Vectors with 34 SPARK_Mode => Off 35is 36 37 Growth_Factor : constant := 2; 38 -- When growing a container, multiply current capacity by this. Doubling 39 -- leads to amortized linear-time copying. 40 41 type Int is range System.Min_Int .. System.Max_Int; 42 43 procedure Free is 44 new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); 45 46 type Maximal_Array_Ptr is access all Elements_Array (Array_Index) 47 with Storage_Size => 0; 48 type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index) 49 with Storage_Size => 0; 50 51 function Elems (Container : in out Vector) return Maximal_Array_Ptr; 52 function Elemsc 53 (Container : Vector) return Maximal_Array_Ptr_Const; 54 -- Returns a pointer to the Elements array currently in use -- either 55 -- Container.Elements_Ptr or a pointer to Container.Elements. We work with 56 -- pointers to a bogus array subtype that is constrained with the maximum 57 -- possible bounds. This means that the pointer is a thin pointer. This is 58 -- necessary because 'Unrestricted_Access doesn't work when it produces 59 -- access-to-unconstrained and is returned from a function. 60 -- 61 -- Note that this is dangerous: make sure calls to this use an indexed 62 -- component or slice that is within the bounds 1 .. Length (Container). 63 64 function Get_Element 65 (Container : Vector; 66 Position : Capacity_Range) return Element_Type; 67 68 function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base; 69 70 function Current_Capacity (Container : Vector) return Capacity_Range; 71 72 procedure Insert_Space 73 (Container : in out Vector; 74 Before : Extended_Index; 75 Count : Count_Type := 1); 76 77 --------- 78 -- "=" -- 79 --------- 80 81 function "=" (Left : Vector; Right : Vector) return Boolean is 82 begin 83 if Left'Address = Right'Address then 84 return True; 85 end if; 86 87 if Length (Left) /= Length (Right) then 88 return False; 89 end if; 90 91 for J in 1 .. Length (Left) loop 92 if Get_Element (Left, J) /= Get_Element (Right, J) then 93 return False; 94 end if; 95 end loop; 96 97 return True; 98 end "="; 99 100 ------------ 101 -- Append -- 102 ------------ 103 104 procedure Append (Container : in out Vector; New_Item : Vector) is 105 begin 106 if Is_Empty (New_Item) then 107 return; 108 end if; 109 110 if Container.Last >= Index_Type'Last then 111 raise Constraint_Error with "vector is already at its maximum length"; 112 end if; 113 114 Insert (Container, Container.Last + 1, New_Item); 115 end Append; 116 117 procedure Append (Container : in out Vector; New_Item : Element_Type) is 118 begin 119 Append (Container, New_Item, 1); 120 end Append; 121 122 procedure Append 123 (Container : in out Vector; 124 New_Item : Element_Type; 125 Count : Count_Type) 126 is 127 begin 128 if Count = 0 then 129 return; 130 end if; 131 132 if Container.Last >= Index_Type'Last then 133 raise Constraint_Error with "vector is already at its maximum length"; 134 end if; 135 136 Insert (Container, Container.Last + 1, New_Item, Count); 137 end Append; 138 139 ------------ 140 -- Assign -- 141 ------------ 142 143 procedure Assign (Target : in out Vector; Source : Vector) is 144 LS : constant Capacity_Range := Length (Source); 145 146 begin 147 if Target'Address = Source'Address then 148 return; 149 end if; 150 151 if Bounded and then Target.Capacity < LS then 152 raise Constraint_Error; 153 end if; 154 155 Clear (Target); 156 Append (Target, Source); 157 end Assign; 158 159 -------------- 160 -- Capacity -- 161 -------------- 162 163 function Capacity (Container : Vector) return Capacity_Range is 164 begin 165 return 166 (if Bounded then 167 Container.Capacity 168 else 169 Capacity_Range'Last); 170 end Capacity; 171 172 ----------- 173 -- Clear -- 174 ----------- 175 176 procedure Clear (Container : in out Vector) is 177 begin 178 Container.Last := No_Index; 179 180 -- Free element, note that this is OK if Elements_Ptr is null 181 182 Free (Container.Elements_Ptr); 183 end Clear; 184 185 -------------- 186 -- Contains -- 187 -------------- 188 189 function Contains 190 (Container : Vector; 191 Item : Element_Type) return Boolean 192 is 193 begin 194 return Find_Index (Container, Item) /= No_Index; 195 end Contains; 196 197 ---------- 198 -- Copy -- 199 ---------- 200 201 function Copy 202 (Source : Vector; 203 Capacity : Capacity_Range := 0) return Vector 204 is 205 LS : constant Capacity_Range := Length (Source); 206 C : Capacity_Range; 207 208 begin 209 if Capacity = 0 then 210 C := LS; 211 elsif Capacity >= LS then 212 C := Capacity; 213 else 214 raise Capacity_Error; 215 end if; 216 217 return Target : Vector (C) do 218 Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS); 219 Target.Last := Source.Last; 220 end return; 221 end Copy; 222 223 ---------------------- 224 -- Current_Capacity -- 225 ---------------------- 226 227 function Current_Capacity (Container : Vector) return Capacity_Range is 228 begin 229 return 230 (if Container.Elements_Ptr = null then 231 Container.Elements'Length 232 else 233 Container.Elements_Ptr.all'Length); 234 end Current_Capacity; 235 236 ------------ 237 -- Delete -- 238 ------------ 239 240 procedure Delete (Container : in out Vector; Index : Extended_Index) is 241 begin 242 Delete (Container, Index, 1); 243 end Delete; 244 245 procedure Delete 246 (Container : in out Vector; 247 Index : Extended_Index; 248 Count : Count_Type) 249 is 250 Old_Last : constant Index_Type'Base := Container.Last; 251 Old_Len : constant Count_Type := Length (Container); 252 New_Last : Index_Type'Base; 253 Count2 : Count_Type'Base; -- count of items from Index to Old_Last 254 Off : Count_Type'Base; -- Index expressed as offset from IT'First 255 256 begin 257 -- Delete removes items from the vector, the number of which is the 258 -- minimum of the specified Count and the items (if any) that exist from 259 -- Index to Container.Last. There are no constraints on the specified 260 -- value of Count (it can be larger than what's available at this 261 -- position in the vector, for example), but there are constraints on 262 -- the allowed values of the Index. 263 264 -- As a precondition on the generic actual Index_Type, the base type 265 -- must include Index_Type'Pred (Index_Type'First); this is the value 266 -- that Container.Last assumes when the vector is empty. However, we do 267 -- not allow that as the value for Index when specifying which items 268 -- should be deleted, so we must manually check. (That the user is 269 -- allowed to specify the value at all here is a consequence of the 270 -- declaration of the Extended_Index subtype, which includes the values 271 -- in the base range that immediately precede and immediately follow the 272 -- values in the Index_Type.) 273 274 if Index < Index_Type'First then 275 raise Constraint_Error with "Index is out of range (too small)"; 276 end if; 277 278 -- We do allow a value greater than Container.Last to be specified as 279 -- the Index, but only if it's immediately greater. This allows the 280 -- corner case of deleting no items from the back end of the vector to 281 -- be treated as a no-op. (It is assumed that specifying an index value 282 -- greater than Last + 1 indicates some deeper flaw in the caller's 283 -- algorithm, so that case is treated as a proper error.) 284 285 if Index > Old_Last then 286 if Index > Old_Last + 1 then 287 raise Constraint_Error with "Index is out of range (too large)"; 288 end if; 289 290 return; 291 end if; 292 293 if Count = 0 then 294 return; 295 end if; 296 297 -- We first calculate what's available for deletion starting at 298 -- Index. Here and elsewhere we use the wider of Index_Type'Base and 299 -- Count_Type'Base as the type for intermediate values. (See function 300 -- Length for more information.) 301 302 if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then 303 Count2 := Count_Type'Base (Old_Last) - Count_Type'Base (Index) + 1; 304 else 305 Count2 := Count_Type'Base (Old_Last - Index + 1); 306 end if; 307 308 -- If more elements are requested (Count) for deletion than are 309 -- available (Count2) for deletion beginning at Index, then everything 310 -- from Index is deleted. There are no elements to slide down, and so 311 -- all we need to do is set the value of Container.Last. 312 313 if Count >= Count2 then 314 Container.Last := Index - 1; 315 return; 316 end if; 317 318 -- There are some elements aren't being deleted (the requested count was 319 -- less than the available count), so we must slide them down to Index. 320 -- We first calculate the index values of the respective array slices, 321 -- using the wider of Index_Type'Base and Count_Type'Base as the type 322 -- for intermediate calculations. 323 324 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then 325 Off := Count_Type'Base (Index - Index_Type'First); 326 New_Last := Old_Last - Index_Type'Base (Count); 327 else 328 Off := Count_Type'Base (Index) - Count_Type'Base (Index_Type'First); 329 New_Last := Index_Type'Base (Count_Type'Base (Old_Last) - Count); 330 end if; 331 332 -- The array index values for each slice have already been determined, 333 -- so we just slide down to Index the elements that weren't deleted. 334 335 declare 336 EA : Maximal_Array_Ptr renames Elems (Container); 337 Idx : constant Count_Type := EA'First + Off; 338 begin 339 EA (Idx .. Old_Len - Count) := EA (Idx + Count .. Old_Len); 340 Container.Last := New_Last; 341 end; 342 end Delete; 343 344 ------------------ 345 -- Delete_First -- 346 ------------------ 347 348 procedure Delete_First (Container : in out Vector) is 349 begin 350 Delete_First (Container, 1); 351 end Delete_First; 352 353 procedure Delete_First (Container : in out Vector; Count : Count_Type) is 354 begin 355 if Count = 0 then 356 return; 357 358 elsif Count >= Length (Container) then 359 Clear (Container); 360 return; 361 362 else 363 Delete (Container, Index_Type'First, Count); 364 end if; 365 end Delete_First; 366 367 ----------------- 368 -- Delete_Last -- 369 ----------------- 370 371 procedure Delete_Last (Container : in out Vector) is 372 begin 373 Delete_Last (Container, 1); 374 end Delete_Last; 375 376 procedure Delete_Last (Container : in out Vector; Count : Count_Type) is 377 begin 378 if Count = 0 then 379 return; 380 end if; 381 382 -- There is no restriction on how large Count can be when deleting 383 -- items. If it is equal or greater than the current length, then this 384 -- is equivalent to clearing the vector. (In particular, there's no need 385 -- for us to actually calculate the new value for Last.) 386 387 -- If the requested count is less than the current length, then we must 388 -- calculate the new value for Last. For the type we use the widest of 389 -- Index_Type'Base and Count_Type'Base for the intermediate values of 390 -- our calculation. (See the comments in Length for more information.) 391 392 if Count >= Length (Container) then 393 Container.Last := No_Index; 394 395 elsif Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then 396 Container.Last := Container.Last - Index_Type'Base (Count); 397 398 else 399 Container.Last := 400 Index_Type'Base (Count_Type'Base (Container.Last) - Count); 401 end if; 402 end Delete_Last; 403 404 ------------- 405 -- Element -- 406 ------------- 407 408 function Element 409 (Container : Vector; 410 Index : Index_Type) return Element_Type 411 is 412 begin 413 if Index > Container.Last then 414 raise Constraint_Error with "Index is out of range"; 415 end if; 416 417 declare 418 II : constant Int'Base := Int (Index) - Int (No_Index); 419 I : constant Capacity_Range := Capacity_Range (II); 420 begin 421 return Get_Element (Container, I); 422 end; 423 end Element; 424 425 -------------- 426 -- Elements -- 427 -------------- 428 429 function Elems (Container : in out Vector) return Maximal_Array_Ptr is 430 begin 431 return 432 (if Container.Elements_Ptr = null then 433 Container.Elements'Unrestricted_Access 434 else 435 Container.Elements_Ptr.all'Unrestricted_Access); 436 end Elems; 437 438 function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is 439 begin 440 return 441 (if Container.Elements_Ptr = null then 442 Container.Elements'Unrestricted_Access 443 else 444 Container.Elements_Ptr.all'Unrestricted_Access); 445 end Elemsc; 446 447 ---------------- 448 -- Find_Index -- 449 ---------------- 450 451 function Find_Index 452 (Container : Vector; 453 Item : Element_Type; 454 Index : Index_Type := Index_Type'First) return Extended_Index 455 is 456 K : Capacity_Range; 457 Last : constant Index_Type := Last_Index (Container); 458 459 begin 460 K := Capacity_Range (Int (Index) - Int (No_Index)); 461 for Indx in Index .. Last loop 462 if Get_Element (Container, K) = Item then 463 return Indx; 464 end if; 465 466 K := K + 1; 467 end loop; 468 469 return No_Index; 470 end Find_Index; 471 472 ------------------- 473 -- First_Element -- 474 ------------------- 475 476 function First_Element (Container : Vector) return Element_Type is 477 begin 478 if Is_Empty (Container) then 479 raise Constraint_Error with "Container is empty"; 480 else 481 return Get_Element (Container, 1); 482 end if; 483 end First_Element; 484 485 ----------------- 486 -- First_Index -- 487 ----------------- 488 489 function First_Index (Container : Vector) return Index_Type is 490 pragma Unreferenced (Container); 491 begin 492 return Index_Type'First; 493 end First_Index; 494 495 ------------------ 496 -- Formal_Model -- 497 ------------------ 498 499 package body Formal_Model is 500 501 ------------------------- 502 -- M_Elements_In_Union -- 503 ------------------------- 504 505 function M_Elements_In_Union 506 (Container : M.Sequence; 507 Left : M.Sequence; 508 Right : M.Sequence) return Boolean 509 is 510 Elem : Element_Type; 511 512 begin 513 for Index in Index_Type'First .. M.Last (Container) loop 514 Elem := Element (Container, Index); 515 516 if not M.Contains (Left, Index_Type'First, M.Last (Left), Elem) 517 and then 518 not M.Contains (Right, Index_Type'First, M.Last (Right), Elem) 519 then 520 return False; 521 end if; 522 end loop; 523 524 return True; 525 end M_Elements_In_Union; 526 527 ------------------------- 528 -- M_Elements_Included -- 529 ------------------------- 530 531 function M_Elements_Included 532 (Left : M.Sequence; 533 L_Fst : Index_Type := Index_Type'First; 534 L_Lst : Extended_Index; 535 Right : M.Sequence; 536 R_Fst : Index_Type := Index_Type'First; 537 R_Lst : Extended_Index) return Boolean 538 is 539 begin 540 for I in L_Fst .. L_Lst loop 541 declare 542 Found : Boolean := False; 543 J : Extended_Index := R_Fst - 1; 544 545 begin 546 while not Found and J < R_Lst loop 547 J := J + 1; 548 if Element (Left, I) = Element (Right, J) then 549 Found := True; 550 end if; 551 end loop; 552 553 if not Found then 554 return False; 555 end if; 556 end; 557 end loop; 558 559 return True; 560 end M_Elements_Included; 561 562 ------------------------- 563 -- M_Elements_Reversed -- 564 ------------------------- 565 566 function M_Elements_Reversed 567 (Left : M.Sequence; 568 Right : M.Sequence) return Boolean 569 is 570 L : constant Index_Type := M.Last (Left); 571 572 begin 573 if L /= M.Last (Right) then 574 return False; 575 end if; 576 577 for I in Index_Type'First .. L loop 578 if Element (Left, I) /= Element (Right, L - I + 1) 579 then 580 return False; 581 end if; 582 end loop; 583 584 return True; 585 end M_Elements_Reversed; 586 587 ------------------------ 588 -- M_Elements_Swapted -- 589 ------------------------ 590 591 function M_Elements_Swapped 592 (Left : M.Sequence; 593 Right : M.Sequence; 594 X : Index_Type; 595 Y : Index_Type) return Boolean 596 is 597 begin 598 if M.Length (Left) /= M.Length (Right) 599 or else Element (Left, X) /= Element (Right, Y) 600 or else Element (Left, Y) /= Element (Right, X) 601 then 602 return False; 603 end if; 604 605 for I in Index_Type'First .. M.Last (Left) loop 606 if I /= X and then I /= Y 607 and then Element (Left, I) /= Element (Right, I) 608 then 609 return False; 610 end if; 611 end loop; 612 613 return True; 614 end M_Elements_Swapped; 615 616 ----------- 617 -- Model -- 618 ----------- 619 620 function Model (Container : Vector) return M.Sequence is 621 R : M.Sequence; 622 623 begin 624 for Position in 1 .. Length (Container) loop 625 R := M.Add (R, Elemsc (Container) (Position)); 626 end loop; 627 628 return R; 629 end Model; 630 631 end Formal_Model; 632 633 --------------------- 634 -- Generic_Sorting -- 635 --------------------- 636 637 package body Generic_Sorting with SPARK_Mode => Off is 638 639 ------------------ 640 -- Formal_Model -- 641 ------------------ 642 643 package body Formal_Model is 644 645 ----------------------- 646 -- M_Elements_Sorted -- 647 ----------------------- 648 649 function M_Elements_Sorted (Container : M.Sequence) return Boolean is 650 begin 651 if M.Length (Container) = 0 then 652 return True; 653 end if; 654 655 declare 656 E1 : Element_Type := Element (Container, Index_Type'First); 657 658 begin 659 for I in Index_Type'First + 1 .. M.Last (Container) loop 660 declare 661 E2 : constant Element_Type := Element (Container, I); 662 663 begin 664 if E2 < E1 then 665 return False; 666 end if; 667 668 E1 := E2; 669 end; 670 end loop; 671 end; 672 673 return True; 674 end M_Elements_Sorted; 675 676 end Formal_Model; 677 678 --------------- 679 -- Is_Sorted -- 680 --------------- 681 682 function Is_Sorted (Container : Vector) return Boolean is 683 L : constant Capacity_Range := Length (Container); 684 685 begin 686 for J in 1 .. L - 1 loop 687 if Get_Element (Container, J + 1) < 688 Get_Element (Container, J) 689 then 690 return False; 691 end if; 692 end loop; 693 694 return True; 695 end Is_Sorted; 696 697 ---------- 698 -- Sort -- 699 ---------- 700 701 procedure Sort (Container : in out Vector) is 702 procedure Sort is 703 new Generic_Array_Sort 704 (Index_Type => Array_Index, 705 Element_Type => Element_Type, 706 Array_Type => Elements_Array, 707 "<" => "<"); 708 709 Len : constant Capacity_Range := Length (Container); 710 711 begin 712 if Container.Last <= Index_Type'First then 713 return; 714 else 715 Sort (Elems (Container) (1 .. Len)); 716 end if; 717 end Sort; 718 719 ----------- 720 -- Merge -- 721 ----------- 722 723 procedure Merge (Target : in out Vector; Source : in out Vector) is 724 I : Count_Type; 725 J : Count_Type; 726 727 begin 728 if Target'Address = Source'Address then 729 raise Program_Error with "Target and Source denote same container"; 730 end if; 731 732 if Length (Source) = 0 then 733 return; 734 end if; 735 736 if Length (Target) = 0 then 737 Move (Target => Target, Source => Source); 738 return; 739 end if; 740 741 I := Length (Target); 742 743 declare 744 New_Length : constant Count_Type := I + Length (Source); 745 746 begin 747 if not Bounded 748 and then Current_Capacity (Target) < Capacity_Range (New_Length) 749 then 750 Reserve_Capacity 751 (Target, 752 Capacity_Range'Max 753 (Current_Capacity (Target) * Growth_Factor, 754 Capacity_Range (New_Length))); 755 end if; 756 757 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then 758 Target.Last := No_Index + Index_Type'Base (New_Length); 759 760 else 761 Target.Last := 762 Index_Type'Base (Count_Type'Base (No_Index) + New_Length); 763 end if; 764 end; 765 766 declare 767 TA : Maximal_Array_Ptr renames Elems (Target); 768 SA : Maximal_Array_Ptr renames Elems (Source); 769 770 begin 771 J := Length (Target); 772 while Length (Source) /= 0 loop 773 if I = 0 then 774 TA (1 .. J) := SA (1 .. Length (Source)); 775 Source.Last := No_Index; 776 exit; 777 end if; 778 779 if SA (Length (Source)) < TA (I) then 780 TA (J) := TA (I); 781 I := I - 1; 782 783 else 784 TA (J) := SA (Length (Source)); 785 Source.Last := Source.Last - 1; 786 end if; 787 788 J := J - 1; 789 end loop; 790 end; 791 end Merge; 792 793 end Generic_Sorting; 794 795 ----------------- 796 -- Get_Element -- 797 ----------------- 798 799 function Get_Element 800 (Container : Vector; 801 Position : Capacity_Range) return Element_Type 802 is 803 begin 804 return Elemsc (Container) (Position); 805 end Get_Element; 806 807 ----------------- 808 -- Has_Element -- 809 ----------------- 810 811 function Has_Element 812 (Container : Vector; 813 Position : Extended_Index) return Boolean 814 is 815 begin 816 return Position in First_Index (Container) .. Last_Index (Container); 817 end Has_Element; 818 819 ------------ 820 -- Insert -- 821 ------------ 822 823 procedure Insert 824 (Container : in out Vector; 825 Before : Extended_Index; 826 New_Item : Element_Type) 827 is 828 begin 829 Insert (Container, Before, New_Item, 1); 830 end Insert; 831 832 procedure Insert 833 (Container : in out Vector; 834 Before : Extended_Index; 835 New_Item : Element_Type; 836 Count : Count_Type) 837 is 838 J : Count_Type'Base; -- scratch 839 840 begin 841 -- Use Insert_Space to create the "hole" (the destination slice) 842 843 Insert_Space (Container, Before, Count); 844 845 J := To_Array_Index (Before); 846 847 Elems (Container) (J .. J - 1 + Count) := (others => New_Item); 848 end Insert; 849 850 procedure Insert 851 (Container : in out Vector; 852 Before : Extended_Index; 853 New_Item : Vector) 854 is 855 N : constant Count_Type := Length (New_Item); 856 B : Count_Type; -- index Before converted to Count_Type 857 858 begin 859 if Container'Address = New_Item'Address then 860 raise Program_Error with 861 "Container and New_Item denote same container"; 862 end if; 863 864 -- Use Insert_Space to create the "hole" (the destination slice) into 865 -- which we copy the source items. 866 867 Insert_Space (Container, Before, Count => N); 868 869 if N = 0 then 870 871 -- There's nothing else to do here (vetting of parameters was 872 -- performed already in Insert_Space), so we simply return. 873 874 return; 875 end if; 876 877 B := To_Array_Index (Before); 878 879 Elems (Container) (B .. B + N - 1) := Elemsc (New_Item) (1 .. N); 880 end Insert; 881 882 ------------------ 883 -- Insert_Space -- 884 ------------------ 885 886 procedure Insert_Space 887 (Container : in out Vector; 888 Before : Extended_Index; 889 Count : Count_Type := 1) 890 is 891 Old_Length : constant Count_Type := Length (Container); 892 893 Max_Length : Count_Type'Base; -- determined from range of Index_Type 894 New_Length : Count_Type'Base; -- sum of current length and Count 895 896 Index : Index_Type'Base; -- scratch for intermediate values 897 J : Count_Type'Base; -- scratch 898 899 begin 900 -- As a precondition on the generic actual Index_Type, the base type 901 -- must include Index_Type'Pred (Index_Type'First); this is the value 902 -- that Container.Last assumes when the vector is empty. However, we do 903 -- not allow that as the value for Index when specifying where the new 904 -- items should be inserted, so we must manually check. (That the user 905 -- is allowed to specify the value at all here is a consequence of the 906 -- declaration of the Extended_Index subtype, which includes the values 907 -- in the base range that immediately precede and immediately follow the 908 -- values in the Index_Type.) 909 910 if Before < Index_Type'First then 911 raise Constraint_Error with 912 "Before index is out of range (too small)"; 913 end if; 914 915 -- We do allow a value greater than Container.Last to be specified as 916 -- the Index, but only if it's immediately greater. This allows for the 917 -- case of appending items to the back end of the vector. (It is assumed 918 -- that specifying an index value greater than Last + 1 indicates some 919 -- deeper flaw in the caller's algorithm, so that case is treated as a 920 -- proper error.) 921 922 if Before > Container.Last 923 and then Before - 1 > Container.Last 924 then 925 raise Constraint_Error with 926 "Before index is out of range (too large)"; 927 end if; 928 929 -- We treat inserting 0 items into the container as a no-op, so we 930 -- simply return. 931 932 if Count = 0 then 933 return; 934 end if; 935 936 -- There are two constraints we need to satisfy. The first constraint is 937 -- that a container cannot have more than Count_Type'Last elements, so 938 -- we must check the sum of the current length and the insertion count. 939 -- Note that the value cannot be simply added because the result may 940 -- overflow. 941 942 if Old_Length > Count_Type'Last - Count then 943 raise Constraint_Error with "Count is out of range"; 944 end if; 945 946 -- It is now safe compute the length of the new vector, without fear of 947 -- overflow. 948 949 New_Length := Old_Length + Count; 950 951 -- The second constraint is that the new Last index value cannot exceed 952 -- Index_Type'Last. In each branch below, we calculate the maximum 953 -- length (computed from the range of values in Index_Type), and then 954 -- compare the new length to the maximum length. If the new length is 955 -- acceptable, then we compute the new last index from that. 956 957 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then 958 959 -- We have to handle the case when there might be more values in the 960 -- range of Index_Type than in the range of Count_Type. 961 962 if Index_Type'First <= 0 then 963 964 -- We know that No_Index (the same as Index_Type'First - 1) is 965 -- less than 0, so it is safe to compute the following sum without 966 -- fear of overflow. 967 968 Index := No_Index + Index_Type'Base (Count_Type'Last); 969 970 if Index <= Index_Type'Last then 971 972 -- We have determined that range of Index_Type has at least as 973 -- many values as in Count_Type, so Count_Type'Last is the 974 -- maximum number of items that are allowed. 975 976 Max_Length := Count_Type'Last; 977 978 else 979 -- The range of Index_Type has fewer values than in Count_Type, 980 -- so the maximum number of items is computed from the range of 981 -- the Index_Type. 982 983 Max_Length := Count_Type'Base (Index_Type'Last - No_Index); 984 end if; 985 986 else 987 -- No_Index is equal or greater than 0, so we can safely compute 988 -- the difference without fear of overflow (which we would have to 989 -- worry about if No_Index were less than 0, but that case is 990 -- handled above). 991 992 if Index_Type'Last - No_Index >= Count_Type'Pos (Count_Type'Last) 993 then 994 -- We have determined that range of Index_Type has at least as 995 -- many values as in Count_Type, so Count_Type'Last is the 996 -- maximum number of items that are allowed. 997 998 Max_Length := Count_Type'Last; 999 1000 else 1001 -- The range of Index_Type has fewer values than in Count_Type, 1002 -- so the maximum number of items is computed from the range of 1003 -- the Index_Type. 1004 1005 Max_Length := Count_Type'Base (Index_Type'Last - No_Index); 1006 end if; 1007 end if; 1008 1009 elsif Index_Type'First <= 0 then 1010 1011 -- We know that No_Index (the same as Index_Type'First - 1) is less 1012 -- than 0, so it is safe to compute the following sum without fear of 1013 -- overflow. 1014 1015 J := Count_Type'Base (No_Index) + Count_Type'Last; 1016 1017 if J <= Count_Type'Base (Index_Type'Last) then 1018 1019 -- We have determined that range of Index_Type has at least as 1020 -- many values as in Count_Type, so Count_Type'Last is the maximum 1021 -- number of items that are allowed. 1022 1023 Max_Length := Count_Type'Last; 1024 1025 else 1026 -- The range of Index_Type has fewer values than Count_Type does, 1027 -- so the maximum number of items is computed from the range of 1028 -- the Index_Type. 1029 1030 Max_Length := 1031 Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); 1032 end if; 1033 1034 else 1035 -- No_Index is equal or greater than 0, so we can safely compute the 1036 -- difference without fear of overflow (which we would have to worry 1037 -- about if No_Index were less than 0, but that case is handled 1038 -- above). 1039 1040 Max_Length := 1041 Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); 1042 end if; 1043 1044 -- We have just computed the maximum length (number of items). We must 1045 -- now compare the requested length to the maximum length, as we do not 1046 -- allow a vector expand beyond the maximum (because that would create 1047 -- an internal array with a last index value greater than 1048 -- Index_Type'Last, with no way to index those elements). 1049 1050 if New_Length > Max_Length then 1051 raise Constraint_Error with "Count is out of range"; 1052 end if; 1053 1054 J := To_Array_Index (Before); 1055 1056 -- Increase the capacity of container if needed 1057 1058 if not Bounded 1059 and then Current_Capacity (Container) < Capacity_Range (New_Length) 1060 then 1061 Reserve_Capacity 1062 (Container, 1063 Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor, 1064 Capacity_Range (New_Length))); 1065 end if; 1066 1067 declare 1068 EA : Maximal_Array_Ptr renames Elems (Container); 1069 1070 begin 1071 if Before <= Container.Last then 1072 1073 -- The new items are being inserted before some existing 1074 -- elements, so we must slide the existing elements up to their 1075 -- new home. 1076 1077 EA (J + Count .. New_Length) := EA (J .. Old_Length); 1078 end if; 1079 end; 1080 1081 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then 1082 Container.Last := No_Index + Index_Type'Base (New_Length); 1083 1084 else 1085 Container.Last := 1086 Index_Type'Base (Count_Type'Base (No_Index) + New_Length); 1087 end if; 1088 end Insert_Space; 1089 1090 -------------- 1091 -- Is_Empty -- 1092 -------------- 1093 1094 function Is_Empty (Container : Vector) return Boolean is 1095 begin 1096 return Last_Index (Container) < Index_Type'First; 1097 end Is_Empty; 1098 1099 ------------------ 1100 -- Last_Element -- 1101 ------------------ 1102 1103 function Last_Element (Container : Vector) return Element_Type is 1104 begin 1105 if Is_Empty (Container) then 1106 raise Constraint_Error with "Container is empty"; 1107 else 1108 return Get_Element (Container, Length (Container)); 1109 end if; 1110 end Last_Element; 1111 1112 ---------------- 1113 -- Last_Index -- 1114 ---------------- 1115 1116 function Last_Index (Container : Vector) return Extended_Index is 1117 begin 1118 return Container.Last; 1119 end Last_Index; 1120 1121 ------------ 1122 -- Length -- 1123 ------------ 1124 1125 function Length (Container : Vector) return Capacity_Range is 1126 L : constant Int := Int (Container.Last); 1127 F : constant Int := Int (Index_Type'First); 1128 N : constant Int'Base := L - F + 1; 1129 1130 begin 1131 return Capacity_Range (N); 1132 end Length; 1133 1134 ---------- 1135 -- Move -- 1136 ---------- 1137 1138 procedure Move (Target : in out Vector; Source : in out Vector) is 1139 LS : constant Capacity_Range := Length (Source); 1140 1141 begin 1142 if Target'Address = Source'Address then 1143 return; 1144 end if; 1145 1146 if Bounded and then Target.Capacity < LS then 1147 raise Constraint_Error; 1148 end if; 1149 1150 Clear (Target); 1151 Append (Target, Source); 1152 Clear (Source); 1153 end Move; 1154 1155 ------------ 1156 -- Prepend -- 1157 ------------ 1158 1159 procedure Prepend (Container : in out Vector; New_Item : Vector) is 1160 begin 1161 Insert (Container, Index_Type'First, New_Item); 1162 end Prepend; 1163 1164 procedure Prepend (Container : in out Vector; New_Item : Element_Type) is 1165 begin 1166 Prepend (Container, New_Item, 1); 1167 end Prepend; 1168 1169 procedure Prepend 1170 (Container : in out Vector; 1171 New_Item : Element_Type; 1172 Count : Count_Type) 1173 is 1174 begin 1175 Insert (Container, Index_Type'First, New_Item, Count); 1176 end Prepend; 1177 1178 --------------------- 1179 -- Replace_Element -- 1180 --------------------- 1181 1182 procedure Replace_Element 1183 (Container : in out Vector; 1184 Index : Index_Type; 1185 New_Item : Element_Type) 1186 is 1187 begin 1188 if Index > Container.Last then 1189 raise Constraint_Error with "Index is out of range"; 1190 end if; 1191 1192 declare 1193 II : constant Int'Base := Int (Index) - Int (No_Index); 1194 I : constant Capacity_Range := Capacity_Range (II); 1195 1196 begin 1197 Elems (Container) (I) := New_Item; 1198 end; 1199 end Replace_Element; 1200 1201 ---------------------- 1202 -- Reserve_Capacity -- 1203 ---------------------- 1204 1205 procedure Reserve_Capacity 1206 (Container : in out Vector; 1207 Capacity : Capacity_Range) 1208 is 1209 begin 1210 if Bounded then 1211 if Capacity > Container.Capacity then 1212 raise Constraint_Error with "Capacity is out of range"; 1213 end if; 1214 1215 else 1216 if Capacity > Formal_Vectors.Current_Capacity (Container) then 1217 declare 1218 New_Elements : constant Elements_Array_Ptr := 1219 new Elements_Array (1 .. Capacity); 1220 L : constant Capacity_Range := Length (Container); 1221 1222 begin 1223 New_Elements (1 .. L) := Elemsc (Container) (1 .. L); 1224 Free (Container.Elements_Ptr); 1225 Container.Elements_Ptr := New_Elements; 1226 end; 1227 end if; 1228 end if; 1229 end Reserve_Capacity; 1230 1231 ---------------------- 1232 -- Reverse_Elements -- 1233 ---------------------- 1234 1235 procedure Reverse_Elements (Container : in out Vector) is 1236 begin 1237 if Length (Container) <= 1 then 1238 return; 1239 end if; 1240 1241 declare 1242 I, J : Capacity_Range; 1243 E : Elements_Array renames 1244 Elems (Container) (1 .. Length (Container)); 1245 1246 begin 1247 I := 1; 1248 J := Length (Container); 1249 while I < J loop 1250 declare 1251 EI : constant Element_Type := E (I); 1252 1253 begin 1254 E (I) := E (J); 1255 E (J) := EI; 1256 end; 1257 1258 I := I + 1; 1259 J := J - 1; 1260 end loop; 1261 end; 1262 end Reverse_Elements; 1263 1264 ------------------------ 1265 -- Reverse_Find_Index -- 1266 ------------------------ 1267 1268 function Reverse_Find_Index 1269 (Container : Vector; 1270 Item : Element_Type; 1271 Index : Index_Type := Index_Type'Last) return Extended_Index 1272 is 1273 Last : Index_Type'Base; 1274 K : Capacity_Range; 1275 1276 begin 1277 if Index > Last_Index (Container) then 1278 Last := Last_Index (Container); 1279 else 1280 Last := Index; 1281 end if; 1282 1283 K := Capacity_Range (Int (Last) - Int (No_Index)); 1284 for Indx in reverse Index_Type'First .. Last loop 1285 if Get_Element (Container, K) = Item then 1286 return Indx; 1287 end if; 1288 1289 K := K - 1; 1290 end loop; 1291 1292 return No_Index; 1293 end Reverse_Find_Index; 1294 1295 ---------- 1296 -- Swap -- 1297 ---------- 1298 1299 procedure Swap 1300 (Container : in out Vector; 1301 I : Index_Type; 1302 J : Index_Type) 1303 is 1304 begin 1305 if I > Container.Last then 1306 raise Constraint_Error with "I index is out of range"; 1307 end if; 1308 1309 if J > Container.Last then 1310 raise Constraint_Error with "J index is out of range"; 1311 end if; 1312 1313 if I = J then 1314 return; 1315 end if; 1316 1317 declare 1318 II : constant Int'Base := Int (I) - Int (No_Index); 1319 JJ : constant Int'Base := Int (J) - Int (No_Index); 1320 1321 EI : Element_Type renames Elems (Container) (Capacity_Range (II)); 1322 EJ : Element_Type renames Elems (Container) (Capacity_Range (JJ)); 1323 1324 EI_Copy : constant Element_Type := EI; 1325 1326 begin 1327 EI := EJ; 1328 EJ := EI_Copy; 1329 end; 1330 end Swap; 1331 1332 -------------------- 1333 -- To_Array_Index -- 1334 -------------------- 1335 1336 function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base is 1337 Offset : Count_Type'Base; 1338 1339 begin 1340 -- We know that 1341 -- Index >= Index_Type'First 1342 -- hence we also know that 1343 -- Index - Index_Type'First >= 0 1344 1345 -- The issue is that even though 0 is guaranteed to be a value in 1346 -- the type Index_Type'Base, there's no guarantee that the difference 1347 -- is a value in that type. To prevent overflow we use the wider 1348 -- of Count_Type'Base and Index_Type'Base to perform intermediate 1349 -- calculations. 1350 1351 if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then 1352 Offset := Count_Type'Base (Index - Index_Type'First); 1353 1354 else 1355 Offset := 1356 Count_Type'Base (Index) - Count_Type'Base (Index_Type'First); 1357 end if; 1358 1359 -- The array index subtype for all container element arrays always 1360 -- starts with 1. 1361 1362 return 1 + Offset; 1363 end To_Array_Index; 1364 1365 --------------- 1366 -- To_Vector -- 1367 --------------- 1368 1369 function To_Vector 1370 (New_Item : Element_Type; 1371 Length : Capacity_Range) return Vector 1372 is 1373 begin 1374 if Length = 0 then 1375 return Empty_Vector; 1376 end if; 1377 1378 declare 1379 First : constant Int := Int (Index_Type'First); 1380 Last_As_Int : constant Int'Base := First + Int (Length) - 1; 1381 Last : Index_Type; 1382 1383 begin 1384 if Last_As_Int > Index_Type'Pos (Index_Type'Last) then 1385 raise Constraint_Error with "Length is out of range"; -- ??? 1386 end if; 1387 1388 Last := Index_Type (Last_As_Int); 1389 1390 return 1391 (Capacity => Length, 1392 Last => Last, 1393 Elements_Ptr => <>, 1394 Elements => (others => New_Item)); 1395 end; 1396 end To_Vector; 1397 1398end Ada.Containers.Formal_Vectors; 1399