GCC v8.2
[gcc.git] / gcc / ada / libgnat / a-cforma.adb
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-2018, 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;