1 ------------------------------------------------------------------------------
3 -- GNAT LIBRARY COMPONENTS --
5 -- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS --
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 System
; use type System
.Address
;
30 package body Ada
.Containers
.Formal_Doubly_Linked_Lists
with
33 -----------------------
34 -- Local Subprograms --
35 -----------------------
38 (Container
: in out List
;
39 New_Item
: Element_Type
;
40 New_Node
: out Count_Type
);
42 procedure Free
(Container
: in out List
; X
: Count_Type
);
44 procedure Insert_Internal
45 (Container
: in out List
;
47 New_Node
: Count_Type
);
49 function Vet
(L
: List
; Position
: Cursor
) return Boolean;
55 function "=" (Left
: List
; Right
: List
) return Boolean is
60 if Left
'Address = Right
'Address then
64 if Left
.Length
/= Right
.Length
then
71 if Left
.Nodes
(LI
).Element
/= Right
.Nodes
(LI
).Element
then
75 LI
:= Left
.Nodes
(LI
).Next
;
76 RI
:= Right
.Nodes
(RI
).Next
;
87 (Container
: in out List
;
88 New_Item
: Element_Type
;
89 New_Node
: out Count_Type
)
91 N
: Node_Array
renames Container
.Nodes
;
94 if Container
.Free
>= 0 then
95 New_Node
:= Container
.Free
;
96 N
(New_Node
).Element
:= New_Item
;
97 Container
.Free
:= N
(New_Node
).Next
;
100 New_Node
:= abs Container
.Free
;
101 N
(New_Node
).Element
:= New_Item
;
102 Container
.Free
:= Container
.Free
- 1;
110 procedure Append
(Container
: in out List
; New_Item
: Element_Type
) is
112 Insert
(Container
, No_Element
, New_Item
, 1);
116 (Container
: in out List
;
117 New_Item
: Element_Type
;
121 Insert
(Container
, No_Element
, New_Item
, Count
);
128 procedure Assign
(Target
: in out List
; Source
: List
) is
129 N
: Node_Array
renames Source
.Nodes
;
133 if Target
'Address = Source
'Address then
137 if Target
.Capacity
< Source
.Length
then
138 raise Constraint_Error
with -- ???
139 "Source length exceeds Target capacity";
146 Append
(Target
, N
(J
).Element
, 1);
155 procedure Clear
(Container
: in out List
) is
156 N
: Node_Array
renames Container
.Nodes
;
160 if Container
.Length
= 0 then
161 pragma Assert
(Container
.First
= 0);
162 pragma Assert
(Container
.Last
= 0);
166 pragma Assert
(Container
.First
>= 1);
167 pragma Assert
(Container
.Last
>= 1);
168 pragma Assert
(N
(Container
.First
).Prev
= 0);
169 pragma Assert
(N
(Container
.Last
).Next
= 0);
171 while Container
.Length
> 1 loop
172 X
:= Container
.First
;
174 Container
.First
:= N
(X
).Next
;
175 N
(Container
.First
).Prev
:= 0;
177 Container
.Length
:= Container
.Length
- 1;
182 X
:= Container
.First
;
184 Container
.First
:= 0;
186 Container
.Length
:= 0;
197 Item
: Element_Type
) return Boolean
200 return Find
(Container
, Item
) /= No_Element
;
209 Capacity
: Count_Type
:= 0) return List
211 C
: constant Count_Type
:= Count_Type
'Max (Source
.Capacity
, Capacity
);
216 if 0 < Capacity
and then Capacity
< Source
.Capacity
then
217 raise Capacity_Error
;
221 while N
<= Source
.Capacity
loop
222 P
.Nodes
(N
).Prev
:= Source
.Nodes
(N
).Prev
;
223 P
.Nodes
(N
).Next
:= Source
.Nodes
(N
).Next
;
224 P
.Nodes
(N
).Element
:= Source
.Nodes
(N
).Element
;
228 P
.Free
:= Source
.Free
;
229 P
.Length
:= Source
.Length
;
230 P
.First
:= Source
.First
;
231 P
.Last
:= Source
.Last
;
234 N
:= Source
.Capacity
+ 1;
248 procedure Delete
(Container
: in out List
; Position
: in out Cursor
) is
251 (Container
=> Container
,
252 Position
=> Position
,
257 (Container
: in out List
;
258 Position
: in out Cursor
;
261 N
: Node_Array
renames Container
.Nodes
;
265 if not Has_Element
(Container
=> Container
,
266 Position
=> Position
)
268 raise Constraint_Error
with "Position cursor has no element";
271 pragma Assert
(Vet
(Container
, Position
), "bad cursor in Delete");
272 pragma Assert
(Container
.First
>= 1);
273 pragma Assert
(Container
.Last
>= 1);
274 pragma Assert
(N
(Container
.First
).Prev
= 0);
275 pragma Assert
(N
(Container
.Last
).Next
= 0);
277 if Position
.Node
= Container
.First
then
278 Delete_First
(Container
, Count
);
279 Position
:= No_Element
;
284 Position
:= No_Element
;
288 for Index
in 1 .. Count
loop
289 pragma Assert
(Container
.Length
>= 2);
292 Container
.Length
:= Container
.Length
- 1;
294 if X
= Container
.Last
then
295 Position
:= No_Element
;
297 Container
.Last
:= N
(X
).Prev
;
298 N
(Container
.Last
).Next
:= 0;
304 Position
.Node
:= N
(X
).Next
;
305 pragma Assert
(N
(Position
.Node
).Prev
>= 0);
307 N
(N
(X
).Next
).Prev
:= N
(X
).Prev
;
308 N
(N
(X
).Prev
).Next
:= N
(X
).Next
;
313 Position
:= No_Element
;
320 procedure Delete_First
(Container
: in out List
) is
323 (Container
=> Container
,
327 procedure Delete_First
(Container
: in out List
; Count
: Count_Type
) is
328 N
: Node_Array
renames Container
.Nodes
;
332 if Count
>= Container
.Length
then
341 for J
in 1 .. Count
loop
342 X
:= Container
.First
;
343 pragma Assert
(N
(N
(X
).Next
).Prev
= Container
.First
);
345 Container
.First
:= N
(X
).Next
;
346 N
(Container
.First
).Prev
:= 0;
348 Container
.Length
:= Container
.Length
- 1;
358 procedure Delete_Last
(Container
: in out List
) is
361 (Container
=> Container
,
365 procedure Delete_Last
(Container
: in out List
; Count
: Count_Type
) is
366 N
: Node_Array
renames Container
.Nodes
;
370 if Count
>= Container
.Length
then
379 for J
in 1 .. Count
loop
381 pragma Assert
(N
(N
(X
).Prev
).Next
= Container
.Last
);
383 Container
.Last
:= N
(X
).Prev
;
384 N
(Container
.Last
).Next
:= 0;
386 Container
.Length
:= Container
.Length
- 1;
398 Position
: Cursor
) return Element_Type
401 if not Has_Element
(Container
=> Container
, Position
=> Position
) then
402 raise Constraint_Error
with "Position cursor has no element";
405 return Container
.Nodes
(Position
.Node
).Element
;
415 Position
: Cursor
:= No_Element
) return Cursor
417 From
: Count_Type
:= Position
.Node
;
420 if From
= 0 and Container
.Length
= 0 then
425 From
:= Container
.First
;
428 if Position
.Node
/= 0 and then not Has_Element
(Container
, Position
) then
429 raise Constraint_Error
with "Position cursor has no element";
433 if Container
.Nodes
(From
).Element
= Item
then
434 return (Node
=> From
);
437 From
:= Container
.Nodes
(From
).Next
;
447 function First
(Container
: List
) return Cursor
is
449 if Container
.First
= 0 then
453 return (Node
=> Container
.First
);
460 function First_Element
(Container
: List
) return Element_Type
is
461 F
: constant Count_Type
:= Container
.First
;
465 raise Constraint_Error
with "list is empty";
467 return Container
.Nodes
(F
).Element
;
475 package body Formal_Model
is
477 ----------------------------
478 -- Lift_Abstraction_Level --
479 ----------------------------
481 procedure Lift_Abstraction_Level
(Container
: List
) is null;
483 -------------------------
484 -- M_Elements_In_Union --
485 -------------------------
487 function M_Elements_In_Union
488 (Container
: M
.Sequence
;
490 Right
: M
.Sequence
) return Boolean
495 for Index
in 1 .. M
.Length
(Container
) loop
496 Elem
:= Element
(Container
, Index
);
498 if not M
.Contains
(Left
, 1, M
.Length
(Left
), Elem
)
499 and then not M
.Contains
(Right
, 1, M
.Length
(Right
), Elem
)
506 end M_Elements_In_Union
;
508 -------------------------
509 -- M_Elements_Included --
510 -------------------------
512 function M_Elements_Included
514 L_Fst
: Positive_Count_Type
:= 1;
517 R_Fst
: Positive_Count_Type
:= 1;
518 R_Lst
: Count_Type
) return Boolean
521 for I
in L_Fst
.. L_Lst
loop
523 Found
: Boolean := False;
524 J
: Count_Type
:= R_Fst
- 1;
527 while not Found
and J
< R_Lst
loop
529 if Element
(Left
, I
) = Element
(Right
, J
) then
541 end M_Elements_Included
;
543 -------------------------
544 -- M_Elements_Reversed --
545 -------------------------
547 function M_Elements_Reversed
549 Right
: M
.Sequence
) return Boolean
551 L
: constant Count_Type
:= M
.Length
(Left
);
554 if L
/= M
.Length
(Right
) then
559 if Element
(Left
, I
) /= Element
(Right
, L
- I
+ 1) then
565 end M_Elements_Reversed
;
567 ------------------------
568 -- M_Elements_Swapted --
569 ------------------------
571 function M_Elements_Swapped
574 X
: Positive_Count_Type
;
575 Y
: Positive_Count_Type
) return Boolean
578 if M
.Length
(Left
) /= M
.Length
(Right
)
579 or else Element
(Left
, X
) /= Element
(Right
, Y
)
580 or else Element
(Left
, Y
) /= Element
(Right
, X
)
585 for I
in 1 .. M
.Length
(Left
) loop
586 if I
/= X
and then I
/= Y
587 and then Element
(Left
, I
) /= Element
(Right
, I
)
594 end M_Elements_Swapped
;
600 function Model
(Container
: List
) return M
.Sequence
is
601 Position
: Count_Type
:= Container
.First
;
605 -- Can't use First, Next or Element here, since they depend on models
606 -- for their postconditions.
608 while Position
/= 0 loop
609 R
:= M
.Add
(R
, Container
.Nodes
(Position
).Element
);
610 Position
:= Container
.Nodes
(Position
).Next
;
616 -----------------------
617 -- Mapping_Preserved --
618 -----------------------
620 function Mapping_Preserved
621 (M_Left
: M
.Sequence
;
622 M_Right
: M
.Sequence
;
624 P_Right
: P
.Map
) return Boolean
628 if not P
.Has_Key
(P_Right
, C
)
629 or else P
.Get
(P_Left
, C
) > M
.Length
(M_Left
)
630 or else P
.Get
(P_Right
, C
) > M
.Length
(M_Right
)
631 or else M
.Get
(M_Left
, P
.Get
(P_Left
, C
)) /=
632 M
.Get
(M_Right
, P
.Get
(P_Right
, C
))
638 for C
of P_Right
loop
639 if not P
.Has_Key
(P_Left
, C
) then
645 end Mapping_Preserved
;
647 -------------------------
648 -- P_Positions_Shifted --
649 -------------------------
651 function P_Positions_Shifted
654 Cut
: Positive_Count_Type
;
655 Count
: Count_Type
:= 1) return Boolean
659 if not P
.Has_Key
(Big
, Cu
) then
666 Pos
: constant Positive_Count_Type
:= P
.Get
(Big
, Cu
);
670 if not P
.Has_Key
(Small
, Cu
)
671 or else Pos
/= P
.Get
(Small
, Cu
)
676 elsif Pos
>= Cut
+ Count
then
677 if not P
.Has_Key
(Small
, Cu
)
678 or else Pos
/= P
.Get
(Small
, Cu
) + Count
684 if P
.Has_Key
(Small
, Cu
) then
692 end P_Positions_Shifted
;
694 -------------------------
695 -- P_Positions_Swapped --
696 -------------------------
698 function P_Positions_Swapped
702 Y
: Cursor
) return Boolean
705 if not P
.Has_Key
(Left
, X
)
706 or not P
.Has_Key
(Left
, Y
)
707 or not P
.Has_Key
(Right
, X
)
708 or not P
.Has_Key
(Right
, Y
)
713 if P
.Get
(Left
, X
) /= P
.Get
(Right
, Y
)
714 or P
.Get
(Left
, Y
) /= P
.Get
(Right
, X
)
720 if not P
.Has_Key
(Right
, C
) then
726 if not P
.Has_Key
(Left
, C
)
729 and P
.Get
(Left
, C
) /= P
.Get
(Right
, C
))
736 end P_Positions_Swapped
;
738 ---------------------------
739 -- P_Positions_Truncated --
740 ---------------------------
742 function P_Positions_Truncated
745 Cut
: Positive_Count_Type
;
746 Count
: Count_Type
:= 1) return Boolean
750 if not P
.Has_Key
(Big
, Cu
) then
757 Pos
: constant Positive_Count_Type
:= P
.Get
(Big
, Cu
);
761 if not P
.Has_Key
(Small
, Cu
)
762 or else Pos
/= P
.Get
(Small
, Cu
)
767 elsif Pos
>= Cut
+ Count
then
770 elsif P
.Has_Key
(Small
, Cu
) then
777 end P_Positions_Truncated
;
783 function Positions
(Container
: List
) return P
.Map
is
785 Position
: Count_Type
:= Container
.First
;
789 -- Can't use First, Next or Element here, since they depend on models
790 -- for their postconditions.
792 while Position
/= 0 loop
793 R
:= P
.Add
(R
, (Node
=> Position
), I
);
794 pragma Assert
(P
.Length
(R
) = I
);
795 Position
:= Container
.Nodes
(Position
).Next
;
808 procedure Free
(Container
: in out List
; X
: Count_Type
) is
809 pragma Assert
(X
> 0);
810 pragma Assert
(X
<= Container
.Capacity
);
812 N
: Node_Array
renames Container
.Nodes
;
815 N
(X
).Prev
:= -1; -- Node is deallocated (not on active list)
817 if Container
.Free
>= 0 then
818 N
(X
).Next
:= Container
.Free
;
821 elsif X
+ 1 = abs Container
.Free
then
822 N
(X
).Next
:= 0; -- Not strictly necessary, but marginally safer
823 Container
.Free
:= Container
.Free
+ 1;
826 Container
.Free
:= abs Container
.Free
;
828 if Container
.Free
> Container
.Capacity
then
832 for J
in Container
.Free
.. Container
.Capacity
- 1 loop
836 N
(Container
.Capacity
).Next
:= 0;
839 N
(X
).Next
:= Container
.Free
;
844 ---------------------
845 -- Generic_Sorting --
846 ---------------------
848 package body Generic_Sorting
with SPARK_Mode
=> Off
is
854 package body Formal_Model
is
856 -----------------------
857 -- M_Elements_Sorted --
858 -----------------------
860 function M_Elements_Sorted
(Container
: M
.Sequence
) return Boolean is
862 if M
.Length
(Container
) = 0 then
867 E1
: Element_Type
:= Element
(Container
, 1);
870 for I
in 2 .. M
.Length
(Container
) loop
872 E2
: constant Element_Type
:= Element
(Container
, I
);
885 end M_Elements_Sorted
;
893 function Is_Sorted
(Container
: List
) return Boolean is
894 Nodes
: Node_Array
renames Container
.Nodes
;
895 Node
: Count_Type
:= Container
.First
;
898 for J
in 2 .. Container
.Length
loop
899 if Nodes
(Nodes
(Node
).Next
).Element
< Nodes
(Node
).Element
then
902 Node
:= Nodes
(Node
).Next
;
913 procedure Merge
(Target
: in out List
; Source
: in out List
) is
914 LN
: Node_Array
renames Target
.Nodes
;
915 RN
: Node_Array
renames Source
.Nodes
;
920 if Target
'Address = Source
'Address then
921 raise Program_Error
with "Target and Source denote same container";
924 LI
:= First
(Target
);
925 RI
:= First
(Source
);
926 while RI
.Node
/= 0 loop
928 (RN
(RI
.Node
).Next
= 0
929 or else not (RN
(RN
(RI
.Node
).Next
).Element
<
930 RN
(RI
.Node
).Element
));
933 Splice
(Target
, No_Element
, Source
);
938 (LN
(LI
.Node
).Next
= 0
939 or else not (LN
(LN
(LI
.Node
).Next
).Element
<
940 LN
(LI
.Node
).Element
));
942 if RN
(RI
.Node
).Element
< LN
(LI
.Node
).Element
then
945 pragma Warnings
(Off
, RJ
);
947 RI
.Node
:= RN
(RI
.Node
).Next
;
948 Splice
(Target
, LI
, Source
, RJ
);
952 LI
.Node
:= LN
(LI
.Node
).Next
;
961 procedure Sort
(Container
: in out List
) is
962 N
: Node_Array
renames Container
.Nodes
;
964 procedure Partition
(Pivot
: Count_Type
; Back
: Count_Type
);
965 procedure Sort
(Front
: Count_Type
; Back
: Count_Type
);
971 procedure Partition
(Pivot
: Count_Type
; Back
: Count_Type
) is
975 Node
:= N
(Pivot
).Next
;
976 while Node
/= Back
loop
977 if N
(Node
).Element
< N
(Pivot
).Element
then
979 Prev
: constant Count_Type
:= N
(Node
).Prev
;
980 Next
: constant Count_Type
:= N
(Node
).Next
;
983 N
(Prev
).Next
:= Next
;
986 Container
.Last
:= Prev
;
988 N
(Next
).Prev
:= Prev
;
991 N
(Node
).Next
:= Pivot
;
992 N
(Node
).Prev
:= N
(Pivot
).Prev
;
994 N
(Pivot
).Prev
:= Node
;
996 if N
(Node
).Prev
= 0 then
997 Container
.First
:= Node
;
999 N
(N
(Node
).Prev
).Next
:= Node
;
1006 Node
:= N
(Node
).Next
;
1015 procedure Sort
(Front
: Count_Type
; Back
: Count_Type
) is
1020 Pivot
:= Container
.First
;
1022 Pivot
:= N
(Front
).Next
;
1025 if Pivot
/= Back
then
1026 Partition
(Pivot
, Back
);
1027 Sort
(Front
, Pivot
);
1032 -- Start of processing for Sort
1035 if Container
.Length
<= 1 then
1039 pragma Assert
(N
(Container
.First
).Prev
= 0);
1040 pragma Assert
(N
(Container
.Last
).Next
= 0);
1042 Sort
(Front
=> 0, Back
=> 0);
1044 pragma Assert
(N
(Container
.First
).Prev
= 0);
1045 pragma Assert
(N
(Container
.Last
).Next
= 0);
1048 end Generic_Sorting
;
1054 function Has_Element
(Container
: List
; Position
: Cursor
) return Boolean is
1056 if Position
.Node
= 0 then
1060 return Container
.Nodes
(Position
.Node
).Prev
/= -1;
1068 (Container
: in out List
;
1070 New_Item
: Element_Type
;
1071 Position
: out Cursor
;
1077 if Before
.Node
/= 0 then
1078 pragma Assert
(Vet
(Container
, Before
), "bad cursor in Insert");
1086 if Container
.Length
> Container
.Capacity
- Count
then
1087 raise Constraint_Error
with "new length exceeds capacity";
1090 Allocate
(Container
, New_Item
, New_Node
=> J
);
1091 Insert_Internal
(Container
, Before
.Node
, New_Node
=> J
);
1092 Position
:= (Node
=> J
);
1094 for Index
in 2 .. Count
loop
1095 Allocate
(Container
, New_Item
, New_Node
=> J
);
1096 Insert_Internal
(Container
, Before
.Node
, New_Node
=> J
);
1101 (Container
: in out List
;
1103 New_Item
: Element_Type
;
1104 Position
: out Cursor
)
1108 (Container
=> Container
,
1110 New_Item
=> New_Item
,
1111 Position
=> Position
,
1116 (Container
: in out List
;
1118 New_Item
: Element_Type
;
1124 Insert
(Container
, Before
, New_Item
, Position
, Count
);
1128 (Container
: in out List
;
1130 New_Item
: Element_Type
)
1135 Insert
(Container
, Before
, New_Item
, Position
, 1);
1138 ---------------------
1139 -- Insert_Internal --
1140 ---------------------
1142 procedure Insert_Internal
1143 (Container
: in out List
;
1144 Before
: Count_Type
;
1145 New_Node
: Count_Type
)
1147 N
: Node_Array
renames Container
.Nodes
;
1150 if Container
.Length
= 0 then
1151 pragma Assert
(Before
= 0);
1152 pragma Assert
(Container
.First
= 0);
1153 pragma Assert
(Container
.Last
= 0);
1155 Container
.First
:= New_Node
;
1156 Container
.Last
:= New_Node
;
1158 N
(Container
.First
).Prev
:= 0;
1159 N
(Container
.Last
).Next
:= 0;
1161 elsif Before
= 0 then
1162 pragma Assert
(N
(Container
.Last
).Next
= 0);
1164 N
(Container
.Last
).Next
:= New_Node
;
1165 N
(New_Node
).Prev
:= Container
.Last
;
1167 Container
.Last
:= New_Node
;
1168 N
(Container
.Last
).Next
:= 0;
1170 elsif Before
= Container
.First
then
1171 pragma Assert
(N
(Container
.First
).Prev
= 0);
1173 N
(Container
.First
).Prev
:= New_Node
;
1174 N
(New_Node
).Next
:= Container
.First
;
1176 Container
.First
:= New_Node
;
1177 N
(Container
.First
).Prev
:= 0;
1180 pragma Assert
(N
(Container
.First
).Prev
= 0);
1181 pragma Assert
(N
(Container
.Last
).Next
= 0);
1183 N
(New_Node
).Next
:= Before
;
1184 N
(New_Node
).Prev
:= N
(Before
).Prev
;
1186 N
(N
(Before
).Prev
).Next
:= New_Node
;
1187 N
(Before
).Prev
:= New_Node
;
1190 Container
.Length
:= Container
.Length
+ 1;
1191 end Insert_Internal
;
1197 function Is_Empty
(Container
: List
) return Boolean is
1199 return Length
(Container
) = 0;
1206 function Last
(Container
: List
) return Cursor
is
1208 if Container
.Last
= 0 then
1212 return (Node
=> Container
.Last
);
1219 function Last_Element
(Container
: List
) return Element_Type
is
1220 L
: constant Count_Type
:= Container
.Last
;
1224 raise Constraint_Error
with "list is empty";
1226 return Container
.Nodes
(L
).Element
;
1234 function Length
(Container
: List
) return Count_Type
is
1236 return Container
.Length
;
1243 procedure Move
(Target
: in out List
; Source
: in out List
) is
1244 N
: Node_Array
renames Source
.Nodes
;
1248 if Target
'Address = Source
'Address then
1252 if Target
.Capacity
< Source
.Length
then
1253 raise Constraint_Error
with -- ???
1254 "Source length exceeds Target capacity";
1259 while Source
.Length
> 1 loop
1260 pragma Assert
(Source
.First
in 1 .. Source
.Capacity
);
1261 pragma Assert
(Source
.Last
/= Source
.First
);
1262 pragma Assert
(N
(Source
.First
).Prev
= 0);
1263 pragma Assert
(N
(Source
.Last
).Next
= 0);
1265 -- Copy first element from Source to Target
1268 Append
(Target
, N
(X
).Element
); -- optimize away???
1270 -- Unlink first node of Source
1272 Source
.First
:= N
(X
).Next
;
1273 N
(Source
.First
).Prev
:= 0;
1275 Source
.Length
:= Source
.Length
- 1;
1277 -- The representation invariants for Source have been restored. It is
1278 -- now safe to free the unlinked node, without fear of corrupting the
1279 -- active links of Source.
1281 -- Note that the algorithm we use here models similar algorithms used
1282 -- in the unbounded form of the doubly-linked list container. In that
1283 -- case, Free is an instantation of Unchecked_Deallocation, which can
1284 -- fail (because PE will be raised if controlled Finalize fails), so
1285 -- we must defer the call until the last step. Here in the bounded
1286 -- form, Free merely links the node we have just "deallocated" onto a
1287 -- list of inactive nodes, so technically Free cannot fail. However,
1288 -- for consistency, we handle Free the same way here as we do for the
1289 -- unbounded form, with the pessimistic assumption that it can fail.
1294 if Source
.Length
= 1 then
1295 pragma Assert
(Source
.First
in 1 .. Source
.Capacity
);
1296 pragma Assert
(Source
.Last
= Source
.First
);
1297 pragma Assert
(N
(Source
.First
).Prev
= 0);
1298 pragma Assert
(N
(Source
.Last
).Next
= 0);
1300 -- Copy element from Source to Target
1303 Append
(Target
, N
(X
).Element
);
1305 -- Unlink node of Source
1311 -- Return the unlinked node to the free store
1321 procedure Next
(Container
: List
; Position
: in out Cursor
) is
1323 Position
:= Next
(Container
, Position
);
1326 function Next
(Container
: List
; Position
: Cursor
) return Cursor
is
1328 if Position
.Node
= 0 then
1332 if not Has_Element
(Container
, Position
) then
1333 raise Program_Error
with "Position cursor has no element";
1336 return (Node
=> Container
.Nodes
(Position
.Node
).Next
);
1343 procedure Prepend
(Container
: in out List
; New_Item
: Element_Type
) is
1345 Insert
(Container
, First
(Container
), New_Item
, 1);
1349 (Container
: in out List
;
1350 New_Item
: Element_Type
;
1354 Insert
(Container
, First
(Container
), New_Item
, Count
);
1361 procedure Previous
(Container
: List
; Position
: in out Cursor
) is
1363 Position
:= Previous
(Container
, Position
);
1366 function Previous
(Container
: List
; Position
: Cursor
) return Cursor
is
1368 if Position
.Node
= 0 then
1372 if not Has_Element
(Container
, Position
) then
1373 raise Program_Error
with "Position cursor has no element";
1376 return (Node
=> Container
.Nodes
(Position
.Node
).Prev
);
1379 ---------------------
1380 -- Replace_Element --
1381 ---------------------
1383 procedure Replace_Element
1384 (Container
: in out List
;
1386 New_Item
: Element_Type
)
1389 if not Has_Element
(Container
, Position
) then
1390 raise Constraint_Error
with "Position cursor has no element";
1394 (Vet
(Container
, Position
), "bad cursor in Replace_Element");
1396 Container
.Nodes
(Position
.Node
).Element
:= New_Item
;
1397 end Replace_Element
;
1399 ----------------------
1400 -- Reverse_Elements --
1401 ----------------------
1403 procedure Reverse_Elements
(Container
: in out List
) is
1404 N
: Node_Array
renames Container
.Nodes
;
1405 I
: Count_Type
:= Container
.First
;
1406 J
: Count_Type
:= Container
.Last
;
1408 procedure Swap
(L
: Count_Type
; R
: Count_Type
);
1414 procedure Swap
(L
: Count_Type
; R
: Count_Type
) is
1415 LN
: constant Count_Type
:= N
(L
).Next
;
1416 LP
: constant Count_Type
:= N
(L
).Prev
;
1418 RN
: constant Count_Type
:= N
(R
).Next
;
1419 RP
: constant Count_Type
:= N
(R
).Prev
;
1434 pragma Assert
(RP
= L
);
1448 -- Start of processing for Reverse_Elements
1451 if Container
.Length
<= 1 then
1455 pragma Assert
(N
(Container
.First
).Prev
= 0);
1456 pragma Assert
(N
(Container
.Last
).Next
= 0);
1458 Container
.First
:= J
;
1459 Container
.Last
:= I
;
1461 Swap
(L
=> I
, R
=> J
);
1469 Swap
(L
=> J
, R
=> I
);
1478 pragma Assert
(N
(Container
.First
).Prev
= 0);
1479 pragma Assert
(N
(Container
.Last
).Next
= 0);
1480 end Reverse_Elements
;
1486 function Reverse_Find
1488 Item
: Element_Type
;
1489 Position
: Cursor
:= No_Element
) return Cursor
1491 CFirst
: Count_Type
:= Position
.Node
;
1495 CFirst
:= Container
.Last
;
1498 if Container
.Length
= 0 then
1502 while CFirst
/= 0 loop
1503 if Container
.Nodes
(CFirst
).Element
= Item
then
1504 return (Node
=> CFirst
);
1506 CFirst
:= Container
.Nodes
(CFirst
).Prev
;
1519 (Target
: in out List
;
1521 Source
: in out List
)
1523 SN
: Node_Array
renames Source
.Nodes
;
1526 if Target
'Address = Source
'Address then
1527 raise Program_Error
with "Target and Source denote same container";
1530 if Before
.Node
/= 0 then
1531 pragma Assert
(Vet
(Target
, Before
), "bad cursor in Splice");
1534 pragma Assert
(SN
(Source
.First
).Prev
= 0);
1535 pragma Assert
(SN
(Source
.Last
).Next
= 0);
1537 if Target
.Length
> Count_Type
'Base'Last - Source.Length then
1538 raise Constraint_Error with "new length exceeds maximum";
1541 if Target.Length + Source.Length > Target.Capacity then
1542 raise Constraint_Error;
1546 Insert (Target, Before, SN (Source.Last).Element);
1547 Delete_Last (Source);
1548 exit when Is_Empty (Source);
1553 (Target : in out List;
1555 Source : in out List;
1556 Position : in out Cursor)
1558 Target_Position : Cursor;
1561 if Target'Address = Source'Address then
1562 raise Program_Error with "Target and Source denote same container";
1565 if Position.Node = 0 then
1566 raise Constraint_Error with "Position cursor has no element";
1569 pragma Assert (Vet (Source, Position), "bad Position cursor in Splice");
1571 if Target.Length >= Target.Capacity then
1572 raise Constraint_Error;
1576 (Container => Target,
1578 New_Item => Source.Nodes (Position.Node).Element,
1579 Position => Target_Position);
1581 Delete (Source, Position);
1582 Position := Target_Position;
1586 (Container : in out List;
1590 N : Node_Array renames Container.Nodes;
1593 if Before.Node /= 0 then
1595 (Vet (Container, Before), "bad Before cursor in Splice");
1598 if Position.Node = 0 then
1599 raise Constraint_Error with "Position cursor has no element";
1603 (Vet (Container, Position), "bad Position cursor in Splice");
1605 if Position.Node = Before.Node
1606 or else N (Position.Node).Next = Before.Node
1611 pragma Assert (Container.Length >= 2);
1613 if Before.Node = 0 then
1614 pragma Assert (Position.Node /= Container.Last);
1616 if Position.Node = Container.First then
1617 Container.First := N (Position.Node).Next;
1618 N (Container.First).Prev := 0;
1621 N (N (Position.Node).Prev).Next := N (Position.Node).Next;
1622 N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
1625 N (Container.Last).Next := Position.Node;
1626 N (Position.Node).Prev := Container.Last;
1628 Container.Last := Position.Node;
1629 N (Container.Last).Next := 0;
1634 if Before.Node = Container.First then
1635 pragma Assert (Position.Node /= Container.First);
1637 if Position.Node = Container.Last then
1638 Container.Last := N (Position.Node).Prev;
1639 N (Container.Last).Next := 0;
1642 N (N (Position.Node).Prev).Next := N (Position.Node).Next;
1643 N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
1646 N (Container.First).Prev := Position.Node;
1647 N (Position.Node).Next := Container.First;
1649 Container.First := Position.Node;
1650 N (Container.First).Prev := 0;
1655 if Position.Node = Container.First then
1656 Container.First := N (Position.Node).Next;
1657 N (Container.First).Prev := 0;
1659 elsif Position.Node = Container.Last then
1660 Container.Last := N (Position.Node).Prev;
1661 N (Container.Last).Next := 0;
1664 N (N (Position.Node).Prev).Next := N (Position.Node).Next;
1665 N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
1668 N (N (Before.Node).Prev).Next := Position.Node;
1669 N (Position.Node).Prev := N (Before.Node).Prev;
1671 N (Before.Node).Prev := Position.Node;
1672 N (Position.Node).Next := Before.Node;
1674 pragma Assert (N (Container.First).Prev = 0);
1675 pragma Assert (N (Container.Last).Next = 0);
1683 (Container : in out List;
1689 raise Constraint_Error with "I cursor has no element";
1693 raise Constraint_Error with "J cursor has no element";
1696 if I.Node = J.Node then
1700 pragma Assert (Vet (Container, I), "bad I cursor in Swap");
1701 pragma Assert (Vet (Container, J), "bad J cursor in Swap");
1704 NN : Node_Array renames Container.Nodes;
1705 NI : Node_Type renames NN (I.Node);
1706 NJ : Node_Type renames NN (J.Node);
1708 EI_Copy : constant Element_Type := NI.Element;
1711 NI.Element := NJ.Element;
1712 NJ.Element := EI_Copy;
1720 procedure Swap_Links
1721 (Container : in out List;
1730 raise Constraint_Error with "I cursor has no element";
1734 raise Constraint_Error with "J cursor has no element";
1737 if I.Node = J.Node then
1741 pragma Assert (Vet (Container, I), "bad I cursor in Swap_Links");
1742 pragma Assert (Vet (Container, J), "bad J cursor in Swap_Links");
1744 I_Next := Next (Container, I);
1747 Splice (Container, Before => I, Position => J);
1750 J_Next := Next (Container, J);
1753 Splice (Container, Before => J, Position => I);
1756 pragma Assert (Container.Length >= 3);
1757 Splice (Container, Before => I_Next, Position => J);
1758 Splice (Container, Before => J_Next, Position => I);
1767 function Vet (L : List; Position : Cursor) return Boolean is
1768 N : Node_Array renames L.Nodes;
1771 if L.Length = 0 then
1783 if Position.Node > L.Capacity then
1787 if N (Position.Node).Prev < 0
1788 or else N (Position.Node).Prev > L.Capacity
1793 if N (Position.Node).Next > L.Capacity then
1797 if N (L.First).Prev /= 0 then
1801 if N (L.Last).Next /= 0 then
1805 if N (Position.Node).Prev = 0 and then Position.Node /= L.First then
1809 if N (Position.Node).Next = 0 and then Position.Node /= L.Last then
1813 if L.Length = 1 then
1814 return L.First = L.Last;
1817 if L.First = L.Last then
1821 if N (L.First).Next = 0 then
1825 if N (L.Last).Prev = 0 then
1829 if N (N (L.First).Next).Prev /= L.First then
1833 if N (N (L.Last).Prev).Next /= L.Last then
1837 if L.Length = 2 then
1838 if N (L.First).Next /= L.Last then
1842 if N (L.Last).Prev /= L.First then
1849 if N (L.First).Next = L.Last then
1853 if N (L.Last).Prev = L.First then
1857 if Position.Node = L.First then
1861 if Position.Node = L.Last then
1865 if N (Position.Node).Next = 0 then
1869 if N (Position.Node).Prev = 0 then
1873 if N (N (Position.Node).Next).Prev /= Position.Node then
1877 if N (N (Position.Node).Prev).Next /= Position.Node then
1881 if L.Length = 3 then
1882 if N (L.First).Next /= Position.Node then
1886 if N (L.Last).Prev /= Position.Node then
1894 end Ada.Containers.Formal_Doubly_Linked_Lists;