generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
- (HT : in out Map;
+ (HT : in out HT_Types.Hash_Table_Type;
Node : out Count_Type);
function Hash_Node (Node : Node_Type) return Hash_Type;
-- Start of processing for Assign
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- correct exception ???
"Source length exceeds Target capacity";
-- Generic_Allocate --
----------------------
- procedure Generic_Allocate (HT : in out Map; Node : out Count_Type) is
+ procedure Generic_Allocate
+ (HT : in out HT_Types.Hash_Table_Type;
+ Node : out Count_Type)
+ is
procedure Allocate is
new HT_Ops.Generic_Allocate (Set_Element);
begin
- Allocate (HT.Content, Node);
- HT.Content.Nodes (Node).Has_Element := True;
+ Allocate (HT, Node);
+ HT.Nodes (Node).Has_Element := True;
end Generic_Allocate;
-----------------
if not Inserted then
declare
- N : Node_Type renames Container.Content.Nodes (Position.Node);
+ P : constant Count_Type := Position.Node;
+ N : Node_Type renames Container.Content.Nodes (P);
begin
N.Key := Key;
N.Element := New_Item;
procedure Assign_Key (Node : in out Node_Type);
pragma Inline (Assign_Key);
- function New_Node return Count_Type;
+ procedure New_Node
+ (HT : in out HT_Types.Hash_Table_Type;
+ Node : out Count_Type);
pragma Inline (New_Node);
procedure Local_Insert is
-- New_Node --
--------------
- function New_Node return Count_Type is
- Result : Count_Type;
+ procedure New_Node
+ (HT : in out HT_Types.Hash_Table_Type;
+ Node : out Count_Type)
+ is
begin
- Allocate (Container, Result);
- return Result;
+ Allocate (HT, Node);
end New_Node;
-- Start of processing for Insert
Key : Key_Type;
New_Item : Element_Type)
is
- Position : Cursor;
- Inserted : Boolean;
+ Unused_Position : Cursor;
+ Inserted : Boolean;
begin
- Insert (Container, Key, New_Item, Position, Inserted);
+ Insert (Container, Key, New_Item, Unused_Position, Inserted);
if not Inserted then
raise Constraint_Error with "attempt to insert key already in map";
Y : Count_Type;
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- ???
"Source length exceeds Target capacity";
generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
- (HT : in out Set;
+ (HT : in out Hash_Table_Type;
Node : out Count_Type);
function Hash_Node (Node : Node_Type) return Hash_Type;
--------------------
procedure Insert_Element (Source_Node : Count_Type) is
- N : Node_Type renames Source.Content.Nodes (Source_Node);
- X : Count_Type;
- B : Boolean;
+ N : Node_Type renames Source.Content.Nodes (Source_Node);
+ Unused_X : Count_Type;
+ B : Boolean;
begin
- Insert (Target, N.Element, X, B);
+ Insert (Target, N.Element, Unused_X, B);
pragma Assert (B);
end Insert_Element;
-- Start of processing for Assign
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Storage_Error with "not enough capacity"; -- SE or CE? ???
end if;
SN : Nodes_Type renames Source.Content.Nodes;
begin
- if Target'Address = Source'Address then
- Clear (Target);
- return;
- end if;
-
Src_Length := Source.Content.Length;
if Src_Length = 0 then
-------------
procedure Process (L_Node : Count_Type) is
- B : Boolean;
- E : Element_Type renames Left.Content.Nodes (L_Node).Element;
- X : Count_Type;
+ B : Boolean;
+ E : Element_Type renames Left.Content.Nodes (L_Node).Element;
+ Unused_X : Count_Type;
begin
if Find (Right, E).Node = 0 then
- Insert (Target, E, X, B);
+ Insert (Target, E, Unused_X, B);
pragma Assert (B);
end if;
end Process;
end Difference;
function Difference (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
-
begin
- if Left'Address = Right'Address then
- return Empty_Set;
- end if;
-
if Length (Left) = 0 then
return Empty_Set;
end if;
return Copy (Left);
end if;
- C := Length (Left);
- H := Default_Modulus (C);
-
- return S : Set (C, H) do
- Difference (Left, Right, Target => S);
- end return;
+ declare
+ C : constant Count_Type := Length (Left);
+ H : constant Hash_Type := Default_Modulus (C);
+ begin
+ return S : Set (C, H) do
+ Difference (Left, Right, Target => S);
+ end return;
+ end;
end Difference;
-------------
function Equivalent_Sets (Left, Right : Set) return Boolean is
function Find_Equivalent_Key
- (R_HT : Hash_Table_Type'Class;
+ (R_HT : Hash_Table_Type;
L_Node : Node_Type) return Boolean;
pragma Inline (Find_Equivalent_Key);
-------------------------
function Find_Equivalent_Key
- (R_HT : Hash_Table_Type'Class;
+ (R_HT : Hash_Table_Type;
L_Node : Node_Type) return Boolean
is
R_Index : constant Hash_Type :=
-- Generic_Allocate --
----------------------
- procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
+ procedure Generic_Allocate
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type)
+ is
procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
begin
- Allocate (HT.Content, Node);
- HT.Content.Nodes (Node).Has_Element := True;
+ Allocate (HT, Node);
+ HT.Nodes (Node).Has_Element := True;
end Generic_Allocate;
package body Generic_Keys with SPARK_Mode => Off is
end Insert;
procedure Insert (Container : in out Set; New_Item : Element_Type) is
- Inserted : Boolean;
- Position : Cursor;
+ Inserted : Boolean;
+ Unused_Position : Cursor;
begin
- Insert (Container, New_Item, Position, Inserted);
+ Insert (Container, New_Item, Unused_Position, Inserted);
if not Inserted then
raise Constraint_Error with
procedure Allocate_Set_Element (Node : in out Node_Type);
pragma Inline (Allocate_Set_Element);
- function New_Node return Count_Type;
+ procedure New_Node
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type);
pragma Inline (New_Node);
procedure Local_Insert is
-- New_Node --
--------------
- function New_Node return Count_Type is
- Result : Count_Type;
+ procedure New_Node
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type)
+ is
begin
- Allocate (Container, Result);
- return Result;
+ Allocate (HT, Node);
end New_Node;
-- Start of processing for Insert
TN : Nodes_Type renames Target.Content.Nodes;
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Source.Content.Length = 0 then
Clear (Target);
return;
-------------
procedure Process (L_Node : Count_Type) is
- E : Element_Type renames Left.Content.Nodes (L_Node).Element;
- X : Count_Type;
- B : Boolean;
+ E : Element_Type renames Left.Content.Nodes (L_Node).Element;
+ Unused_X : Count_Type;
+ B : Boolean;
begin
if Find (Right, E).Node /= 0 then
- Insert (Target, E, X, B);
+ Insert (Target, E, Unused_X, B);
pragma Assert (B);
end if;
end Process;
end Intersection;
function Intersection (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
+ C : constant Count_Type :=
+ Count_Type'Min (Length (Left), Length (Right)); -- ???
+ H : constant Hash_Type := Default_Modulus (C);
begin
- if Left'Address = Right'Address then
- return Copy (Left);
- end if;
-
- C := Count_Type'Min (Length (Left), Length (Right)); -- ???
- H := Default_Modulus (C);
-
return S : Set (C, H) do
if Length (Left) /= 0 and Length (Right) /= 0 then
Intersection (Left, Right, Target => S);
Subset_Nodes : Nodes_Type renames Subset.Content.Nodes;
begin
- if Subset'Address = Of_Set'Address then
- return True;
- end if;
-
if Length (Subset) > Length (Of_Set) then
return False;
end if;
Subset_Node := First (Subset).Node;
while Subset_Node /= 0 loop
declare
- N : Node_Type renames Subset_Nodes (Subset_Node);
+ S : constant Count_Type := Subset_Node;
+ N : Node_Type renames Subset_Nodes (S);
E : Element_Type renames N.Element;
begin
X, Y : Count_Type;
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- ???
"Source length exceeds Target capacity";
return False;
end if;
- if Left'Address = Right'Address then
- return True;
- end if;
-
Left_Node := First (Left).Node;
while Left_Node /= 0 loop
declare
- N : Node_Type renames Left_Nodes (Left_Node);
+ L : constant Count_Type := Left_Node;
+ N : Node_Type renames Left_Nodes (L);
E : Element_Type renames N.Element;
begin
if Find (Right, E).Node /= 0 then
-------------
procedure Process (Source_Node : Count_Type) is
- B : Boolean;
- N : Node_Type renames Source.Content.Nodes (Source_Node);
- X : Count_Type;
+ B : Boolean;
+ N : Node_Type renames Source.Content.Nodes (Source_Node);
+ Unused_X : Count_Type;
begin
if Is_In (Target, N) then
Delete (Target, N.Element);
else
- Insert (Target, N.Element, X, B);
+ Insert (Target, N.Element, Unused_X, B);
pragma Assert (B);
end if;
end Process;
-- Start of processing for Symmetric_Difference
begin
- if Target'Address = Source'Address then
- Clear (Target);
- return;
- end if;
-
if Length (Target) = 0 then
Assign (Target, Source);
return;
end Symmetric_Difference;
function Symmetric_Difference (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
-
begin
- if Left'Address = Right'Address then
- return Empty_Set;
- end if;
-
if Length (Right) = 0 then
return Copy (Left);
end if;
return Copy (Right);
end if;
- C := Length (Left) + Length (Right);
- H := Default_Modulus (C);
-
- return S : Set (C, H) do
- Difference (Left, Right, S);
- Difference (Right, Left, S);
- end return;
+ declare
+ C : constant Count_Type := Length (Left) + Length (Right);
+ H : constant Hash_Type := Default_Modulus (C);
+ begin
+ return S : Set (C, H) do
+ Difference (Left, Right, S);
+ Difference (Right, Left, S);
+ end return;
+ end;
end Symmetric_Difference;
------------
------------
function To_Set (New_Item : Element_Type) return Set is
- X : Count_Type;
- B : Boolean;
+ Unused_X : Count_Type;
+ B : Boolean;
begin
return S : Set (Capacity => 1, Modulus => 1) do
- Insert (S, New_Item, X, B);
+ Insert (S, New_Item, Unused_X, B);
pragma Assert (B);
end return;
end To_Set;
N : Node_Type renames Source.Content.Nodes (Src_Node);
E : Element_Type renames N.Element;
- X : Count_Type;
- B : Boolean;
+ Unused_X : Count_Type;
+ Unused_B : Boolean;
begin
- Insert (Target, E, X, B);
+ Insert (Target, E, Unused_X, Unused_B);
end Process;
-- Start of processing for Union
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
Iterate (Source.Content);
end Union;
function Union (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
-
begin
- if Left'Address = Right'Address then
- return Copy (Left);
- end if;
-
if Length (Right) = 0 then
return Copy (Left);
end if;
return Copy (Right);
end if;
- C := Length (Left) + Length (Right);
- H := Default_Modulus (C);
- return S : Set (C, H) do
- Assign (Target => S, Source => Left);
- Union (Target => S, Source => Right);
- end return;
+ declare
+ C : constant Count_Type := Length (Left) + Length (Right);
+ H : constant Hash_Type := Default_Modulus (C);
+ begin
+ return S : Set (C, H) do
+ Assign (Target => S, Source => Left);
+ Union (Target => S, Source => Right);
+ end return;
+ end;
end Union;
---------
-----------------------------
function Checked_Equivalent_Keys
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type;
Node : Count_Type) return Boolean
is
-------------------
function Checked_Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type
is
begin
--------------------------
procedure Delete_Key_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
X : out Count_Type)
is
----------
function Find
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Count_Type
is
Indx : Hash_Type;
return 0;
end if;
- Indx := Checked_Index (HT'Unrestricted_Access.all, Key);
+ Indx := Checked_Index (HT, Key);
Node := HT.Buckets (Indx);
while Node /= 0 loop
- if Checked_Equivalent_Keys
- (HT'Unrestricted_Access.all, Key, Node)
- then
+ if Checked_Equivalent_Keys (HT, Key, Node) then
return Node;
end if;
Node := Next (HT.Nodes (Node));
--------------------------------
procedure Generic_Conditional_Insert
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
Node : out Count_Type;
Inserted : out Boolean)
raise Capacity_Error with "no more capacity for insertion";
end if;
- Node := New_Node;
+ New_Node (HT, Node);
Set_Next (HT.Nodes (Node), Next => 0);
Inserted := True;
raise Capacity_Error with "no more capacity for insertion";
end if;
- Node := New_Node;
+ New_Node (HT, Node);
Set_Next (HT.Nodes (Node), Next => HT.Buckets (Indx));
Inserted := True;
-----------------------------
procedure Generic_Replace_Element
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : Count_Type;
Key : Key_Type)
is
-----------
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type is
begin
return HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
pragma Pure;
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type;
pragma Inline (Index);
-- Returns the bucket number (array index value) for the given key
function Checked_Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type;
pragma Inline (Checked_Index);
-- Calls Index, but also locks and unlocks the container, per AI05-0022, in
-- order to detect element tampering by the generic actual Hash function.
function Checked_Equivalent_Keys
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type;
Node : Count_Type) return Boolean;
-- Calls Equivalent_Keys, but locks and unlocks the container, per
-- AI05-0022, in order to detect element tampering by that generic actual.
procedure Delete_Key_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
X : out Count_Type);
-- Removes the node (if any) with the given key from the hash table,
-- table is busy.
function Find
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Count_Type;
-- Returns the node (if any) corresponding to the given key
generic
- with function New_Node return Count_Type;
+ with procedure New_Node
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type);
procedure Generic_Conditional_Insert
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
Node : out Count_Type;
Inserted : out Boolean);
with function Hash (Node : Node_Type) return Hash_Type;
with procedure Assign (Node : in out Node_Type; Key : Key_Type);
procedure Generic_Replace_Element
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : Count_Type;
Key : Key_Type);
-- Assigns Key to Node, possibly changing its equivalence class. If Node
-------------------
function Checked_Index
- (Hash_Table : Hash_Table_Type'Class;
+ (Hash_Table : Hash_Table_Type;
Node : Count_Type) return Hash_Type
is
begin
-- Clear --
-----------
- procedure Clear (HT : in out Hash_Table_Type'Class) is
+ procedure Clear (HT : in out Hash_Table_Type) is
begin
HT.Length := 0;
-- HT.Busy := 0;
--------------------------
procedure Delete_Node_At_Index
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Indx : Hash_Type;
X : Count_Type)
is
---------------------------
procedure Delete_Node_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type)
is
pragma Assert (X /= 0);
-- First --
-----------
- function First (HT : Hash_Table_Type'Class) return Count_Type is
+ function First (HT : Hash_Table_Type) return Count_Type is
Indx : Hash_Type;
begin
----------
procedure Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type)
is
N : Nodes_Type renames HT.Nodes;
----------------------
procedure Generic_Allocate
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : out Count_Type)
is
N : Nodes_Type renames HT.Nodes;
-------------------
function Generic_Equal
- (L, R : Hash_Table_Type'Class) return Boolean
+ (L, R : Hash_Table_Type) return Boolean
is
L_Index : Hash_Type;
L_Node : Count_Type;
N : Count_Type;
begin
- if L'Address = R'Address then
- return True;
- end if;
-
if L.Length /= R.Length then
return False;
end if;
-- Generic_Iteration --
-----------------------
- procedure Generic_Iteration (HT : Hash_Table_Type'Class) is
+ procedure Generic_Iteration (HT : Hash_Table_Type) is
Node : Count_Type;
begin
procedure Generic_Read
(Stream : not null access Root_Stream_Type'Class;
- HT : out Hash_Table_Type'Class)
+ HT : out Hash_Table_Type)
is
N : Count_Type'Base;
procedure Generic_Write
(Stream : not null access Root_Stream_Type'Class;
- HT : Hash_Table_Type'Class)
+ HT : Hash_Table_Type)
is
procedure Write (Node : Count_Type);
pragma Inline (Write);
end Index;
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Node_Type) return Hash_Type is
begin
return Index (HT.Buckets, Node);
----------
function Next
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Count_Type) return Count_Type
is
Result : Count_Type;
-- This was the last node in the bucket, so move to the next
-- bucket, and start searching for next node from there.
- First := Checked_Index (HT'Unrestricted_Access.all, Node) + 1;
+ First := Checked_Index (HT, Node) + 1;
for Indx in First .. HT.Buckets'Last loop
Result := HT.Buckets (Indx);
-- Uses the hash value of Node to compute its Buckets array index
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Node_Type) return Hash_Type;
pragma Inline (Index);
-- Uses the hash value of Node to compute its Hash_Table buckets array
-- index.
function Checked_Index
- (Hash_Table : Hash_Table_Type'Class;
+ (Hash_Table : Hash_Table_Type;
Node : Count_Type) return Hash_Type;
-- Calls Index, but also locks and unlocks the container, per AI05-0022, in
-- order to detect element tampering by the generic actual Hash function.
generic
with function Find
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Node_Type) return Boolean;
- function Generic_Equal (L, R : Hash_Table_Type'Class) return Boolean;
+ function Generic_Equal (L, R : Hash_Table_Type) return Boolean;
-- Used to implement hashed container equality. For each node in hash table
-- L, it calls Find to search for an equivalent item in hash table R. If
-- Find returns False for any node then Generic_Equal terminates
-- immediately and returns False. Otherwise if Find returns True for every
-- node then Generic_Equal returns True.
- procedure Clear (HT : in out Hash_Table_Type'Class);
+ procedure Clear (HT : in out Hash_Table_Type);
-- Deallocates each node in hash table HT. (Note that it only deallocates
-- the nodes, not the buckets array.) Program_Error is raised if the hash
-- table is busy.
procedure Delete_Node_At_Index
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Indx : Hash_Type;
X : Count_Type);
-- Delete a node whose bucket position is known. extracted from following
-- not correspond to the hash code that determines its bucket.
procedure Delete_Node_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type);
-- Removes node X from the hash table without deallocating the node
generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : out Count_Type);
-- Claim a node from the free store. Generic_Allocate first
-- calls Set_Element on the potential node, and then returns
-- the node's index as the value of the Node parameter.
procedure Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type);
-- Return a node back to the free store, from where it had
-- been previously claimed via Generic_Allocate.
- function First (HT : Hash_Table_Type'Class) return Count_Type;
+ function First (HT : Hash_Table_Type) return Count_Type;
-- Returns the head of the list in the first (lowest-index) non-empty
-- bucket.
function Next
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Count_Type) return Count_Type;
-- Returns the node that immediately follows Node. This corresponds to
-- either the next node in the same bucket, or (if Node is the last node in
generic
with procedure Process (Node : Count_Type);
- procedure Generic_Iteration (HT : Hash_Table_Type'Class);
+ procedure Generic_Iteration (HT : Hash_Table_Type);
-- Calls Process for each node in hash table HT
generic
Node : Node_Type);
procedure Generic_Write
(Stream : not null access Root_Stream_Type'Class;
- HT : Hash_Table_Type'Class);
+ HT : Hash_Table_Type);
-- Used to implement the streaming attribute for hashed containers. It
-- calls Write for each node to write its value into Stream.
return Count_Type;
procedure Generic_Read
(Stream : not null access Root_Stream_Type'Class;
- HT : out Hash_Table_Type'Class);
+ HT : out Hash_Table_Type);
-- Used to implement the streaming attribute for hashed containers. It
-- first clears hash table HT, then populates the hash table by calling
-- New_Node for each item in Stream.
type Hash_Table_Type
(Capacity : Count_Type;
Modulus : Hash_Type) is
- tagged record
+ record
Length : Count_Type := 0;
Free : Count_Type'Base := -1;
Nodes : Nodes_Type (1 .. Capacity);