comparison gcc/ada/libgnat/a-cfhama.adb @ 111:04ced10e8804

gcc 7
author kono
date Fri, 27 Oct 2017 22:46:09 +0900
parents
children 84e7813d76e9
comparison
equal deleted inserted replaced
68:561a7518be6b 111:04ced10e8804
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 ------------------------------------------------------------------------------
27
28 with Ada.Containers.Hash_Tables.Generic_Bounded_Operations;
29 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Operations);
30
31 with Ada.Containers.Hash_Tables.Generic_Bounded_Keys;
32 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys);
33
34 with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
35
36 with System; use type System.Address;
37
38 package body Ada.Containers.Formal_Hashed_Maps with
39 SPARK_Mode => Off
40 is
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
888 end Ada.Containers.Formal_Hashed_Maps;