------------------------------------------------------------------------------
-- Copyright (c) 2014-2015, Natacha Porté --
-- --
-- Permission to use, copy, modify, and distribute this software for any --
-- purpose with or without fee is hereby granted, provided that the above --
-- copyright notice and this permission notice appear in all copies. --
-- --
-- THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES --
-- WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF --
-- MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR --
-- ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES --
-- WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN --
-- ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF --
-- OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. --
------------------------------------------------------------------------------
------------------------------------------------------------------------------
-- Natools.Constant_Indefinite_Ordered_Sets provides an implementation of --
-- indefinite ordered maps with immutable mapping, based on a sorted array. --
-- This makes it task-safe as long as the mapping is only read. --
-- --
-- All the types exposed have referential semantics, in that assignment is --
-- cheap and uses the same actual object. It is as task-safe as the current --
-- implementation of Natools.References. --
-- Cursors also hold a reference, which is used to identify the parent map, --
-- so after an assignment or a call to Clear or Move, the link between the --
-- map object and the cursor is broken, but the cursor is still usable and --
-- behaves as the original version of the maps. --
-- --
-- There are two types defined here, depending on their restrictions and --
-- safety against concurrent accesses: --
-- * Constant_Map cannot be changed in any way, but is completely --
-- task-safe (unless some referential magic is performed, like --
-- tampering checks in standard containers) --
-- * Updatable_Map allows read-write operations on stored elements, but --
-- it is up to the client to ensure there operations are task-safe, --
-- e.g. by using an atomic or protected Element_Type. --
-- --
-- Insertion and deletion primitives are provided as function rather than --
-- procedures, to emphasize that they actually create a new map with the --
-- requested change. Since most of the map is blindly duplicated, they are --
-- all in O(n) time, which makes them a quite inefficient way to build --
-- maps. For a significant number of changes, it's probably better to go --
-- through an unsafe map. --
-- --
-- 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 Element (Position : Cursor) return Element_Type
with Pre => Has_Element (Position) or else raise Constraint_Error;
function Key (Position : Cursor) return Key_Type
with Pre => Has_Element (Position) or else raise Constraint_Error;
procedure Query_Element
(Position : in Cursor;
Process : not null access procedure (Key : in Key_Type;
Element : in Element_Type))
with Pre => Has_Element (Position) or else raise Constraint_Error;
function Next (Position : Cursor) return Cursor;
procedure Next (Position : in out Cursor);
function Previous (Position : Cursor) return Cursor;
procedure Previous (Position : in out Cursor);
function "<" (Left, Right : Cursor) return Boolean
with Pre => (Has_Element (Left) and then Has_Element (Right))
or else raise Constraint_Error;
function ">" (Left, Right : Cursor) return Boolean
with Pre => (Has_Element (Left) and then Has_Element (Right))
or else raise Constraint_Error;
function "<" (Left : Cursor; Right : Key_Type) return Boolean
with Pre => Has_Element (Left) or else raise Constraint_Error;
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);
function To_Unsafe_Map (Container : Constant_Map) return Unsafe_Maps.Map;
function Is_Related (Container : Constant_Map; Position : Cursor)
return Boolean;
function "=" (Left, Right : Constant_Map) return Boolean;
function Length (Container : Constant_Map) return Ada.Containers.Count_Type;
function Is_Empty (Container : Constant_Map) return Boolean;
function First (Container : Constant_Map) return Cursor;
function First_Element (Container : Constant_Map) return Element_Type
with Pre => (not Is_Empty (Container)) or else raise Constraint_Error;
function First_Key (Container : Constant_Map) return Key_Type
with Pre => (not Is_Empty (Container)) or else raise Constraint_Error;
function Last (Container : Constant_Map) return Cursor;
function Last_Element (Container : Constant_Map) return Element_Type
with Pre => (not Is_Empty (Container)) or else raise Constraint_Error;
function Last_Key (Container : Constant_Map) return Key_Type
with Pre => (not Is_Empty (Container)) or else raise Constraint_Error;
function Find (Container : Constant_Map; Key : Key_Type) return Cursor;
function Element
(Container : Constant_Map;
Key : Key_Type)
return Element_Type;
function Floor (Container : Constant_Map; Key : Key_Type) return Cursor;
function Ceiling (Container : Constant_Map; Key : Key_Type) return Cursor;
function Contains (Container : Constant_Map; Key : Key_Type) return Boolean;
procedure Iterate
(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;
function Iterate (Container : in Constant_Map; First, Last : 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;
function Insert
(Source : in Constant_Map;
Key : in Key_Type;
New_Item : in Element_Type;
Position : out Cursor;
Inserted : out Boolean)
return Constant_Map;
function Insert
(Source : in Constant_Map;
Key : in Key_Type;
New_Item : in Element_Type)
return Constant_Map;
function Include
(Source : in Constant_Map;
Key : in Key_Type;
New_Item : in Element_Type)
return Constant_Map;
function Replace
(Source : in Constant_Map;
Key : in Key_Type;
New_Item : in Element_Type)
return Constant_Map;
function Replace_Element
(Source : in Constant_Map;
Position : in Cursor;
New_Item : in Element_Type)
return Constant_Map;
function Replace_Element
(Source : in Constant_Map;
Position : in Cursor;
New_Item : in Element_Type;
New_Position : out Cursor)
return Constant_Map;
function Exclude
(Source : in Constant_Map;
Key : in Key_Type)
return Constant_Map;
function Delete
(Source : in Constant_Map;
Key : in Key_Type)
return Constant_Map;
function Delete
(Source : in Constant_Map;
Position : in Cursor)
return Constant_Map;
type Updatable_Map is new Constant_Map with private
with Constant_Indexing => Constant_Reference_For_Bugged_GNAT,
Variable_Indexing => Reference,
Default_Iterator => Iterate,
Iterator_Element => Element_Type;
pragma Preelaborable_Initialization (Updatable_Map);
function Constant_Reference_For_Bugged_GNAT
(Container : aliased in Updatable_Map;
Position : in Cursor)
return Constant_Reference_Type;
function Constant_Reference_For_Bugged_GNAT
(Container : aliased in Updatable_Map;
Key : in Key_Type)
return Constant_Reference_Type;
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;
Empty_Constant_Map : constant Constant_Map;
Empty_Updatable_Map : constant Updatable_Map;
private
type Key_Access is access Key_Type;
type Element_Access is access Element_Type;
type Node is record
Key : not null Key_Access;
Element : not null Element_Access;
end record;
use type Ada.Containers.Count_Type;
subtype Count_Type is Ada.Containers.Count_Type;
subtype Index_Type is Count_Type range 1 .. Count_Type'Last;
type Node_Array is array (Index_Type range <>) of Node;
procedure Free is new Ada.Unchecked_Deallocation
(Key_Type, Key_Access);
procedure Free is new Ada.Unchecked_Deallocation
(Element_Type, Element_Access);
type Backend_Array (Size : Index_Type) -- cannot be empty
is new Ada.Finalization.Limited_Controlled with
record
Nodes : Node_Array (1 .. Size);
Finalized : Boolean := False;
end record;
function Create
(Size : Index_Type;
Key_Factory : not null access function (Index : Index_Type)
return Key_Type;
Element_Factory : not null access function (Index : Index_Type)
return Element_Type)
return Backend_Array;
overriding procedure Finalize (Object : in out Backend_Array);
package Backend_Refs is new References
(Backend_Array,
Storage_Pools.Access_In_Default_Pool'Storage_Pool,
Storage_Pools.Access_In_Default_Pool'Storage_Pool);
function Make_Backend
(Size : Count_Type;
Key_Factory : not null access function (Index : Index_Type)
return Key_Type;
Element_Factory : not null access function (Index : Index_Type)
return Element_Type)
return Backend_Refs.Immutable_Reference;
function Make_Backend (Map : Unsafe_Maps.Map)
return Backend_Refs.Immutable_Reference;
procedure Search
(Nodes : in Node_Array;
Key : in Key_Type;
Floor : out Count_Type;
Ceiling : out Count_Type);
type Constant_Map is tagged record
Backend : Backend_Refs.Immutable_Reference;
end record;
function Is_Empty (Container : Constant_Map) return Boolean
is (Container.Backend.Is_Empty);
type Updatable_Map is new Constant_Map with null record;
type Cursor (Is_Empty : Boolean := True) is record
case Is_Empty is
when True => null;
when False =>
Index : Index_Type;
Backend : Backend_Refs.Immutable_Reference;
end case;
end record;
function Is_Valid (Position : Cursor) return Boolean
is (Position.Is_Empty
or else (not Position.Backend.Is_Empty
and then Position.Index <= Position.Backend.Query.Data.Size));
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);
type Range_Iterator is new Map_Iterator_Interfaces.Reversible_Iterator
with record
Backend : Backend_Refs.Immutable_Reference;
First_Position : Cursor;
Last_Position : Cursor;
end record;
-- with Dynamic_Predicate => not Range_Iterator.Backend.Is_Empty
-- and then Has_Element (Range_Iterator.First_Position)
-- and then Has_Element (Range_Iterator.Last_Position)
-- and then not Range_Iterator.First_Position
-- > Range_Iterator.Last_Position;
overriding function First (Object : Range_Iterator) return Cursor;
overriding function Last (Object : Range_Iterator) return Cursor;
overriding function Next
(Object : Range_Iterator;
Position : Cursor) return Cursor
with Pre => Position.Is_Empty
or else Backend_Refs."=" (Position.Backend, Object.Backend);
overriding function Previous
(Object : Range_Iterator;
Position : Cursor) return Cursor
with Pre => Position.Is_Empty
or else Backend_Refs."=" (Position.Backend, Object.Backend);
Empty_Constant_Map : constant Constant_Map := (Backend => <>);
Empty_Updatable_Map : constant Updatable_Map := (Backend => <>);
No_Element : constant Cursor := (Is_Empty => True);
end Natools.Constant_Indefinite_Ordered_Maps;