1 ------------------------------------------------------------------------------
3 -- GNAT LIBRARY COMPONENTS --
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 --
9 -- Copyright (C) 2010-2017, Free Software Foundation, Inc. --
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. --
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. --
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
41 -----------------------
42 -- Local Subprograms --
43 -----------------------
45 -- All local subprograms require comments ???
47 function Equivalent_Keys
49 Node
: Node_Type
) return Boolean;
50 pragma Inline
(Equivalent_Keys
);
57 with procedure Set_Element
(Node
: in out Node_Type
);
58 procedure Generic_Allocate
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
;
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 --------------------------
78 new Hash_Tables
.Generic_Bounded_Operations
79 (HT_Types
=> HT_Types
,
80 Hash_Node
=> Hash_Node
,
82 Set_Next
=> Set_Next
);
85 new Hash_Tables
.Generic_Bounded_Keys
86 (HT_Types
=> HT_Types
,
91 Equivalent_Keys
=> Equivalent_Keys
);
97 function "=" (Left
, Right
: Map
) return Boolean is
99 if Length
(Left
) /= Length
(Right
) then
103 if Length
(Left
) = 0 then
112 Node
:= Left
.First
.Node
;
117 Key
=> Left
.Nodes
(Node
).Key
).Node
;
120 Right
.Nodes
(ENode
).Element
/= Left
.Nodes
(Node
).Element
125 Node
:= HT_Ops
.Next
(Left
, Node
);
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
);
147 procedure Insert_Element
(Source_Node
: Count_Type
) is
148 N
: Node_Type
renames Source
.Nodes
(Source_Node
);
150 Insert
(Target
, N
.Key
, N
.Element
);
153 -- Start of processing for Assign
156 if Target
'Address = Source
'Address then
160 if Target
.Capacity
< Length
(Source
) then
161 raise Constraint_Error
with -- correct exception ???
162 "Source length exceeds Target capacity";
167 Insert_Elements
(Source
);
174 function Capacity
(Container
: Map
) return Count_Type
is
176 return Container
.Nodes
'Length;
183 procedure Clear
(Container
: in out Map
) is
185 HT_Ops
.Clear
(Container
);
192 function Contains
(Container
: Map
; Key
: Key_Type
) return Boolean is
194 return Find
(Container
, Key
) /= No_Element
;
203 Capacity
: Count_Type
:= 0) return Map
205 C
: constant Count_Type
:=
206 Count_Type
'Max (Capacity
, Source
.Capacity
);
210 Target
: Map
(C
, Source
.Modulus
);
213 if 0 < Capacity
and then Capacity
< Source
.Capacity
then
214 raise Capacity_Error
;
217 Target
.Length
:= Source
.Length
;
218 Target
.Free
:= Source
.Free
;
221 while H
<= Source
.Modulus
loop
222 Target
.Buckets
(H
) := Source
.Buckets
(H
);
227 while N
<= Source
.Capacity
loop
228 Target
.Nodes
(N
) := Source
.Nodes
(N
);
234 Free
(Target
, Cu
.Node
);
241 ---------------------
242 -- Default_Modulus --
243 ---------------------
245 function Default_Modulus
(Capacity
: Count_Type
) return Hash_Type
is
247 return To_Prime
(Capacity
);
254 procedure Delete
(Container
: in out Map
; Key
: Key_Type
) is
258 Key_Ops
.Delete_Key_Sans_Free
(Container
, Key
, X
);
261 raise Constraint_Error
with "attempt to delete key not in map";
267 procedure Delete
(Container
: in out Map
; Position
: in out Cursor
) is
269 if not Has_Element
(Container
, Position
) then
270 raise Constraint_Error
with
271 "Position cursor of Delete has no element";
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
;
286 function Element
(Container
: Map
; Key
: Key_Type
) return Element_Type
is
287 Node
: constant Count_Type
:= Find
(Container
, Key
).Node
;
291 raise Constraint_Error
with
292 "no element available because key not in map";
295 return Container
.Nodes
(Node
).Element
;
298 function Element
(Container
: Map
; Position
: Cursor
) return Element_Type
is
300 if not Has_Element
(Container
, Position
) then
301 raise Constraint_Error
with "Position cursor equals No_Element";
305 (Vet
(Container
, Position
), "bad cursor in function Element");
307 return Container
.Nodes
(Position
.Node
).Element
;
310 ---------------------
311 -- Equivalent_Keys --
312 ---------------------
314 function Equivalent_Keys
316 Node
: Node_Type
) return Boolean
319 return Equivalent_Keys
(Key
, Node
.Key
);
326 procedure Exclude
(Container
: in out Map
; Key
: Key_Type
) is
329 Key_Ops
.Delete_Key_Sans_Free
(Container
, Key
, X
);
337 function Find
(Container
: Map
; Key
: Key_Type
) return Cursor
is
338 Node
: constant Count_Type
:= Key_Ops
.Find
(Container
, Key
);
345 return (Node
=> Node
);
352 function First
(Container
: Map
) return Cursor
is
353 Node
: constant Count_Type
:= HT_Ops
.First
(Container
);
360 return (Node
=> Node
);
367 package body Formal_Model
is
374 (Container
: K
.Sequence
;
375 Key
: Key_Type
) return Count_Type
378 for I
in 1 .. K
.Length
(Container
) loop
379 if Equivalent_Keys
(Key
, K
.Get
(Container
, I
)) then
386 ---------------------
387 -- K_Keys_Included --
388 ---------------------
390 function K_Keys_Included
392 Right
: K
.Sequence
) return Boolean
395 for I
in 1 .. K
.Length
(Left
) loop
396 if not K
.Contains
(Right
, 1, K
.Length
(Right
), K
.Get
(Left
, I
))
409 function Keys
(Container
: Map
) return K
.Sequence
is
410 Position
: Count_Type
:= HT_Ops
.First
(Container
);
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
);
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
;
439 P_Right
: P
.Map
) return Boolean
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
))
454 end Mapping_Preserved
;
460 function Model
(Container
: Map
) return M
.Map
is
461 Position
: Count_Type
:= HT_Ops
.First
(Container
);
465 -- Can't use First, Next or Element here, since they depend on models
466 -- for their postconditions.
468 while Position
/= 0 loop
472 New_Key
=> Container
.Nodes
(Position
).Key
,
473 New_Item
=> Container
.Nodes
(Position
).Element
);
475 Position
:= HT_Ops
.Next
(Container
, Position
);
485 function Positions
(Container
: Map
) return P
.Map
is
487 Position
: Count_Type
:= HT_Ops
.First
(Container
);
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
);
510 procedure Free
(HT
: in out Map
; X
: Count_Type
) is
512 HT
.Nodes
(X
).Has_Element
:= False;
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
);
526 HT
.Nodes
(Node
).Has_Element
:= True;
527 end Generic_Allocate
;
533 function Has_Element
(Container
: Map
; Position
: Cursor
) return Boolean is
536 or else not Container
.Nodes
(Position
.Node
).Has_Element
548 function Hash_Node
(Node
: Node_Type
) return Hash_Type
is
550 return Hash
(Node
.Key
);
558 (Container
: in out Map
;
560 New_Item
: Element_Type
)
566 Insert
(Container
, Key
, New_Item
, Position
, Inserted
);
570 N
: Node_Type
renames Container
.Nodes
(Position
.Node
);
573 N
.Element
:= New_Item
;
583 (Container
: in out Map
;
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
);
605 procedure Assign_Key
(Node
: in out Node_Type
) is
608 Node
.Element
:= New_Item
;
615 function New_Node
return Count_Type
is
618 Allocate
(Container
, Result
);
622 -- Start of processing for Insert
625 Local_Insert
(Container
, Key
, Position
.Node
, Inserted
);
629 (Container
: in out Map
;
631 New_Item
: Element_Type
)
634 pragma Unreferenced
(Position
);
639 Insert
(Container
, Key
, New_Item
, Position
, Inserted
);
642 raise Constraint_Error
with "attempt to insert key already in map";
650 function Is_Empty
(Container
: Map
) return Boolean is
652 return Length
(Container
) = 0;
659 function Key
(Container
: Map
; Position
: Cursor
) return Key_Type
is
661 if not Has_Element
(Container
, Position
) then
662 raise Constraint_Error
with
663 "Position cursor of function Key has no element";
666 pragma Assert
(Vet
(Container
, Position
), "bad cursor in function Key");
668 return Container
.Nodes
(Position
.Node
).Key
;
675 function Length
(Container
: Map
) return Count_Type
is
677 return Container
.Length
;
685 (Target
: in out Map
;
688 NN
: HT_Types
.Nodes_Type
renames Source
.Nodes
;
693 if Target
'Address = Source
'Address then
697 if Target
.Capacity
< Length
(Source
) then
698 raise Constraint_Error
with -- ???
699 "Source length exceeds Target capacity";
704 if Source
.Length
= 0 then
708 X
:= HT_Ops
.First
(Source
);
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
);
725 function Next
(Node
: Node_Type
) return Count_Type
is
730 function Next
(Container
: Map
; Position
: Cursor
) return Cursor
is
732 if Position
.Node
= 0 then
736 if not Has_Element
(Container
, Position
) then
737 raise Constraint_Error
with "Position has no element";
740 pragma Assert
(Vet
(Container
, Position
), "bad cursor in function Next");
743 Node
: constant Count_Type
:= HT_Ops
.Next
(Container
, Position
.Node
);
750 return (Node
=> Node
);
754 procedure Next
(Container
: Map
; Position
: in out Cursor
) is
756 Position
:= Next
(Container
, Position
);
764 (Container
: in out Map
;
766 New_Item
: Element_Type
)
768 Node
: constant Count_Type
:= Key_Ops
.Find
(Container
, Key
);
772 raise Constraint_Error
with "attempt to replace key not in map";
776 N
: Node_Type
renames Container
.Nodes
(Node
);
779 N
.Element
:= New_Item
;
783 ---------------------
784 -- Replace_Element --
785 ---------------------
787 procedure Replace_Element
788 (Container
: in out Map
;
790 New_Item
: Element_Type
)
793 if not Has_Element
(Container
, Position
) then
794 raise Constraint_Error
with
795 "Position cursor of Replace_Element has no element";
799 (Vet
(Container
, Position
), "bad cursor in Replace_Element");
801 Container
.Nodes
(Position
.Node
).Element
:= New_Item
;
804 ----------------------
805 -- Reserve_Capacity --
806 ----------------------
808 procedure Reserve_Capacity
809 (Container
: in out Map
;
810 Capacity
: Count_Type
)
813 if Capacity
> Container
.Capacity
then
814 raise Capacity_Error
with "requested capacity is too large";
816 end Reserve_Capacity
;
822 procedure Set_Next
(Node
: in out Node_Type
; Next
: Count_Type
) is
831 function Vet
(Container
: Map
; Position
: Cursor
) return Boolean is
833 if Position
.Node
= 0 then
841 if Container
.Length
= 0 then
845 if Container
.Capacity
= 0 then
849 if Container
.Buckets
'Length = 0 then
853 if Position
.Node
> Container
.Capacity
then
857 if Container
.Nodes
(Position
.Node
).Next
= Position
.Node
then
863 (Key_Ops
.Index
(Container
, Container
.Nodes
(Position
.Node
).Key
));
865 for J
in 1 .. Container
.Length
loop
866 if X
= Position
.Node
then
874 if X
= Container
.Nodes
(X
).Next
then
876 -- Prevent unnecessary looping
881 X
:= Container
.Nodes
(X
).Next
;
888 end Ada
.Containers
.Formal_Hashed_Maps
;