|
111
|
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 -- --
|
|
|
9 -- Copyright (C) 2010-2017, Free Software Foundation, Inc. --
|
|
|
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
|
|
|
37 package body Ada.Containers.Formal_Ordered_Maps with
|
|
|
38 SPARK_Mode => Off
|
|
|
39 is
|
|
|
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
|
|
|
48 function Color
|
|
|
49 (Node : Node_Type) return Ada.Containers.Red_Black_Trees.Color_Type;
|
|
|
50 pragma Inline (Color);
|
|
|
51
|
|
|
52 function Left_Son (Node : Node_Type) return Count_Type;
|
|
|
53 pragma Inline (Left_Son);
|
|
|
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;
|
|
|
59 pragma Inline (Right_Son);
|
|
|
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
|
|
|
79 -- All need comments ???
|
|
|
80
|
|
|
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
|
|
|
87 procedure Free (Tree : in out Map; X : Count_Type);
|
|
|
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
|
|
|
99 --------------------------
|
|
|
100 -- Local Instantiations --
|
|
|
101 --------------------------
|
|
|
102
|
|
|
103 package Tree_Operations is
|
|
|
104 new Red_Black_Trees.Generic_Bounded_Operations
|
|
|
105 (Tree_Types => Tree_Types,
|
|
|
106 Left => Left_Son,
|
|
|
107 Right => Right_Son);
|
|
|
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;
|
|
|
124 Node : Count_Type;
|
|
|
125 ENode : Count_Type;
|
|
|
126
|
|
|
127 begin
|
|
|
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
|
|
|
136 Lst := Next (Left, Last (Left).Node);
|
|
|
137
|
|
|
138 Node := First (Left).Node;
|
|
|
139 while Node /= Lst loop
|
|
|
140 ENode := Find (Right, Left.Nodes (Node).Key).Node;
|
|
|
141
|
|
|
142 if ENode = 0 or else
|
|
|
143 Left.Nodes (Node).Element /= Right.Nodes (ENode).Element
|
|
|
144 then
|
|
|
145 return False;
|
|
|
146 end if;
|
|
|
147
|
|
|
148 Node := Next (Left, Node);
|
|
|
149 end loop;
|
|
|
150
|
|
|
151 return True;
|
|
|
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
|
|
|
169 SN : Node_Type renames Source.Nodes (Source_Node);
|
|
|
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
|
|
|
177 procedure Insert_Post is new Key_Ops.Generic_Insert_Post (New_Node);
|
|
|
178
|
|
|
179 procedure Unconditional_Insert_Sans_Hint is
|
|
|
180 new Key_Ops.Generic_Unconditional_Insert (Insert_Post);
|
|
|
181
|
|
|
182 procedure Unconditional_Insert_Avec_Hint is
|
|
|
183 new Key_Ops.Generic_Unconditional_Insert_With_Hint
|
|
|
184 (Insert_Post,
|
|
|
185 Unconditional_Insert_Sans_Hint);
|
|
|
186
|
|
|
187 procedure Allocate is new Generic_Allocate (Set_Element);
|
|
|
188
|
|
|
189 --------------
|
|
|
190 -- New_Node --
|
|
|
191 --------------
|
|
|
192
|
|
|
193 function New_Node return Count_Type is
|
|
|
194 Result : Count_Type;
|
|
|
195 begin
|
|
|
196 Allocate (Target, Result);
|
|
|
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
|
|
|
216 (Tree => Target,
|
|
|
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
|
|
|
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
|
|
|
233 Tree_Operations.Clear_Tree (Target);
|
|
|
234 Append_Elements (Source);
|
|
|
235 end Assign;
|
|
|
236
|
|
|
237 -------------
|
|
|
238 -- Ceiling --
|
|
|
239 -------------
|
|
|
240
|
|
|
241 function Ceiling (Container : Map; Key : Key_Type) return Cursor is
|
|
|
242 Node : constant Count_Type := Key_Ops.Ceiling (Container, Key);
|
|
|
243
|
|
|
244 begin
|
|
|
245 if Node = 0 then
|
|
|
246 return No_Element;
|
|
|
247 end if;
|
|
|
248
|
|
|
249 return (Node => Node);
|
|
|
250 end Ceiling;
|
|
|
251
|
|
|
252 -----------
|
|
|
253 -- Clear --
|
|
|
254 -----------
|
|
|
255
|
|
|
256 procedure Clear (Container : in out Map) is
|
|
|
257 begin
|
|
|
258 Tree_Operations.Clear_Tree (Container);
|
|
|
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;
|
|
|
286
|
|
|
287 begin
|
|
|
288 if 0 < Capacity and then Capacity < Source.Capacity then
|
|
|
289 raise Capacity_Error;
|
|
|
290 end if;
|
|
|
291
|
|
|
292 return Target : Map (Count_Type'Max (Source.Capacity, Capacity)) do
|
|
|
293 if Length (Source) > 0 then
|
|
|
294 Target.Length := Source.Length;
|
|
|
295 Target.Root := Source.Root;
|
|
|
296 Target.First := Source.First;
|
|
|
297 Target.Last := Source.Last;
|
|
|
298 Target.Free := Source.Free;
|
|
|
299
|
|
|
300 while Node <= Source.Capacity loop
|
|
|
301 Target.Nodes (Node).Element :=
|
|
|
302 Source.Nodes (Node).Element;
|
|
|
303 Target.Nodes (Node).Key :=
|
|
|
304 Source.Nodes (Node).Key;
|
|
|
305 Target.Nodes (Node).Parent :=
|
|
|
306 Source.Nodes (Node).Parent;
|
|
|
307 Target.Nodes (Node).Left :=
|
|
|
308 Source.Nodes (Node).Left;
|
|
|
309 Target.Nodes (Node).Right :=
|
|
|
310 Source.Nodes (Node).Right;
|
|
|
311 Target.Nodes (Node).Color :=
|
|
|
312 Source.Nodes (Node).Color;
|
|
|
313 Target.Nodes (Node).Has_Element :=
|
|
|
314 Source.Nodes (Node).Has_Element;
|
|
|
315 Node := Node + 1;
|
|
|
316 end loop;
|
|
|
317
|
|
|
318 while Node <= Target.Capacity loop
|
|
|
319 N := Node;
|
|
|
320 Formal_Ordered_Maps.Free (Tree => Target, X => N);
|
|
|
321 Node := Node + 1;
|
|
|
322 end loop;
|
|
|
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
|
|
|
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
|
|
|
338 pragma Assert (Vet (Container, Position.Node),
|
|
|
339 "Position cursor of Delete is bad");
|
|
|
340
|
|
|
341 Tree_Operations.Delete_Node_Sans_Free (Container,
|
|
|
342 Position.Node);
|
|
|
343 Formal_Ordered_Maps.Free (Container, Position.Node);
|
|
|
344 Position := No_Element;
|
|
|
345 end Delete;
|
|
|
346
|
|
|
347 procedure Delete (Container : in out Map; Key : Key_Type) is
|
|
|
348 X : constant Node_Access := Key_Ops.Find (Container, Key);
|
|
|
349
|
|
|
350 begin
|
|
|
351 if X = 0 then
|
|
|
352 raise Constraint_Error with "key not in map";
|
|
|
353 end if;
|
|
|
354
|
|
|
355 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
356 Formal_Ordered_Maps.Free (Container, X);
|
|
|
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;
|
|
|
365 begin
|
|
|
366 if X /= 0 then
|
|
|
367 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
368 Formal_Ordered_Maps.Free (Container, X);
|
|
|
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;
|
|
|
378 begin
|
|
|
379 if X /= 0 then
|
|
|
380 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
381 Formal_Ordered_Maps.Free (Container, X);
|
|
|
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
|
|
|
396 pragma Assert (Vet (Container, Position.Node),
|
|
|
397 "Position cursor of function Element is bad");
|
|
|
398
|
|
|
399 return Container.Nodes (Position.Node).Element;
|
|
|
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
|
|
|
411 return Container.Nodes (Node).Element;
|
|
|
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
|
|
|
434 X : constant Node_Access := Key_Ops.Find (Container, Key);
|
|
|
435 begin
|
|
|
436 if X /= 0 then
|
|
|
437 Tree_Operations.Delete_Node_Sans_Free (Container, X);
|
|
|
438 Formal_Ordered_Maps.Free (Container, X);
|
|
|
439 end if;
|
|
|
440 end Exclude;
|
|
|
441
|
|
|
442 ----------
|
|
|
443 -- Find --
|
|
|
444 ----------
|
|
|
445
|
|
|
446 function Find (Container : Map; Key : Key_Type) return Cursor is
|
|
|
447 Node : constant Count_Type := Key_Ops.Find (Container, Key);
|
|
|
448
|
|
|
449 begin
|
|
|
450 if Node = 0 then
|
|
|
451 return No_Element;
|
|
|
452 end if;
|
|
|
453
|
|
|
454 return (Node => Node);
|
|
|
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
|
|
|
467 return (Node => Container.First);
|
|
|
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
|
|
|
480 return Container.Nodes (First (Container).Node).Element;
|
|
|
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
|
|
|
493 return Container.Nodes (First (Container).Node).Key;
|
|
|
494 end First_Key;
|
|
|
495
|
|
|
496 -----------
|
|
|
497 -- Floor --
|
|
|
498 -----------
|
|
|
499
|
|
|
500 function Floor (Container : Map; Key : Key_Type) return Cursor is
|
|
|
501 Node : constant Count_Type := Key_Ops.Floor (Container, Key);
|
|
|
502
|
|
|
503 begin
|
|
|
504 if Node = 0 then
|
|
|
505 return No_Element;
|
|
|
506 end if;
|
|
|
507
|
|
|
508 return (Node => Node);
|
|
|
509 end Floor;
|
|
|
510
|
|
|
511 ------------------
|
|
|
512 -- Formal_Model --
|
|
|
513 ------------------
|
|
|
514
|
|
|
515 package body Formal_Model is
|
|
|
516
|
|
|
517 ----------
|
|
|
518 -- Find --
|
|
|
519 ----------
|
|
|
520
|
|
|
521 function Find
|
|
|
522 (Container : K.Sequence;
|
|
|
523 Key : Key_Type) return Count_Type
|
|
|
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
|
|
|
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
|
|
|
639 R :=
|
|
|
640 M.Add
|
|
|
641 (Container => R,
|
|
|
642 New_Key => Container.Nodes (Position).Key,
|
|
|
643 New_Item => Container.Nodes (Position).Element);
|
|
|
644
|
|
|
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
|
|
|
723 ----------
|
|
|
724 -- Free --
|
|
|
725 ----------
|
|
|
726
|
|
|
727 procedure Free
|
|
|
728 (Tree : in out Map;
|
|
|
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
|
|
|
744 procedure Allocate is
|
|
|
745 new Tree_Operations.Generic_Allocate (Set_Element);
|
|
|
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
|
|
|
761 return Container.Nodes (Position.Node).Has_Element;
|
|
|
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
|
|
|
780 declare
|
|
|
781 N : Node_Type renames Container.Nodes (Position.Node);
|
|
|
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
|
|
|
796 function New_Node return Node_Access;
|
|
|
797 -- Comment ???
|
|
|
798
|
|
|
799 procedure Insert_Post is
|
|
|
800 new Key_Ops.Generic_Insert_Post (New_Node);
|
|
|
801
|
|
|
802 procedure Insert_Sans_Hint is
|
|
|
803 new Key_Ops.Generic_Conditional_Insert (Insert_Post);
|
|
|
804
|
|
|
805 --------------
|
|
|
806 -- New_Node --
|
|
|
807 --------------
|
|
|
808
|
|
|
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);
|
|
|
812
|
|
|
813 procedure Initialize (Node : in out Node_Type) is
|
|
|
814 begin
|
|
|
815 Node.Key := Key;
|
|
|
816 Node.Element := New_Item;
|
|
|
817 end Initialize;
|
|
|
818
|
|
|
819 X : Node_Access;
|
|
|
820
|
|
|
821 begin
|
|
|
822 Allocate_Node (Container, X);
|
|
|
823 return X;
|
|
|
824 end New_Node;
|
|
|
825
|
|
|
826 -- Start of processing for Insert
|
|
|
827
|
|
|
828 begin
|
|
|
829 Insert_Sans_Hint
|
|
|
830 (Container,
|
|
|
831 Key,
|
|
|
832 Position.Node,
|
|
|
833 Inserted);
|
|
|
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
|
|
|
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
|
|
|
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
|
|
|
898 pragma Assert (Vet (Container, Position.Node),
|
|
|
899 "Position cursor of function Key is bad");
|
|
|
900
|
|
|
901 return Container.Nodes (Position.Node).Key;
|
|
|
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;
|
|
|
913
|
|
|
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
|
|
|
927 return Container.Nodes (Last (Container).Node).Element;
|
|
|
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
|
|
|
940 return Container.Nodes (Last (Container).Node).Key;
|
|
|
941 end Last_Key;
|
|
|
942
|
|
|
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
|
|
|
958 return Container.Length;
|
|
|
959 end Length;
|
|
|
960
|
|
|
961 ----------
|
|
|
962 -- Move --
|
|
|
963 ----------
|
|
|
964
|
|
|
965 procedure Move (Target : in out Map; Source : in out Map) is
|
|
|
966 NN : Tree_Types.Nodes_Type renames Source.Nodes;
|
|
|
967 X : Node_Access;
|
|
|
968
|
|
|
969 begin
|
|
|
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
|
|
|
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
|
|
|
986 -- then delete the element from the source. Another possibility is
|
|
|
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
|
|
|
992 Tree_Operations.Delete_Node_Sans_Free (Source, X);
|
|
|
993 Formal_Ordered_Maps.Free (Source, X);
|
|
|
994 end loop;
|
|
|
995 end Move;
|
|
|
996
|
|
|
997 ----------
|
|
|
998 -- Next --
|
|
|
999 ----------
|
|
|
1000
|
|
|
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
|
|
|
1016 pragma Assert (Vet (Container, Position.Node),
|
|
|
1017 "bad cursor in Next");
|
|
|
1018
|
|
|
1019 return (Node => Tree_Operations.Next (Container, Position.Node));
|
|
|
1020 end Next;
|
|
|
1021
|
|
|
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
|
|
|
1050 pragma Assert (Vet (Container, Position.Node),
|
|
|
1051 "bad cursor in Previous");
|
|
|
1052
|
|
|
1053 declare
|
|
|
1054 Node : constant Count_Type :=
|
|
|
1055 Tree_Operations.Previous (Container, Position.Node);
|
|
|
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
|
|
|
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
|
|
|
1076 declare
|
|
|
1077 Node : constant Node_Access := Key_Ops.Find (Container, Key);
|
|
|
1078
|
|
|
1079 begin
|
|
|
1080 if Node = 0 then
|
|
|
1081 raise Constraint_Error with "key not in map";
|
|
|
1082 end if;
|
|
|
1083
|
|
|
1084 declare
|
|
|
1085 N : Node_Type renames Container.Nodes (Node);
|
|
|
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
|
|
|
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
|
|
|
1108 pragma Assert (Vet (Container, Position.Node),
|
|
|
1109 "Position cursor of Replace_Element is bad");
|
|
|
1110
|
|
|
1111 Container.Nodes (Position.Node).Element := New_Item;
|
|
|
1112 end Replace_Element;
|
|
|
1113
|
|
|
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
|
|
|
1127 procedure Set_Color (Node : in out Node_Type; Color : Color_Type) is
|
|
|
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
|
|
|
1159 end Ada.Containers.Formal_Ordered_Maps;
|
