]>
Commit | Line | Data |
---|---|---|
bd65a2d7 AC |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT LIBRARY COMPONENTS -- | |
4 | -- -- | |
5 | -- A D A . C O N T A I N E R S . F O R M A L _ O R D E R E D _ M A P S -- | |
6 | -- -- | |
7 | -- B o d y -- | |
8 | -- -- | |
4b490c1e | 9 | -- Copyright (C) 2010-2020, Free Software Foundation, Inc. -- |
bd65a2d7 AC |
10 | -- -- |
11 | -- GNAT is free software; you can redistribute it and/or modify it under -- | |
12 | -- terms of the GNU General Public License as published by the Free Soft- -- | |
13 | -- ware Foundation; either version 3, or (at your option) any later ver- -- | |
14 | -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- | |
15 | -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- | |
16 | -- or FITNESS FOR A PARTICULAR PURPOSE. -- | |
17 | -- -- | |
18 | -- As a special exception under Section 7 of GPL version 3, you are granted -- | |
19 | -- additional permissions described in the GCC Runtime Library Exception, -- | |
20 | -- version 3.1, as published by the Free Software Foundation. -- | |
21 | -- -- | |
22 | -- You should have received a copy of the GNU General Public License and -- | |
23 | -- a copy of the GCC Runtime Library Exception along with this program; -- | |
24 | -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- | |
25 | -- <http://www.gnu.org/licenses/>. -- | |
26 | ------------------------------------------------------------------------------ | |
27 | ||
28 | with Ada.Containers.Red_Black_Trees.Generic_Bounded_Operations; | |
29 | pragma Elaborate_All | |
30 | (Ada.Containers.Red_Black_Trees.Generic_Bounded_Operations); | |
31 | ||
32 | with Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys; | |
33 | pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys); | |
34 | ||
35 | with System; use type System.Address; | |
36 | ||
5fde9688 AC |
37 | package body Ada.Containers.Formal_Ordered_Maps with |
38 | SPARK_Mode => Off | |
39 | is | |
bd65a2d7 AC |
40 | |
41 | ----------------------------- | |
42 | -- Node Access Subprograms -- | |
43 | ----------------------------- | |
44 | ||
45 | -- These subprograms provide a functional interface to access fields | |
46 | -- of a node, and a procedural interface for modifying these values. | |
47 | ||
5ffe0bab AC |
48 | function Color |
49 | (Node : Node_Type) return Ada.Containers.Red_Black_Trees.Color_Type; | |
bd65a2d7 AC |
50 | pragma Inline (Color); |
51 | ||
52 | function Left_Son (Node : Node_Type) return Count_Type; | |
c6d2191a | 53 | pragma Inline (Left_Son); |
bd65a2d7 AC |
54 | |
55 | function Parent (Node : Node_Type) return Count_Type; | |
56 | pragma Inline (Parent); | |
57 | ||
58 | function Right_Son (Node : Node_Type) return Count_Type; | |
c6d2191a | 59 | pragma Inline (Right_Son); |
bd65a2d7 AC |
60 | |
61 | procedure Set_Color | |
62 | (Node : in out Node_Type; | |
63 | Color : Ada.Containers.Red_Black_Trees.Color_Type); | |
64 | pragma Inline (Set_Color); | |
65 | ||
66 | procedure Set_Left (Node : in out Node_Type; Left : Count_Type); | |
67 | pragma Inline (Set_Left); | |
68 | ||
69 | procedure Set_Right (Node : in out Node_Type; Right : Count_Type); | |
70 | pragma Inline (Set_Right); | |
71 | ||
72 | procedure Set_Parent (Node : in out Node_Type; Parent : Count_Type); | |
73 | pragma Inline (Set_Parent); | |
74 | ||
75 | ----------------------- | |
76 | -- Local Subprograms -- | |
77 | ----------------------- | |
78 | ||
5ffe0bab AC |
79 | -- All need comments ??? |
80 | ||
bd65a2d7 AC |
81 | generic |
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); | |
86 | ||
686d0984 | 87 | procedure Free (Tree : in out Map; X : Count_Type); |
bd65a2d7 AC |
88 | |
89 | function Is_Greater_Key_Node | |
90 | (Left : Key_Type; | |
91 | Right : Node_Type) return Boolean; | |
92 | pragma Inline (Is_Greater_Key_Node); | |
93 | ||
94 | function Is_Less_Key_Node | |
95 | (Left : Key_Type; | |
96 | Right : Node_Type) return Boolean; | |
97 | pragma Inline (Is_Less_Key_Node); | |
98 | ||
bd65a2d7 AC |
99 | -------------------------- |
100 | -- Local Instantiations -- | |
101 | -------------------------- | |
102 | ||
103 | package Tree_Operations is | |
104 | new Red_Black_Trees.Generic_Bounded_Operations | |
105 | (Tree_Types => Tree_Types, | |
5ffe0bab AC |
106 | Left => Left_Son, |
107 | Right => Right_Son); | |
bd65a2d7 AC |
108 | |
109 | use Tree_Operations; | |
110 | ||
111 | package Key_Ops is | |
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); | |
117 | ||
118 | --------- | |
119 | -- "=" -- | |
120 | --------- | |
121 | ||
122 | function "=" (Left, Right : Map) return Boolean is | |
123 | Lst : Count_Type; | |
5ffe0bab | 124 | Node : Count_Type; |
bd65a2d7 | 125 | ENode : Count_Type; |
bd65a2d7 | 126 | |
5ffe0bab | 127 | begin |
bd65a2d7 AC |
128 | if Length (Left) /= Length (Right) then |
129 | return False; | |
130 | end if; | |
131 | ||
132 | if Is_Empty (Left) then | |
133 | return True; | |
134 | end if; | |
135 | ||
686d0984 | 136 | Lst := Next (Left, Last (Left).Node); |
5ffe0bab AC |
137 | |
138 | Node := First (Left).Node; | |
bd65a2d7 | 139 | while Node /= Lst loop |
686d0984 | 140 | ENode := Find (Right, Left.Nodes (Node).Key).Node; |
5ffe0bab | 141 | |
bd65a2d7 | 142 | if ENode = 0 or else |
686d0984 | 143 | Left.Nodes (Node).Element /= Right.Nodes (ENode).Element |
bd65a2d7 AC |
144 | then |
145 | return False; | |
146 | end if; | |
5ffe0bab | 147 | |
686d0984 | 148 | Node := Next (Left, Node); |
bd65a2d7 AC |
149 | end loop; |
150 | ||
151 | return True; | |
bd65a2d7 AC |
152 | end "="; |
153 | ||
154 | ------------ | |
155 | -- Assign -- | |
156 | ------------ | |
157 | ||
158 | procedure Assign (Target : in out Map; Source : Map) is | |
159 | procedure Append_Element (Source_Node : Count_Type); | |
160 | ||
161 | procedure Append_Elements is | |
162 | new Tree_Operations.Generic_Iteration (Append_Element); | |
163 | ||
164 | -------------------- | |
165 | -- Append_Element -- | |
166 | -------------------- | |
167 | ||
168 | procedure Append_Element (Source_Node : Count_Type) is | |
686d0984 | 169 | SN : Node_Type renames Source.Nodes (Source_Node); |
bd65a2d7 AC |
170 | |
171 | procedure Set_Element (Node : in out Node_Type); | |
172 | pragma Inline (Set_Element); | |
173 | ||
174 | function New_Node return Count_Type; | |
175 | pragma Inline (New_Node); | |
176 | ||
5ffe0bab | 177 | procedure Insert_Post is new Key_Ops.Generic_Insert_Post (New_Node); |
bd65a2d7 AC |
178 | |
179 | procedure Unconditional_Insert_Sans_Hint is | |
5ffe0bab | 180 | new Key_Ops.Generic_Unconditional_Insert (Insert_Post); |
bd65a2d7 AC |
181 | |
182 | procedure Unconditional_Insert_Avec_Hint is | |
5ffe0bab AC |
183 | new Key_Ops.Generic_Unconditional_Insert_With_Hint |
184 | (Insert_Post, | |
185 | Unconditional_Insert_Sans_Hint); | |
bd65a2d7 | 186 | |
5ffe0bab | 187 | procedure Allocate is new Generic_Allocate (Set_Element); |
bd65a2d7 AC |
188 | |
189 | -------------- | |
190 | -- New_Node -- | |
191 | -------------- | |
192 | ||
193 | function New_Node return Count_Type is | |
194 | Result : Count_Type; | |
bd65a2d7 | 195 | begin |
686d0984 | 196 | Allocate (Target, Result); |
bd65a2d7 AC |
197 | return Result; |
198 | end New_Node; | |
199 | ||
200 | ----------------- | |
201 | -- Set_Element -- | |
202 | ----------------- | |
203 | ||
204 | procedure Set_Element (Node : in out Node_Type) is | |
205 | begin | |
206 | Node.Key := SN.Key; | |
207 | Node.Element := SN.Element; | |
208 | end Set_Element; | |
209 | ||
210 | Target_Node : Count_Type; | |
211 | ||
212 | -- Start of processing for Append_Element | |
213 | ||
214 | begin | |
215 | Unconditional_Insert_Avec_Hint | |
686d0984 | 216 | (Tree => Target, |
bd65a2d7 AC |
217 | Hint => 0, |
218 | Key => SN.Key, | |
219 | Node => Target_Node); | |
220 | end Append_Element; | |
221 | ||
222 | -- Start of processing for Assign | |
223 | ||
224 | begin | |
bd65a2d7 AC |
225 | if Target'Address = Source'Address then |
226 | return; | |
227 | end if; | |
228 | ||
229 | if Target.Capacity < Length (Source) then | |
230 | raise Storage_Error with "not enough capacity"; -- SE or CE? ??? | |
231 | end if; | |
232 | ||
686d0984 AC |
233 | Tree_Operations.Clear_Tree (Target); |
234 | Append_Elements (Source); | |
bd65a2d7 AC |
235 | end Assign; |
236 | ||
237 | ------------- | |
238 | -- Ceiling -- | |
239 | ------------- | |
240 | ||
241 | function Ceiling (Container : Map; Key : Key_Type) return Cursor is | |
5ffe0bab | 242 | Node : constant Count_Type := Key_Ops.Ceiling (Container, Key); |
bd65a2d7 | 243 | |
686d0984 AC |
244 | begin |
245 | if Node = 0 then | |
246 | return No_Element; | |
bd65a2d7 AC |
247 | end if; |
248 | ||
686d0984 | 249 | return (Node => Node); |
bd65a2d7 AC |
250 | end Ceiling; |
251 | ||
252 | ----------- | |
253 | -- Clear -- | |
254 | ----------- | |
255 | ||
256 | procedure Clear (Container : in out Map) is | |
257 | begin | |
686d0984 | 258 | Tree_Operations.Clear_Tree (Container); |
bd65a2d7 AC |
259 | end Clear; |
260 | ||
261 | ----------- | |
262 | -- Color -- | |
263 | ----------- | |
264 | ||
265 | function Color (Node : Node_Type) return Color_Type is | |
266 | begin | |
267 | return Node.Color; | |
268 | end Color; | |
269 | ||
270 | -------------- | |
271 | -- Contains -- | |
272 | -------------- | |
273 | ||
274 | function Contains (Container : Map; Key : Key_Type) return Boolean is | |
275 | begin | |
276 | return Find (Container, Key) /= No_Element; | |
277 | end Contains; | |
278 | ||
279 | ---------- | |
280 | -- Copy -- | |
281 | ---------- | |
282 | ||
283 | function Copy (Source : Map; Capacity : Count_Type := 0) return Map is | |
284 | Node : Count_Type := 1; | |
285 | N : Count_Type; | |
5ffe0bab | 286 | |
bd65a2d7 | 287 | begin |
b1d12996 AC |
288 | if 0 < Capacity and then Capacity < Source.Capacity then |
289 | raise Capacity_Error; | |
290 | end if; | |
291 | ||
bd65a2d7 AC |
292 | return Target : Map (Count_Type'Max (Source.Capacity, Capacity)) do |
293 | if Length (Source) > 0 then | |
686d0984 AC |
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; | |
bd65a2d7 AC |
299 | |
300 | while Node <= Source.Capacity loop | |
686d0984 AC |
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; | |
bd65a2d7 AC |
315 | Node := Node + 1; |
316 | end loop; | |
317 | ||
318 | while Node <= Target.Capacity loop | |
319 | N := Node; | |
686d0984 | 320 | Formal_Ordered_Maps.Free (Tree => Target, X => N); |
bd65a2d7 AC |
321 | Node := Node + 1; |
322 | end loop; | |
bd65a2d7 AC |
323 | end if; |
324 | end return; | |
325 | end Copy; | |
326 | ||
327 | ------------ | |
328 | -- Delete -- | |
329 | ------------ | |
330 | ||
331 | procedure Delete (Container : in out Map; Position : in out Cursor) is | |
332 | begin | |
bd65a2d7 AC |
333 | if not Has_Element (Container, Position) then |
334 | raise Constraint_Error with | |
335 | "Position cursor of Delete has no element"; | |
336 | end if; | |
337 | ||
686d0984 | 338 | pragma Assert (Vet (Container, Position.Node), |
bd65a2d7 AC |
339 | "Position cursor of Delete is bad"); |
340 | ||
686d0984 | 341 | Tree_Operations.Delete_Node_Sans_Free (Container, |
bd65a2d7 | 342 | Position.Node); |
686d0984 | 343 | Formal_Ordered_Maps.Free (Container, Position.Node); |
f2acfbce | 344 | Position := No_Element; |
bd65a2d7 AC |
345 | end Delete; |
346 | ||
347 | procedure Delete (Container : in out Map; Key : Key_Type) is | |
686d0984 AC |
348 | X : constant Node_Access := Key_Ops.Find (Container, Key); |
349 | ||
bd65a2d7 | 350 | begin |
686d0984 AC |
351 | if X = 0 then |
352 | raise Constraint_Error with "key not in map"; | |
bd65a2d7 | 353 | end if; |
bd65a2d7 | 354 | |
686d0984 AC |
355 | Tree_Operations.Delete_Node_Sans_Free (Container, X); |
356 | Formal_Ordered_Maps.Free (Container, X); | |
bd65a2d7 AC |
357 | end Delete; |
358 | ||
359 | ------------------ | |
360 | -- Delete_First -- | |
361 | ------------------ | |
362 | ||
363 | procedure Delete_First (Container : in out Map) is | |
364 | X : constant Node_Access := First (Container).Node; | |
bd65a2d7 | 365 | begin |
bd65a2d7 | 366 | if X /= 0 then |
686d0984 AC |
367 | Tree_Operations.Delete_Node_Sans_Free (Container, X); |
368 | Formal_Ordered_Maps.Free (Container, X); | |
bd65a2d7 AC |
369 | end if; |
370 | end Delete_First; | |
371 | ||
372 | ----------------- | |
373 | -- Delete_Last -- | |
374 | ----------------- | |
375 | ||
376 | procedure Delete_Last (Container : in out Map) is | |
377 | X : constant Node_Access := Last (Container).Node; | |
bd65a2d7 | 378 | begin |
bd65a2d7 | 379 | if X /= 0 then |
686d0984 AC |
380 | Tree_Operations.Delete_Node_Sans_Free (Container, X); |
381 | Formal_Ordered_Maps.Free (Container, X); | |
bd65a2d7 AC |
382 | end if; |
383 | end Delete_Last; | |
384 | ||
385 | ------------- | |
386 | -- Element -- | |
387 | ------------- | |
388 | ||
389 | function Element (Container : Map; Position : Cursor) return Element_Type is | |
390 | begin | |
391 | if not Has_Element (Container, Position) then | |
392 | raise Constraint_Error with | |
393 | "Position cursor of function Element has no element"; | |
394 | end if; | |
395 | ||
686d0984 | 396 | pragma Assert (Vet (Container, Position.Node), |
bd65a2d7 AC |
397 | "Position cursor of function Element is bad"); |
398 | ||
686d0984 | 399 | return Container.Nodes (Position.Node).Element; |
bd65a2d7 AC |
400 | |
401 | end Element; | |
402 | ||
403 | function Element (Container : Map; Key : Key_Type) return Element_Type is | |
404 | Node : constant Node_Access := Find (Container, Key).Node; | |
405 | ||
406 | begin | |
407 | if Node = 0 then | |
408 | raise Constraint_Error with "key not in map"; | |
409 | end if; | |
410 | ||
686d0984 | 411 | return Container.Nodes (Node).Element; |
bd65a2d7 AC |
412 | end Element; |
413 | ||
414 | --------------------- | |
415 | -- Equivalent_Keys -- | |
416 | --------------------- | |
417 | ||
418 | function Equivalent_Keys (Left, Right : Key_Type) return Boolean is | |
419 | begin | |
420 | if Left < Right | |
421 | or else Right < Left | |
422 | then | |
423 | return False; | |
424 | else | |
425 | return True; | |
426 | end if; | |
427 | end Equivalent_Keys; | |
428 | ||
429 | ------------- | |
430 | -- Exclude -- | |
431 | ------------- | |
432 | ||
433 | procedure Exclude (Container : in out Map; Key : Key_Type) is | |
686d0984 | 434 | X : constant Node_Access := Key_Ops.Find (Container, Key); |
bd65a2d7 | 435 | begin |
bd65a2d7 | 436 | if X /= 0 then |
686d0984 AC |
437 | Tree_Operations.Delete_Node_Sans_Free (Container, X); |
438 | Formal_Ordered_Maps.Free (Container, X); | |
bd65a2d7 AC |
439 | end if; |
440 | end Exclude; | |
441 | ||
442 | ---------- | |
443 | -- Find -- | |
444 | ---------- | |
445 | ||
446 | function Find (Container : Map; Key : Key_Type) return Cursor is | |
5ffe0bab | 447 | Node : constant Count_Type := Key_Ops.Find (Container, Key); |
bd65a2d7 | 448 | |
686d0984 AC |
449 | begin |
450 | if Node = 0 then | |
451 | return No_Element; | |
452 | end if; | |
bd65a2d7 | 453 | |
686d0984 | 454 | return (Node => Node); |
bd65a2d7 AC |
455 | end Find; |
456 | ||
457 | ----------- | |
458 | -- First -- | |
459 | ----------- | |
460 | ||
461 | function First (Container : Map) return Cursor is | |
462 | begin | |
463 | if Length (Container) = 0 then | |
464 | return No_Element; | |
465 | end if; | |
466 | ||
686d0984 | 467 | return (Node => Container.First); |
bd65a2d7 AC |
468 | end First; |
469 | ||
470 | ------------------- | |
471 | -- First_Element -- | |
472 | ------------------- | |
473 | ||
474 | function First_Element (Container : Map) return Element_Type is | |
475 | begin | |
476 | if Is_Empty (Container) then | |
477 | raise Constraint_Error with "map is empty"; | |
478 | end if; | |
479 | ||
686d0984 | 480 | return Container.Nodes (First (Container).Node).Element; |
bd65a2d7 AC |
481 | end First_Element; |
482 | ||
483 | --------------- | |
484 | -- First_Key -- | |
485 | --------------- | |
486 | ||
487 | function First_Key (Container : Map) return Key_Type is | |
488 | begin | |
489 | if Is_Empty (Container) then | |
490 | raise Constraint_Error with "map is empty"; | |
491 | end if; | |
492 | ||
686d0984 | 493 | return Container.Nodes (First (Container).Node).Key; |
bd65a2d7 AC |
494 | end First_Key; |
495 | ||
496 | ----------- | |
497 | -- Floor -- | |
498 | ----------- | |
499 | ||
500 | function Floor (Container : Map; Key : Key_Type) return Cursor is | |
5ffe0bab | 501 | Node : constant Count_Type := Key_Ops.Floor (Container, Key); |
bd65a2d7 | 502 | |
686d0984 AC |
503 | begin |
504 | if Node = 0 then | |
505 | return No_Element; | |
bd65a2d7 AC |
506 | end if; |
507 | ||
686d0984 | 508 | return (Node => Node); |
bd65a2d7 AC |
509 | end Floor; |
510 | ||
f2acfbce CD |
511 | ------------------ |
512 | -- Formal_Model -- | |
513 | ------------------ | |
514 | ||
515 | package body Formal_Model is | |
516 | ||
8ab31c0c AC |
517 | ---------- |
518 | -- Find -- | |
519 | ---------- | |
520 | ||
d5fa5335 HK |
521 | function Find |
522 | (Container : K.Sequence; | |
523 | Key : Key_Type) return Count_Type | |
8ab31c0c AC |
524 | is |
525 | begin | |
526 | for I in 1 .. K.Length (Container) loop | |
527 | if Equivalent_Keys (Key, K.Get (Container, I)) then | |
528 | return I; | |
529 | elsif Key < K.Get (Container, I) then | |
530 | return 0; | |
531 | end if; | |
532 | end loop; | |
533 | return 0; | |
534 | end Find; | |
535 | ||
f2acfbce CD |
536 | ------------------------- |
537 | -- K_Bigger_Than_Range -- | |
538 | ------------------------- | |
539 | ||
540 | function K_Bigger_Than_Range | |
541 | (Container : K.Sequence; | |
542 | Fst : Positive_Count_Type; | |
543 | Lst : Count_Type; | |
544 | Key : Key_Type) return Boolean | |
545 | is | |
546 | begin | |
547 | for I in Fst .. Lst loop | |
548 | if not (K.Get (Container, I) < Key) then | |
549 | return False; | |
550 | end if; | |
551 | end loop; | |
552 | return True; | |
553 | end K_Bigger_Than_Range; | |
554 | ||
555 | --------------- | |
556 | -- K_Is_Find -- | |
557 | --------------- | |
558 | ||
559 | function K_Is_Find | |
560 | (Container : K.Sequence; | |
561 | Key : Key_Type; | |
562 | Position : Count_Type) return Boolean | |
563 | is | |
564 | begin | |
565 | for I in 1 .. Position - 1 loop | |
566 | if Key < K.Get (Container, I) then | |
567 | return False; | |
568 | end if; | |
569 | end loop; | |
570 | ||
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 | |
574 | return False; | |
575 | end if; | |
576 | end loop; | |
577 | end if; | |
578 | return True; | |
579 | end K_Is_Find; | |
580 | ||
581 | -------------------------- | |
582 | -- K_Smaller_Than_Range -- | |
583 | -------------------------- | |
584 | ||
585 | function K_Smaller_Than_Range | |
586 | (Container : K.Sequence; | |
587 | Fst : Positive_Count_Type; | |
588 | Lst : Count_Type; | |
589 | Key : Key_Type) return Boolean | |
590 | is | |
591 | begin | |
592 | for I in Fst .. Lst loop | |
593 | if not (Key < K.Get (Container, I)) then | |
594 | return False; | |
595 | end if; | |
596 | end loop; | |
597 | return True; | |
598 | end K_Smaller_Than_Range; | |
599 | ||
600 | ---------- | |
601 | -- Keys -- | |
602 | ---------- | |
603 | ||
604 | function Keys (Container : Map) return K.Sequence is | |
605 | Position : Count_Type := Container.First; | |
606 | R : K.Sequence; | |
607 | ||
608 | begin | |
609 | -- Can't use First, Next or Element here, since they depend on models | |
610 | -- for their postconditions. | |
611 | ||
612 | while Position /= 0 loop | |
613 | R := K.Add (R, Container.Nodes (Position).Key); | |
614 | Position := Tree_Operations.Next (Container, Position); | |
615 | end loop; | |
616 | ||
617 | return R; | |
618 | end Keys; | |
619 | ||
620 | ---------------------------- | |
621 | -- Lift_Abstraction_Level -- | |
622 | ---------------------------- | |
623 | ||
624 | procedure Lift_Abstraction_Level (Container : Map) is null; | |
625 | ||
626 | ----------- | |
627 | -- Model -- | |
628 | ----------- | |
629 | ||
630 | function Model (Container : Map) return M.Map is | |
631 | Position : Count_Type := Container.First; | |
632 | R : M.Map; | |
633 | ||
634 | begin | |
635 | -- Can't use First, Next or Element here, since they depend on models | |
636 | -- for their postconditions. | |
637 | ||
638 | while Position /= 0 loop | |
d5fa5335 HK |
639 | R := |
640 | M.Add | |
641 | (Container => R, | |
642 | New_Key => Container.Nodes (Position).Key, | |
643 | New_Item => Container.Nodes (Position).Element); | |
644 | ||
f2acfbce CD |
645 | Position := Tree_Operations.Next (Container, Position); |
646 | end loop; | |
647 | ||
648 | return R; | |
649 | end Model; | |
650 | ||
651 | ------------------------- | |
652 | -- P_Positions_Shifted -- | |
653 | ------------------------- | |
654 | ||
655 | function P_Positions_Shifted | |
656 | (Small : P.Map; | |
657 | Big : P.Map; | |
658 | Cut : Positive_Count_Type; | |
659 | Count : Count_Type := 1) return Boolean | |
660 | is | |
661 | begin | |
662 | for Cu of Small loop | |
663 | if not P.Has_Key (Big, Cu) then | |
664 | return False; | |
665 | end if; | |
666 | end loop; | |
667 | ||
668 | for Cu of Big loop | |
669 | declare | |
670 | Pos : constant Positive_Count_Type := P.Get (Big, Cu); | |
671 | ||
672 | begin | |
673 | if Pos < Cut then | |
674 | if not P.Has_Key (Small, Cu) | |
675 | or else Pos /= P.Get (Small, Cu) | |
676 | then | |
677 | return False; | |
678 | end if; | |
679 | ||
680 | elsif Pos >= Cut + Count then | |
681 | if not P.Has_Key (Small, Cu) | |
682 | or else Pos /= P.Get (Small, Cu) + Count | |
683 | then | |
684 | return False; | |
685 | end if; | |
686 | ||
687 | else | |
688 | if P.Has_Key (Small, Cu) then | |
689 | return False; | |
690 | end if; | |
691 | end if; | |
692 | end; | |
693 | end loop; | |
694 | ||
695 | return True; | |
696 | end P_Positions_Shifted; | |
697 | ||
698 | --------------- | |
699 | -- Positions -- | |
700 | --------------- | |
701 | ||
702 | function Positions (Container : Map) return P.Map is | |
703 | I : Count_Type := 1; | |
704 | Position : Count_Type := Container.First; | |
705 | R : P.Map; | |
706 | ||
707 | begin | |
708 | -- Can't use First, Next or Element here, since they depend on models | |
709 | -- for their postconditions. | |
710 | ||
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); | |
715 | I := I + 1; | |
716 | end loop; | |
717 | ||
718 | return R; | |
719 | end Positions; | |
720 | ||
721 | end Formal_Model; | |
722 | ||
bd65a2d7 AC |
723 | ---------- |
724 | -- Free -- | |
725 | ---------- | |
726 | ||
727 | procedure Free | |
686d0984 | 728 | (Tree : in out Map; |
bd65a2d7 AC |
729 | X : Count_Type) |
730 | is | |
731 | begin | |
732 | Tree.Nodes (X).Has_Element := False; | |
733 | Tree_Operations.Free (Tree, X); | |
734 | end Free; | |
735 | ||
736 | ---------------------- | |
737 | -- Generic_Allocate -- | |
738 | ---------------------- | |
739 | ||
740 | procedure Generic_Allocate | |
741 | (Tree : in out Tree_Types.Tree_Type'Class; | |
742 | Node : out Count_Type) | |
743 | is | |
bd65a2d7 AC |
744 | procedure Allocate is |
745 | new Tree_Operations.Generic_Allocate (Set_Element); | |
bd65a2d7 AC |
746 | begin |
747 | Allocate (Tree, Node); | |
748 | Tree.Nodes (Node).Has_Element := True; | |
749 | end Generic_Allocate; | |
750 | ||
751 | ----------------- | |
752 | -- Has_Element -- | |
753 | ----------------- | |
754 | ||
755 | function Has_Element (Container : Map; Position : Cursor) return Boolean is | |
756 | begin | |
757 | if Position.Node = 0 then | |
758 | return False; | |
759 | end if; | |
760 | ||
686d0984 | 761 | return Container.Nodes (Position.Node).Has_Element; |
bd65a2d7 AC |
762 | end Has_Element; |
763 | ||
764 | ------------- | |
765 | -- Include -- | |
766 | ------------- | |
767 | ||
768 | procedure Include | |
769 | (Container : in out Map; | |
770 | Key : Key_Type; | |
771 | New_Item : Element_Type) | |
772 | is | |
773 | Position : Cursor; | |
774 | Inserted : Boolean; | |
775 | ||
776 | begin | |
777 | Insert (Container, Key, New_Item, Position, Inserted); | |
778 | ||
779 | if not Inserted then | |
bd65a2d7 | 780 | declare |
686d0984 | 781 | N : Node_Type renames Container.Nodes (Position.Node); |
bd65a2d7 AC |
782 | begin |
783 | N.Key := Key; | |
784 | N.Element := New_Item; | |
785 | end; | |
786 | end if; | |
787 | end Include; | |
788 | ||
789 | procedure Insert | |
790 | (Container : in out Map; | |
791 | Key : Key_Type; | |
792 | New_Item : Element_Type; | |
793 | Position : out Cursor; | |
794 | Inserted : out Boolean) | |
795 | is | |
686d0984 | 796 | function New_Node return Node_Access; |
5ffe0bab | 797 | -- Comment ??? |
bd65a2d7 | 798 | |
686d0984 AC |
799 | procedure Insert_Post is |
800 | new Key_Ops.Generic_Insert_Post (New_Node); | |
bd65a2d7 | 801 | |
686d0984 AC |
802 | procedure Insert_Sans_Hint is |
803 | new Key_Ops.Generic_Conditional_Insert (Insert_Post); | |
bd65a2d7 | 804 | |
686d0984 AC |
805 | -------------- |
806 | -- New_Node -- | |
807 | -------------- | |
bd65a2d7 | 808 | |
686d0984 AC |
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); | |
bd65a2d7 | 812 | |
686d0984 | 813 | procedure Initialize (Node : in out Node_Type) is |
bd65a2d7 | 814 | begin |
686d0984 AC |
815 | Node.Key := Key; |
816 | Node.Element := New_Item; | |
817 | end Initialize; | |
bd65a2d7 | 818 | |
686d0984 | 819 | X : Node_Access; |
bd65a2d7 AC |
820 | |
821 | begin | |
686d0984 AC |
822 | Allocate_Node (Container, X); |
823 | return X; | |
824 | end New_Node; | |
825 | ||
5ffe0bab | 826 | -- Start of processing for Insert |
686d0984 AC |
827 | |
828 | begin | |
829 | Insert_Sans_Hint | |
830 | (Container, | |
831 | Key, | |
832 | Position.Node, | |
833 | Inserted); | |
bd65a2d7 AC |
834 | end Insert; |
835 | ||
836 | procedure Insert | |
837 | (Container : in out Map; | |
838 | Key : Key_Type; | |
839 | New_Item : Element_Type) | |
840 | is | |
841 | Position : Cursor; | |
842 | Inserted : Boolean; | |
843 | ||
844 | begin | |
845 | Insert (Container, Key, New_Item, Position, Inserted); | |
846 | ||
847 | if not Inserted then | |
848 | raise Constraint_Error with "key already in map"; | |
849 | end if; | |
850 | end Insert; | |
851 | ||
bd65a2d7 AC |
852 | -------------- |
853 | -- Is_Empty -- | |
854 | -------------- | |
855 | ||
856 | function Is_Empty (Container : Map) return Boolean is | |
857 | begin | |
858 | return Length (Container) = 0; | |
859 | end Is_Empty; | |
860 | ||
861 | ------------------------- | |
862 | -- Is_Greater_Key_Node -- | |
863 | ------------------------- | |
864 | ||
865 | function Is_Greater_Key_Node | |
866 | (Left : Key_Type; | |
867 | Right : Node_Type) return Boolean | |
868 | is | |
869 | begin | |
870 | -- k > node same as node < k | |
871 | ||
872 | return Right.Key < Left; | |
873 | end Is_Greater_Key_Node; | |
874 | ||
875 | ---------------------- | |
876 | -- Is_Less_Key_Node -- | |
877 | ---------------------- | |
878 | ||
879 | function Is_Less_Key_Node | |
880 | (Left : Key_Type; | |
881 | Right : Node_Type) return Boolean | |
882 | is | |
883 | begin | |
884 | return Left < Right.Key; | |
885 | end Is_Less_Key_Node; | |
886 | ||
bd65a2d7 AC |
887 | --------- |
888 | -- Key -- | |
889 | --------- | |
890 | ||
891 | function Key (Container : Map; Position : Cursor) return Key_Type is | |
892 | begin | |
893 | if not Has_Element (Container, Position) then | |
894 | raise Constraint_Error with | |
895 | "Position cursor of function Key has no element"; | |
896 | end if; | |
897 | ||
686d0984 | 898 | pragma Assert (Vet (Container, Position.Node), |
bd65a2d7 AC |
899 | "Position cursor of function Key is bad"); |
900 | ||
686d0984 | 901 | return Container.Nodes (Position.Node).Key; |
bd65a2d7 AC |
902 | end Key; |
903 | ||
904 | ---------- | |
905 | -- Last -- | |
906 | ---------- | |
907 | ||
908 | function Last (Container : Map) return Cursor is | |
909 | begin | |
910 | if Length (Container) = 0 then | |
911 | return No_Element; | |
912 | end if; | |
5ffe0bab | 913 | |
bd65a2d7 AC |
914 | return (Node => Container.Last); |
915 | end Last; | |
916 | ||
917 | ------------------ | |
918 | -- Last_Element -- | |
919 | ------------------ | |
920 | ||
921 | function Last_Element (Container : Map) return Element_Type is | |
922 | begin | |
923 | if Is_Empty (Container) then | |
924 | raise Constraint_Error with "map is empty"; | |
925 | end if; | |
926 | ||
686d0984 | 927 | return Container.Nodes (Last (Container).Node).Element; |
bd65a2d7 AC |
928 | end Last_Element; |
929 | ||
930 | -------------- | |
931 | -- Last_Key -- | |
932 | -------------- | |
933 | ||
934 | function Last_Key (Container : Map) return Key_Type is | |
935 | begin | |
936 | if Is_Empty (Container) then | |
937 | raise Constraint_Error with "map is empty"; | |
938 | end if; | |
939 | ||
686d0984 | 940 | return Container.Nodes (Last (Container).Node).Key; |
bd65a2d7 AC |
941 | end Last_Key; |
942 | ||
bd65a2d7 AC |
943 | -------------- |
944 | -- Left_Son -- | |
945 | -------------- | |
946 | ||
947 | function Left_Son (Node : Node_Type) return Count_Type is | |
948 | begin | |
949 | return Node.Left; | |
950 | end Left_Son; | |
951 | ||
952 | ------------ | |
953 | -- Length -- | |
954 | ------------ | |
955 | ||
956 | function Length (Container : Map) return Count_Type is | |
957 | begin | |
686d0984 | 958 | return Container.Length; |
bd65a2d7 AC |
959 | end Length; |
960 | ||
961 | ---------- | |
962 | -- Move -- | |
963 | ---------- | |
964 | ||
965 | procedure Move (Target : in out Map; Source : in out Map) is | |
686d0984 | 966 | NN : Tree_Types.Nodes_Type renames Source.Nodes; |
bd65a2d7 AC |
967 | X : Node_Access; |
968 | ||
969 | begin | |
bd65a2d7 AC |
970 | if Target'Address = Source'Address then |
971 | return; | |
972 | end if; | |
973 | ||
974 | if Target.Capacity < Length (Source) then | |
975 | raise Constraint_Error with -- ??? | |
976 | "Source length exceeds Target capacity"; | |
977 | end if; | |
978 | ||
bd65a2d7 AC |
979 | Clear (Target); |
980 | ||
981 | loop | |
982 | X := First (Source).Node; | |
983 | exit when X = 0; | |
984 | ||
985 | -- Here we insert a copy of the source element into the target, and | |
5ffe0bab | 986 | -- then delete the element from the source. Another possibility is |
bd65a2d7 AC |
987 | -- that delete it first (and hang onto its index), then insert it. |
988 | -- ??? | |
989 | ||
990 | Insert (Target, NN (X).Key, NN (X).Element); -- optimize??? | |
991 | ||
686d0984 AC |
992 | Tree_Operations.Delete_Node_Sans_Free (Source, X); |
993 | Formal_Ordered_Maps.Free (Source, X); | |
bd65a2d7 AC |
994 | end loop; |
995 | end Move; | |
996 | ||
997 | ---------- | |
998 | -- Next -- | |
999 | ---------- | |
1000 | ||
bd65a2d7 AC |
1001 | procedure Next (Container : Map; Position : in out Cursor) is |
1002 | begin | |
1003 | Position := Next (Container, Position); | |
1004 | end Next; | |
1005 | ||
1006 | function Next (Container : Map; Position : Cursor) return Cursor is | |
1007 | begin | |
1008 | if Position = No_Element then | |
1009 | return No_Element; | |
1010 | end if; | |
1011 | ||
1012 | if not Has_Element (Container, Position) then | |
1013 | raise Constraint_Error; | |
1014 | end if; | |
1015 | ||
686d0984 | 1016 | pragma Assert (Vet (Container, Position.Node), |
bd65a2d7 AC |
1017 | "bad cursor in Next"); |
1018 | ||
686d0984 | 1019 | return (Node => Tree_Operations.Next (Container, Position.Node)); |
bd65a2d7 AC |
1020 | end Next; |
1021 | ||
bd65a2d7 AC |
1022 | ------------ |
1023 | -- Parent -- | |
1024 | ------------ | |
1025 | ||
1026 | function Parent (Node : Node_Type) return Count_Type is | |
1027 | begin | |
1028 | return Node.Parent; | |
1029 | end Parent; | |
1030 | ||
1031 | -------------- | |
1032 | -- Previous -- | |
1033 | -------------- | |
1034 | ||
1035 | procedure Previous (Container : Map; Position : in out Cursor) is | |
1036 | begin | |
1037 | Position := Previous (Container, Position); | |
1038 | end Previous; | |
1039 | ||
1040 | function Previous (Container : Map; Position : Cursor) return Cursor is | |
1041 | begin | |
1042 | if Position = No_Element then | |
1043 | return No_Element; | |
1044 | end if; | |
1045 | ||
1046 | if not Has_Element (Container, Position) then | |
1047 | raise Constraint_Error; | |
1048 | end if; | |
1049 | ||
686d0984 | 1050 | pragma Assert (Vet (Container, Position.Node), |
bd65a2d7 AC |
1051 | "bad cursor in Previous"); |
1052 | ||
bd65a2d7 | 1053 | declare |
bd65a2d7 | 1054 | Node : constant Count_Type := |
15f0f591 | 1055 | Tree_Operations.Previous (Container, Position.Node); |
bd65a2d7 AC |
1056 | |
1057 | begin | |
1058 | if Node = 0 then | |
1059 | return No_Element; | |
1060 | end if; | |
1061 | ||
1062 | return (Node => Node); | |
1063 | end; | |
1064 | end Previous; | |
1065 | ||
bd65a2d7 AC |
1066 | ------------- |
1067 | -- Replace -- | |
1068 | ------------- | |
1069 | ||
1070 | procedure Replace | |
1071 | (Container : in out Map; | |
1072 | Key : Key_Type; | |
1073 | New_Item : Element_Type) | |
1074 | is | |
1075 | begin | |
bd65a2d7 | 1076 | declare |
686d0984 | 1077 | Node : constant Node_Access := Key_Ops.Find (Container, Key); |
bd65a2d7 AC |
1078 | |
1079 | begin | |
1080 | if Node = 0 then | |
1081 | raise Constraint_Error with "key not in map"; | |
1082 | end if; | |
1083 | ||
bd65a2d7 | 1084 | declare |
686d0984 | 1085 | N : Node_Type renames Container.Nodes (Node); |
bd65a2d7 AC |
1086 | begin |
1087 | N.Key := Key; | |
1088 | N.Element := New_Item; | |
1089 | end; | |
1090 | end; | |
1091 | end Replace; | |
1092 | ||
1093 | --------------------- | |
1094 | -- Replace_Element -- | |
1095 | --------------------- | |
1096 | ||
1097 | procedure Replace_Element | |
1098 | (Container : in out Map; | |
1099 | Position : Cursor; | |
1100 | New_Item : Element_Type) | |
1101 | is | |
1102 | begin | |
bd65a2d7 AC |
1103 | if not Has_Element (Container, Position) then |
1104 | raise Constraint_Error with | |
1105 | "Position cursor of Replace_Element has no element"; | |
1106 | end if; | |
1107 | ||
686d0984 | 1108 | pragma Assert (Vet (Container, Position.Node), |
bd65a2d7 AC |
1109 | "Position cursor of Replace_Element is bad"); |
1110 | ||
686d0984 | 1111 | Container.Nodes (Position.Node).Element := New_Item; |
bd65a2d7 AC |
1112 | end Replace_Element; |
1113 | ||
bd65a2d7 AC |
1114 | --------------- |
1115 | -- Right_Son -- | |
1116 | --------------- | |
1117 | ||
1118 | function Right_Son (Node : Node_Type) return Count_Type is | |
1119 | begin | |
1120 | return Node.Right; | |
1121 | end Right_Son; | |
1122 | ||
1123 | --------------- | |
1124 | -- Set_Color -- | |
1125 | --------------- | |
1126 | ||
5ffe0bab | 1127 | procedure Set_Color (Node : in out Node_Type; Color : Color_Type) is |
bd65a2d7 AC |
1128 | begin |
1129 | Node.Color := Color; | |
1130 | end Set_Color; | |
1131 | ||
1132 | -------------- | |
1133 | -- Set_Left -- | |
1134 | -------------- | |
1135 | ||
1136 | procedure Set_Left (Node : in out Node_Type; Left : Count_Type) is | |
1137 | begin | |
1138 | Node.Left := Left; | |
1139 | end Set_Left; | |
1140 | ||
1141 | ---------------- | |
1142 | -- Set_Parent -- | |
1143 | ---------------- | |
1144 | ||
1145 | procedure Set_Parent (Node : in out Node_Type; Parent : Count_Type) is | |
1146 | begin | |
1147 | Node.Parent := Parent; | |
1148 | end Set_Parent; | |
1149 | ||
1150 | --------------- | |
1151 | -- Set_Right -- | |
1152 | --------------- | |
1153 | ||
1154 | procedure Set_Right (Node : in out Node_Type; Right : Count_Type) is | |
1155 | begin | |
1156 | Node.Right := Right; | |
1157 | end Set_Right; | |
1158 | ||
bd65a2d7 | 1159 | end Ada.Containers.Formal_Ordered_Maps; |