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 _ H A S H E D _ M A P S -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2010-2021, 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.Hash_Tables.Generic_Bounded_Operations; 29pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Operations); 30 31with Ada.Containers.Hash_Tables.Generic_Bounded_Keys; 32pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys); 33 34with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers; 35 36with System; use type System.Address; 37 38package body Ada.Containers.Formal_Hashed_Maps with 39 SPARK_Mode => Off 40is 41 ----------------------- 42 -- Local Subprograms -- 43 ----------------------- 44 45 -- All local subprograms require comments ??? 46 47 function Equivalent_Keys 48 (Key : Key_Type; 49 Node : Node_Type) return Boolean; 50 pragma Inline (Equivalent_Keys); 51 52 procedure Free 53 (HT : in out Map; 54 X : Count_Type); 55 56 generic 57 with procedure Set_Element (Node : in out Node_Type); 58 procedure Generic_Allocate 59 (HT : in out Map; 60 Node : out Count_Type); 61 62 function Hash_Node (Node : Node_Type) return Hash_Type; 63 pragma Inline (Hash_Node); 64 65 function Next (Node : Node_Type) return Count_Type; 66 pragma Inline (Next); 67 68 procedure Set_Next (Node : in out Node_Type; Next : Count_Type); 69 pragma Inline (Set_Next); 70 71 function Vet (Container : Map; Position : Cursor) return Boolean; 72 73 -------------------------- 74 -- Local Instantiations -- 75 -------------------------- 76 77 package HT_Ops is 78 new Hash_Tables.Generic_Bounded_Operations 79 (HT_Types => HT_Types, 80 Hash_Node => Hash_Node, 81 Next => Next, 82 Set_Next => Set_Next); 83 84 package Key_Ops is 85 new Hash_Tables.Generic_Bounded_Keys 86 (HT_Types => HT_Types, 87 Next => Next, 88 Set_Next => Set_Next, 89 Key_Type => Key_Type, 90 Hash => Hash, 91 Equivalent_Keys => Equivalent_Keys); 92 93 --------- 94 -- "=" -- 95 --------- 96 97 function "=" (Left, Right : Map) return Boolean is 98 begin 99 if Length (Left) /= Length (Right) then 100 return False; 101 end if; 102 103 if Length (Left) = 0 then 104 return True; 105 end if; 106 107 declare 108 Node : Count_Type; 109 ENode : Count_Type; 110 111 begin 112 Node := First (Left).Node; 113 while Node /= 0 loop 114 ENode := 115 Find 116 (Container => Right, 117 Key => Left.Content.Nodes (Node).Key).Node; 118 119 if ENode = 0 or else 120 Right.Content.Nodes (ENode).Element /= 121 Left.Content.Nodes (Node).Element 122 then 123 return False; 124 end if; 125 126 Node := HT_Ops.Next (Left.Content, Node); 127 end loop; 128 129 return True; 130 end; 131 end "="; 132 133 ------------ 134 -- Assign -- 135 ------------ 136 137 procedure Assign (Target : in out Map; Source : Map) is 138 procedure Insert_Element (Source_Node : Count_Type); 139 pragma Inline (Insert_Element); 140 141 procedure Insert_Elements is 142 new HT_Ops.Generic_Iteration (Insert_Element); 143 144 -------------------- 145 -- Insert_Element -- 146 -------------------- 147 148 procedure Insert_Element (Source_Node : Count_Type) is 149 N : Node_Type renames Source.Content.Nodes (Source_Node); 150 begin 151 Insert (Target, N.Key, N.Element); 152 end Insert_Element; 153 154 -- Start of processing for Assign 155 156 begin 157 if Target'Address = Source'Address then 158 return; 159 end if; 160 161 if Target.Capacity < Length (Source) then 162 raise Constraint_Error with -- correct exception ??? 163 "Source length exceeds Target capacity"; 164 end if; 165 166 Clear (Target); 167 168 Insert_Elements (Source.Content); 169 end Assign; 170 171 -------------- 172 -- Capacity -- 173 -------------- 174 175 function Capacity (Container : Map) return Count_Type is 176 begin 177 return Container.Content.Nodes'Length; 178 end Capacity; 179 180 ----------- 181 -- Clear -- 182 ----------- 183 184 procedure Clear (Container : in out Map) is 185 begin 186 HT_Ops.Clear (Container.Content); 187 end Clear; 188 189 ------------------------ 190 -- Constant_Reference -- 191 ------------------------ 192 193 function Constant_Reference 194 (Container : aliased Map; 195 Position : Cursor) return not null access constant Element_Type 196 is 197 begin 198 if not Has_Element (Container, Position) then 199 raise Constraint_Error with "Position cursor has no element"; 200 end if; 201 202 pragma Assert 203 (Vet (Container, Position), 204 "bad cursor in function Constant_Reference"); 205 206 return Container.Content.Nodes (Position.Node).Element'Access; 207 end Constant_Reference; 208 209 function Constant_Reference 210 (Container : aliased Map; 211 Key : Key_Type) return not null access constant Element_Type 212 is 213 Node : constant Count_Type := Find (Container, Key).Node; 214 215 begin 216 if Node = 0 then 217 raise Constraint_Error with 218 "no element available because key not in map"; 219 end if; 220 221 return Container.Content.Nodes (Node).Element'Access; 222 end Constant_Reference; 223 224 -------------- 225 -- Contains -- 226 -------------- 227 228 function Contains (Container : Map; Key : Key_Type) return Boolean is 229 begin 230 return Find (Container, Key) /= No_Element; 231 end Contains; 232 233 ---------- 234 -- Copy -- 235 ---------- 236 237 function Copy 238 (Source : Map; 239 Capacity : Count_Type := 0) return Map 240 is 241 C : constant Count_Type := 242 Count_Type'Max (Capacity, Source.Capacity); 243 Cu : Cursor; 244 H : Hash_Type; 245 N : Count_Type; 246 Target : Map (C, Source.Modulus); 247 248 begin 249 if 0 < Capacity and then Capacity < Source.Capacity then 250 raise Capacity_Error; 251 end if; 252 253 Target.Content.Length := Source.Content.Length; 254 Target.Content.Free := Source.Content.Free; 255 256 H := 1; 257 while H <= Source.Modulus loop 258 Target.Content.Buckets (H) := Source.Content.Buckets (H); 259 H := H + 1; 260 end loop; 261 262 N := 1; 263 while N <= Source.Capacity loop 264 Target.Content.Nodes (N) := Source.Content.Nodes (N); 265 N := N + 1; 266 end loop; 267 268 while N <= C loop 269 Cu := (Node => N); 270 Free (Target, Cu.Node); 271 N := N + 1; 272 end loop; 273 274 return Target; 275 end Copy; 276 277 --------------------- 278 -- Default_Modulus -- 279 --------------------- 280 281 function Default_Modulus (Capacity : Count_Type) return Hash_Type is 282 begin 283 return To_Prime (Capacity); 284 end Default_Modulus; 285 286 ------------ 287 -- Delete -- 288 ------------ 289 290 procedure Delete (Container : in out Map; Key : Key_Type) is 291 X : Count_Type; 292 293 begin 294 Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X); 295 296 if X = 0 then 297 raise Constraint_Error with "attempt to delete key not in map"; 298 end if; 299 300 Free (Container, X); 301 end Delete; 302 303 procedure Delete (Container : in out Map; Position : in out Cursor) is 304 begin 305 if not Has_Element (Container, Position) then 306 raise Constraint_Error with 307 "Position cursor of Delete has no element"; 308 end if; 309 310 pragma Assert (Vet (Container, Position), "bad cursor in Delete"); 311 312 HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node); 313 314 Free (Container, Position.Node); 315 Position := No_Element; 316 end Delete; 317 318 ------------- 319 -- Element -- 320 ------------- 321 322 function Element (Container : Map; Key : Key_Type) return Element_Type is 323 Node : constant Count_Type := Find (Container, Key).Node; 324 325 begin 326 if Node = 0 then 327 raise Constraint_Error with 328 "no element available because key not in map"; 329 end if; 330 331 return Container.Content.Nodes (Node).Element; 332 end Element; 333 334 function Element (Container : Map; Position : Cursor) return Element_Type is 335 begin 336 if not Has_Element (Container, Position) then 337 raise Constraint_Error with "Position cursor equals No_Element"; 338 end if; 339 340 pragma Assert 341 (Vet (Container, Position), "bad cursor in function Element"); 342 343 return Container.Content.Nodes (Position.Node).Element; 344 end Element; 345 346 --------------------- 347 -- Equivalent_Keys -- 348 --------------------- 349 350 function Equivalent_Keys 351 (Key : Key_Type; 352 Node : Node_Type) return Boolean 353 is 354 begin 355 return Equivalent_Keys (Key, Node.Key); 356 end Equivalent_Keys; 357 358 ------------- 359 -- Exclude -- 360 ------------- 361 362 procedure Exclude (Container : in out Map; Key : Key_Type) is 363 X : Count_Type; 364 begin 365 Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X); 366 Free (Container, X); 367 end Exclude; 368 369 ---------- 370 -- Find -- 371 ---------- 372 373 function Find (Container : Map; Key : Key_Type) return Cursor is 374 Node : constant Count_Type := Key_Ops.Find (Container.Content, Key); 375 376 begin 377 if Node = 0 then 378 return No_Element; 379 end if; 380 381 return (Node => Node); 382 end Find; 383 384 ----------- 385 -- First -- 386 ----------- 387 388 function First (Container : Map) return Cursor is 389 Node : constant Count_Type := HT_Ops.First (Container.Content); 390 391 begin 392 if Node = 0 then 393 return No_Element; 394 end if; 395 396 return (Node => Node); 397 end First; 398 399 ------------------ 400 -- Formal_Model -- 401 ------------------ 402 403 package body Formal_Model is 404 405 ---------- 406 -- Find -- 407 ---------- 408 409 function Find 410 (Container : K.Sequence; 411 Key : Key_Type) return Count_Type 412 is 413 begin 414 for I in 1 .. K.Length (Container) loop 415 if Equivalent_Keys (Key, K.Get (Container, I)) then 416 return I; 417 end if; 418 end loop; 419 return 0; 420 end Find; 421 422 --------------------- 423 -- K_Keys_Included -- 424 --------------------- 425 426 function K_Keys_Included 427 (Left : K.Sequence; 428 Right : K.Sequence) return Boolean 429 is 430 begin 431 for I in 1 .. K.Length (Left) loop 432 if not K.Contains (Right, 1, K.Length (Right), K.Get (Left, I)) 433 then 434 return False; 435 end if; 436 end loop; 437 438 return True; 439 end K_Keys_Included; 440 441 ---------- 442 -- Keys -- 443 ---------- 444 445 function Keys (Container : Map) return K.Sequence is 446 Position : Count_Type := HT_Ops.First (Container.Content); 447 R : K.Sequence; 448 449 begin 450 -- Can't use First, Next or Element here, since they depend on models 451 -- for their postconditions. 452 453 while Position /= 0 loop 454 R := K.Add (R, Container.Content.Nodes (Position).Key); 455 Position := HT_Ops.Next (Container.Content, Position); 456 end loop; 457 458 return R; 459 end Keys; 460 461 ---------------------------- 462 -- Lift_Abstraction_Level -- 463 ---------------------------- 464 465 procedure Lift_Abstraction_Level (Container : Map) is null; 466 467 ----------------------- 468 -- Mapping_Preserved -- 469 ----------------------- 470 471 function Mapping_Preserved 472 (K_Left : K.Sequence; 473 K_Right : K.Sequence; 474 P_Left : P.Map; 475 P_Right : P.Map) return Boolean 476 is 477 begin 478 for C of P_Left loop 479 if not P.Has_Key (P_Right, C) 480 or else P.Get (P_Left, C) > K.Length (K_Left) 481 or else P.Get (P_Right, C) > K.Length (K_Right) 482 or else K.Get (K_Left, P.Get (P_Left, C)) /= 483 K.Get (K_Right, P.Get (P_Right, C)) 484 then 485 return False; 486 end if; 487 end loop; 488 489 return True; 490 end Mapping_Preserved; 491 492 ----------- 493 -- Model -- 494 ----------- 495 496 function Model (Container : Map) return M.Map is 497 Position : Count_Type := HT_Ops.First (Container.Content); 498 R : M.Map; 499 500 begin 501 -- Can't use First, Next or Element here, since they depend on models 502 -- for their postconditions. 503 504 while Position /= 0 loop 505 R := 506 M.Add 507 (Container => R, 508 New_Key => Container.Content.Nodes (Position).Key, 509 New_Item => Container.Content.Nodes (Position).Element); 510 511 Position := HT_Ops.Next (Container.Content, Position); 512 end loop; 513 514 return R; 515 end Model; 516 517 --------------- 518 -- Positions -- 519 --------------- 520 521 function Positions (Container : Map) return P.Map is 522 I : Count_Type := 1; 523 Position : Count_Type := HT_Ops.First (Container.Content); 524 R : P.Map; 525 526 begin 527 -- Can't use First, Next or Element here, since they depend on models 528 -- for their postconditions. 529 530 while Position /= 0 loop 531 R := P.Add (R, (Node => Position), I); 532 pragma Assert (P.Length (R) = I); 533 Position := HT_Ops.Next (Container.Content, Position); 534 I := I + 1; 535 end loop; 536 537 return R; 538 end Positions; 539 540 end Formal_Model; 541 542 ---------- 543 -- Free -- 544 ---------- 545 546 procedure Free (HT : in out Map; X : Count_Type) is 547 begin 548 if X /= 0 then 549 pragma Assert (X <= HT.Capacity); 550 HT.Content.Nodes (X).Has_Element := False; 551 HT_Ops.Free (HT.Content, X); 552 end if; 553 end Free; 554 555 ---------------------- 556 -- Generic_Allocate -- 557 ---------------------- 558 559 procedure Generic_Allocate (HT : in out Map; Node : out Count_Type) is 560 procedure Allocate is 561 new HT_Ops.Generic_Allocate (Set_Element); 562 563 begin 564 Allocate (HT.Content, Node); 565 HT.Content.Nodes (Node).Has_Element := True; 566 end Generic_Allocate; 567 568 ----------------- 569 -- Has_Element -- 570 ----------------- 571 572 function Has_Element (Container : Map; Position : Cursor) return Boolean is 573 begin 574 if Position.Node = 0 575 or else not Container.Content.Nodes (Position.Node).Has_Element 576 then 577 return False; 578 else 579 return True; 580 end if; 581 end Has_Element; 582 583 --------------- 584 -- Hash_Node -- 585 --------------- 586 587 function Hash_Node (Node : Node_Type) return Hash_Type is 588 begin 589 return Hash (Node.Key); 590 end Hash_Node; 591 592 ------------- 593 -- Include -- 594 ------------- 595 596 procedure Include 597 (Container : in out Map; 598 Key : Key_Type; 599 New_Item : Element_Type) 600 is 601 Position : Cursor; 602 Inserted : Boolean; 603 604 begin 605 Insert (Container, Key, New_Item, Position, Inserted); 606 607 if not Inserted then 608 declare 609 N : Node_Type renames Container.Content.Nodes (Position.Node); 610 begin 611 N.Key := Key; 612 N.Element := New_Item; 613 end; 614 end if; 615 end Include; 616 617 ------------ 618 -- Insert -- 619 ------------ 620 621 procedure Insert 622 (Container : in out Map; 623 Key : Key_Type; 624 New_Item : Element_Type; 625 Position : out Cursor; 626 Inserted : out Boolean) 627 is 628 procedure Assign_Key (Node : in out Node_Type); 629 pragma Inline (Assign_Key); 630 631 function New_Node return Count_Type; 632 pragma Inline (New_Node); 633 634 procedure Local_Insert is 635 new Key_Ops.Generic_Conditional_Insert (New_Node); 636 637 procedure Allocate is 638 new Generic_Allocate (Assign_Key); 639 640 ----------------- 641 -- Assign_Key -- 642 ----------------- 643 644 procedure Assign_Key (Node : in out Node_Type) is 645 begin 646 Node.Key := Key; 647 Node.Element := New_Item; 648 end Assign_Key; 649 650 -------------- 651 -- New_Node -- 652 -------------- 653 654 function New_Node return Count_Type is 655 Result : Count_Type; 656 begin 657 Allocate (Container, Result); 658 return Result; 659 end New_Node; 660 661 -- Start of processing for Insert 662 663 begin 664 Local_Insert (Container.Content, Key, Position.Node, Inserted); 665 end Insert; 666 667 procedure Insert 668 (Container : in out Map; 669 Key : Key_Type; 670 New_Item : Element_Type) 671 is 672 Position : Cursor; 673 pragma Unreferenced (Position); 674 675 Inserted : Boolean; 676 677 begin 678 Insert (Container, Key, New_Item, Position, Inserted); 679 680 if not Inserted then 681 raise Constraint_Error with "attempt to insert key already in map"; 682 end if; 683 end Insert; 684 685 -------------- 686 -- Is_Empty -- 687 -------------- 688 689 function Is_Empty (Container : Map) return Boolean is 690 begin 691 return Length (Container) = 0; 692 end Is_Empty; 693 694 --------- 695 -- Key -- 696 --------- 697 698 function Key (Container : Map; Position : Cursor) return Key_Type is 699 begin 700 if not Has_Element (Container, Position) then 701 raise Constraint_Error with 702 "Position cursor of function Key has no element"; 703 end if; 704 705 pragma Assert (Vet (Container, Position), "bad cursor in function Key"); 706 707 return Container.Content.Nodes (Position.Node).Key; 708 end Key; 709 710 ------------ 711 -- Length -- 712 ------------ 713 714 function Length (Container : Map) return Count_Type is 715 begin 716 return Container.Content.Length; 717 end Length; 718 719 ---------- 720 -- Move -- 721 ---------- 722 723 procedure Move 724 (Target : in out Map; 725 Source : in out Map) 726 is 727 NN : HT_Types.Nodes_Type renames Source.Content.Nodes; 728 X : Count_Type; 729 Y : Count_Type; 730 731 begin 732 if Target'Address = Source'Address then 733 return; 734 end if; 735 736 if Target.Capacity < Length (Source) then 737 raise Constraint_Error with -- ??? 738 "Source length exceeds Target capacity"; 739 end if; 740 741 Clear (Target); 742 743 if Source.Content.Length = 0 then 744 return; 745 end if; 746 747 X := HT_Ops.First (Source.Content); 748 while X /= 0 loop 749 Insert (Target, NN (X).Key, NN (X).Element); -- optimize??? 750 751 Y := HT_Ops.Next (Source.Content, X); 752 753 HT_Ops.Delete_Node_Sans_Free (Source.Content, X); 754 Free (Source, X); 755 756 X := Y; 757 end loop; 758 end Move; 759 760 ---------- 761 -- Next -- 762 ---------- 763 764 function Next (Node : Node_Type) return Count_Type is 765 begin 766 return Node.Next; 767 end Next; 768 769 function Next (Container : Map; Position : Cursor) return Cursor is 770 begin 771 if Position.Node = 0 then 772 return No_Element; 773 end if; 774 775 if not Has_Element (Container, Position) then 776 raise Constraint_Error with "Position has no element"; 777 end if; 778 779 pragma Assert (Vet (Container, Position), "bad cursor in function Next"); 780 781 declare 782 Node : constant Count_Type := 783 HT_Ops.Next (Container.Content, Position.Node); 784 785 begin 786 if Node = 0 then 787 return No_Element; 788 end if; 789 790 return (Node => Node); 791 end; 792 end Next; 793 794 procedure Next (Container : Map; Position : in out Cursor) is 795 begin 796 Position := Next (Container, Position); 797 end Next; 798 799 --------------- 800 -- Reference -- 801 --------------- 802 803 function Reference 804 (Container : not null access Map; 805 Position : Cursor) return not null access Element_Type 806 is 807 begin 808 if not Has_Element (Container.all, Position) then 809 raise Constraint_Error with "Position cursor has no element"; 810 end if; 811 812 pragma Assert 813 (Vet (Container.all, Position), "bad cursor in function Reference"); 814 815 return Container.Content.Nodes (Position.Node).Element'Access; 816 end Reference; 817 818 function Reference 819 (Container : not null access Map; 820 Key : Key_Type) return not null access Element_Type 821 is 822 Node : constant Count_Type := Find (Container.all, Key).Node; 823 824 begin 825 if Node = 0 then 826 raise Constraint_Error with 827 "no element available because key not in map"; 828 end if; 829 830 return Container.Content.Nodes (Node).Element'Access; 831 end Reference; 832 833 ------------- 834 -- Replace -- 835 ------------- 836 837 procedure Replace 838 (Container : in out Map; 839 Key : Key_Type; 840 New_Item : Element_Type) 841 is 842 Node : constant Count_Type := Key_Ops.Find (Container.Content, Key); 843 844 begin 845 if Node = 0 then 846 raise Constraint_Error with "attempt to replace key not in map"; 847 end if; 848 849 declare 850 N : Node_Type renames Container.Content.Nodes (Node); 851 begin 852 N.Key := Key; 853 N.Element := New_Item; 854 end; 855 end Replace; 856 857 --------------------- 858 -- Replace_Element -- 859 --------------------- 860 861 procedure Replace_Element 862 (Container : in out Map; 863 Position : Cursor; 864 New_Item : Element_Type) 865 is 866 begin 867 if not Has_Element (Container, Position) then 868 raise Constraint_Error with 869 "Position cursor of Replace_Element has no element"; 870 end if; 871 872 pragma Assert 873 (Vet (Container, Position), "bad cursor in Replace_Element"); 874 875 Container.Content.Nodes (Position.Node).Element := New_Item; 876 end Replace_Element; 877 878 ---------------------- 879 -- Reserve_Capacity -- 880 ---------------------- 881 882 procedure Reserve_Capacity 883 (Container : in out Map; 884 Capacity : Count_Type) 885 is 886 begin 887 if Capacity > Container.Capacity then 888 raise Capacity_Error with "requested capacity is too large"; 889 end if; 890 end Reserve_Capacity; 891 892 -------------- 893 -- Set_Next -- 894 -------------- 895 896 procedure Set_Next (Node : in out Node_Type; Next : Count_Type) is 897 begin 898 Node.Next := Next; 899 end Set_Next; 900 901 --------- 902 -- Vet -- 903 --------- 904 905 function Vet (Container : Map; Position : Cursor) return Boolean is 906 begin 907 if Position.Node = 0 then 908 return True; 909 end if; 910 911 declare 912 X : Count_Type; 913 914 begin 915 if Container.Content.Length = 0 then 916 return False; 917 end if; 918 919 if Container.Capacity = 0 then 920 return False; 921 end if; 922 923 if Container.Content.Buckets'Length = 0 then 924 return False; 925 end if; 926 927 if Position.Node > Container.Capacity then 928 return False; 929 end if; 930 931 if Container.Content.Nodes (Position.Node).Next = Position.Node then 932 return False; 933 end if; 934 935 X := 936 Container.Content.Buckets 937 (Key_Ops.Index 938 (Container.Content, 939 Container.Content.Nodes (Position.Node).Key)); 940 941 for J in 1 .. Container.Content.Length loop 942 if X = Position.Node then 943 return True; 944 end if; 945 946 if X = 0 then 947 return False; 948 end if; 949 950 if X = Container.Content.Nodes (X).Next then 951 952 -- Prevent unnecessary looping 953 954 return False; 955 end if; 956 957 X := Container.Content.Nodes (X).Next; 958 end loop; 959 960 return False; 961 end; 962 end Vet; 963 964end Ada.Containers.Formal_Hashed_Maps; 965