Daily bump.
[official-gcc.git] / gcc / ada / a-cfhama.adb
blobbf782c6c8df698572191aa194ca2fc8297f9d986
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-2017, 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 ------------------------------------------------------------------------------
28 with Ada.Containers.Hash_Tables.Generic_Bounded_Operations;
29 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Operations);
31 with Ada.Containers.Hash_Tables.Generic_Bounded_Keys;
32 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys);
34 with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
36 with System; use type System.Address;
38 package body Ada.Containers.Formal_Hashed_Maps with
39 SPARK_Mode => Off
41 -----------------------
42 -- Local Subprograms --
43 -----------------------
45 -- All local subprograms require comments ???
47 function Equivalent_Keys
48 (Key : Key_Type;
49 Node : Node_Type) return Boolean;
50 pragma Inline (Equivalent_Keys);
52 procedure Free
53 (HT : in out Map;
54 X : Count_Type);
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);
62 function Hash_Node (Node : Node_Type) return Hash_Type;
63 pragma Inline (Hash_Node);
65 function Next (Node : Node_Type) return Count_Type;
66 pragma Inline (Next);
68 procedure Set_Next (Node : in out Node_Type; Next : Count_Type);
69 pragma Inline (Set_Next);
71 function Vet (Container : Map; Position : Cursor) return Boolean;
73 --------------------------
74 -- Local Instantiations --
75 --------------------------
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);
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);
93 ---------
94 -- "=" --
95 ---------
97 function "=" (Left, Right : Map) return Boolean is
98 begin
99 if Length (Left) /= Length (Right) then
100 return False;
101 end if;
103 if Length (Left) = 0 then
104 return True;
105 end if;
107 declare
108 Node : Count_Type;
109 ENode : Count_Type;
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;
119 if ENode = 0 or else
120 Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
121 then
122 return False;
123 end if;
125 Node := HT_Ops.Next (Left, Node);
126 end loop;
128 return True;
129 end;
130 end "=";
132 ------------
133 -- Assign --
134 ------------
136 procedure Assign (Target : in out Map; Source : Map) is
137 procedure Insert_Element (Source_Node : Count_Type);
138 pragma Inline (Insert_Element);
140 procedure Insert_Elements is
141 new HT_Ops.Generic_Iteration (Insert_Element);
143 --------------------
144 -- Insert_Element --
145 --------------------
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;
153 -- Start of processing for Assign
155 begin
156 if Target'Address = Source'Address then
157 return;
158 end if;
160 if Target.Capacity < Length (Source) then
161 raise Constraint_Error with -- correct exception ???
162 "Source length exceeds Target capacity";
163 end if;
165 Clear (Target);
167 Insert_Elements (Source);
168 end Assign;
170 --------------
171 -- Capacity --
172 --------------
174 function Capacity (Container : Map) return Count_Type is
175 begin
176 return Container.Nodes'Length;
177 end Capacity;
179 -----------
180 -- Clear --
181 -----------
183 procedure Clear (Container : in out Map) is
184 begin
185 HT_Ops.Clear (Container);
186 end Clear;
188 --------------
189 -- Contains --
190 --------------
192 function Contains (Container : Map; Key : Key_Type) return Boolean is
193 begin
194 return Find (Container, Key) /= No_Element;
195 end Contains;
197 ----------
198 -- Copy --
199 ----------
201 function Copy
202 (Source : Map;
203 Capacity : Count_Type := 0) return Map
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);
212 begin
213 if 0 < Capacity and then Capacity < Source.Capacity then
214 raise Capacity_Error;
215 end if;
217 Target.Length := Source.Length;
218 Target.Free := Source.Free;
220 H := 1;
221 while H <= Source.Modulus loop
222 Target.Buckets (H) := Source.Buckets (H);
223 H := H + 1;
224 end loop;
226 N := 1;
227 while N <= Source.Capacity loop
228 Target.Nodes (N) := Source.Nodes (N);
229 N := N + 1;
230 end loop;
232 while N <= C loop
233 Cu := (Node => N);
234 Free (Target, Cu.Node);
235 N := N + 1;
236 end loop;
238 return Target;
239 end Copy;
241 ---------------------
242 -- Default_Modulus --
243 ---------------------
245 function Default_Modulus (Capacity : Count_Type) return Hash_Type is
246 begin
247 return To_Prime (Capacity);
248 end Default_Modulus;
250 ------------
251 -- Delete --
252 ------------
254 procedure Delete (Container : in out Map; Key : Key_Type) is
255 X : Count_Type;
257 begin
258 Key_Ops.Delete_Key_Sans_Free (Container, Key, X);
260 if X = 0 then
261 raise Constraint_Error with "attempt to delete key not in map";
262 end if;
264 Free (Container, X);
265 end Delete;
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;
274 pragma Assert (Vet (Container, Position), "bad cursor in Delete");
276 HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
278 Free (Container, Position.Node);
279 Position := No_Element;
280 end Delete;
282 -------------
283 -- Element --
284 -------------
286 function Element (Container : Map; Key : Key_Type) return Element_Type is
287 Node : constant Count_Type := Find (Container, Key).Node;
289 begin
290 if Node = 0 then
291 raise Constraint_Error with
292 "no element available because key not in map";
293 end if;
295 return Container.Nodes (Node).Element;
296 end Element;
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;
304 pragma Assert
305 (Vet (Container, Position), "bad cursor in function Element");
307 return Container.Nodes (Position.Node).Element;
308 end Element;
310 ---------------------
311 -- Equivalent_Keys --
312 ---------------------
314 function Equivalent_Keys
315 (Key : Key_Type;
316 Node : Node_Type) return Boolean
318 begin
319 return Equivalent_Keys (Key, Node.Key);
320 end Equivalent_Keys;
322 -------------
323 -- Exclude --
324 -------------
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;
333 ----------
334 -- Find --
335 ----------
337 function Find (Container : Map; Key : Key_Type) return Cursor is
338 Node : constant Count_Type := Key_Ops.Find (Container, Key);
340 begin
341 if Node = 0 then
342 return No_Element;
343 end if;
345 return (Node => Node);
346 end Find;
348 -----------
349 -- First --
350 -----------
352 function First (Container : Map) return Cursor is
353 Node : constant Count_Type := HT_Ops.First (Container);
355 begin
356 if Node = 0 then
357 return No_Element;
358 end if;
360 return (Node => Node);
361 end First;
363 ------------------
364 -- Formal_Model --
365 ------------------
367 package body Formal_Model is
369 ----------
370 -- Find --
371 ----------
373 function Find
374 (Container : K.Sequence;
375 Key : Key_Type) return Count_Type
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;
386 ---------------------
387 -- K_Keys_Included --
388 ---------------------
390 function K_Keys_Included
391 (Left : K.Sequence;
392 Right : K.Sequence) return Boolean
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;
402 return True;
403 end K_Keys_Included;
405 ----------
406 -- Keys --
407 ----------
409 function Keys (Container : Map) return K.Sequence is
410 Position : Count_Type := HT_Ops.First (Container);
411 R : K.Sequence;
413 begin
414 -- Can't use First, Next or Element here, since they depend on models
415 -- for their postconditions.
417 while Position /= 0 loop
418 R := K.Add (R, Container.Nodes (Position).Key);
419 Position := HT_Ops.Next (Container, Position);
420 end loop;
422 return R;
423 end Keys;
425 ----------------------------
426 -- Lift_Abstraction_Level --
427 ----------------------------
429 procedure Lift_Abstraction_Level (Container : Map) is null;
431 -----------------------
432 -- Mapping_preserved --
433 -----------------------
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
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;
453 return True;
454 end Mapping_Preserved;
456 -----------
457 -- Model --
458 -----------
460 function Model (Container : Map) return M.Map is
461 Position : Count_Type := HT_Ops.First (Container);
462 R : M.Map;
464 begin
465 -- Can't use First, Next or Element here, since they depend on models
466 -- for their postconditions.
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);
475 Position := HT_Ops.Next (Container, Position);
476 end loop;
478 return R;
479 end Model;
481 ---------------
482 -- Positions --
483 ---------------
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;
490 begin
491 -- Can't use First, Next or Element here, since they depend on models
492 -- for their postconditions.
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;
501 return R;
502 end Positions;
504 end Formal_Model;
506 ----------
507 -- Free --
508 ----------
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;
516 ----------------------
517 -- Generic_Allocate --
518 ----------------------
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);
524 begin
525 Allocate (HT, Node);
526 HT.Nodes (Node).Has_Element := True;
527 end Generic_Allocate;
529 -----------------
530 -- Has_Element --
531 -----------------
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;
544 ---------------
545 -- Hash_Node --
546 ---------------
548 function Hash_Node (Node : Node_Type) return Hash_Type is
549 begin
550 return Hash (Node.Key);
551 end Hash_Node;
553 -------------
554 -- Include --
555 -------------
557 procedure Include
558 (Container : in out Map;
559 Key : Key_Type;
560 New_Item : Element_Type)
562 Position : Cursor;
563 Inserted : Boolean;
565 begin
566 Insert (Container, Key, New_Item, Position, Inserted);
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;
578 ------------
579 -- Insert --
580 ------------
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)
589 procedure Assign_Key (Node : in out Node_Type);
590 pragma Inline (Assign_Key);
592 function New_Node return Count_Type;
593 pragma Inline (New_Node);
595 procedure Local_Insert is
596 new Key_Ops.Generic_Conditional_Insert (New_Node);
598 procedure Allocate is
599 new Generic_Allocate (Assign_Key);
601 -----------------
602 -- Assign_Key --
603 -----------------
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;
611 --------------
612 -- New_Node --
613 --------------
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;
622 -- Start of processing for Insert
624 begin
625 Local_Insert (Container, Key, Position.Node, Inserted);
626 end Insert;
628 procedure Insert
629 (Container : in out Map;
630 Key : Key_Type;
631 New_Item : Element_Type)
633 Position : Cursor;
634 pragma Unreferenced (Position);
636 Inserted : Boolean;
638 begin
639 Insert (Container, Key, New_Item, Position, Inserted);
641 if not Inserted then
642 raise Constraint_Error with "attempt to insert key already in map";
643 end if;
644 end Insert;
646 --------------
647 -- Is_Empty --
648 --------------
650 function Is_Empty (Container : Map) return Boolean is
651 begin
652 return Length (Container) = 0;
653 end Is_Empty;
655 ---------
656 -- Key --
657 ---------
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;
666 pragma Assert (Vet (Container, Position), "bad cursor in function Key");
668 return Container.Nodes (Position.Node).Key;
669 end Key;
671 ------------
672 -- Length --
673 ------------
675 function Length (Container : Map) return Count_Type is
676 begin
677 return Container.Length;
678 end Length;
680 ----------
681 -- Move --
682 ----------
684 procedure Move
685 (Target : in out Map;
686 Source : in out Map)
688 NN : HT_Types.Nodes_Type renames Source.Nodes;
689 X : Count_Type;
690 Y : Count_Type;
692 begin
693 if Target'Address = Source'Address then
694 return;
695 end if;
697 if Target.Capacity < Length (Source) then
698 raise Constraint_Error with -- ???
699 "Source length exceeds Target capacity";
700 end if;
702 Clear (Target);
704 if Source.Length = 0 then
705 return;
706 end if;
708 X := HT_Ops.First (Source);
709 while X /= 0 loop
710 Insert (Target, NN (X).Key, NN (X).Element); -- optimize???
712 Y := HT_Ops.Next (Source, X);
714 HT_Ops.Delete_Node_Sans_Free (Source, X);
715 Free (Source, X);
717 X := Y;
718 end loop;
719 end Move;
721 ----------
722 -- Next --
723 ----------
725 function Next (Node : Node_Type) return Count_Type is
726 begin
727 return Node.Next;
728 end Next;
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;
736 if not Has_Element (Container, Position) then
737 raise Constraint_Error with "Position has no element";
738 end if;
740 pragma Assert (Vet (Container, Position), "bad cursor in function Next");
742 declare
743 Node : constant Count_Type := HT_Ops.Next (Container, Position.Node);
745 begin
746 if Node = 0 then
747 return No_Element;
748 end if;
750 return (Node => Node);
751 end;
752 end Next;
754 procedure Next (Container : Map; Position : in out Cursor) is
755 begin
756 Position := Next (Container, Position);
757 end Next;
759 -------------
760 -- Replace --
761 -------------
763 procedure Replace
764 (Container : in out Map;
765 Key : Key_Type;
766 New_Item : Element_Type)
768 Node : constant Count_Type := Key_Ops.Find (Container, Key);
770 begin
771 if Node = 0 then
772 raise Constraint_Error with "attempt to replace key not in map";
773 end if;
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;
783 ---------------------
784 -- Replace_Element --
785 ---------------------
787 procedure Replace_Element
788 (Container : in out Map;
789 Position : Cursor;
790 New_Item : Element_Type)
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;
798 pragma Assert
799 (Vet (Container, Position), "bad cursor in Replace_Element");
801 Container.Nodes (Position.Node).Element := New_Item;
802 end Replace_Element;
804 ----------------------
805 -- Reserve_Capacity --
806 ----------------------
808 procedure Reserve_Capacity
809 (Container : in out Map;
810 Capacity : Count_Type)
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;
818 --------------
819 -- Set_Next --
820 --------------
822 procedure Set_Next (Node : in out Node_Type; Next : Count_Type) is
823 begin
824 Node.Next := Next;
825 end Set_Next;
827 ---------
828 -- Vet --
829 ---------
831 function Vet (Container : Map; Position : Cursor) return Boolean is
832 begin
833 if Position.Node = 0 then
834 return True;
835 end if;
837 declare
838 X : Count_Type;
840 begin
841 if Container.Length = 0 then
842 return False;
843 end if;
845 if Container.Capacity = 0 then
846 return False;
847 end if;
849 if Container.Buckets'Length = 0 then
850 return False;
851 end if;
853 if Position.Node > Container.Capacity then
854 return False;
855 end if;
857 if Container.Nodes (Position.Node).Next = Position.Node then
858 return False;
859 end if;
861 X :=
862 Container.Buckets
863 (Key_Ops.Index (Container, Container.Nodes (Position.Node).Key));
865 for J in 1 .. Container.Length loop
866 if X = Position.Node then
867 return True;
868 end if;
870 if X = 0 then
871 return False;
872 end if;
874 if X = Container.Nodes (X).Next then
876 -- Prevent unnecessary looping
878 return False;
879 end if;
881 X := Container.Nodes (X).Next;
882 end loop;
884 return False;
885 end;
886 end Vet;
888 end Ada.Containers.Formal_Hashed_Maps;