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 _ O R D E R 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
.Red_Black_Trees
.Generic_Bounded_Operations
;
30 (Ada
.Containers
.Red_Black_Trees
.Generic_Bounded_Operations
);
32 with Ada
.Containers
.Red_Black_Trees
.Generic_Bounded_Keys
;
33 pragma Elaborate_All
(Ada
.Containers
.Red_Black_Trees
.Generic_Bounded_Keys
);
35 with System
; use type System
.Address
;
37 package body Ada
.Containers
.Formal_Ordered_Maps
with
41 -----------------------------
42 -- Node Access Subprograms --
43 -----------------------------
45 -- These subprograms provide a functional interface to access fields
46 -- of a node, and a procedural interface for modifying these values.
49 (Node
: Node_Type
) return Ada
.Containers
.Red_Black_Trees
.Color_Type
;
50 pragma Inline
(Color
);
52 function Left_Son
(Node
: Node_Type
) return Count_Type
;
53 pragma Inline
(Left_Son
);
55 function Parent
(Node
: Node_Type
) return Count_Type
;
56 pragma Inline
(Parent
);
58 function Right_Son
(Node
: Node_Type
) return Count_Type
;
59 pragma Inline
(Right_Son
);
62 (Node
: in out Node_Type
;
63 Color
: Ada
.Containers
.Red_Black_Trees
.Color_Type
);
64 pragma Inline
(Set_Color
);
66 procedure Set_Left
(Node
: in out Node_Type
; Left
: Count_Type
);
67 pragma Inline
(Set_Left
);
69 procedure Set_Right
(Node
: in out Node_Type
; Right
: Count_Type
);
70 pragma Inline
(Set_Right
);
72 procedure Set_Parent
(Node
: in out Node_Type
; Parent
: Count_Type
);
73 pragma Inline
(Set_Parent
);
75 -----------------------
76 -- Local Subprograms --
77 -----------------------
79 -- All need comments ???
82 with procedure Set_Element
(Node
: in out Node_Type
);
83 procedure Generic_Allocate
84 (Tree
: in out Tree_Types
.Tree_Type
'Class;
85 Node
: out Count_Type
);
87 procedure Free
(Tree
: in out Map
; X
: Count_Type
);
89 function Is_Greater_Key_Node
91 Right
: Node_Type
) return Boolean;
92 pragma Inline
(Is_Greater_Key_Node
);
94 function Is_Less_Key_Node
96 Right
: Node_Type
) return Boolean;
97 pragma Inline
(Is_Less_Key_Node
);
99 --------------------------
100 -- Local Instantiations --
101 --------------------------
103 package Tree_Operations
is
104 new Red_Black_Trees
.Generic_Bounded_Operations
105 (Tree_Types
=> Tree_Types
,
112 new Red_Black_Trees
.Generic_Bounded_Keys
113 (Tree_Operations
=> Tree_Operations
,
114 Key_Type
=> Key_Type
,
115 Is_Less_Key_Node
=> Is_Less_Key_Node
,
116 Is_Greater_Key_Node
=> Is_Greater_Key_Node
);
122 function "=" (Left
, Right
: Map
) return Boolean is
128 if Length
(Left
) /= Length
(Right
) then
132 if Is_Empty
(Left
) then
136 Lst
:= Next
(Left
, Last
(Left
).Node
);
138 Node
:= First
(Left
).Node
;
139 while Node
/= Lst
loop
140 ENode
:= Find
(Right
, Left
.Nodes
(Node
).Key
).Node
;
143 Left
.Nodes
(Node
).Element
/= Right
.Nodes
(ENode
).Element
148 Node
:= Next
(Left
, Node
);
158 procedure Assign
(Target
: in out Map
; Source
: Map
) is
159 procedure Append_Element
(Source_Node
: Count_Type
);
161 procedure Append_Elements
is
162 new Tree_Operations
.Generic_Iteration
(Append_Element
);
168 procedure Append_Element
(Source_Node
: Count_Type
) is
169 SN
: Node_Type
renames Source
.Nodes
(Source_Node
);
171 procedure Set_Element
(Node
: in out Node_Type
);
172 pragma Inline
(Set_Element
);
174 function New_Node
return Count_Type
;
175 pragma Inline
(New_Node
);
177 procedure Insert_Post
is new Key_Ops
.Generic_Insert_Post
(New_Node
);
179 procedure Unconditional_Insert_Sans_Hint
is
180 new Key_Ops
.Generic_Unconditional_Insert
(Insert_Post
);
182 procedure Unconditional_Insert_Avec_Hint
is
183 new Key_Ops
.Generic_Unconditional_Insert_With_Hint
185 Unconditional_Insert_Sans_Hint
);
187 procedure Allocate
is new Generic_Allocate
(Set_Element
);
193 function New_Node
return Count_Type
is
196 Allocate
(Target
, Result
);
204 procedure Set_Element
(Node
: in out Node_Type
) is
207 Node
.Element
:= SN
.Element
;
210 Target_Node
: Count_Type
;
212 -- Start of processing for Append_Element
215 Unconditional_Insert_Avec_Hint
219 Node
=> Target_Node
);
222 -- Start of processing for Assign
225 if Target
'Address = Source
'Address then
229 if Target
.Capacity
< Length
(Source
) then
230 raise Storage_Error
with "not enough capacity"; -- SE or CE? ???
233 Tree_Operations
.Clear_Tree
(Target
);
234 Append_Elements
(Source
);
241 function Ceiling
(Container
: Map
; Key
: Key_Type
) return Cursor
is
242 Node
: constant Count_Type
:= Key_Ops
.Ceiling
(Container
, Key
);
249 return (Node
=> Node
);
256 procedure Clear
(Container
: in out Map
) is
258 Tree_Operations
.Clear_Tree
(Container
);
265 function Color
(Node
: Node_Type
) return Color_Type
is
274 function Contains
(Container
: Map
; Key
: Key_Type
) return Boolean is
276 return Find
(Container
, Key
) /= No_Element
;
283 function Copy
(Source
: Map
; Capacity
: Count_Type
:= 0) return Map
is
284 Node
: Count_Type
:= 1;
288 if 0 < Capacity
and then Capacity
< Source
.Capacity
then
289 raise Capacity_Error
;
292 return Target
: Map
(Count_Type
'Max (Source
.Capacity
, Capacity
)) do
293 if Length
(Source
) > 0 then
294 Target
.Length
:= Source
.Length
;
295 Target
.Root
:= Source
.Root
;
296 Target
.First
:= Source
.First
;
297 Target
.Last
:= Source
.Last
;
298 Target
.Free
:= Source
.Free
;
300 while Node
<= Source
.Capacity
loop
301 Target
.Nodes
(Node
).Element
:=
302 Source
.Nodes
(Node
).Element
;
303 Target
.Nodes
(Node
).Key
:=
304 Source
.Nodes
(Node
).Key
;
305 Target
.Nodes
(Node
).Parent
:=
306 Source
.Nodes
(Node
).Parent
;
307 Target
.Nodes
(Node
).Left
:=
308 Source
.Nodes
(Node
).Left
;
309 Target
.Nodes
(Node
).Right
:=
310 Source
.Nodes
(Node
).Right
;
311 Target
.Nodes
(Node
).Color
:=
312 Source
.Nodes
(Node
).Color
;
313 Target
.Nodes
(Node
).Has_Element
:=
314 Source
.Nodes
(Node
).Has_Element
;
318 while Node
<= Target
.Capacity
loop
320 Formal_Ordered_Maps
.Free
(Tree
=> Target
, X
=> N
);
331 procedure Delete
(Container
: in out Map
; Position
: in out Cursor
) is
333 if not Has_Element
(Container
, Position
) then
334 raise Constraint_Error
with
335 "Position cursor of Delete has no element";
338 pragma Assert
(Vet
(Container
, Position
.Node
),
339 "Position cursor of Delete is bad");
341 Tree_Operations
.Delete_Node_Sans_Free
(Container
,
343 Formal_Ordered_Maps
.Free
(Container
, Position
.Node
);
344 Position
:= No_Element
;
347 procedure Delete
(Container
: in out Map
; Key
: Key_Type
) is
348 X
: constant Node_Access
:= Key_Ops
.Find
(Container
, Key
);
352 raise Constraint_Error
with "key not in map";
355 Tree_Operations
.Delete_Node_Sans_Free
(Container
, X
);
356 Formal_Ordered_Maps
.Free
(Container
, X
);
363 procedure Delete_First
(Container
: in out Map
) is
364 X
: constant Node_Access
:= First
(Container
).Node
;
367 Tree_Operations
.Delete_Node_Sans_Free
(Container
, X
);
368 Formal_Ordered_Maps
.Free
(Container
, X
);
376 procedure Delete_Last
(Container
: in out Map
) is
377 X
: constant Node_Access
:= Last
(Container
).Node
;
380 Tree_Operations
.Delete_Node_Sans_Free
(Container
, X
);
381 Formal_Ordered_Maps
.Free
(Container
, X
);
389 function Element
(Container
: Map
; Position
: Cursor
) return Element_Type
is
391 if not Has_Element
(Container
, Position
) then
392 raise Constraint_Error
with
393 "Position cursor of function Element has no element";
396 pragma Assert
(Vet
(Container
, Position
.Node
),
397 "Position cursor of function Element is bad");
399 return Container
.Nodes
(Position
.Node
).Element
;
403 function Element
(Container
: Map
; Key
: Key_Type
) return Element_Type
is
404 Node
: constant Node_Access
:= Find
(Container
, Key
).Node
;
408 raise Constraint_Error
with "key not in map";
411 return Container
.Nodes
(Node
).Element
;
414 ---------------------
415 -- Equivalent_Keys --
416 ---------------------
418 function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean is
433 procedure Exclude
(Container
: in out Map
; Key
: Key_Type
) is
434 X
: constant Node_Access
:= Key_Ops
.Find
(Container
, Key
);
437 Tree_Operations
.Delete_Node_Sans_Free
(Container
, X
);
438 Formal_Ordered_Maps
.Free
(Container
, X
);
446 function Find
(Container
: Map
; Key
: Key_Type
) return Cursor
is
447 Node
: constant Count_Type
:= Key_Ops
.Find
(Container
, Key
);
454 return (Node
=> Node
);
461 function First
(Container
: Map
) return Cursor
is
463 if Length
(Container
) = 0 then
467 return (Node
=> Container
.First
);
474 function First_Element
(Container
: Map
) return Element_Type
is
476 if Is_Empty
(Container
) then
477 raise Constraint_Error
with "map is empty";
480 return Container
.Nodes
(First
(Container
).Node
).Element
;
487 function First_Key
(Container
: Map
) return Key_Type
is
489 if Is_Empty
(Container
) then
490 raise Constraint_Error
with "map is empty";
493 return Container
.Nodes
(First
(Container
).Node
).Key
;
500 function Floor
(Container
: Map
; Key
: Key_Type
) return Cursor
is
501 Node
: constant Count_Type
:= Key_Ops
.Floor
(Container
, Key
);
508 return (Node
=> Node
);
515 package body Formal_Model
is
522 (Container
: K
.Sequence
;
523 Key
: Key_Type
) return Count_Type
526 for I
in 1 .. K
.Length
(Container
) loop
527 if Equivalent_Keys
(Key
, K
.Get
(Container
, I
)) then
529 elsif Key
< K
.Get
(Container
, I
) then
536 -------------------------
537 -- K_Bigger_Than_Range --
538 -------------------------
540 function K_Bigger_Than_Range
541 (Container
: K
.Sequence
;
542 Fst
: Positive_Count_Type
;
544 Key
: Key_Type
) return Boolean
547 for I
in Fst
.. Lst
loop
548 if not (K
.Get
(Container
, I
) < Key
) then
553 end K_Bigger_Than_Range
;
560 (Container
: K
.Sequence
;
562 Position
: Count_Type
) return Boolean
565 for I
in 1 .. Position
- 1 loop
566 if Key
< K
.Get
(Container
, I
) then
571 if Position
< K
.Length
(Container
) then
572 for I
in Position
+ 1 .. K
.Length
(Container
) loop
573 if K
.Get
(Container
, I
) < Key
then
581 --------------------------
582 -- K_Smaller_Than_Range --
583 --------------------------
585 function K_Smaller_Than_Range
586 (Container
: K
.Sequence
;
587 Fst
: Positive_Count_Type
;
589 Key
: Key_Type
) return Boolean
592 for I
in Fst
.. Lst
loop
593 if not (Key
< K
.Get
(Container
, I
)) then
598 end K_Smaller_Than_Range
;
604 function Keys
(Container
: Map
) return K
.Sequence
is
605 Position
: Count_Type
:= Container
.First
;
609 -- Can't use First, Next or Element here, since they depend on models
610 -- for their postconditions.
612 while Position
/= 0 loop
613 R
:= K
.Add
(R
, Container
.Nodes
(Position
).Key
);
614 Position
:= Tree_Operations
.Next
(Container
, Position
);
620 ----------------------------
621 -- Lift_Abstraction_Level --
622 ----------------------------
624 procedure Lift_Abstraction_Level
(Container
: Map
) is null;
630 function Model
(Container
: Map
) return M
.Map
is
631 Position
: Count_Type
:= Container
.First
;
635 -- Can't use First, Next or Element here, since they depend on models
636 -- for their postconditions.
638 while Position
/= 0 loop
642 New_Key
=> Container
.Nodes
(Position
).Key
,
643 New_Item
=> Container
.Nodes
(Position
).Element
);
645 Position
:= Tree_Operations
.Next
(Container
, Position
);
651 -------------------------
652 -- P_Positions_Shifted --
653 -------------------------
655 function P_Positions_Shifted
658 Cut
: Positive_Count_Type
;
659 Count
: Count_Type
:= 1) return Boolean
663 if not P
.Has_Key
(Big
, Cu
) then
670 Pos
: constant Positive_Count_Type
:= P
.Get
(Big
, Cu
);
674 if not P
.Has_Key
(Small
, Cu
)
675 or else Pos
/= P
.Get
(Small
, Cu
)
680 elsif Pos
>= Cut
+ Count
then
681 if not P
.Has_Key
(Small
, Cu
)
682 or else Pos
/= P
.Get
(Small
, Cu
) + Count
688 if P
.Has_Key
(Small
, Cu
) then
696 end P_Positions_Shifted
;
702 function Positions
(Container
: Map
) return P
.Map
is
704 Position
: Count_Type
:= Container
.First
;
708 -- Can't use First, Next or Element here, since they depend on models
709 -- for their postconditions.
711 while Position
/= 0 loop
712 R
:= P
.Add
(R
, (Node
=> Position
), I
);
713 pragma Assert
(P
.Length
(R
) = I
);
714 Position
:= Tree_Operations
.Next
(Container
, Position
);
732 Tree
.Nodes
(X
).Has_Element
:= False;
733 Tree_Operations
.Free
(Tree
, X
);
736 ----------------------
737 -- Generic_Allocate --
738 ----------------------
740 procedure Generic_Allocate
741 (Tree
: in out Tree_Types
.Tree_Type
'Class;
742 Node
: out Count_Type
)
744 procedure Allocate
is
745 new Tree_Operations
.Generic_Allocate
(Set_Element
);
747 Allocate
(Tree
, Node
);
748 Tree
.Nodes
(Node
).Has_Element
:= True;
749 end Generic_Allocate
;
755 function Has_Element
(Container
: Map
; Position
: Cursor
) return Boolean is
757 if Position
.Node
= 0 then
761 return Container
.Nodes
(Position
.Node
).Has_Element
;
769 (Container
: in out Map
;
771 New_Item
: Element_Type
)
777 Insert
(Container
, Key
, New_Item
, Position
, Inserted
);
781 N
: Node_Type
renames Container
.Nodes
(Position
.Node
);
784 N
.Element
:= New_Item
;
790 (Container
: in out Map
;
792 New_Item
: Element_Type
;
793 Position
: out Cursor
;
794 Inserted
: out Boolean)
796 function New_Node
return Node_Access
;
799 procedure Insert_Post
is
800 new Key_Ops
.Generic_Insert_Post
(New_Node
);
802 procedure Insert_Sans_Hint
is
803 new Key_Ops
.Generic_Conditional_Insert
(Insert_Post
);
809 function New_Node
return Node_Access
is
810 procedure Initialize
(Node
: in out Node_Type
);
811 procedure Allocate_Node
is new Generic_Allocate
(Initialize
);
813 procedure Initialize
(Node
: in out Node_Type
) is
816 Node
.Element
:= New_Item
;
822 Allocate_Node
(Container
, X
);
826 -- Start of processing for Insert
837 (Container
: in out Map
;
839 New_Item
: Element_Type
)
845 Insert
(Container
, Key
, New_Item
, Position
, Inserted
);
848 raise Constraint_Error
with "key already in map";
856 function Is_Empty
(Container
: Map
) return Boolean is
858 return Length
(Container
) = 0;
861 -------------------------
862 -- Is_Greater_Key_Node --
863 -------------------------
865 function Is_Greater_Key_Node
867 Right
: Node_Type
) return Boolean
870 -- k > node same as node < k
872 return Right
.Key
< Left
;
873 end Is_Greater_Key_Node
;
875 ----------------------
876 -- Is_Less_Key_Node --
877 ----------------------
879 function Is_Less_Key_Node
881 Right
: Node_Type
) return Boolean
884 return Left
< Right
.Key
;
885 end Is_Less_Key_Node
;
891 function Key
(Container
: Map
; Position
: Cursor
) return Key_Type
is
893 if not Has_Element
(Container
, Position
) then
894 raise Constraint_Error
with
895 "Position cursor of function Key has no element";
898 pragma Assert
(Vet
(Container
, Position
.Node
),
899 "Position cursor of function Key is bad");
901 return Container
.Nodes
(Position
.Node
).Key
;
908 function Last
(Container
: Map
) return Cursor
is
910 if Length
(Container
) = 0 then
914 return (Node
=> Container
.Last
);
921 function Last_Element
(Container
: Map
) return Element_Type
is
923 if Is_Empty
(Container
) then
924 raise Constraint_Error
with "map is empty";
927 return Container
.Nodes
(Last
(Container
).Node
).Element
;
934 function Last_Key
(Container
: Map
) return Key_Type
is
936 if Is_Empty
(Container
) then
937 raise Constraint_Error
with "map is empty";
940 return Container
.Nodes
(Last
(Container
).Node
).Key
;
947 function Left_Son
(Node
: Node_Type
) return Count_Type
is
956 function Length
(Container
: Map
) return Count_Type
is
958 return Container
.Length
;
965 procedure Move
(Target
: in out Map
; Source
: in out Map
) is
966 NN
: Tree_Types
.Nodes_Type
renames Source
.Nodes
;
970 if Target
'Address = Source
'Address then
974 if Target
.Capacity
< Length
(Source
) then
975 raise Constraint_Error
with -- ???
976 "Source length exceeds Target capacity";
982 X
:= First
(Source
).Node
;
985 -- Here we insert a copy of the source element into the target, and
986 -- then delete the element from the source. Another possibility is
987 -- that delete it first (and hang onto its index), then insert it.
990 Insert
(Target
, NN
(X
).Key
, NN
(X
).Element
); -- optimize???
992 Tree_Operations
.Delete_Node_Sans_Free
(Source
, X
);
993 Formal_Ordered_Maps
.Free
(Source
, X
);
1001 procedure Next
(Container
: Map
; Position
: in out Cursor
) is
1003 Position
:= Next
(Container
, Position
);
1006 function Next
(Container
: Map
; Position
: Cursor
) return Cursor
is
1008 if Position
= No_Element
then
1012 if not Has_Element
(Container
, Position
) then
1013 raise Constraint_Error
;
1016 pragma Assert
(Vet
(Container
, Position
.Node
),
1017 "bad cursor in Next");
1019 return (Node
=> Tree_Operations
.Next
(Container
, Position
.Node
));
1026 function Parent
(Node
: Node_Type
) return Count_Type
is
1035 procedure Previous
(Container
: Map
; Position
: in out Cursor
) is
1037 Position
:= Previous
(Container
, Position
);
1040 function Previous
(Container
: Map
; Position
: Cursor
) return Cursor
is
1042 if Position
= No_Element
then
1046 if not Has_Element
(Container
, Position
) then
1047 raise Constraint_Error
;
1050 pragma Assert
(Vet
(Container
, Position
.Node
),
1051 "bad cursor in Previous");
1054 Node
: constant Count_Type
:=
1055 Tree_Operations
.Previous
(Container
, Position
.Node
);
1062 return (Node
=> Node
);
1071 (Container
: in out Map
;
1073 New_Item
: Element_Type
)
1077 Node
: constant Node_Access
:= Key_Ops
.Find
(Container
, Key
);
1081 raise Constraint_Error
with "key not in map";
1085 N
: Node_Type
renames Container
.Nodes
(Node
);
1088 N
.Element
:= New_Item
;
1093 ---------------------
1094 -- Replace_Element --
1095 ---------------------
1097 procedure Replace_Element
1098 (Container
: in out Map
;
1100 New_Item
: Element_Type
)
1103 if not Has_Element
(Container
, Position
) then
1104 raise Constraint_Error
with
1105 "Position cursor of Replace_Element has no element";
1108 pragma Assert
(Vet
(Container
, Position
.Node
),
1109 "Position cursor of Replace_Element is bad");
1111 Container
.Nodes
(Position
.Node
).Element
:= New_Item
;
1112 end Replace_Element
;
1118 function Right_Son
(Node
: Node_Type
) return Count_Type
is
1127 procedure Set_Color
(Node
: in out Node_Type
; Color
: Color_Type
) is
1129 Node
.Color
:= Color
;
1136 procedure Set_Left
(Node
: in out Node_Type
; Left
: Count_Type
) is
1145 procedure Set_Parent
(Node
: in out Node_Type
; Parent
: Count_Type
) is
1147 Node
.Parent
:= Parent
;
1154 procedure Set_Right
(Node
: in out Node_Type
; Right
: Count_Type
) is
1156 Node
.Right
:= Right
;
1159 end Ada
.Containers
.Formal_Ordered_Maps
;