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