|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT LIBRARY COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS --
|
|
|
6 -- --
|
|
|
7 -- B o d y --
|
|
|
8 -- --
|
|
145
|
9 -- Copyright (C) 2010-2019, Free Software Foundation, Inc. --
|
|
111
|
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 System; use type System.Address;
|
|
|
29
|
|
|
30 package body Ada.Containers.Formal_Doubly_Linked_Lists with
|
|
|
31 SPARK_Mode => Off
|
|
|
32 is
|
|
|
33 -----------------------
|
|
|
34 -- Local Subprograms --
|
|
|
35 -----------------------
|
|
|
36
|
|
|
37 procedure Allocate
|
|
|
38 (Container : in out List;
|
|
|
39 New_Item : Element_Type;
|
|
|
40 New_Node : out Count_Type);
|
|
|
41
|
|
|
42 procedure Free (Container : in out List; X : Count_Type);
|
|
|
43
|
|
|
44 procedure Insert_Internal
|
|
|
45 (Container : in out List;
|
|
|
46 Before : Count_Type;
|
|
|
47 New_Node : Count_Type);
|
|
|
48
|
|
|
49 function Vet (L : List; Position : Cursor) return Boolean;
|
|
|
50
|
|
|
51 ---------
|
|
|
52 -- "=" --
|
|
|
53 ---------
|
|
|
54
|
|
|
55 function "=" (Left : List; Right : List) return Boolean is
|
|
|
56 LI : Count_Type;
|
|
|
57 RI : Count_Type;
|
|
|
58
|
|
|
59 begin
|
|
|
60 if Left'Address = Right'Address then
|
|
|
61 return True;
|
|
|
62 end if;
|
|
|
63
|
|
|
64 if Left.Length /= Right.Length then
|
|
|
65 return False;
|
|
|
66 end if;
|
|
|
67
|
|
|
68 LI := Left.First;
|
|
|
69 RI := Left.First;
|
|
|
70 while LI /= 0 loop
|
|
|
71 if Left.Nodes (LI).Element /= Right.Nodes (LI).Element then
|
|
|
72 return False;
|
|
|
73 end if;
|
|
|
74
|
|
|
75 LI := Left.Nodes (LI).Next;
|
|
|
76 RI := Right.Nodes (RI).Next;
|
|
|
77 end loop;
|
|
|
78
|
|
|
79 return True;
|
|
|
80 end "=";
|
|
|
81
|
|
|
82 --------------
|
|
|
83 -- Allocate --
|
|
|
84 --------------
|
|
|
85
|
|
|
86 procedure Allocate
|
|
|
87 (Container : in out List;
|
|
|
88 New_Item : Element_Type;
|
|
|
89 New_Node : out Count_Type)
|
|
|
90 is
|
|
|
91 N : Node_Array renames Container.Nodes;
|
|
|
92
|
|
|
93 begin
|
|
|
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;
|
|
|
98
|
|
|
99 else
|
|
|
100 New_Node := abs Container.Free;
|
|
|
101 N (New_Node).Element := New_Item;
|
|
|
102 Container.Free := Container.Free - 1;
|
|
|
103 end if;
|
|
|
104 end Allocate;
|
|
|
105
|
|
|
106 ------------
|
|
|
107 -- Append --
|
|
|
108 ------------
|
|
|
109
|
|
|
110 procedure Append (Container : in out List; New_Item : Element_Type) is
|
|
|
111 begin
|
|
|
112 Insert (Container, No_Element, New_Item, 1);
|
|
|
113 end Append;
|
|
|
114
|
|
|
115 procedure Append
|
|
|
116 (Container : in out List;
|
|
|
117 New_Item : Element_Type;
|
|
|
118 Count : Count_Type)
|
|
|
119 is
|
|
|
120 begin
|
|
|
121 Insert (Container, No_Element, New_Item, Count);
|
|
|
122 end Append;
|
|
|
123
|
|
|
124 ------------
|
|
|
125 -- Assign --
|
|
|
126 ------------
|
|
|
127
|
|
|
128 procedure Assign (Target : in out List; Source : List) is
|
|
|
129 N : Node_Array renames Source.Nodes;
|
|
|
130 J : Count_Type;
|
|
|
131
|
|
|
132 begin
|
|
|
133 if Target'Address = Source'Address then
|
|
|
134 return;
|
|
|
135 end if;
|
|
|
136
|
|
|
137 if Target.Capacity < Source.Length then
|
|
|
138 raise Constraint_Error with -- ???
|
|
|
139 "Source length exceeds Target capacity";
|
|
|
140 end if;
|
|
|
141
|
|
|
142 Clear (Target);
|
|
|
143
|
|
|
144 J := Source.First;
|
|
|
145 while J /= 0 loop
|
|
|
146 Append (Target, N (J).Element, 1);
|
|
|
147 J := N (J).Next;
|
|
|
148 end loop;
|
|
|
149 end Assign;
|
|
|
150
|
|
|
151 -----------
|
|
|
152 -- Clear --
|
|
|
153 -----------
|
|
|
154
|
|
|
155 procedure Clear (Container : in out List) is
|
|
|
156 N : Node_Array renames Container.Nodes;
|
|
|
157 X : Count_Type;
|
|
|
158
|
|
|
159 begin
|
|
|
160 if Container.Length = 0 then
|
|
|
161 pragma Assert (Container.First = 0);
|
|
|
162 pragma Assert (Container.Last = 0);
|
|
|
163 return;
|
|
|
164 end if;
|
|
|
165
|
|
|
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);
|
|
|
170
|
|
|
171 while Container.Length > 1 loop
|
|
|
172 X := Container.First;
|
|
|
173
|
|
|
174 Container.First := N (X).Next;
|
|
|
175 N (Container.First).Prev := 0;
|
|
|
176
|
|
|
177 Container.Length := Container.Length - 1;
|
|
|
178
|
|
|
179 Free (Container, X);
|
|
|
180 end loop;
|
|
|
181
|
|
|
182 X := Container.First;
|
|
|
183
|
|
|
184 Container.First := 0;
|
|
|
185 Container.Last := 0;
|
|
|
186 Container.Length := 0;
|
|
|
187
|
|
|
188 Free (Container, X);
|
|
|
189 end Clear;
|
|
|
190
|
|
|
191 --------------
|
|
|
192 -- Contains --
|
|
|
193 --------------
|
|
|
194
|
|
|
195 function Contains
|
|
|
196 (Container : List;
|
|
|
197 Item : Element_Type) return Boolean
|
|
|
198 is
|
|
|
199 begin
|
|
|
200 return Find (Container, Item) /= No_Element;
|
|
|
201 end Contains;
|
|
|
202
|
|
|
203 ----------
|
|
|
204 -- Copy --
|
|
|
205 ----------
|
|
|
206
|
|
|
207 function Copy
|
|
|
208 (Source : List;
|
|
|
209 Capacity : Count_Type := 0) return List
|
|
|
210 is
|
|
|
211 C : constant Count_Type := Count_Type'Max (Source.Capacity, Capacity);
|
|
|
212 N : Count_Type;
|
|
|
213 P : List (C);
|
|
|
214
|
|
|
215 begin
|
|
|
216 if 0 < Capacity and then Capacity < Source.Capacity then
|
|
|
217 raise Capacity_Error;
|
|
|
218 end if;
|
|
|
219
|
|
|
220 N := 1;
|
|
|
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;
|
|
|
225 N := N + 1;
|
|
|
226 end loop;
|
|
|
227
|
|
|
228 P.Free := Source.Free;
|
|
|
229 P.Length := Source.Length;
|
|
|
230 P.First := Source.First;
|
|
|
231 P.Last := Source.Last;
|
|
|
232
|
|
|
233 if P.Free >= 0 then
|
|
|
234 N := Source.Capacity + 1;
|
|
|
235 while N <= C loop
|
|
|
236 Free (P, N);
|
|
|
237 N := N + 1;
|
|
|
238 end loop;
|
|
|
239 end if;
|
|
|
240
|
|
|
241 return P;
|
|
|
242 end Copy;
|
|
|
243
|
|
|
244 ------------
|
|
|
245 -- Delete --
|
|
|
246 ------------
|
|
|
247
|
|
|
248 procedure Delete (Container : in out List; Position : in out Cursor) is
|
|
|
249 begin
|
|
|
250 Delete
|
|
|
251 (Container => Container,
|
|
|
252 Position => Position,
|
|
|
253 Count => 1);
|
|
|
254 end Delete;
|
|
|
255
|
|
|
256 procedure Delete
|
|
|
257 (Container : in out List;
|
|
|
258 Position : in out Cursor;
|
|
|
259 Count : Count_Type)
|
|
|
260 is
|
|
|
261 N : Node_Array renames Container.Nodes;
|
|
|
262 X : Count_Type;
|
|
|
263
|
|
|
264 begin
|
|
|
265 if not Has_Element (Container => Container,
|
|
|
266 Position => Position)
|
|
|
267 then
|
|
|
268 raise Constraint_Error with "Position cursor has no element";
|
|
|
269 end if;
|
|
|
270
|
|
|
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);
|
|
|
276
|
|
|
277 if Position.Node = Container.First then
|
|
|
278 Delete_First (Container, Count);
|
|
|
279 Position := No_Element;
|
|
|
280 return;
|
|
|
281 end if;
|
|
|
282
|
|
|
283 if Count = 0 then
|
|
|
284 Position := No_Element;
|
|
|
285 return;
|
|
|
286 end if;
|
|
|
287
|
|
|
288 for Index in 1 .. Count loop
|
|
|
289 pragma Assert (Container.Length >= 2);
|
|
|
290
|
|
|
291 X := Position.Node;
|
|
|
292 Container.Length := Container.Length - 1;
|
|
|
293
|
|
|
294 if X = Container.Last then
|
|
|
295 Position := No_Element;
|
|
|
296
|
|
|
297 Container.Last := N (X).Prev;
|
|
|
298 N (Container.Last).Next := 0;
|
|
|
299
|
|
|
300 Free (Container, X);
|
|
|
301 return;
|
|
|
302 end if;
|
|
|
303
|
|
|
304 Position.Node := N (X).Next;
|
|
|
305 pragma Assert (N (Position.Node).Prev >= 0);
|
|
|
306
|
|
|
307 N (N (X).Next).Prev := N (X).Prev;
|
|
|
308 N (N (X).Prev).Next := N (X).Next;
|
|
|
309
|
|
|
310 Free (Container, X);
|
|
|
311 end loop;
|
|
|
312
|
|
|
313 Position := No_Element;
|
|
|
314 end Delete;
|
|
|
315
|
|
|
316 ------------------
|
|
|
317 -- Delete_First --
|
|
|
318 ------------------
|
|
|
319
|
|
|
320 procedure Delete_First (Container : in out List) is
|
|
|
321 begin
|
|
|
322 Delete_First
|
|
|
323 (Container => Container,
|
|
|
324 Count => 1);
|
|
|
325 end Delete_First;
|
|
|
326
|
|
|
327 procedure Delete_First (Container : in out List; Count : Count_Type) is
|
|
|
328 N : Node_Array renames Container.Nodes;
|
|
|
329 X : Count_Type;
|
|
|
330
|
|
|
331 begin
|
|
|
332 if Count >= Container.Length then
|
|
|
333 Clear (Container);
|
|
|
334 return;
|
|
|
335 end if;
|
|
|
336
|
|
|
337 if Count = 0 then
|
|
|
338 return;
|
|
|
339 end if;
|
|
|
340
|
|
|
341 for J in 1 .. Count loop
|
|
|
342 X := Container.First;
|
|
|
343 pragma Assert (N (N (X).Next).Prev = Container.First);
|
|
|
344
|
|
|
345 Container.First := N (X).Next;
|
|
|
346 N (Container.First).Prev := 0;
|
|
|
347
|
|
|
348 Container.Length := Container.Length - 1;
|
|
|
349
|
|
|
350 Free (Container, X);
|
|
|
351 end loop;
|
|
|
352 end Delete_First;
|
|
|
353
|
|
|
354 -----------------
|
|
|
355 -- Delete_Last --
|
|
|
356 -----------------
|
|
|
357
|
|
|
358 procedure Delete_Last (Container : in out List) is
|
|
|
359 begin
|
|
|
360 Delete_Last
|
|
|
361 (Container => Container,
|
|
|
362 Count => 1);
|
|
|
363 end Delete_Last;
|
|
|
364
|
|
|
365 procedure Delete_Last (Container : in out List; Count : Count_Type) is
|
|
|
366 N : Node_Array renames Container.Nodes;
|
|
|
367 X : Count_Type;
|
|
|
368
|
|
|
369 begin
|
|
|
370 if Count >= Container.Length then
|
|
|
371 Clear (Container);
|
|
|
372 return;
|
|
|
373 end if;
|
|
|
374
|
|
|
375 if Count = 0 then
|
|
|
376 return;
|
|
|
377 end if;
|
|
|
378
|
|
|
379 for J in 1 .. Count loop
|
|
|
380 X := Container.Last;
|
|
|
381 pragma Assert (N (N (X).Prev).Next = Container.Last);
|
|
|
382
|
|
|
383 Container.Last := N (X).Prev;
|
|
|
384 N (Container.Last).Next := 0;
|
|
|
385
|
|
|
386 Container.Length := Container.Length - 1;
|
|
|
387
|
|
|
388 Free (Container, X);
|
|
|
389 end loop;
|
|
|
390 end Delete_Last;
|
|
|
391
|
|
|
392 -------------
|
|
|
393 -- Element --
|
|
|
394 -------------
|
|
|
395
|
|
|
396 function Element
|
|
|
397 (Container : List;
|
|
|
398 Position : Cursor) return Element_Type
|
|
|
399 is
|
|
|
400 begin
|
|
|
401 if not Has_Element (Container => Container, Position => Position) then
|
|
|
402 raise Constraint_Error with "Position cursor has no element";
|
|
|
403 end if;
|
|
|
404
|
|
|
405 return Container.Nodes (Position.Node).Element;
|
|
|
406 end Element;
|
|
|
407
|
|
|
408 ----------
|
|
|
409 -- Find --
|
|
|
410 ----------
|
|
|
411
|
|
|
412 function Find
|
|
|
413 (Container : List;
|
|
|
414 Item : Element_Type;
|
|
|
415 Position : Cursor := No_Element) return Cursor
|
|
|
416 is
|
|
|
417 From : Count_Type := Position.Node;
|
|
|
418
|
|
|
419 begin
|
|
|
420 if From = 0 and Container.Length = 0 then
|
|
|
421 return No_Element;
|
|
|
422 end if;
|
|
|
423
|
|
|
424 if From = 0 then
|
|
|
425 From := Container.First;
|
|
|
426 end if;
|
|
|
427
|
|
|
428 if Position.Node /= 0 and then not Has_Element (Container, Position) then
|
|
|
429 raise Constraint_Error with "Position cursor has no element";
|
|
|
430 end if;
|
|
|
431
|
|
|
432 while From /= 0 loop
|
|
|
433 if Container.Nodes (From).Element = Item then
|
|
|
434 return (Node => From);
|
|
|
435 end if;
|
|
|
436
|
|
|
437 From := Container.Nodes (From).Next;
|
|
|
438 end loop;
|
|
|
439
|
|
|
440 return No_Element;
|
|
|
441 end Find;
|
|
|
442
|
|
|
443 -----------
|
|
|
444 -- First --
|
|
|
445 -----------
|
|
|
446
|
|
|
447 function First (Container : List) return Cursor is
|
|
|
448 begin
|
|
|
449 if Container.First = 0 then
|
|
|
450 return No_Element;
|
|
|
451 end if;
|
|
|
452
|
|
|
453 return (Node => Container.First);
|
|
|
454 end First;
|
|
|
455
|
|
|
456 -------------------
|
|
|
457 -- First_Element --
|
|
|
458 -------------------
|
|
|
459
|
|
|
460 function First_Element (Container : List) return Element_Type is
|
|
|
461 F : constant Count_Type := Container.First;
|
|
|
462
|
|
|
463 begin
|
|
|
464 if F = 0 then
|
|
|
465 raise Constraint_Error with "list is empty";
|
|
|
466 else
|
|
|
467 return Container.Nodes (F).Element;
|
|
|
468 end if;
|
|
|
469 end First_Element;
|
|
|
470
|
|
|
471 ------------------
|
|
|
472 -- Formal_Model --
|
|
|
473 ------------------
|
|
|
474
|
|
|
475 package body Formal_Model is
|
|
|
476
|
|
|
477 ----------------------------
|
|
|
478 -- Lift_Abstraction_Level --
|
|
|
479 ----------------------------
|
|
|
480
|
|
|
481 procedure Lift_Abstraction_Level (Container : List) is null;
|
|
|
482
|
|
|
483 -------------------------
|
|
|
484 -- M_Elements_In_Union --
|
|
|
485 -------------------------
|
|
|
486
|
|
|
487 function M_Elements_In_Union
|
|
|
488 (Container : M.Sequence;
|
|
|
489 Left : M.Sequence;
|
|
|
490 Right : M.Sequence) return Boolean
|
|
|
491 is
|
|
|
492 Elem : Element_Type;
|
|
|
493
|
|
|
494 begin
|
|
|
495 for Index in 1 .. M.Length (Container) loop
|
|
|
496 Elem := Element (Container, Index);
|
|
|
497
|
|
|
498 if not M.Contains (Left, 1, M.Length (Left), Elem)
|
|
|
499 and then not M.Contains (Right, 1, M.Length (Right), Elem)
|
|
|
500 then
|
|
|
501 return False;
|
|
|
502 end if;
|
|
|
503 end loop;
|
|
|
504
|
|
|
505 return True;
|
|
|
506 end M_Elements_In_Union;
|
|
|
507
|
|
|
508 -------------------------
|
|
|
509 -- M_Elements_Included --
|
|
|
510 -------------------------
|
|
|
511
|
|
|
512 function M_Elements_Included
|
|
|
513 (Left : M.Sequence;
|
|
|
514 L_Fst : Positive_Count_Type := 1;
|
|
|
515 L_Lst : Count_Type;
|
|
|
516 Right : M.Sequence;
|
|
|
517 R_Fst : Positive_Count_Type := 1;
|
|
|
518 R_Lst : Count_Type) return Boolean
|
|
|
519 is
|
|
|
520 begin
|
|
|
521 for I in L_Fst .. L_Lst loop
|
|
|
522 declare
|
|
|
523 Found : Boolean := False;
|
|
|
524 J : Count_Type := R_Fst - 1;
|
|
|
525
|
|
|
526 begin
|
|
|
527 while not Found and J < R_Lst loop
|
|
|
528 J := J + 1;
|
|
|
529 if Element (Left, I) = Element (Right, J) then
|
|
|
530 Found := True;
|
|
|
531 end if;
|
|
|
532 end loop;
|
|
|
533
|
|
|
534 if not Found then
|
|
|
535 return False;
|
|
|
536 end if;
|
|
|
537 end;
|
|
|
538 end loop;
|
|
|
539
|
|
|
540 return True;
|
|
|
541 end M_Elements_Included;
|
|
|
542
|
|
|
543 -------------------------
|
|
|
544 -- M_Elements_Reversed --
|
|
|
545 -------------------------
|
|
|
546
|
|
|
547 function M_Elements_Reversed
|
|
|
548 (Left : M.Sequence;
|
|
|
549 Right : M.Sequence) return Boolean
|
|
|
550 is
|
|
|
551 L : constant Count_Type := M.Length (Left);
|
|
|
552
|
|
|
553 begin
|
|
|
554 if L /= M.Length (Right) then
|
|
|
555 return False;
|
|
|
556 end if;
|
|
|
557
|
|
|
558 for I in 1 .. L loop
|
|
|
559 if Element (Left, I) /= Element (Right, L - I + 1) then
|
|
|
560 return False;
|
|
|
561 end if;
|
|
|
562 end loop;
|
|
|
563
|
|
|
564 return True;
|
|
|
565 end M_Elements_Reversed;
|
|
|
566
|
|
|
567 ------------------------
|
|
131
|
568 -- M_Elements_Swapped --
|
|
111
|
569 ------------------------
|
|
|
570
|
|
|
571 function M_Elements_Swapped
|
|
|
572 (Left : M.Sequence;
|
|
|
573 Right : M.Sequence;
|
|
|
574 X : Positive_Count_Type;
|
|
|
575 Y : Positive_Count_Type) return Boolean
|
|
|
576 is
|
|
|
577 begin
|
|
|
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)
|
|
|
581 then
|
|
|
582 return False;
|
|
|
583 end if;
|
|
|
584
|
|
|
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)
|
|
|
588 then
|
|
|
589 return False;
|
|
|
590 end if;
|
|
|
591 end loop;
|
|
|
592
|
|
|
593 return True;
|
|
|
594 end M_Elements_Swapped;
|
|
|
595
|
|
|
596 -----------
|
|
|
597 -- Model --
|
|
|
598 -----------
|
|
|
599
|
|
|
600 function Model (Container : List) return M.Sequence is
|
|
|
601 Position : Count_Type := Container.First;
|
|
|
602 R : M.Sequence;
|
|
|
603
|
|
|
604 begin
|
|
|
605 -- Can't use First, Next or Element here, since they depend on models
|
|
|
606 -- for their postconditions.
|
|
|
607
|
|
|
608 while Position /= 0 loop
|
|
|
609 R := M.Add (R, Container.Nodes (Position).Element);
|
|
|
610 Position := Container.Nodes (Position).Next;
|
|
|
611 end loop;
|
|
|
612
|
|
|
613 return R;
|
|
|
614 end Model;
|
|
|
615
|
|
|
616 -----------------------
|
|
|
617 -- Mapping_Preserved --
|
|
|
618 -----------------------
|
|
|
619
|
|
|
620 function Mapping_Preserved
|
|
|
621 (M_Left : M.Sequence;
|
|
|
622 M_Right : M.Sequence;
|
|
|
623 P_Left : P.Map;
|
|
|
624 P_Right : P.Map) return Boolean
|
|
|
625 is
|
|
|
626 begin
|
|
|
627 for C of P_Left loop
|
|
|
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))
|
|
|
633 then
|
|
|
634 return False;
|
|
|
635 end if;
|
|
|
636 end loop;
|
|
|
637
|
|
|
638 for C of P_Right loop
|
|
|
639 if not P.Has_Key (P_Left, C) then
|
|
|
640 return False;
|
|
|
641 end if;
|
|
|
642 end loop;
|
|
|
643
|
|
|
644 return True;
|
|
|
645 end Mapping_Preserved;
|
|
|
646
|
|
|
647 -------------------------
|
|
|
648 -- P_Positions_Shifted --
|
|
|
649 -------------------------
|
|
|
650
|
|
|
651 function P_Positions_Shifted
|
|
|
652 (Small : P.Map;
|
|
|
653 Big : P.Map;
|
|
|
654 Cut : Positive_Count_Type;
|
|
|
655 Count : Count_Type := 1) return Boolean
|
|
|
656 is
|
|
|
657 begin
|
|
|
658 for Cu of Small loop
|
|
|
659 if not P.Has_Key (Big, Cu) then
|
|
|
660 return False;
|
|
|
661 end if;
|
|
|
662 end loop;
|
|
|
663
|
|
|
664 for Cu of Big loop
|
|
|
665 declare
|
|
|
666 Pos : constant Positive_Count_Type := P.Get (Big, Cu);
|
|
|
667
|
|
|
668 begin
|
|
|
669 if Pos < Cut then
|
|
|
670 if not P.Has_Key (Small, Cu)
|
|
|
671 or else Pos /= P.Get (Small, Cu)
|
|
|
672 then
|
|
|
673 return False;
|
|
|
674 end if;
|
|
|
675
|
|
|
676 elsif Pos >= Cut + Count then
|
|
|
677 if not P.Has_Key (Small, Cu)
|
|
|
678 or else Pos /= P.Get (Small, Cu) + Count
|
|
|
679 then
|
|
|
680 return False;
|
|
|
681 end if;
|
|
|
682
|
|
|
683 else
|
|
|
684 if P.Has_Key (Small, Cu) then
|
|
|
685 return False;
|
|
|
686 end if;
|
|
|
687 end if;
|
|
|
688 end;
|
|
|
689 end loop;
|
|
|
690
|
|
|
691 return True;
|
|
|
692 end P_Positions_Shifted;
|
|
|
693
|
|
|
694 -------------------------
|
|
|
695 -- P_Positions_Swapped --
|
|
|
696 -------------------------
|
|
|
697
|
|
|
698 function P_Positions_Swapped
|
|
|
699 (Left : P.Map;
|
|
|
700 Right : P.Map;
|
|
|
701 X : Cursor;
|
|
|
702 Y : Cursor) return Boolean
|
|
|
703 is
|
|
|
704 begin
|
|
|
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)
|
|
|
709 then
|
|
|
710 return False;
|
|
|
711 end if;
|
|
|
712
|
|
|
713 if P.Get (Left, X) /= P.Get (Right, Y)
|
|
|
714 or P.Get (Left, Y) /= P.Get (Right, X)
|
|
|
715 then
|
|
|
716 return False;
|
|
|
717 end if;
|
|
|
718
|
|
|
719 for C of Left loop
|
|
|
720 if not P.Has_Key (Right, C) then
|
|
|
721 return False;
|
|
|
722 end if;
|
|
|
723 end loop;
|
|
|
724
|
|
|
725 for C of Right loop
|
|
|
726 if not P.Has_Key (Left, C)
|
|
|
727 or else (C /= X
|
|
|
728 and C /= Y
|
|
|
729 and P.Get (Left, C) /= P.Get (Right, C))
|
|
|
730 then
|
|
|
731 return False;
|
|
|
732 end if;
|
|
|
733 end loop;
|
|
|
734
|
|
|
735 return True;
|
|
|
736 end P_Positions_Swapped;
|
|
|
737
|
|
|
738 ---------------------------
|
|
|
739 -- P_Positions_Truncated --
|
|
|
740 ---------------------------
|
|
|
741
|
|
|
742 function P_Positions_Truncated
|
|
|
743 (Small : P.Map;
|
|
|
744 Big : P.Map;
|
|
|
745 Cut : Positive_Count_Type;
|
|
|
746 Count : Count_Type := 1) return Boolean
|
|
|
747 is
|
|
|
748 begin
|
|
|
749 for Cu of Small loop
|
|
|
750 if not P.Has_Key (Big, Cu) then
|
|
|
751 return False;
|
|
|
752 end if;
|
|
|
753 end loop;
|
|
|
754
|
|
|
755 for Cu of Big loop
|
|
|
756 declare
|
|
|
757 Pos : constant Positive_Count_Type := P.Get (Big, Cu);
|
|
|
758
|
|
|
759 begin
|
|
|
760 if Pos < Cut then
|
|
|
761 if not P.Has_Key (Small, Cu)
|
|
|
762 or else Pos /= P.Get (Small, Cu)
|
|
|
763 then
|
|
|
764 return False;
|
|
|
765 end if;
|
|
|
766
|
|
|
767 elsif Pos >= Cut + Count then
|
|
|
768 return False;
|
|
|
769
|
|
|
770 elsif P.Has_Key (Small, Cu) then
|
|
|
771 return False;
|
|
|
772 end if;
|
|
|
773 end;
|
|
|
774 end loop;
|
|
|
775
|
|
|
776 return True;
|
|
|
777 end P_Positions_Truncated;
|
|
|
778
|
|
|
779 ---------------
|
|
|
780 -- Positions --
|
|
|
781 ---------------
|
|
|
782
|
|
|
783 function Positions (Container : List) return P.Map is
|
|
|
784 I : Count_Type := 1;
|
|
|
785 Position : Count_Type := Container.First;
|
|
|
786 R : P.Map;
|
|
|
787
|
|
|
788 begin
|
|
|
789 -- Can't use First, Next or Element here, since they depend on models
|
|
|
790 -- for their postconditions.
|
|
|
791
|
|
|
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;
|
|
|
796 I := I + 1;
|
|
|
797 end loop;
|
|
|
798
|
|
|
799 return R;
|
|
|
800 end Positions;
|
|
|
801
|
|
|
802 end Formal_Model;
|
|
|
803
|
|
|
804 ----------
|
|
|
805 -- Free --
|
|
|
806 ----------
|
|
|
807
|
|
|
808 procedure Free (Container : in out List; X : Count_Type) is
|
|
|
809 pragma Assert (X > 0);
|
|
|
810 pragma Assert (X <= Container.Capacity);
|
|
|
811
|
|
|
812 N : Node_Array renames Container.Nodes;
|
|
|
813
|
|
|
814 begin
|
|
|
815 N (X).Prev := -1; -- Node is deallocated (not on active list)
|
|
|
816
|
|
|
817 if Container.Free >= 0 then
|
|
|
818 N (X).Next := Container.Free;
|
|
|
819 Container.Free := X;
|
|
|
820
|
|
|
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;
|
|
|
824
|
|
|
825 else
|
|
|
826 Container.Free := abs Container.Free;
|
|
|
827
|
|
|
828 if Container.Free > Container.Capacity then
|
|
|
829 Container.Free := 0;
|
|
|
830
|
|
|
831 else
|
|
|
832 for J in Container.Free .. Container.Capacity - 1 loop
|
|
|
833 N (J).Next := J + 1;
|
|
|
834 end loop;
|
|
|
835
|
|
|
836 N (Container.Capacity).Next := 0;
|
|
|
837 end if;
|
|
|
838
|
|
|
839 N (X).Next := Container.Free;
|
|
|
840 Container.Free := X;
|
|
|
841 end if;
|
|
|
842 end Free;
|
|
|
843
|
|
|
844 ---------------------
|
|
|
845 -- Generic_Sorting --
|
|
|
846 ---------------------
|
|
|
847
|
|
|
848 package body Generic_Sorting with SPARK_Mode => Off is
|
|
|
849
|
|
|
850 ------------------
|
|
|
851 -- Formal_Model --
|
|
|
852 ------------------
|
|
|
853
|
|
|
854 package body Formal_Model is
|
|
|
855
|
|
|
856 -----------------------
|
|
|
857 -- M_Elements_Sorted --
|
|
|
858 -----------------------
|
|
|
859
|
|
|
860 function M_Elements_Sorted (Container : M.Sequence) return Boolean is
|
|
|
861 begin
|
|
|
862 if M.Length (Container) = 0 then
|
|
|
863 return True;
|
|
|
864 end if;
|
|
|
865
|
|
|
866 declare
|
|
|
867 E1 : Element_Type := Element (Container, 1);
|
|
|
868
|
|
|
869 begin
|
|
|
870 for I in 2 .. M.Length (Container) loop
|
|
|
871 declare
|
|
|
872 E2 : constant Element_Type := Element (Container, I);
|
|
|
873
|
|
|
874 begin
|
|
|
875 if E2 < E1 then
|
|
|
876 return False;
|
|
|
877 end if;
|
|
|
878
|
|
|
879 E1 := E2;
|
|
|
880 end;
|
|
|
881 end loop;
|
|
|
882 end;
|
|
|
883
|
|
|
884 return True;
|
|
|
885 end M_Elements_Sorted;
|
|
|
886
|
|
|
887 end Formal_Model;
|
|
|
888
|
|
|
889 ---------------
|
|
|
890 -- Is_Sorted --
|
|
|
891 ---------------
|
|
|
892
|
|
|
893 function Is_Sorted (Container : List) return Boolean is
|
|
|
894 Nodes : Node_Array renames Container.Nodes;
|
|
|
895 Node : Count_Type := Container.First;
|
|
|
896
|
|
|
897 begin
|
|
|
898 for J in 2 .. Container.Length loop
|
|
|
899 if Nodes (Nodes (Node).Next).Element < Nodes (Node).Element then
|
|
|
900 return False;
|
|
|
901 else
|
|
|
902 Node := Nodes (Node).Next;
|
|
|
903 end if;
|
|
|
904 end loop;
|
|
|
905
|
|
|
906 return True;
|
|
|
907 end Is_Sorted;
|
|
|
908
|
|
|
909 -----------
|
|
|
910 -- Merge --
|
|
|
911 -----------
|
|
|
912
|
|
|
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;
|
|
|
916 LI : Cursor;
|
|
|
917 RI : Cursor;
|
|
|
918
|
|
|
919 begin
|
|
|
920 if Target'Address = Source'Address then
|
|
|
921 raise Program_Error with "Target and Source denote same container";
|
|
|
922 end if;
|
|
|
923
|
|
|
924 LI := First (Target);
|
|
|
925 RI := First (Source);
|
|
|
926 while RI.Node /= 0 loop
|
|
|
927 pragma Assert
|
|
|
928 (RN (RI.Node).Next = 0
|
|
|
929 or else not (RN (RN (RI.Node).Next).Element <
|
|
|
930 RN (RI.Node).Element));
|
|
|
931
|
|
|
932 if LI.Node = 0 then
|
|
|
933 Splice (Target, No_Element, Source);
|
|
|
934 return;
|
|
|
935 end if;
|
|
|
936
|
|
|
937 pragma Assert
|
|
|
938 (LN (LI.Node).Next = 0
|
|
|
939 or else not (LN (LN (LI.Node).Next).Element <
|
|
|
940 LN (LI.Node).Element));
|
|
|
941
|
|
|
942 if RN (RI.Node).Element < LN (LI.Node).Element then
|
|
|
943 declare
|
|
|
944 RJ : Cursor := RI;
|
|
|
945 pragma Warnings (Off, RJ);
|
|
|
946 begin
|
|
|
947 RI.Node := RN (RI.Node).Next;
|
|
|
948 Splice (Target, LI, Source, RJ);
|
|
|
949 end;
|
|
|
950
|
|
|
951 else
|
|
|
952 LI.Node := LN (LI.Node).Next;
|
|
|
953 end if;
|
|
|
954 end loop;
|
|
|
955 end Merge;
|
|
|
956
|
|
|
957 ----------
|
|
|
958 -- Sort --
|
|
|
959 ----------
|
|
|
960
|
|
|
961 procedure Sort (Container : in out List) is
|
|
|
962 N : Node_Array renames Container.Nodes;
|
|
|
963
|
|
|
964 procedure Partition (Pivot : Count_Type; Back : Count_Type);
|
|
|
965 procedure Sort (Front : Count_Type; Back : Count_Type);
|
|
|
966
|
|
|
967 ---------------
|
|
|
968 -- Partition --
|
|
|
969 ---------------
|
|
|
970
|
|
|
971 procedure Partition (Pivot : Count_Type; Back : Count_Type) is
|
|
|
972 Node : Count_Type;
|
|
|
973
|
|
|
974 begin
|
|
|
975 Node := N (Pivot).Next;
|
|
|
976 while Node /= Back loop
|
|
|
977 if N (Node).Element < N (Pivot).Element then
|
|
|
978 declare
|
|
|
979 Prev : constant Count_Type := N (Node).Prev;
|
|
|
980 Next : constant Count_Type := N (Node).Next;
|
|
|
981
|
|
|
982 begin
|
|
|
983 N (Prev).Next := Next;
|
|
|
984
|
|
|
985 if Next = 0 then
|
|
|
986 Container.Last := Prev;
|
|
|
987 else
|
|
|
988 N (Next).Prev := Prev;
|
|
|
989 end if;
|
|
|
990
|
|
|
991 N (Node).Next := Pivot;
|
|
|
992 N (Node).Prev := N (Pivot).Prev;
|
|
|
993
|
|
|
994 N (Pivot).Prev := Node;
|
|
|
995
|
|
|
996 if N (Node).Prev = 0 then
|
|
|
997 Container.First := Node;
|
|
|
998 else
|
|
|
999 N (N (Node).Prev).Next := Node;
|
|
|
1000 end if;
|
|
|
1001
|
|
|
1002 Node := Next;
|
|
|
1003 end;
|
|
|
1004
|
|
|
1005 else
|
|
|
1006 Node := N (Node).Next;
|
|
|
1007 end if;
|
|
|
1008 end loop;
|
|
|
1009 end Partition;
|
|
|
1010
|
|
|
1011 ----------
|
|
|
1012 -- Sort --
|
|
|
1013 ----------
|
|
|
1014
|
|
|
1015 procedure Sort (Front : Count_Type; Back : Count_Type) is
|
|
|
1016 Pivot : Count_Type;
|
|
|
1017
|
|
|
1018 begin
|
|
|
1019 if Front = 0 then
|
|
|
1020 Pivot := Container.First;
|
|
|
1021 else
|
|
|
1022 Pivot := N (Front).Next;
|
|
|
1023 end if;
|
|
|
1024
|
|
|
1025 if Pivot /= Back then
|
|
|
1026 Partition (Pivot, Back);
|
|
|
1027 Sort (Front, Pivot);
|
|
|
1028 Sort (Pivot, Back);
|
|
|
1029 end if;
|
|
|
1030 end Sort;
|
|
|
1031
|
|
|
1032 -- Start of processing for Sort
|
|
|
1033
|
|
|
1034 begin
|
|
|
1035 if Container.Length <= 1 then
|
|
|
1036 return;
|
|
|
1037 end if;
|
|
|
1038
|
|
|
1039 pragma Assert (N (Container.First).Prev = 0);
|
|
|
1040 pragma Assert (N (Container.Last).Next = 0);
|
|
|
1041
|
|
|
1042 Sort (Front => 0, Back => 0);
|
|
|
1043
|
|
|
1044 pragma Assert (N (Container.First).Prev = 0);
|
|
|
1045 pragma Assert (N (Container.Last).Next = 0);
|
|
|
1046 end Sort;
|
|
|
1047
|
|
|
1048 end Generic_Sorting;
|
|
|
1049
|
|
|
1050 -----------------
|
|
|
1051 -- Has_Element --
|
|
|
1052 -----------------
|
|
|
1053
|
|
|
1054 function Has_Element (Container : List; Position : Cursor) return Boolean is
|
|
|
1055 begin
|
|
|
1056 if Position.Node = 0 then
|
|
|
1057 return False;
|
|
|
1058 end if;
|
|
|
1059
|
|
|
1060 return Container.Nodes (Position.Node).Prev /= -1;
|
|
|
1061 end Has_Element;
|
|
|
1062
|
|
|
1063 ------------
|
|
|
1064 -- Insert --
|
|
|
1065 ------------
|
|
|
1066
|
|
|
1067 procedure Insert
|
|
|
1068 (Container : in out List;
|
|
|
1069 Before : Cursor;
|
|
|
1070 New_Item : Element_Type;
|
|
|
1071 Position : out Cursor;
|
|
|
1072 Count : Count_Type)
|
|
|
1073 is
|
|
|
1074 J : Count_Type;
|
|
|
1075
|
|
|
1076 begin
|
|
|
1077 if Before.Node /= 0 then
|
|
|
1078 pragma Assert (Vet (Container, Before), "bad cursor in Insert");
|
|
|
1079 end if;
|
|
|
1080
|
|
|
1081 if Count = 0 then
|
|
|
1082 Position := Before;
|
|
|
1083 return;
|
|
|
1084 end if;
|
|
|
1085
|
|
|
1086 if Container.Length > Container.Capacity - Count then
|
|
|
1087 raise Constraint_Error with "new length exceeds capacity";
|
|
|
1088 end if;
|
|
|
1089
|
|
|
1090 Allocate (Container, New_Item, New_Node => J);
|
|
|
1091 Insert_Internal (Container, Before.Node, New_Node => J);
|
|
|
1092 Position := (Node => J);
|
|
|
1093
|
|
|
1094 for Index in 2 .. Count loop
|
|
|
1095 Allocate (Container, New_Item, New_Node => J);
|
|
|
1096 Insert_Internal (Container, Before.Node, New_Node => J);
|
|
|
1097 end loop;
|
|
|
1098 end Insert;
|
|
|
1099
|
|
|
1100 procedure Insert
|
|
|
1101 (Container : in out List;
|
|
|
1102 Before : Cursor;
|
|
|
1103 New_Item : Element_Type;
|
|
|
1104 Position : out Cursor)
|
|
|
1105 is
|
|
|
1106 begin
|
|
|
1107 Insert
|
|
|
1108 (Container => Container,
|
|
|
1109 Before => Before,
|
|
|
1110 New_Item => New_Item,
|
|
|
1111 Position => Position,
|
|
|
1112 Count => 1);
|
|
|
1113 end Insert;
|
|
|
1114
|
|
|
1115 procedure Insert
|
|
|
1116 (Container : in out List;
|
|
|
1117 Before : Cursor;
|
|
|
1118 New_Item : Element_Type;
|
|
|
1119 Count : Count_Type)
|
|
|
1120 is
|
|
|
1121 Position : Cursor;
|
|
|
1122
|
|
|
1123 begin
|
|
|
1124 Insert (Container, Before, New_Item, Position, Count);
|
|
|
1125 end Insert;
|
|
|
1126
|
|
|
1127 procedure Insert
|
|
|
1128 (Container : in out List;
|
|
|
1129 Before : Cursor;
|
|
|
1130 New_Item : Element_Type)
|
|
|
1131 is
|
|
|
1132 Position : Cursor;
|
|
|
1133
|
|
|
1134 begin
|
|
|
1135 Insert (Container, Before, New_Item, Position, 1);
|
|
|
1136 end Insert;
|
|
|
1137
|
|
|
1138 ---------------------
|
|
|
1139 -- Insert_Internal --
|
|
|
1140 ---------------------
|
|
|
1141
|
|
|
1142 procedure Insert_Internal
|
|
|
1143 (Container : in out List;
|
|
|
1144 Before : Count_Type;
|
|
|
1145 New_Node : Count_Type)
|
|
|
1146 is
|
|
|
1147 N : Node_Array renames Container.Nodes;
|
|
|
1148
|
|
|
1149 begin
|
|
|
1150 if Container.Length = 0 then
|
|
|
1151 pragma Assert (Before = 0);
|
|
|
1152 pragma Assert (Container.First = 0);
|
|
|
1153 pragma Assert (Container.Last = 0);
|
|
|
1154
|
|
|
1155 Container.First := New_Node;
|
|
|
1156 Container.Last := New_Node;
|
|
|
1157
|
|
|
1158 N (Container.First).Prev := 0;
|
|
|
1159 N (Container.Last).Next := 0;
|
|
|
1160
|
|
|
1161 elsif Before = 0 then
|
|
|
1162 pragma Assert (N (Container.Last).Next = 0);
|
|
|
1163
|
|
|
1164 N (Container.Last).Next := New_Node;
|
|
|
1165 N (New_Node).Prev := Container.Last;
|
|
|
1166
|
|
|
1167 Container.Last := New_Node;
|
|
|
1168 N (Container.Last).Next := 0;
|
|
|
1169
|
|
|
1170 elsif Before = Container.First then
|
|
|
1171 pragma Assert (N (Container.First).Prev = 0);
|
|
|
1172
|
|
|
1173 N (Container.First).Prev := New_Node;
|
|
|
1174 N (New_Node).Next := Container.First;
|
|
|
1175
|
|
|
1176 Container.First := New_Node;
|
|
|
1177 N (Container.First).Prev := 0;
|
|
|
1178
|
|
|
1179 else
|
|
|
1180 pragma Assert (N (Container.First).Prev = 0);
|
|
|
1181 pragma Assert (N (Container.Last).Next = 0);
|
|
|
1182
|
|
|
1183 N (New_Node).Next := Before;
|
|
|
1184 N (New_Node).Prev := N (Before).Prev;
|
|
|
1185
|
|
|
1186 N (N (Before).Prev).Next := New_Node;
|
|
|
1187 N (Before).Prev := New_Node;
|
|
|
1188 end if;
|
|
|
1189
|
|
|
1190 Container.Length := Container.Length + 1;
|
|
|
1191 end Insert_Internal;
|
|
|
1192
|
|
|
1193 --------------
|
|
|
1194 -- Is_Empty --
|
|
|
1195 --------------
|
|
|
1196
|
|
|
1197 function Is_Empty (Container : List) return Boolean is
|
|
|
1198 begin
|
|
|
1199 return Length (Container) = 0;
|
|
|
1200 end Is_Empty;
|
|
|
1201
|
|
|
1202 ----------
|
|
|
1203 -- Last --
|
|
|
1204 ----------
|
|
|
1205
|
|
|
1206 function Last (Container : List) return Cursor is
|
|
|
1207 begin
|
|
|
1208 if Container.Last = 0 then
|
|
|
1209 return No_Element;
|
|
|
1210 end if;
|
|
|
1211
|
|
|
1212 return (Node => Container.Last);
|
|
|
1213 end Last;
|
|
|
1214
|
|
|
1215 ------------------
|
|
|
1216 -- Last_Element --
|
|
|
1217 ------------------
|
|
|
1218
|
|
|
1219 function Last_Element (Container : List) return Element_Type is
|
|
|
1220 L : constant Count_Type := Container.Last;
|
|
|
1221
|
|
|
1222 begin
|
|
|
1223 if L = 0 then
|
|
|
1224 raise Constraint_Error with "list is empty";
|
|
|
1225 else
|
|
|
1226 return Container.Nodes (L).Element;
|
|
|
1227 end if;
|
|
|
1228 end Last_Element;
|
|
|
1229
|
|
|
1230 ------------
|
|
|
1231 -- Length --
|
|
|
1232 ------------
|
|
|
1233
|
|
|
1234 function Length (Container : List) return Count_Type is
|
|
|
1235 begin
|
|
|
1236 return Container.Length;
|
|
|
1237 end Length;
|
|
|
1238
|
|
|
1239 ----------
|
|
|
1240 -- Move --
|
|
|
1241 ----------
|
|
|
1242
|
|
|
1243 procedure Move (Target : in out List; Source : in out List) is
|
|
|
1244 N : Node_Array renames Source.Nodes;
|
|
|
1245 X : Count_Type;
|
|
|
1246
|
|
|
1247 begin
|
|
|
1248 if Target'Address = Source'Address then
|
|
|
1249 return;
|
|
|
1250 end if;
|
|
|
1251
|
|
|
1252 if Target.Capacity < Source.Length then
|
|
|
1253 raise Constraint_Error with -- ???
|
|
|
1254 "Source length exceeds Target capacity";
|
|
|
1255 end if;
|
|
|
1256
|
|
|
1257 Clear (Target);
|
|
|
1258
|
|
|
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);
|
|
|
1264
|
|
|
1265 -- Copy first element from Source to Target
|
|
|
1266
|
|
|
1267 X := Source.First;
|
|
|
1268 Append (Target, N (X).Element); -- optimize away???
|
|
|
1269
|
|
|
1270 -- Unlink first node of Source
|
|
|
1271
|
|
|
1272 Source.First := N (X).Next;
|
|
|
1273 N (Source.First).Prev := 0;
|
|
|
1274
|
|
|
1275 Source.Length := Source.Length - 1;
|
|
|
1276
|
|
|
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.
|
|
|
1280
|
|
|
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.
|
|
|
1290
|
|
|
1291 Free (Source, X);
|
|
|
1292 end loop;
|
|
|
1293
|
|
|
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);
|
|
|
1299
|
|
|
1300 -- Copy element from Source to Target
|
|
|
1301
|
|
|
1302 X := Source.First;
|
|
|
1303 Append (Target, N (X).Element);
|
|
|
1304
|
|
|
1305 -- Unlink node of Source
|
|
|
1306
|
|
|
1307 Source.First := 0;
|
|
|
1308 Source.Last := 0;
|
|
|
1309 Source.Length := 0;
|
|
|
1310
|
|
|
1311 -- Return the unlinked node to the free store
|
|
|
1312
|
|
|
1313 Free (Source, X);
|
|
|
1314 end if;
|
|
|
1315 end Move;
|
|
|
1316
|
|
|
1317 ----------
|
|
|
1318 -- Next --
|
|
|
1319 ----------
|
|
|
1320
|
|
|
1321 procedure Next (Container : List; Position : in out Cursor) is
|
|
|
1322 begin
|
|
|
1323 Position := Next (Container, Position);
|
|
|
1324 end Next;
|
|
|
1325
|
|
|
1326 function Next (Container : List; Position : Cursor) return Cursor is
|
|
|
1327 begin
|
|
|
1328 if Position.Node = 0 then
|
|
|
1329 return No_Element;
|
|
|
1330 end if;
|
|
|
1331
|
|
|
1332 if not Has_Element (Container, Position) then
|
|
|
1333 raise Program_Error with "Position cursor has no element";
|
|
|
1334 end if;
|
|
|
1335
|
|
|
1336 return (Node => Container.Nodes (Position.Node).Next);
|
|
|
1337 end Next;
|
|
|
1338
|
|
|
1339 -------------
|
|
|
1340 -- Prepend --
|
|
|
1341 -------------
|
|
|
1342
|
|
|
1343 procedure Prepend (Container : in out List; New_Item : Element_Type) is
|
|
|
1344 begin
|
|
|
1345 Insert (Container, First (Container), New_Item, 1);
|
|
|
1346 end Prepend;
|
|
|
1347
|
|
|
1348 procedure Prepend
|
|
|
1349 (Container : in out List;
|
|
|
1350 New_Item : Element_Type;
|
|
|
1351 Count : Count_Type)
|
|
|
1352 is
|
|
|
1353 begin
|
|
|
1354 Insert (Container, First (Container), New_Item, Count);
|
|
|
1355 end Prepend;
|
|
|
1356
|
|
|
1357 --------------
|
|
|
1358 -- Previous --
|
|
|
1359 --------------
|
|
|
1360
|
|
|
1361 procedure Previous (Container : List; Position : in out Cursor) is
|
|
|
1362 begin
|
|
|
1363 Position := Previous (Container, Position);
|
|
|
1364 end Previous;
|
|
|
1365
|
|
|
1366 function Previous (Container : List; Position : Cursor) return Cursor is
|
|
|
1367 begin
|
|
|
1368 if Position.Node = 0 then
|
|
|
1369 return No_Element;
|
|
|
1370 end if;
|
|
|
1371
|
|
|
1372 if not Has_Element (Container, Position) then
|
|
|
1373 raise Program_Error with "Position cursor has no element";
|
|
|
1374 end if;
|
|
|
1375
|
|
|
1376 return (Node => Container.Nodes (Position.Node).Prev);
|
|
|
1377 end Previous;
|
|
|
1378
|
|
|
1379 ---------------------
|
|
|
1380 -- Replace_Element --
|
|
|
1381 ---------------------
|
|
|
1382
|
|
|
1383 procedure Replace_Element
|
|
|
1384 (Container : in out List;
|
|
|
1385 Position : Cursor;
|
|
|
1386 New_Item : Element_Type)
|
|
|
1387 is
|
|
|
1388 begin
|
|
|
1389 if not Has_Element (Container, Position) then
|
|
|
1390 raise Constraint_Error with "Position cursor has no element";
|
|
|
1391 end if;
|
|
|
1392
|
|
|
1393 pragma Assert
|
|
|
1394 (Vet (Container, Position), "bad cursor in Replace_Element");
|
|
|
1395
|
|
|
1396 Container.Nodes (Position.Node).Element := New_Item;
|
|
|
1397 end Replace_Element;
|
|
|
1398
|
|
|
1399 ----------------------
|
|
|
1400 -- Reverse_Elements --
|
|
|
1401 ----------------------
|
|
|
1402
|
|
|
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;
|
|
|
1407
|
|
|
1408 procedure Swap (L : Count_Type; R : Count_Type);
|
|
|
1409
|
|
|
1410 ----------
|
|
|
1411 -- Swap --
|
|
|
1412 ----------
|
|
|
1413
|
|
|
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;
|
|
|
1417
|
|
|
1418 RN : constant Count_Type := N (R).Next;
|
|
|
1419 RP : constant Count_Type := N (R).Prev;
|
|
|
1420
|
|
|
1421 begin
|
|
|
1422 if LP /= 0 then
|
|
|
1423 N (LP).Next := R;
|
|
|
1424 end if;
|
|
|
1425
|
|
|
1426 if RN /= 0 then
|
|
|
1427 N (RN).Prev := L;
|
|
|
1428 end if;
|
|
|
1429
|
|
|
1430 N (L).Next := RN;
|
|
|
1431 N (R).Prev := LP;
|
|
|
1432
|
|
|
1433 if LN = R then
|
|
|
1434 pragma Assert (RP = L);
|
|
|
1435
|
|
|
1436 N (L).Prev := R;
|
|
|
1437 N (R).Next := L;
|
|
|
1438
|
|
|
1439 else
|
|
|
1440 N (L).Prev := RP;
|
|
|
1441 N (RP).Next := L;
|
|
|
1442
|
|
|
1443 N (R).Next := LN;
|
|
|
1444 N (LN).Prev := R;
|
|
|
1445 end if;
|
|
|
1446 end Swap;
|
|
|
1447
|
|
|
1448 -- Start of processing for Reverse_Elements
|
|
|
1449
|
|
|
1450 begin
|
|
|
1451 if Container.Length <= 1 then
|
|
|
1452 return;
|
|
|
1453 end if;
|
|
|
1454
|
|
|
1455 pragma Assert (N (Container.First).Prev = 0);
|
|
|
1456 pragma Assert (N (Container.Last).Next = 0);
|
|
|
1457
|
|
|
1458 Container.First := J;
|
|
|
1459 Container.Last := I;
|
|
|
1460 loop
|
|
|
1461 Swap (L => I, R => J);
|
|
|
1462
|
|
|
1463 J := N (J).Next;
|
|
|
1464 exit when I = J;
|
|
|
1465
|
|
|
1466 I := N (I).Prev;
|
|
|
1467 exit when I = J;
|
|
|
1468
|
|
|
1469 Swap (L => J, R => I);
|
|
|
1470
|
|
|
1471 I := N (I).Next;
|
|
|
1472 exit when I = J;
|
|
|
1473
|
|
|
1474 J := N (J).Prev;
|
|
|
1475 exit when I = J;
|
|
|
1476 end loop;
|
|
|
1477
|
|
|
1478 pragma Assert (N (Container.First).Prev = 0);
|
|
|
1479 pragma Assert (N (Container.Last).Next = 0);
|
|
|
1480 end Reverse_Elements;
|
|
|
1481
|
|
|
1482 ------------------
|
|
|
1483 -- Reverse_Find --
|
|
|
1484 ------------------
|
|
|
1485
|
|
|
1486 function Reverse_Find
|
|
|
1487 (Container : List;
|
|
|
1488 Item : Element_Type;
|
|
|
1489 Position : Cursor := No_Element) return Cursor
|
|
|
1490 is
|
|
|
1491 CFirst : Count_Type := Position.Node;
|
|
|
1492
|
|
|
1493 begin
|
|
|
1494 if CFirst = 0 then
|
|
|
1495 CFirst := Container.Last;
|
|
|
1496 end if;
|
|
|
1497
|
|
|
1498 if Container.Length = 0 then
|
|
|
1499 return No_Element;
|
|
|
1500
|
|
|
1501 else
|
|
|
1502 while CFirst /= 0 loop
|
|
|
1503 if Container.Nodes (CFirst).Element = Item then
|
|
|
1504 return (Node => CFirst);
|
|
|
1505 else
|
|
|
1506 CFirst := Container.Nodes (CFirst).Prev;
|
|
|
1507 end if;
|
|
|
1508 end loop;
|
|
|
1509
|
|
|
1510 return No_Element;
|
|
|
1511 end if;
|
|
|
1512 end Reverse_Find;
|
|
|
1513
|
|
|
1514 ------------
|
|
|
1515 -- Splice --
|
|
|
1516 ------------
|
|
|
1517
|
|
|
1518 procedure Splice
|
|
|
1519 (Target : in out List;
|
|
|
1520 Before : Cursor;
|
|
|
1521 Source : in out List)
|
|
|
1522 is
|
|
|
1523 SN : Node_Array renames Source.Nodes;
|
|
|
1524
|
|
|
1525 begin
|
|
|
1526 if Target'Address = Source'Address then
|
|
|
1527 raise Program_Error with "Target and Source denote same container";
|
|
|
1528 end if;
|
|
|
1529
|
|
|
1530 if Before.Node /= 0 then
|
|
|
1531 pragma Assert (Vet (Target, Before), "bad cursor in Splice");
|
|
|
1532 end if;
|
|
|
1533
|
|
|
1534 pragma Assert (SN (Source.First).Prev = 0);
|
|
|
1535 pragma Assert (SN (Source.Last).Next = 0);
|
|
|
1536
|
|
|
1537 if Target.Length > Count_Type'Base'Last - Source.Length then
|
|
|
1538 raise Constraint_Error with "new length exceeds maximum";
|
|
|
1539 end if;
|
|
|
1540
|
|
|
1541 if Target.Length + Source.Length > Target.Capacity then
|
|
|
1542 raise Constraint_Error;
|
|
|
1543 end if;
|
|
|
1544
|
|
|
1545 loop
|
|
|
1546 Insert (Target, Before, SN (Source.Last).Element);
|
|
|
1547 Delete_Last (Source);
|
|
|
1548 exit when Is_Empty (Source);
|
|
|
1549 end loop;
|
|
|
1550 end Splice;
|
|
|
1551
|
|
|
1552 procedure Splice
|
|
|
1553 (Target : in out List;
|
|
|
1554 Before : Cursor;
|
|
|
1555 Source : in out List;
|
|
|
1556 Position : in out Cursor)
|
|
|
1557 is
|
|
|
1558 Target_Position : Cursor;
|
|
|
1559
|
|
|
1560 begin
|
|
|
1561 if Target'Address = Source'Address then
|
|
|
1562 raise Program_Error with "Target and Source denote same container";
|
|
|
1563 end if;
|
|
|
1564
|
|
|
1565 if Position.Node = 0 then
|
|
|
1566 raise Constraint_Error with "Position cursor has no element";
|
|
|
1567 end if;
|
|
|
1568
|
|
|
1569 pragma Assert (Vet (Source, Position), "bad Position cursor in Splice");
|
|
|
1570
|
|
|
1571 if Target.Length >= Target.Capacity then
|
|
|
1572 raise Constraint_Error;
|
|
|
1573 end if;
|
|
|
1574
|
|
|
1575 Insert
|
|
|
1576 (Container => Target,
|
|
|
1577 Before => Before,
|
|
|
1578 New_Item => Source.Nodes (Position.Node).Element,
|
|
|
1579 Position => Target_Position);
|
|
|
1580
|
|
|
1581 Delete (Source, Position);
|
|
|
1582 Position := Target_Position;
|
|
|
1583 end Splice;
|
|
|
1584
|
|
|
1585 procedure Splice
|
|
|
1586 (Container : in out List;
|
|
|
1587 Before : Cursor;
|
|
|
1588 Position : Cursor)
|
|
|
1589 is
|
|
|
1590 N : Node_Array renames Container.Nodes;
|
|
|
1591
|
|
|
1592 begin
|
|
|
1593 if Before.Node /= 0 then
|
|
|
1594 pragma Assert
|
|
|
1595 (Vet (Container, Before), "bad Before cursor in Splice");
|
|
|
1596 end if;
|
|
|
1597
|
|
|
1598 if Position.Node = 0 then
|
|
|
1599 raise Constraint_Error with "Position cursor has no element";
|
|
|
1600 end if;
|
|
|
1601
|
|
|
1602 pragma Assert
|
|
|
1603 (Vet (Container, Position), "bad Position cursor in Splice");
|
|
|
1604
|
|
|
1605 if Position.Node = Before.Node
|
|
|
1606 or else N (Position.Node).Next = Before.Node
|
|
|
1607 then
|
|
|
1608 return;
|
|
|
1609 end if;
|
|
|
1610
|
|
|
1611 pragma Assert (Container.Length >= 2);
|
|
|
1612
|
|
|
1613 if Before.Node = 0 then
|
|
|
1614 pragma Assert (Position.Node /= Container.Last);
|
|
|
1615
|
|
|
1616 if Position.Node = Container.First then
|
|
|
1617 Container.First := N (Position.Node).Next;
|
|
|
1618 N (Container.First).Prev := 0;
|
|
|
1619
|
|
|
1620 else
|
|
|
1621 N (N (Position.Node).Prev).Next := N (Position.Node).Next;
|
|
|
1622 N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
|
|
|
1623 end if;
|
|
|
1624
|
|
|
1625 N (Container.Last).Next := Position.Node;
|
|
|
1626 N (Position.Node).Prev := Container.Last;
|
|
|
1627
|
|
|
1628 Container.Last := Position.Node;
|
|
|
1629 N (Container.Last).Next := 0;
|
|
|
1630
|
|
|
1631 return;
|
|
|
1632 end if;
|
|
|
1633
|
|
|
1634 if Before.Node = Container.First then
|
|
|
1635 pragma Assert (Position.Node /= Container.First);
|
|
|
1636
|
|
|
1637 if Position.Node = Container.Last then
|
|
|
1638 Container.Last := N (Position.Node).Prev;
|
|
|
1639 N (Container.Last).Next := 0;
|
|
|
1640
|
|
|
1641 else
|
|
|
1642 N (N (Position.Node).Prev).Next := N (Position.Node).Next;
|
|
|
1643 N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
|
|
|
1644 end if;
|
|
|
1645
|
|
|
1646 N (Container.First).Prev := Position.Node;
|
|
|
1647 N (Position.Node).Next := Container.First;
|
|
|
1648
|
|
|
1649 Container.First := Position.Node;
|
|
|
1650 N (Container.First).Prev := 0;
|
|
|
1651
|
|
|
1652 return;
|
|
|
1653 end if;
|
|
|
1654
|
|
|
1655 if Position.Node = Container.First then
|
|
|
1656 Container.First := N (Position.Node).Next;
|
|
|
1657 N (Container.First).Prev := 0;
|
|
|
1658
|
|
|
1659 elsif Position.Node = Container.Last then
|
|
|
1660 Container.Last := N (Position.Node).Prev;
|
|
|
1661 N (Container.Last).Next := 0;
|
|
|
1662
|
|
|
1663 else
|
|
|
1664 N (N (Position.Node).Prev).Next := N (Position.Node).Next;
|
|
|
1665 N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
|
|
|
1666 end if;
|
|
|
1667
|
|
|
1668 N (N (Before.Node).Prev).Next := Position.Node;
|
|
|
1669 N (Position.Node).Prev := N (Before.Node).Prev;
|
|
|
1670
|
|
|
1671 N (Before.Node).Prev := Position.Node;
|
|
|
1672 N (Position.Node).Next := Before.Node;
|
|
|
1673
|
|
|
1674 pragma Assert (N (Container.First).Prev = 0);
|
|
|
1675 pragma Assert (N (Container.Last).Next = 0);
|
|
|
1676 end Splice;
|
|
|
1677
|
|
|
1678 ----------
|
|
|
1679 -- Swap --
|
|
|
1680 ----------
|
|
|
1681
|
|
|
1682 procedure Swap
|
|
|
1683 (Container : in out List;
|
|
|
1684 I : Cursor;
|
|
|
1685 J : Cursor)
|
|
|
1686 is
|
|
|
1687 begin
|
|
|
1688 if I.Node = 0 then
|
|
|
1689 raise Constraint_Error with "I cursor has no element";
|
|
|
1690 end if;
|
|
|
1691
|
|
|
1692 if J.Node = 0 then
|
|
|
1693 raise Constraint_Error with "J cursor has no element";
|
|
|
1694 end if;
|
|
|
1695
|
|
|
1696 if I.Node = J.Node then
|
|
|
1697 return;
|
|
|
1698 end if;
|
|
|
1699
|
|
|
1700 pragma Assert (Vet (Container, I), "bad I cursor in Swap");
|
|
|
1701 pragma Assert (Vet (Container, J), "bad J cursor in Swap");
|
|
|
1702
|
|
|
1703 declare
|
|
|
1704 NN : Node_Array renames Container.Nodes;
|
|
|
1705 NI : Node_Type renames NN (I.Node);
|
|
|
1706 NJ : Node_Type renames NN (J.Node);
|
|
|
1707
|
|
|
1708 EI_Copy : constant Element_Type := NI.Element;
|
|
|
1709
|
|
|
1710 begin
|
|
|
1711 NI.Element := NJ.Element;
|
|
|
1712 NJ.Element := EI_Copy;
|
|
|
1713 end;
|
|
|
1714 end Swap;
|
|
|
1715
|
|
|
1716 ----------------
|
|
|
1717 -- Swap_Links --
|
|
|
1718 ----------------
|
|
|
1719
|
|
|
1720 procedure Swap_Links
|
|
|
1721 (Container : in out List;
|
|
|
1722 I : Cursor;
|
|
|
1723 J : Cursor)
|
|
|
1724 is
|
|
|
1725 I_Next : Cursor;
|
|
|
1726 J_Next : Cursor;
|
|
|
1727
|
|
|
1728 begin
|
|
|
1729 if I.Node = 0 then
|
|
|
1730 raise Constraint_Error with "I cursor has no element";
|
|
|
1731 end if;
|
|
|
1732
|
|
|
1733 if J.Node = 0 then
|
|
|
1734 raise Constraint_Error with "J cursor has no element";
|
|
|
1735 end if;
|
|
|
1736
|
|
|
1737 if I.Node = J.Node then
|
|
|
1738 return;
|
|
|
1739 end if;
|
|
|
1740
|
|
|
1741 pragma Assert (Vet (Container, I), "bad I cursor in Swap_Links");
|
|
|
1742 pragma Assert (Vet (Container, J), "bad J cursor in Swap_Links");
|
|
|
1743
|
|
|
1744 I_Next := Next (Container, I);
|
|
|
1745
|
|
|
1746 if I_Next = J then
|
|
|
1747 Splice (Container, Before => I, Position => J);
|
|
|
1748
|
|
|
1749 else
|
|
|
1750 J_Next := Next (Container, J);
|
|
|
1751
|
|
|
1752 if J_Next = I then
|
|
|
1753 Splice (Container, Before => J, Position => I);
|
|
|
1754
|
|
|
1755 else
|
|
|
1756 pragma Assert (Container.Length >= 3);
|
|
|
1757 Splice (Container, Before => I_Next, Position => J);
|
|
|
1758 Splice (Container, Before => J_Next, Position => I);
|
|
|
1759 end if;
|
|
|
1760 end if;
|
|
|
1761 end Swap_Links;
|
|
|
1762
|
|
|
1763 ---------
|
|
|
1764 -- Vet --
|
|
|
1765 ---------
|
|
|
1766
|
|
|
1767 function Vet (L : List; Position : Cursor) return Boolean is
|
|
|
1768 N : Node_Array renames L.Nodes;
|
|
|
1769
|
|
|
1770 begin
|
|
|
1771 if L.Length = 0 then
|
|
|
1772 return False;
|
|
|
1773 end if;
|
|
|
1774
|
|
|
1775 if L.First = 0 then
|
|
|
1776 return False;
|
|
|
1777 end if;
|
|
|
1778
|
|
|
1779 if L.Last = 0 then
|
|
|
1780 return False;
|
|
|
1781 end if;
|
|
|
1782
|
|
|
1783 if Position.Node > L.Capacity then
|
|
|
1784 return False;
|
|
|
1785 end if;
|
|
|
1786
|
|
|
1787 if N (Position.Node).Prev < 0
|
|
|
1788 or else N (Position.Node).Prev > L.Capacity
|
|
|
1789 then
|
|
|
1790 return False;
|
|
|
1791 end if;
|
|
|
1792
|
|
|
1793 if N (Position.Node).Next > L.Capacity then
|
|
|
1794 return False;
|
|
|
1795 end if;
|
|
|
1796
|
|
|
1797 if N (L.First).Prev /= 0 then
|
|
|
1798 return False;
|
|
|
1799 end if;
|
|
|
1800
|
|
|
1801 if N (L.Last).Next /= 0 then
|
|
|
1802 return False;
|
|
|
1803 end if;
|
|
|
1804
|
|
|
1805 if N (Position.Node).Prev = 0 and then Position.Node /= L.First then
|
|
|
1806 return False;
|
|
|
1807 end if;
|
|
|
1808
|
|
|
1809 if N (Position.Node).Next = 0 and then Position.Node /= L.Last then
|
|
|
1810 return False;
|
|
|
1811 end if;
|
|
|
1812
|
|
|
1813 if L.Length = 1 then
|
|
|
1814 return L.First = L.Last;
|
|
|
1815 end if;
|
|
|
1816
|
|
|
1817 if L.First = L.Last then
|
|
|
1818 return False;
|
|
|
1819 end if;
|
|
|
1820
|
|
|
1821 if N (L.First).Next = 0 then
|
|
|
1822 return False;
|
|
|
1823 end if;
|
|
|
1824
|
|
|
1825 if N (L.Last).Prev = 0 then
|
|
|
1826 return False;
|
|
|
1827 end if;
|
|
|
1828
|
|
|
1829 if N (N (L.First).Next).Prev /= L.First then
|
|
|
1830 return False;
|
|
|
1831 end if;
|
|
|
1832
|
|
|
1833 if N (N (L.Last).Prev).Next /= L.Last then
|
|
|
1834 return False;
|
|
|
1835 end if;
|
|
|
1836
|
|
|
1837 if L.Length = 2 then
|
|
|
1838 if N (L.First).Next /= L.Last then
|
|
|
1839 return False;
|
|
|
1840 end if;
|
|
|
1841
|
|
|
1842 if N (L.Last).Prev /= L.First then
|
|
|
1843 return False;
|
|
|
1844 end if;
|
|
|
1845
|
|
|
1846 return True;
|
|
|
1847 end if;
|
|
|
1848
|
|
|
1849 if N (L.First).Next = L.Last then
|
|
|
1850 return False;
|
|
|
1851 end if;
|
|
|
1852
|
|
|
1853 if N (L.Last).Prev = L.First then
|
|
|
1854 return False;
|
|
|
1855 end if;
|
|
|
1856
|
|
|
1857 if Position.Node = L.First then
|
|
|
1858 return True;
|
|
|
1859 end if;
|
|
|
1860
|
|
|
1861 if Position.Node = L.Last then
|
|
|
1862 return True;
|
|
|
1863 end if;
|
|
|
1864
|
|
|
1865 if N (Position.Node).Next = 0 then
|
|
|
1866 return False;
|
|
|
1867 end if;
|
|
|
1868
|
|
|
1869 if N (Position.Node).Prev = 0 then
|
|
|
1870 return False;
|
|
|
1871 end if;
|
|
|
1872
|
|
|
1873 if N (N (Position.Node).Next).Prev /= Position.Node then
|
|
|
1874 return False;
|
|
|
1875 end if;
|
|
|
1876
|
|
|
1877 if N (N (Position.Node).Prev).Next /= Position.Node then
|
|
|
1878 return False;
|
|
|
1879 end if;
|
|
|
1880
|
|
|
1881 if L.Length = 3 then
|
|
|
1882 if N (L.First).Next /= Position.Node then
|
|
|
1883 return False;
|
|
|
1884 end if;
|
|
|
1885
|
|
|
1886 if N (L.Last).Prev /= Position.Node then
|
|
|
1887 return False;
|
|
|
1888 end if;
|
|
|
1889 end if;
|
|
|
1890
|
|
|
1891 return True;
|
|
|
1892 end Vet;
|
|
|
1893
|
|
|
1894 end Ada.Containers.Formal_Doubly_Linked_Lists;
|
