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