Natools

--                                                                          --
-- All the subprograms here have the semantics of standard indefinite       --
-- ordered maps (see ARM A.18.6), except for tampering, which becomes       --
-- irrelevant.                                                              --
------------------------------------------------------------------------------

with Ada.Containers.Indefinite_Ordered_Maps;
with Ada.Iterator_Interfaces;

private with Ada.Finalization;
private with Ada.Unchecked_Deallocation;
private with Natools.References;
private with Natools.Storage_Pools;

generic
   type Key_Type (<>) is private;
   type Element_Type (<>) is private;
   with function "<" (Left, Right : Key_Type) return Boolean is <>;
   with function "=" (Left, Right : Element_Type) return Boolean is <>;

package Natools.Constant_Indefinite_Ordered_Maps is
   pragma Preelaborate;

   package Unsafe_Maps is new Ada.Containers.Indefinite_Ordered_Maps
     (Key_Type, Element_Type);

   type Cursor is private;  --  with Type_Invariant => Is_Valid (Cursor);
   pragma Preelaborable_Initialization (Cursor);

   No_Element : constant Cursor;

   procedure Clear (Position : in out Cursor);
   function Is_Valid (Position : Cursor) return Boolean;

   function Has_Element (Position : Cursor) return Boolean;

   function ">" (Left : Cursor; Right : Key_Type) return Boolean
     with Pre => Has_Element (Left) or else raise Constraint_Error;
   function "<" (Left : Key_Type; Right : Cursor) return Boolean
     with Pre => Has_Element (Right) or else raise Constraint_Error;
   function ">" (Left : Key_Type; Right : Cursor) return Boolean
     with Pre => Has_Element (Right) or else raise Constraint_Error;


   package Map_Iterator_Interfaces is new Ada.Iterator_Interfaces
     (Cursor, Has_Element);


   type Constant_Map is tagged private;
--   TODO: add aspects when they don't put GNAT in an infinite loop
--   with Constant_Indexing => Constant_Reference,
--        Default_Iterator => Iterate,
--        Iterator_Element => Element_Type;
   pragma Preelaborable_Initialization (Constant_Map);

   procedure Clear (Container : in out Constant_Map);
   function Create (Source : Unsafe_Maps.Map) return Constant_Map;
   procedure Move (Target : in out Constant_Map; Source : in out Constant_Map);
   procedure Replace
     (Container : in out Constant_Map;
      New_Items : in Unsafe_Maps.Map);

     (Container : in Constant_Map;
      Process : not null access procedure (Position : in Cursor));

   procedure Reverse_Iterate
     (Container : in Constant_Map;
      Process : not null access procedure (Position : in Cursor));

   function Iterate (Container : in Constant_Map)
     return Map_Iterator_Interfaces.Reversible_Iterator'Class;

   function Iterate (Container : in Constant_Map; Start : in Cursor)
     return Map_Iterator_Interfaces.Reversible_Iterator'Class;


   type Constant_Reference_Type
     (Element : not null access constant Element_Type) is private
     with Implicit_Dereference => Element;

   function Constant_Reference
     (Container : aliased in Constant_Map;
      Position : in Cursor)
     return Constant_Reference_Type;

   function Constant_Reference
     (Container : aliased in Constant_Map;
      Key : in Key_Type)
     return Constant_Reference_Type;


   type Updatable_Map is new Constant_Map with private
     with Constant_Indexing => Constant_Reference,
          Variable_Indexing => Reference,
          Default_Iterator => Iterate,
          Iterator_Element => Element_Type;
   pragma Preelaborable_Initialization (Updatable_Map);

   procedure Update_Element
     (Container : in out Updatable_Map;
      Position : in Cursor;
      Process : not null access procedure (Key : in Key_Type;
                                           Element : in out Element_Type))
     with Pre => (Has_Element (Position) or else raise Constraint_Error)
      and then (Is_Related (Container, Position) or else raise Program_Error);


   type Reference_Type (Element : not null access Element_Type) is private
     with Implicit_Dereference => Element;

   function Reference
     (Container : aliased in out Updatable_Map;
      Position : in Cursor)
     return Reference_Type;

   function Reference
     (Container : aliased in out Updatable_Map;
      Key : in Key_Type)
     return Reference_Type;


private

   type Key_Access is access Key_Type;
   type Element_Access is access Element_Type;

   type Node is record

   function Has_Element (Position : Cursor) return Boolean
     is (not Position.Is_Empty);

   function Is_Related (Container : Constant_Map; Position : Cursor)
     return Boolean
     is (Backend_Refs."=" (Container.Backend, Position.Backend));


   type Constant_Reference_Type
     (Element : not null access constant Element_Type)
   is record
      Backend : Backend_Refs.Immutable_Reference;
   end record;


   type Reference_Type (Element : not null access Element_Type) is record
      Backend : Backend_Refs.Immutable_Reference;
   end record;


   type Iterator is new Map_Iterator_Interfaces.Reversible_Iterator with record
      Backend : Backend_Refs.Immutable_Reference;
      Start : Cursor := No_Element;
   end record;

   overriding function First (Object : Iterator) return Cursor;
   overriding function Last  (Object : Iterator) return Cursor;

   overriding function Next
     (Object   : Iterator;
      Position : Cursor) return Cursor
     is (Next (Position))
     with Pre => Position.Is_Empty
        or else Backend_Refs."=" (Position.Backend, Object.Backend);

   overriding function Previous
     (Object   : Iterator;
      Position : Cursor) return Cursor
     is (Previous (Position))
     with Pre => Position.Is_Empty
        or else Backend_Refs."=" (Position.Backend, Object.Backend);


   No_Element : constant Cursor := (Is_Empty => True);

end Natools.Constant_Indefinite_Ordered_Maps;