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