Free (Container, X);
end Clear;
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased List;
+ Position : Cursor) return not null access constant Element_Type
+ is
+ begin
+ if not Has_Element (Container => Container, Position => Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ return Container.Nodes (Position.Node).Element'Access;
+ end Constant_Reference;
+
--------------
-- Contains --
--------------
return (Node => Container.Nodes (Position.Node).Prev);
end Previous;
+ ---------------
+ -- Reference --
+ ---------------
+
+ function Reference
+ (Container : not null access List;
+ Position : Cursor) return not null access Element_Type
+ is
+ begin
+ if not Has_Element (Container.all, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ return Container.Nodes (Position.Node).Element'Access;
+ end Reference;
+
---------------------
-- Replace_Element --
---------------------
Model (Container),
P.Get (Positions (Container), Position));
+ function At_End (E : access constant List) return access constant List
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function At_End
+ (E : access constant Element_Type) return access constant Element_Type
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function Constant_Reference
+ (Container : aliased List;
+ Position : Cursor) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Constant_Reference'Result.all =
+ Element (Model (Container), P.Get (Positions (Container), Position));
+
+ function Reference
+ (Container : not null access List;
+ Position : Cursor) return not null access Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container.all, Position),
+ Post =>
+ Length (Container.all) = Length (At_End (Container).all)
+
+ -- Cursors are preserved
+
+ and Positions (Container.all) = Positions (At_End (Container).all)
+
+ -- Container will have Result.all at position Position
+
+ and At_End (Reference'Result).all =
+ Element (Model (At_End (Container).all),
+ P.Get (Positions (At_End (Container).all), Position))
+
+ -- All other elements are preserved
+
+ and M.Equal_Except
+ (Model (Container.all),
+ Model (At_End (Container).all),
+ P.Get (Positions (At_End (Container).all), Position));
+
procedure Move (Target : in out List; Source : in out List) with
Global => null,
Pre => Target.Capacity >= Length (Source),
type Node_Type is record
Prev : Count_Type'Base := -1;
Next : Count_Type;
- Element : Element_Type;
+ Element : aliased Element_Type;
end record;
function "=" (L, R : Node_Type) return Boolean is abstract;
ENode : Count_Type;
begin
- Node := Left.First.Node;
+ Node := First (Left).Node;
while Node /= 0 loop
ENode :=
Find
(Container => Right,
- Key => Left.Nodes (Node).Key).Node;
+ Key => Left.Content.Nodes (Node).Key).Node;
if ENode = 0 or else
- Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
+ Right.Content.Nodes (ENode).Element /=
+ Left.Content.Nodes (Node).Element
then
return False;
end if;
- Node := HT_Ops.Next (Left, Node);
+ Node := HT_Ops.Next (Left.Content, Node);
end loop;
return True;
--------------------
procedure Insert_Element (Source_Node : Count_Type) is
- N : Node_Type renames Source.Nodes (Source_Node);
+ N : Node_Type renames Source.Content.Nodes (Source_Node);
begin
Insert (Target, N.Key, N.Element);
end Insert_Element;
Clear (Target);
- Insert_Elements (Source);
+ Insert_Elements (Source.Content);
end Assign;
--------------
function Capacity (Container : Map) return Count_Type is
begin
- return Container.Nodes'Length;
+ return Container.Content.Nodes'Length;
end Capacity;
-----------
procedure Clear (Container : in out Map) is
begin
- HT_Ops.Clear (Container);
+ HT_Ops.Clear (Container.Content);
end Clear;
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Position : Cursor) return not null access constant Element_Type
+ is
+ begin
+ if not Has_Element (Container, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert
+ (Vet (Container, Position),
+ "bad cursor in function Constant_Reference");
+
+ return Container.Content.Nodes (Position.Node).Element'Access;
+ end Constant_Reference;
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Key : Key_Type) return not null access constant Element_Type
+ is
+ Node : constant Count_Type := Find (Container, Key).Node;
+
+ begin
+ if Node = 0 then
+ raise Constraint_Error with
+ "no element available because key not in map";
+ end if;
+
+ return Container.Content.Nodes (Node).Element'Access;
+ end Constant_Reference;
+
--------------
-- Contains --
--------------
raise Capacity_Error;
end if;
- Target.Length := Source.Length;
- Target.Free := Source.Free;
+ Target.Content.Length := Source.Content.Length;
+ Target.Content.Free := Source.Content.Free;
H := 1;
while H <= Source.Modulus loop
- Target.Buckets (H) := Source.Buckets (H);
+ Target.Content.Buckets (H) := Source.Content.Buckets (H);
H := H + 1;
end loop;
N := 1;
while N <= Source.Capacity loop
- Target.Nodes (N) := Source.Nodes (N);
+ Target.Content.Nodes (N) := Source.Content.Nodes (N);
N := N + 1;
end loop;
X : Count_Type;
begin
- Key_Ops.Delete_Key_Sans_Free (Container, Key, X);
+ Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X);
if X = 0 then
raise Constraint_Error with "attempt to delete key not in map";
pragma Assert (Vet (Container, Position), "bad cursor in Delete");
- HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
+ HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node);
Free (Container, Position.Node);
Position := No_Element;
"no element available because key not in map";
end if;
- return Container.Nodes (Node).Element;
+ return Container.Content.Nodes (Node).Element;
end Element;
function Element (Container : Map; Position : Cursor) return Element_Type is
pragma Assert
(Vet (Container, Position), "bad cursor in function Element");
- return Container.Nodes (Position.Node).Element;
+ return Container.Content.Nodes (Position.Node).Element;
end Element;
---------------------
procedure Exclude (Container : in out Map; Key : Key_Type) is
X : Count_Type;
begin
- Key_Ops.Delete_Key_Sans_Free (Container, Key, X);
+ Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X);
Free (Container, X);
end Exclude;
----------
function Find (Container : Map; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Ops.Find (Container, Key);
+ Node : constant Count_Type := Key_Ops.Find (Container.Content, Key);
begin
if Node = 0 then
-----------
function First (Container : Map) return Cursor is
- Node : constant Count_Type := HT_Ops.First (Container);
+ Node : constant Count_Type := HT_Ops.First (Container.Content);
begin
if Node = 0 then
----------
function Keys (Container : Map) return K.Sequence is
- Position : Count_Type := HT_Ops.First (Container);
+ Position : Count_Type := HT_Ops.First (Container.Content);
R : K.Sequence;
begin
-- for their postconditions.
while Position /= 0 loop
- R := K.Add (R, Container.Nodes (Position).Key);
- Position := HT_Ops.Next (Container, Position);
+ R := K.Add (R, Container.Content.Nodes (Position).Key);
+ Position := HT_Ops.Next (Container.Content, Position);
end loop;
return R;
-----------
function Model (Container : Map) return M.Map is
- Position : Count_Type := HT_Ops.First (Container);
+ Position : Count_Type := HT_Ops.First (Container.Content);
R : M.Map;
begin
R :=
M.Add
(Container => R,
- New_Key => Container.Nodes (Position).Key,
- New_Item => Container.Nodes (Position).Element);
+ New_Key => Container.Content.Nodes (Position).Key,
+ New_Item => Container.Content.Nodes (Position).Element);
- Position := HT_Ops.Next (Container, Position);
+ Position := HT_Ops.Next (Container.Content, Position);
end loop;
return R;
function Positions (Container : Map) return P.Map is
I : Count_Type := 1;
- Position : Count_Type := HT_Ops.First (Container);
+ Position : Count_Type := HT_Ops.First (Container.Content);
R : P.Map;
begin
while Position /= 0 loop
R := P.Add (R, (Node => Position), I);
pragma Assert (P.Length (R) = I);
- Position := HT_Ops.Next (Container, Position);
+ Position := HT_Ops.Next (Container.Content, Position);
I := I + 1;
end loop;
begin
if X /= 0 then
pragma Assert (X <= HT.Capacity);
- HT.Nodes (X).Has_Element := False;
- HT_Ops.Free (HT, X);
+ HT.Content.Nodes (X).Has_Element := False;
+ HT_Ops.Free (HT.Content, X);
end if;
end Free;
new HT_Ops.Generic_Allocate (Set_Element);
begin
- Allocate (HT, Node);
- HT.Nodes (Node).Has_Element := True;
+ Allocate (HT.Content, Node);
+ HT.Content.Nodes (Node).Has_Element := True;
end Generic_Allocate;
-----------------
function Has_Element (Container : Map; Position : Cursor) return Boolean is
begin
if Position.Node = 0
- or else not Container.Nodes (Position.Node).Has_Element
+ or else not Container.Content.Nodes (Position.Node).Has_Element
then
return False;
else
if not Inserted then
declare
- N : Node_Type renames Container.Nodes (Position.Node);
+ N : Node_Type renames Container.Content.Nodes (Position.Node);
begin
N.Key := Key;
N.Element := New_Item;
-- Start of processing for Insert
begin
- Local_Insert (Container, Key, Position.Node, Inserted);
+ Local_Insert (Container.Content, Key, Position.Node, Inserted);
end Insert;
procedure Insert
pragma Assert (Vet (Container, Position), "bad cursor in function Key");
- return Container.Nodes (Position.Node).Key;
+ return Container.Content.Nodes (Position.Node).Key;
end Key;
------------
function Length (Container : Map) return Count_Type is
begin
- return Container.Length;
+ return Container.Content.Length;
end Length;
----------
(Target : in out Map;
Source : in out Map)
is
- NN : HT_Types.Nodes_Type renames Source.Nodes;
+ NN : HT_Types.Nodes_Type renames Source.Content.Nodes;
X : Count_Type;
Y : Count_Type;
Clear (Target);
- if Source.Length = 0 then
+ if Source.Content.Length = 0 then
return;
end if;
- X := HT_Ops.First (Source);
+ X := HT_Ops.First (Source.Content);
while X /= 0 loop
Insert (Target, NN (X).Key, NN (X).Element); -- optimize???
- Y := HT_Ops.Next (Source, X);
+ Y := HT_Ops.Next (Source.Content, X);
- HT_Ops.Delete_Node_Sans_Free (Source, X);
+ HT_Ops.Delete_Node_Sans_Free (Source.Content, X);
Free (Source, X);
X := Y;
pragma Assert (Vet (Container, Position), "bad cursor in function Next");
declare
- Node : constant Count_Type := HT_Ops.Next (Container, Position.Node);
+ Node : constant Count_Type :=
+ HT_Ops.Next (Container.Content, Position.Node);
begin
if Node = 0 then
Position := Next (Container, Position);
end Next;
+ ---------------
+ -- Reference --
+ ---------------
+
+ function Reference
+ (Container : not null access Map;
+ Position : Cursor) return not null access Element_Type
+ is
+ begin
+ if not Has_Element (Container.all, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert
+ (Vet (Container.all, Position), "bad cursor in function Reference");
+
+ return Container.Content.Nodes (Position.Node).Element'Access;
+ end Reference;
+
+ function Reference
+ (Container : not null access Map;
+ Key : Key_Type) return not null access Element_Type
+ is
+ Node : constant Count_Type := Find (Container.all, Key).Node;
+
+ begin
+ if Node = 0 then
+ raise Constraint_Error with
+ "no element available because key not in map";
+ end if;
+
+ return Container.Content.Nodes (Node).Element'Access;
+ end Reference;
+
-------------
-- Replace --
-------------
Key : Key_Type;
New_Item : Element_Type)
is
- Node : constant Count_Type := Key_Ops.Find (Container, Key);
+ Node : constant Count_Type := Key_Ops.Find (Container.Content, Key);
begin
if Node = 0 then
end if;
declare
- N : Node_Type renames Container.Nodes (Node);
+ N : Node_Type renames Container.Content.Nodes (Node);
begin
N.Key := Key;
N.Element := New_Item;
pragma Assert
(Vet (Container, Position), "bad cursor in Replace_Element");
- Container.Nodes (Position.Node).Element := New_Item;
+ Container.Content.Nodes (Position.Node).Element := New_Item;
end Replace_Element;
----------------------
X : Count_Type;
begin
- if Container.Length = 0 then
+ if Container.Content.Length = 0 then
return False;
end if;
return False;
end if;
- if Container.Buckets'Length = 0 then
+ if Container.Content.Buckets'Length = 0 then
return False;
end if;
return False;
end if;
- if Container.Nodes (Position.Node).Next = Position.Node then
+ if Container.Content.Nodes (Position.Node).Next = Position.Node then
return False;
end if;
X :=
- Container.Buckets
- (Key_Ops.Index (Container, Container.Nodes (Position.Node).Key));
+ Container.Content.Buckets
+ (Key_Ops.Index
+ (Container.Content,
+ Container.Content.Nodes (Position.Node).Key));
- for J in 1 .. Container.Length loop
+ for J in 1 .. Container.Content.Length loop
if X = Position.Node then
return True;
end if;
return False;
end if;
- if X = Container.Nodes (X).Next then
+ if X = Container.Content.Nodes (X).Next then
-- Prevent unnecessary looping
return False;
end if;
- X := Container.Nodes (X).Next;
+ X := Container.Content.Nodes (X).Next;
end loop;
return False;
Model (Container)'Old,
Key (Container, Position));
+ function At_End
+ (E : not null access constant Map) return not null access constant Map
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function At_End
+ (E : access constant Element_Type) return access constant Element_Type
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Position : Cursor) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Constant_Reference'Result.all =
+ Element (Model (Container), Key (Container, Position));
+
+ function Reference
+ (Container : not null access Map;
+ Position : Cursor) return not null access Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container.all, Position),
+ Post =>
+
+ -- Order of keys and cursors is preserved
+
+ Keys (At_End (Container).all) = Keys (Container.all)
+ and Positions (At_End (Container).all) = Positions (Container.all)
+
+ -- The value designated by the result of Reference is now associated
+ -- with the key at position Position in Container.
+
+ and Element (At_End (Container).all, Position) =
+ At_End (Reference'Result).all
+
+ -- Elements associated with other keys are preserved
+
+ and M.Same_Keys
+ (Model (At_End (Container).all),
+ Model (Container.all))
+ and M.Elements_Equal_Except
+ (Model (At_End (Container).all),
+ Model (Container.all),
+ Key (At_End (Container).all, Position));
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Key : Key_Type) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Constant_Reference'Result.all = Element (Model (Container), Key);
+
+ function Reference
+ (Container : not null access Map;
+ Key : Key_Type) return not null access Element_Type
+ with
+ Global => null,
+ Pre => Contains (Container.all, Key),
+ Post =>
+
+ -- Order of keys and cursors is preserved
+
+ Keys (At_End (Container).all) = Keys (Container.all)
+ and Positions (At_End (Container).all) = Positions (Container.all)
+
+ -- The value designated by the result of Reference is now associated
+ -- with Key in Container.
+
+ and Element (Model (At_End (Container).all), Key) =
+ At_End (Reference'Result).all
+
+ -- Elements associated with other keys are preserved
+
+ and M.Same_Keys
+ (Model (At_End (Container).all),
+ Model (Container.all))
+ and M.Elements_Equal_Except
+ (Model (At_End (Container).all),
+ Model (Container.all),
+ Key);
+
procedure Move (Target : in out Map; Source : in out Map) with
Global => null,
Pre => Target.Capacity >= Length (Source),
type Node_Type is record
Key : Key_Type;
- Element : Element_Type;
+ Element : aliased Element_Type;
Next : Count_Type;
Has_Element : Boolean := False;
end record;
package HT_Types is new
Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
- type Map (Capacity : Count_Type; Modulus : Hash_Type) is
- new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+ type Map (Capacity : Count_Type; Modulus : Hash_Type) is record
+ Content : HT_Types.Hash_Table_Type (Capacity, Modulus);
+ end record;
Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
ENode :=
Find
(Container => Right,
- Item => Left.Nodes (Node).Element).Node;
+ Item => Left.Content.Nodes (Node).Element).Node;
if ENode = 0
- or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
+ or else Right.Content.Nodes (ENode).Element /=
+ Left.Content.Nodes (Node).Element
then
return False;
end if;
- Node := HT_Ops.Next (Left, Node);
+ Node := HT_Ops.Next (Left.Content, Node);
end loop;
return True;
--------------------
procedure Insert_Element (Source_Node : Count_Type) is
- N : Node_Type renames Source.Nodes (Source_Node);
+ N : Node_Type renames Source.Content.Nodes (Source_Node);
X : Count_Type;
B : Boolean;
raise Storage_Error with "not enough capacity"; -- SE or CE? ???
end if;
- HT_Ops.Clear (Target);
- Insert_Elements (Source);
+ HT_Ops.Clear (Target.Content);
+ Insert_Elements (Source.Content);
end Assign;
--------------
function Capacity (Container : Set) return Count_Type is
begin
- return Container.Nodes'Length;
+ return Container.Content.Nodes'Length;
end Capacity;
-----------
procedure Clear (Container : in out Set) is
begin
- HT_Ops.Clear (Container);
+ HT_Ops.Clear (Container.Content);
end Clear;
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased Set;
+ Position : Cursor) return not null access constant Element_Type
+ is
+ begin
+ if not Has_Element (Container, Position) then
+ raise Constraint_Error with "Position cursor equals No_Element";
+ end if;
+
+ pragma Assert
+ (Vet (Container, Position), "bad cursor in function Element");
+
+ return Container.Content.Nodes (Position.Node).Element'Access;
+ end Constant_Reference;
+
--------------
-- Contains --
--------------
raise Capacity_Error;
end if;
- Target.Length := Source.Length;
- Target.Free := Source.Free;
+ Target.Content.Length := Source.Content.Length;
+ Target.Content.Free := Source.Content.Free;
H := 1;
while H <= Source.Modulus loop
- Target.Buckets (H) := Source.Buckets (H);
+ Target.Content.Buckets (H) := Source.Content.Buckets (H);
H := H + 1;
end loop;
N := 1;
while N <= Source.Capacity loop
- Target.Nodes (N) := Source.Nodes (N);
+ Target.Content.Nodes (N) := Source.Content.Nodes (N);
N := N + 1;
end loop;
X : Count_Type;
begin
- Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
+ Element_Keys.Delete_Key_Sans_Free (Container.Content, Item, X);
if X = 0 then
raise Constraint_Error with "attempt to delete element not in set";
pragma Assert (Vet (Container, Position), "bad cursor in Delete");
- HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
+ HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node);
Free (Container, Position.Node);
Position := No_Element;
Src_Node : Count_Type;
Tgt_Node : Count_Type;
- TN : Nodes_Type renames Target.Nodes;
- SN : Nodes_Type renames Source.Nodes;
+ TN : Nodes_Type renames Target.Content.Nodes;
+ SN : Nodes_Type renames Source.Content.Nodes;
begin
if Target'Address = Source'Address then
return;
end if;
- Src_Length := Source.Length;
+ Src_Length := Source.Content.Length;
if Src_Length = 0 then
return;
end if;
- if Src_Length >= Target.Length then
- Tgt_Node := HT_Ops.First (Target);
+ if Src_Length >= Target.Content.Length then
+ Tgt_Node := HT_Ops.First (Target.Content);
while Tgt_Node /= 0 loop
- if Element_Keys.Find (Source, TN (Tgt_Node).Element) /= 0 then
+ if Element_Keys.Find (Source.Content, TN (Tgt_Node).Element) /= 0
+ then
declare
X : constant Count_Type := Tgt_Node;
begin
- Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
- HT_Ops.Delete_Node_Sans_Free (Target, X);
+ Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
+ HT_Ops.Delete_Node_Sans_Free (Target.Content, X);
Free (Target, X);
end;
else
- Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
+ Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
end if;
end loop;
return;
else
- Src_Node := HT_Ops.First (Source);
+ Src_Node := HT_Ops.First (Source.Content);
Src_Last := 0;
end if;
while Src_Node /= Src_Last loop
- Tgt_Node := Element_Keys.Find (Target, SN (Src_Node).Element);
+ Tgt_Node := Element_Keys.Find (Target.Content, SN (Src_Node).Element);
if Tgt_Node /= 0 then
- HT_Ops.Delete_Node_Sans_Free (Target, Tgt_Node);
+ HT_Ops.Delete_Node_Sans_Free (Target.Content, Tgt_Node);
Free (Target, Tgt_Node);
end if;
- Src_Node := HT_Ops.Next (Source, Src_Node);
+ Src_Node := HT_Ops.Next (Source.Content, Src_Node);
end loop;
end Difference;
procedure Process (L_Node : Count_Type) is
B : Boolean;
- E : Element_Type renames Left.Nodes (L_Node).Element;
+ E : Element_Type renames Left.Content.Nodes (L_Node).Element;
X : Count_Type;
begin
-- Start of processing for Difference
begin
- Iterate (Left);
+ Iterate (Left.Content);
end Difference;
function Difference (Left : Set; Right : Set) return Set is
end if;
if Length (Right) = 0 then
- return Left.Copy;
+ return Copy (Left);
end if;
C := Length (Left);
pragma Assert
(Vet (Container, Position), "bad cursor in function Element");
- return Container.Nodes (Position.Node).Element;
+ return Container.Content.Nodes (Position.Node).Element;
end Element;
---------------------
-- Start of processing for Equivalent_Sets
begin
- return Is_Equivalent (Left, Right);
+ return Is_Equivalent (Left.Content, Right.Content);
end Equivalent_Sets;
---------------------
procedure Exclude (Container : in out Set; Item : Element_Type) is
X : Count_Type;
begin
- Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
+ Element_Keys.Delete_Key_Sans_Free (Container.Content, Item, X);
Free (Container, X);
end Exclude;
(Container : Set;
Item : Element_Type) return Cursor
is
- Node : constant Count_Type := Element_Keys.Find (Container, Item);
+ Node : constant Count_Type :=
+ Element_Keys.Find (Container.Content, Item);
begin
if Node = 0 then
-----------
function First (Container : Set) return Cursor is
- Node : constant Count_Type := HT_Ops.First (Container);
+ Node : constant Count_Type := HT_Ops.First (Container.Content);
begin
if Node = 0 then
--------------
function Elements (Container : Set) return E.Sequence is
- Position : Count_Type := HT_Ops.First (Container);
+ Position : Count_Type := HT_Ops.First (Container.Content);
R : E.Sequence;
begin
-- for their postconditions.
while Position /= 0 loop
- R := E.Add (R, Container.Nodes (Position).Element);
- Position := HT_Ops.Next (Container, Position);
+ R := E.Add (R, Container.Content.Nodes (Position).Element);
+ Position := HT_Ops.Next (Container.Content, Position);
end loop;
return R;
-----------
function Model (Container : Set) return M.Set is
- Position : Count_Type := HT_Ops.First (Container);
+ Position : Count_Type := HT_Ops.First (Container.Content);
R : M.Set;
begin
R :=
M.Add
(Container => R,
- Item => Container.Nodes (Position).Element);
+ Item => Container.Content.Nodes (Position).Element);
- Position := HT_Ops.Next (Container, Position);
+ Position := HT_Ops.Next (Container.Content, Position);
end loop;
return R;
function Positions (Container : Set) return P.Map is
I : Count_Type := 1;
- Position : Count_Type := HT_Ops.First (Container);
+ Position : Count_Type := HT_Ops.First (Container.Content);
R : P.Map;
begin
while Position /= 0 loop
R := P.Add (R, (Node => Position), I);
pragma Assert (P.Length (R) = I);
- Position := HT_Ops.Next (Container, Position);
+ Position := HT_Ops.Next (Container.Content, Position);
I := I + 1;
end loop;
begin
if X /= 0 then
pragma Assert (X <= HT.Capacity);
- HT.Nodes (X).Has_Element := False;
- HT_Ops.Free (HT, X);
+ HT.Content.Nodes (X).Has_Element := False;
+ HT_Ops.Free (HT.Content, X);
end if;
end Free;
procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
begin
- Allocate (HT, Node);
- HT.Nodes (Node).Has_Element := True;
+ Allocate (HT.Content, Node);
+ HT.Content.Nodes (Node).Has_Element := True;
end Generic_Allocate;
package body Generic_Keys with SPARK_Mode => Off is
X : Count_Type;
begin
- Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
+ Key_Keys.Delete_Key_Sans_Free (Container.Content, Key, X);
if X = 0 then
raise Constraint_Error with "attempt to delete key not in set";
raise Constraint_Error with "key not in map";
end if;
- return Container.Nodes (Node).Element;
+ return Container.Content.Nodes (Node).Element;
end Element;
-------------------------
procedure Exclude (Container : in out Set; Key : Key_Type) is
X : Count_Type;
begin
- Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
+ Key_Keys.Delete_Key_Sans_Free (Container.Content, Key, X);
Free (Container, X);
end Exclude;
(Container : Set;
Key : Key_Type) return Cursor
is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type := Key_Keys.Find (Container.Content, Key);
begin
return (if Node = 0 then No_Element else (Node => Node));
end Find;
(Vet (Container, Position), "bad cursor in function Key");
declare
- N : Node_Type renames Container.Nodes (Position.Node);
+ N : Node_Type renames Container.Content.Nodes (Position.Node);
begin
return Key (N.Element);
end;
Key : Key_Type;
New_Item : Element_Type)
is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type := Key_Keys.Find (Container.Content, Key);
begin
if Node = 0 then
raise Constraint_Error with "attempt to replace key not in set";
end if;
- Replace_Element (Container, Node, New_Item);
+ Replace_Element (Container.Content, Node, New_Item);
end Replace;
end Generic_Keys;
function Has_Element (Container : Set; Position : Cursor) return Boolean is
begin
if Position.Node = 0
- or else not Container.Nodes (Position.Node).Has_Element
+ or else not Container.Content.Nodes (Position.Node).Has_Element
then
return False;
end if;
Insert (Container, New_Item, Position, Inserted);
if not Inserted then
- Container.Nodes (Position.Node).Element := New_Item;
+ Container.Content.Nodes (Position.Node).Element := New_Item;
end if;
end Include;
-- Start of processing for Insert
begin
- Local_Insert (Container, New_Item, Node, Inserted);
+ Local_Insert (Container.Content, New_Item, Node, Inserted);
end Insert;
------------------
procedure Intersection (Target : in out Set; Source : Set) is
Tgt_Node : Count_Type;
- TN : Nodes_Type renames Target.Nodes;
+ TN : Nodes_Type renames Target.Content.Nodes;
begin
if Target'Address = Source'Address then
return;
end if;
- if Source.Length = 0 then
+ if Source.Content.Length = 0 then
Clear (Target);
return;
end if;
- Tgt_Node := HT_Ops.First (Target);
+ Tgt_Node := HT_Ops.First (Target.Content);
while Tgt_Node /= 0 loop
if Find (Source, TN (Tgt_Node).Element).Node /= 0 then
- Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
+ Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
else
declare
X : constant Count_Type := Tgt_Node;
begin
- Tgt_Node := HT_Ops.Next (Target, Tgt_Node);
- HT_Ops.Delete_Node_Sans_Free (Target, X);
+ Tgt_Node := HT_Ops.Next (Target.Content, Tgt_Node);
+ HT_Ops.Delete_Node_Sans_Free (Target.Content, X);
Free (Target, X);
end;
end if;
-------------
procedure Process (L_Node : Count_Type) is
- E : Element_Type renames Left.Nodes (L_Node).Element;
+ E : Element_Type renames Left.Content.Nodes (L_Node).Element;
X : Count_Type;
B : Boolean;
-- Start of processing for Intersection
begin
- Iterate (Left);
+ Iterate (Left.Content);
end Intersection;
function Intersection (Left : Set; Right : Set) return Set is
begin
if Left'Address = Right'Address then
- return Left.Copy;
+ return Copy (Left);
end if;
C := Count_Type'Min (Length (Left), Length (Right)); -- ???
function Is_In (HT : Set; Key : Node_Type) return Boolean is
begin
- return Element_Keys.Find (HT, Key.Element) /= 0;
+ return Element_Keys.Find (HT.Content, Key.Element) /= 0;
end Is_In;
---------------
function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
Subset_Node : Count_Type;
- Subset_Nodes : Nodes_Type renames Subset.Nodes;
+ Subset_Nodes : Nodes_Type renames Subset.Content.Nodes;
begin
if Subset'Address = Of_Set'Address then
end if;
end;
- Subset_Node := HT_Ops.Next (Subset, Subset_Node);
+ Subset_Node := HT_Ops.Next (Subset.Content, Subset_Node);
end loop;
return True;
function Length (Container : Set) return Count_Type is
begin
- return Container.Length;
+ return Container.Content.Length;
end Length;
----------
-- Comments???
procedure Move (Target : in out Set; Source : in out Set) is
- NN : HT_Types.Nodes_Type renames Source.Nodes;
+ NN : HT_Types.Nodes_Type renames Source.Content.Nodes;
X, Y : Count_Type;
begin
Clear (Target);
- if Source.Length = 0 then
+ if Source.Content.Length = 0 then
return;
end if;
- X := HT_Ops.First (Source);
+ X := HT_Ops.First (Source.Content);
while X /= 0 loop
Insert (Target, NN (X).Element); -- optimize???
- Y := HT_Ops.Next (Source, X);
+ Y := HT_Ops.Next (Source.Content, X);
- HT_Ops.Delete_Node_Sans_Free (Source, X);
+ HT_Ops.Delete_Node_Sans_Free (Source.Content, X);
Free (Source, X);
X := Y;
pragma Assert (Vet (Container, Position), "bad cursor in Next");
- return (Node => HT_Ops.Next (Container, Position.Node));
+ return (Node => HT_Ops.Next (Container.Content, Position.Node));
end Next;
procedure Next (Container : Set; Position : in out Cursor) is
function Overlap (Left, Right : Set) return Boolean is
Left_Node : Count_Type;
- Left_Nodes : Nodes_Type renames Left.Nodes;
+ Left_Nodes : Nodes_Type renames Left.Content.Nodes;
begin
if Length (Right) = 0 or Length (Left) = 0 then
end if;
end;
- Left_Node := HT_Ops.Next (Left, Left_Node);
+ Left_Node := HT_Ops.Next (Left.Content, Left_Node);
end loop;
return False;
-------------
procedure Replace (Container : in out Set; New_Item : Element_Type) is
- Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
+ Node : constant Count_Type :=
+ Element_Keys.Find (Container.Content, New_Item);
begin
if Node = 0 then
raise Constraint_Error with "attempt to replace element not in set";
end if;
- Container.Nodes (Node).Element := New_Item;
+ Container.Content.Nodes (Node).Element := New_Item;
end Replace;
---------------------
pragma Assert
(Vet (Container, Position), "bad cursor in Replace_Element");
- Replace_Element (Container, Position.Node, New_Item);
+ Replace_Element (Container.Content, Position.Node, New_Item);
end Replace_Element;
----------------------
procedure Process (Source_Node : Count_Type) is
B : Boolean;
- N : Node_Type renames Source.Nodes (Source_Node);
+ N : Node_Type renames Source.Content.Nodes (Source_Node);
X : Count_Type;
begin
return;
end if;
- Iterate (Source);
+ Iterate (Source.Content);
end Symmetric_Difference;
function Symmetric_Difference (Left : Set; Right : Set) return Set is
end if;
if Length (Right) = 0 then
- return Left.Copy;
+ return Copy (Left);
end if;
if Length (Left) = 0 then
- return Right.Copy;
+ return Copy (Right);
end if;
C := Length (Left) + Length (Right);
-------------
procedure Process (Src_Node : Count_Type) is
- N : Node_Type renames Source.Nodes (Src_Node);
+ N : Node_Type renames Source.Content.Nodes (Src_Node);
E : Element_Type renames N.Element;
X : Count_Type;
return;
end if;
- Iterate (Source);
+ Iterate (Source.Content);
end Union;
function Union (Left : Set; Right : Set) return Set is
begin
if Left'Address = Right'Address then
- return Left.Copy;
+ return Copy (Left);
end if;
if Length (Right) = 0 then
- return Left.Copy;
+ return Copy (Left);
end if;
if Length (Left) = 0 then
- return Right.Copy;
+ return Copy (Right);
end if;
C := Length (Left) + Length (Right);
declare
S : Set renames Container;
- N : Nodes_Type renames S.Nodes;
+ N : Nodes_Type renames S.Content.Nodes;
X : Count_Type;
begin
- if S.Length = 0 then
+ if S.Content.Length = 0 then
return False;
end if;
return False;
end if;
- X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element));
+ X := S.Content.Buckets
+ (Element_Keys.Index (S.Content, N (Position.Node).Element));
- for J in 1 .. S.Length loop
+ for J in 1 .. S.Content.Length loop
if X = Position.Node then
return True;
end if;
Position => Position)
and Positions (Container) = Positions (Container)'Old;
+ function Constant_Reference
+ (Container : aliased Set;
+ Position : Cursor) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Constant_Reference'Result.all =
+ E.Get (Elements (Container), P.Get (Positions (Container), Position));
+
procedure Move (Target : in out Set; Source : in out Set) with
Global => null,
Pre => Target.Capacity >= Length (Source),
type Node_Type is
record
- Element : Element_Type;
+ Element : aliased Element_Type;
Next : Count_Type;
Has_Element : Boolean := False;
end record;
package HT_Types is new
Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
- type Set (Capacity : Count_Type; Modulus : Hash_Type) is
- new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
+ type Set (Capacity : Count_Type; Modulus : Hash_Type) is record
+ Content : HT_Types.Hash_Table_Type (Capacity, Modulus);
+ end record;
use HT_Types;
Free (Container.Elements_Ptr);
end Clear;
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased Vector;
+ Index : Index_Type) return not null access constant Element_Type
+ is
+ begin
+ if Index > Container.Last then
+ raise Constraint_Error with "Index is out of range";
+ end if;
+
+ declare
+ II : constant Int'Base := Int (Index) - Int (No_Index);
+ I : constant Capacity_Range := Capacity_Range (II);
+
+ begin
+ return Constant_Reference (Elemsc (Container) (I));
+ end;
+ end Constant_Reference;
+
--------------
-- Contains --
--------------
Insert (Container, Index_Type'First, New_Item, Count);
end Prepend;
+ ---------------
+ -- Reference --
+ ---------------
+
+ function Reference
+ (Container : not null access Vector;
+ Index : Index_Type) return not null access Element_Type
+ is
+ begin
+ if Index > Container.Last then
+ raise Constraint_Error with "Index is out of range";
+ end if;
+
+ declare
+ II : constant Int'Base := Int (Index) - Int (No_Index);
+ I : constant Capacity_Range := Capacity_Range (II);
+
+ begin
+ if Container.Elements_Ptr = null then
+ return Reference (Container.Elements (I)'Access);
+ else
+ return Reference (Container.Elements_Ptr (I)'Access);
+ end if;
+ end;
+ end Reference;
+
---------------------
-- Replace_Element --
---------------------
Right => Model (Container),
Position => Index);
+ function At_End (E : access constant Vector) return access constant Vector
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function At_End
+ (E : access constant Element_Type) return access constant Element_Type
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function Constant_Reference
+ (Container : aliased Vector;
+ Index : Index_Type) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Index in First_Index (Container) .. Last_Index (Container),
+ Post =>
+ Constant_Reference'Result.all = Element (Model (Container), Index);
+
+ function Reference
+ (Container : not null access Vector;
+ Index : Index_Type) return not null access Element_Type
+ with
+ Global => null,
+ Pre =>
+ Index in First_Index (Container.all) .. Last_Index (Container.all),
+ Post =>
+ Length (Container.all) = Length (At_End (Container).all)
+
+ -- Container will have Result.all at index Index
+
+ and At_End (Reference'Result).all =
+ Element (Model (At_End (Container).all), Index)
+
+ -- All other elements are preserved
+
+ and M.Equal_Except
+ (Left => Model (Container.all),
+ Right => Model (At_End (Container).all),
+ Position => Index);
+
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
use Holders;
subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
- type Elements_Array is array (Array_Index range <>) of Holder;
+ type Elements_Array is array (Array_Index range <>) of aliased Holder;
function "=" (L, R : Elements_Array) return Boolean is abstract;
type Elements_Array_Ptr is access all Elements_Array;
return True;
end if;
- Lst := Next (Left, Last (Left).Node);
+ Lst := Next (Left.Content, Last (Left).Node);
Node := First (Left).Node;
while Node /= Lst loop
- ENode := Find (Right, Left.Nodes (Node).Key).Node;
+ ENode := Find (Right, Left.Content.Nodes (Node).Key).Node;
if ENode = 0 or else
- Left.Nodes (Node).Element /= Right.Nodes (ENode).Element
+ Left.Content.Nodes (Node).Element /=
+ Right.Content.Nodes (ENode).Element
then
return False;
end if;
- Node := Next (Left, Node);
+ Node := Next (Left.Content, Node);
end loop;
return True;
--------------------
procedure Append_Element (Source_Node : Count_Type) is
- SN : Node_Type renames Source.Nodes (Source_Node);
+ SN : Node_Type renames Source.Content.Nodes (Source_Node);
procedure Set_Element (Node : in out Node_Type);
pragma Inline (Set_Element);
function New_Node return Count_Type is
Result : Count_Type;
begin
- Allocate (Target, Result);
+ Allocate (Target.Content, Result);
return Result;
end New_Node;
begin
Unconditional_Insert_Avec_Hint
- (Tree => Target,
+ (Tree => Target.Content,
Hint => 0,
Key => SN.Key,
Node => Target_Node);
raise Storage_Error with "not enough capacity"; -- SE or CE? ???
end if;
- Tree_Operations.Clear_Tree (Target);
- Append_Elements (Source);
+ Tree_Operations.Clear_Tree (Target.Content);
+ Append_Elements (Source.Content);
end Assign;
-------------
-------------
function Ceiling (Container : Map; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Ops.Ceiling (Container, Key);
+ Node : constant Count_Type := Key_Ops.Ceiling (Container.Content, Key);
begin
if Node = 0 then
procedure Clear (Container : in out Map) is
begin
- Tree_Operations.Clear_Tree (Container);
+ Tree_Operations.Clear_Tree (Container.Content);
end Clear;
-----------
return Node.Color;
end Color;
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Position : Cursor) return not null access constant Element_Type
+ is
+ begin
+ if not Has_Element (Container, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert (Vet (Container.Content, Position.Node),
+ "bad cursor in function Constant_Reference");
+
+ return Container.Content.Nodes (Position.Node).Element'Access;
+ end Constant_Reference;
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Key : Key_Type) return not null access constant Element_Type
+ is
+ Node : constant Node_Access := Find (Container, Key).Node;
+
+ begin
+ if Node = 0 then
+ raise Constraint_Error with
+ "no element available because key not in map";
+ end if;
+
+ return Container.Content.Nodes (Node).Element'Access;
+ end Constant_Reference;
+
--------------
-- Contains --
--------------
return Target : Map (Count_Type'Max (Source.Capacity, Capacity)) do
if Length (Source) > 0 then
- Target.Length := Source.Length;
- Target.Root := Source.Root;
- Target.First := Source.First;
- Target.Last := Source.Last;
- Target.Free := Source.Free;
+ Target.Content.Length := Source.Content.Length;
+ Target.Content.Root := Source.Content.Root;
+ Target.Content.First := Source.Content.First;
+ Target.Content.Last := Source.Content.Last;
+ Target.Content.Free := Source.Content.Free;
while Node <= Source.Capacity loop
- Target.Nodes (Node).Element :=
- Source.Nodes (Node).Element;
- Target.Nodes (Node).Key :=
- Source.Nodes (Node).Key;
- Target.Nodes (Node).Parent :=
- Source.Nodes (Node).Parent;
- Target.Nodes (Node).Left :=
- Source.Nodes (Node).Left;
- Target.Nodes (Node).Right :=
- Source.Nodes (Node).Right;
- Target.Nodes (Node).Color :=
- Source.Nodes (Node).Color;
- Target.Nodes (Node).Has_Element :=
- Source.Nodes (Node).Has_Element;
+ Target.Content.Nodes (Node).Element :=
+ Source.Content.Nodes (Node).Element;
+ Target.Content.Nodes (Node).Key :=
+ Source.Content.Nodes (Node).Key;
+ Target.Content.Nodes (Node).Parent :=
+ Source.Content.Nodes (Node).Parent;
+ Target.Content.Nodes (Node).Left :=
+ Source.Content.Nodes (Node).Left;
+ Target.Content.Nodes (Node).Right :=
+ Source.Content.Nodes (Node).Right;
+ Target.Content.Nodes (Node).Color :=
+ Source.Content.Nodes (Node).Color;
+ Target.Content.Nodes (Node).Has_Element :=
+ Source.Content.Nodes (Node).Has_Element;
Node := Node + 1;
end loop;
while Node <= Target.Capacity loop
N := Node;
- Formal_Ordered_Maps.Free (Tree => Target, X => N);
+ Free (Tree => Target, X => N);
Node := Node + 1;
end loop;
end if;
"Position cursor of Delete has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"Position cursor of Delete is bad");
- Tree_Operations.Delete_Node_Sans_Free (Container,
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content,
Position.Node);
- Formal_Ordered_Maps.Free (Container, Position.Node);
+ Free (Container, Position.Node);
Position := No_Element;
end Delete;
procedure Delete (Container : in out Map; Key : Key_Type) is
- X : constant Node_Access := Key_Ops.Find (Container, Key);
+ X : constant Node_Access := Key_Ops.Find (Container.Content, Key);
begin
if X = 0 then
raise Constraint_Error with "key not in map";
end if;
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Maps.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end Delete;
------------------
X : constant Node_Access := First (Container).Node;
begin
if X /= 0 then
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Maps.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end if;
end Delete_First;
X : constant Node_Access := Last (Container).Node;
begin
if X /= 0 then
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Maps.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end if;
end Delete_Last;
"Position cursor of function Element has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"Position cursor of function Element is bad");
- return Container.Nodes (Position.Node).Element;
+ return Container.Content.Nodes (Position.Node).Element;
end Element;
raise Constraint_Error with "key not in map";
end if;
- return Container.Nodes (Node).Element;
+ return Container.Content.Nodes (Node).Element;
end Element;
---------------------
-------------
procedure Exclude (Container : in out Map; Key : Key_Type) is
- X : constant Node_Access := Key_Ops.Find (Container, Key);
+ X : constant Node_Access := Key_Ops.Find (Container.Content, Key);
begin
if X /= 0 then
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Maps.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end if;
end Exclude;
----------
function Find (Container : Map; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Ops.Find (Container, Key);
+ Node : constant Count_Type := Key_Ops.Find (Container.Content, Key);
begin
if Node = 0 then
return No_Element;
end if;
- return (Node => Container.First);
+ return (Node => Container.Content.First);
end First;
-------------------
raise Constraint_Error with "map is empty";
end if;
- return Container.Nodes (First (Container).Node).Element;
+ return Container.Content.Nodes (First (Container).Node).Element;
end First_Element;
---------------
raise Constraint_Error with "map is empty";
end if;
- return Container.Nodes (First (Container).Node).Key;
+ return Container.Content.Nodes (First (Container).Node).Key;
end First_Key;
-----------
-----------
function Floor (Container : Map; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Ops.Floor (Container, Key);
+ Node : constant Count_Type := Key_Ops.Floor (Container.Content, Key);
begin
if Node = 0 then
----------
function Keys (Container : Map) return K.Sequence is
- Position : Count_Type := Container.First;
+ Position : Count_Type := Container.Content.First;
R : K.Sequence;
begin
-- for their postconditions.
while Position /= 0 loop
- R := K.Add (R, Container.Nodes (Position).Key);
- Position := Tree_Operations.Next (Container, Position);
+ R := K.Add (R, Container.Content.Nodes (Position).Key);
+ Position := Tree_Operations.Next (Container.Content, Position);
end loop;
return R;
-----------
function Model (Container : Map) return M.Map is
- Position : Count_Type := Container.First;
+ Position : Count_Type := Container.Content.First;
R : M.Map;
begin
R :=
M.Add
(Container => R,
- New_Key => Container.Nodes (Position).Key,
- New_Item => Container.Nodes (Position).Element);
+ New_Key => Container.Content.Nodes (Position).Key,
+ New_Item => Container.Content.Nodes (Position).Element);
- Position := Tree_Operations.Next (Container, Position);
+ Position := Tree_Operations.Next (Container.Content, Position);
end loop;
return R;
function Positions (Container : Map) return P.Map is
I : Count_Type := 1;
- Position : Count_Type := Container.First;
+ Position : Count_Type := Container.Content.First;
R : P.Map;
begin
while Position /= 0 loop
R := P.Add (R, (Node => Position), I);
pragma Assert (P.Length (R) = I);
- Position := Tree_Operations.Next (Container, Position);
+ Position := Tree_Operations.Next (Container.Content, Position);
I := I + 1;
end loop;
X : Count_Type)
is
begin
- Tree.Nodes (X).Has_Element := False;
- Tree_Operations.Free (Tree, X);
+ Tree.Content.Nodes (X).Has_Element := False;
+ Tree_Operations.Free (Tree.Content, X);
end Free;
----------------------
return False;
end if;
- return Container.Nodes (Position.Node).Has_Element;
+ return Container.Content.Nodes (Position.Node).Has_Element;
end Has_Element;
-------------
if not Inserted then
declare
- N : Node_Type renames Container.Nodes (Position.Node);
+ N : Node_Type renames Container.Content.Nodes (Position.Node);
begin
N.Key := Key;
N.Element := New_Item;
X : Node_Access;
begin
- Allocate_Node (Container, X);
+ Allocate_Node (Container.Content, X);
return X;
end New_Node;
begin
Insert_Sans_Hint
- (Container,
+ (Container.Content,
Key,
Position.Node,
Inserted);
"Position cursor of function Key has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"Position cursor of function Key is bad");
- return Container.Nodes (Position.Node).Key;
+ return Container.Content.Nodes (Position.Node).Key;
end Key;
----------
return No_Element;
end if;
- return (Node => Container.Last);
+ return (Node => Container.Content.Last);
end Last;
------------------
raise Constraint_Error with "map is empty";
end if;
- return Container.Nodes (Last (Container).Node).Element;
+ return Container.Content.Nodes (Last (Container).Node).Element;
end Last_Element;
--------------
raise Constraint_Error with "map is empty";
end if;
- return Container.Nodes (Last (Container).Node).Key;
+ return Container.Content.Nodes (Last (Container).Node).Key;
end Last_Key;
--------------
function Length (Container : Map) return Count_Type is
begin
- return Container.Length;
+ return Container.Content.Length;
end Length;
----------
----------
procedure Move (Target : in out Map; Source : in out Map) is
- NN : Tree_Types.Nodes_Type renames Source.Nodes;
+ NN : Tree_Types.Nodes_Type renames Source.Content.Nodes;
X : Node_Access;
begin
Insert (Target, NN (X).Key, NN (X).Element); -- optimize???
- Tree_Operations.Delete_Node_Sans_Free (Source, X);
+ Tree_Operations.Delete_Node_Sans_Free (Source.Content, X);
Formal_Ordered_Maps.Free (Source, X);
end loop;
end Move;
raise Constraint_Error;
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Next");
- return (Node => Tree_Operations.Next (Container, Position.Node));
+ return (Node => Tree_Operations.Next (Container.Content, Position.Node));
end Next;
------------
raise Constraint_Error;
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Previous");
declare
Node : constant Count_Type :=
- Tree_Operations.Previous (Container, Position.Node);
+ Tree_Operations.Previous (Container.Content, Position.Node);
begin
if Node = 0 then
end;
end Previous;
+ --------------
+ -- Reference --
+ --------------
+
+ function Reference
+ (Container : not null access Map;
+ Position : Cursor) return not null access Element_Type
+ is
+ begin
+ if not Has_Element (Container.all, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert
+ (Vet (Container.Content, Position.Node),
+ "bad cursor in function Reference");
+
+ return Container.Content.Nodes (Position.Node).Element'Access;
+ end Reference;
+
+ function Reference
+ (Container : not null access Map;
+ Key : Key_Type) return not null access Element_Type
+ is
+ Node : constant Count_Type := Find (Container.all, Key).Node;
+
+ begin
+ if Node = 0 then
+ raise Constraint_Error with
+ "no element available because key not in map";
+ end if;
+
+ return Container.Content.Nodes (Node).Element'Access;
+ end Reference;
+
-------------
-- Replace --
-------------
is
begin
declare
- Node : constant Node_Access := Key_Ops.Find (Container, Key);
+ Node : constant Node_Access := Key_Ops.Find (Container.Content, Key);
begin
if Node = 0 then
end if;
declare
- N : Node_Type renames Container.Nodes (Node);
+ N : Node_Type renames Container.Content.Nodes (Node);
begin
N.Key := Key;
N.Element := New_Item;
"Position cursor of Replace_Element has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"Position cursor of Replace_Element is bad");
- Container.Nodes (Position.Node).Element := New_Item;
+ Container.Content.Nodes (Position.Node).Element := New_Item;
end Replace_Element;
---------------
Model (Container)'Old,
Key (Container, Position));
+ function At_End
+ (E : not null access constant Map) return not null access constant Map
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function At_End
+ (E : access constant Element_Type) return access constant Element_Type
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Position : Cursor) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Constant_Reference'Result.all =
+ Element (Model (Container), Key (Container, Position));
+
+ function Reference
+ (Container : not null access Map;
+ Position : Cursor) return not null access Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container.all, Position),
+ Post =>
+
+ -- Order of keys and cursors is preserved
+
+ Keys (At_End (Container).all) = Keys (Container.all)
+ and Positions (At_End (Container).all) = Positions (Container.all)
+
+ -- The value designated by the result of Reference is now associated
+ -- with the key at position Position in Container.
+
+ and Element (At_End (Container).all, Position) =
+ At_End (Reference'Result).all
+
+ -- Elements associated with other keys are preserved
+
+ and M.Same_Keys
+ (Model (At_End (Container).all),
+ Model (Container.all))
+ and M.Elements_Equal_Except
+ (Model (At_End (Container).all),
+ Model (Container.all),
+ Key (At_End (Container).all, Position));
+
+ function Constant_Reference
+ (Container : aliased Map;
+ Key : Key_Type) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Constant_Reference'Result.all = Element (Model (Container), Key);
+
+ function Reference
+ (Container : not null access Map;
+ Key : Key_Type) return not null access Element_Type
+ with
+ Global => null,
+ Pre => Contains (Container.all, Key),
+ Post =>
+
+ -- Order of keys and cursors is preserved
+
+ Keys (At_End (Container).all) = Keys (Container.all)
+ and Positions (At_End (Container).all) = Positions (Container.all)
+
+ -- The value designated by the result of Reference is now associated
+ -- with Key in Container.
+
+ and Element (Model (At_End (Container).all), Key) =
+ At_End (Reference'Result).all
+
+ -- Elements associated with other keys are preserved
+
+ and M.Same_Keys
+ (Model (At_End (Container).all),
+ Model (Container.all))
+ and M.Elements_Equal_Except
+ (Model (At_End (Container).all),
+ Model (Container.all),
+ Key);
+
procedure Move (Target : in out Map; Source : in out Map) with
Global => null,
Pre => Target.Capacity >= Length (Source),
Right : Node_Access := 0;
Color : Red_Black_Trees.Color_Type := Red;
Key : Key_Type;
- Element : Element_Type;
+ Element : aliased Element_Type;
end record;
package Tree_Types is
new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
- type Map (Capacity : Count_Type) is
- new Tree_Types.Tree_Type (Capacity) with null record;
+ type Map (Capacity : Count_Type) is record
+ Content : Tree_Types.Tree_Type (Capacity);
+ end record;
Empty_Map : constant Map := (Capacity => 0, others => <>);
-- Comments needed???
+ procedure Assign
+ (Target : in out Tree_Types.Tree_Type;
+ Source : Tree_Types.Tree_Type);
+
generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
procedure Free (Tree : in out Set; X : Count_Type);
procedure Insert_Sans_Hint
- (Container : in out Set;
+ (Container : in out Tree_Types.Tree_Type;
New_Item : Element_Type;
Node : out Count_Type;
Inserted : out Boolean);
procedure Insert_With_Hint
- (Dst_Set : in out Set;
+ (Dst_Set : in out Tree_Types.Tree_Type;
Dst_Hint : Count_Type;
Src_Node : Node_Type;
Dst_Node : out Count_Type);
package Set_Ops is
new Red_Black_Trees.Generic_Bounded_Set_Operations
(Tree_Operations => Tree_Operations,
- Set_Type => Set,
+ Set_Type => Tree_Types.Tree_Type,
Assign => Assign,
Insert_With_Hint => Insert_With_Hint,
Is_Less => Is_Less_Node_Node);
return True;
end if;
- Lst := Next (Left, Last (Left).Node);
+ Lst := Next (Left.Content, Last (Left).Node);
Node := First (Left).Node;
while Node /= Lst loop
- ENode := Find (Right, Left.Nodes (Node).Element).Node;
+ ENode := Find (Right, Left.Content.Nodes (Node).Element).Node;
if ENode = 0
- or else Left.Nodes (Node).Element /= Right.Nodes (ENode).Element
+ or else Left.Content.Nodes (Node).Element /=
+ Right.Content.Nodes (ENode).Element
then
return False;
end if;
- Node := Next (Left, Node);
+ Node := Next (Left.Content, Node);
end loop;
return True;
-- Assign --
------------
- procedure Assign (Target : in out Set; Source : Set) is
+ procedure Assign
+ (Target : in out Tree_Types.Tree_Type;
+ Source : Tree_Types.Tree_Type)
+ is
procedure Append_Element (Source_Node : Count_Type);
procedure Append_Elements is
Append_Elements (Source);
end Assign;
+ procedure Assign (Target : in out Set; Source : Set) is
+ begin
+ Assign (Target.Content, Source.Content);
+ end Assign;
+
-------------
-- Ceiling --
-------------
function Ceiling (Container : Set; Item : Element_Type) return Cursor is
- Node : constant Count_Type := Element_Keys.Ceiling (Container, Item);
+ Node : constant Count_Type :=
+ Element_Keys.Ceiling (Container.Content, Item);
begin
if Node = 0 then
procedure Clear (Container : in out Set) is
begin
- Tree_Operations.Clear_Tree (Container);
+ Tree_Operations.Clear_Tree (Container.Content);
end Clear;
-----------
return Node.Color;
end Color;
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased Set;
+ Position : Cursor) return not null access constant Element_Type
+ is
+ begin
+ if not Has_Element (Container, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert (Vet (Container.Content, Position.Node),
+ "bad cursor in Element");
+
+ return Container.Content.Nodes (Position.Node).Element'Access;
+ end Constant_Reference;
+
--------------
-- Contains --
--------------
end if;
if Length (Source) > 0 then
- Target.Length := Source.Length;
- Target.Root := Source.Root;
- Target.First := Source.First;
- Target.Last := Source.Last;
- Target.Free := Source.Free;
+ Target.Content.Length := Source.Content.Length;
+ Target.Content.Root := Source.Content.Root;
+ Target.Content.First := Source.Content.First;
+ Target.Content.Last := Source.Content.Last;
+ Target.Content.Free := Source.Content.Free;
Node := 1;
while Node <= Source.Capacity loop
- Target.Nodes (Node).Element :=
- Source.Nodes (Node).Element;
- Target.Nodes (Node).Parent :=
- Source.Nodes (Node).Parent;
- Target.Nodes (Node).Left :=
- Source.Nodes (Node).Left;
- Target.Nodes (Node).Right :=
- Source.Nodes (Node).Right;
- Target.Nodes (Node).Color :=
- Source.Nodes (Node).Color;
- Target.Nodes (Node).Has_Element :=
- Source.Nodes (Node).Has_Element;
+ Target.Content.Nodes (Node).Element :=
+ Source.Content.Nodes (Node).Element;
+ Target.Content.Nodes (Node).Parent :=
+ Source.Content.Nodes (Node).Parent;
+ Target.Content.Nodes (Node).Left :=
+ Source.Content.Nodes (Node).Left;
+ Target.Content.Nodes (Node).Right :=
+ Source.Content.Nodes (Node).Right;
+ Target.Content.Nodes (Node).Color :=
+ Source.Content.Nodes (Node).Color;
+ Target.Content.Nodes (Node).Has_Element :=
+ Source.Content.Nodes (Node).Has_Element;
Node := Node + 1;
end loop;
while Node <= Target.Capacity loop
N := Node;
- Formal_Ordered_Sets.Free (Tree => Target, X => N);
+ Free (Tree => Target, X => N);
Node := Node + 1;
end loop;
end if;
raise Constraint_Error with "Position cursor has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Delete");
- Tree_Operations.Delete_Node_Sans_Free (Container,
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content,
Position.Node);
- Formal_Ordered_Sets.Free (Container, Position.Node);
+ Free (Container, Position.Node);
Position := No_Element;
end Delete;
procedure Delete (Container : in out Set; Item : Element_Type) is
- X : constant Count_Type := Element_Keys.Find (Container, Item);
+ X : constant Count_Type := Element_Keys.Find (Container.Content, Item);
begin
if X = 0 then
raise Constraint_Error with "attempt to delete element not in set";
end if;
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Sets.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end Delete;
------------------
------------------
procedure Delete_First (Container : in out Set) is
- X : constant Count_Type := Container.First;
+ X : constant Count_Type := Container.Content.First;
begin
if X /= 0 then
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Sets.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end if;
end Delete_First;
-----------------
procedure Delete_Last (Container : in out Set) is
- X : constant Count_Type := Container.Last;
+ X : constant Count_Type := Container.Content.Last;
begin
if X /= 0 then
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Sets.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end if;
end Delete_Last;
procedure Difference (Target : in out Set; Source : Set) is
begin
- Set_Ops.Set_Difference (Target, Source);
+ Set_Ops.Set_Difference (Target.Content, Source.Content);
end Difference;
function Difference (Left, Right : Set) return Set is
end if;
if Length (Right) = 0 then
- return Left.Copy;
+ return Copy (Left);
end if;
return S : Set (Length (Left)) do
- Assign (S, Set_Ops.Set_Difference (Left, Right));
+ Assign
+ (S.Content, Set_Ops.Set_Difference (Left.Content, Right.Content));
end return;
end Difference;
raise Constraint_Error with "Position cursor has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Element");
- return Container.Nodes (Position.Node).Element;
+ return Container.Content.Nodes (Position.Node).Element;
end Element;
-------------------------
-- Start of processing for Equivalent_Sets
begin
- return Is_Equivalent (Left, Right);
+ return Is_Equivalent (Left.Content, Right.Content);
end Equivalent_Sets;
-------------
-------------
procedure Exclude (Container : in out Set; Item : Element_Type) is
- X : constant Count_Type := Element_Keys.Find (Container, Item);
+ X : constant Count_Type := Element_Keys.Find (Container.Content, Item);
begin
if X /= 0 then
- Tree_Operations.Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Sets.Free (Container, X);
+ Tree_Operations.Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end if;
end Exclude;
----------
function Find (Container : Set; Item : Element_Type) return Cursor is
- Node : constant Count_Type := Element_Keys.Find (Container, Item);
+ Node : constant Count_Type :=
+ Element_Keys.Find (Container.Content, Item);
begin
if Node = 0 then
return No_Element;
end if;
- return (Node => Container.First);
+ return (Node => Container.Content.First);
end First;
-------------------
end if;
declare
- N : Tree_Types.Nodes_Type renames Container.Nodes;
+ N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
begin
return N (Fst).Element;
end;
function Floor (Container : Set; Item : Element_Type) return Cursor is
begin
declare
- Node : constant Count_Type := Element_Keys.Floor (Container, Item);
+ Node : constant Count_Type :=
+ Element_Keys.Floor (Container.Content, Item);
begin
if Node = 0 then
--------------
function Elements (Container : Set) return E.Sequence is
- Position : Count_Type := Container.First;
+ Position : Count_Type := Container.Content.First;
R : E.Sequence;
begin
-- for their postconditions.
while Position /= 0 loop
- R := E.Add (R, Container.Nodes (Position).Element);
- Position := Tree_Operations.Next (Container, Position);
+ R := E.Add (R, Container.Content.Nodes (Position).Element);
+ Position := Tree_Operations.Next (Container.Content, Position);
end loop;
return R;
-----------
function Model (Container : Set) return M.Set is
- Position : Count_Type := Container.First;
+ Position : Count_Type := Container.Content.First;
R : M.Set;
begin
R :=
M.Add
(Container => R,
- Item => Container.Nodes (Position).Element);
+ Item => Container.Content.Nodes (Position).Element);
- Position := Tree_Operations.Next (Container, Position);
+ Position := Tree_Operations.Next (Container.Content, Position);
end loop;
return R;
function Positions (Container : Set) return P.Map is
I : Count_Type := 1;
- Position : Count_Type := Container.First;
+ Position : Count_Type := Container.Content.First;
R : P.Map;
begin
while Position /= 0 loop
R := P.Add (R, (Node => Position), I);
pragma Assert (P.Length (R) = I);
- Position := Tree_Operations.Next (Container, Position);
+ Position := Tree_Operations.Next (Container.Content, Position);
I := I + 1;
end loop;
procedure Free (Tree : in out Set; X : Count_Type) is
begin
- Tree.Nodes (X).Has_Element := False;
- Tree_Operations.Free (Tree, X);
+ Tree.Content.Nodes (X).Has_Element := False;
+ Tree_Operations.Free (Tree.Content, X);
end Free;
----------------------
-------------
function Ceiling (Container : Set; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Keys.Ceiling (Container, Key);
+ Node : constant Count_Type :=
+ Key_Keys.Ceiling (Container.Content, Key);
begin
if Node = 0 then
------------
procedure Delete (Container : in out Set; Key : Key_Type) is
- X : constant Count_Type := Key_Keys.Find (Container, Key);
+ X : constant Count_Type := Key_Keys.Find (Container.Content, Key);
begin
if X = 0 then
raise Constraint_Error with "attempt to delete key not in set";
end if;
- Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Sets.Free (Container, X);
+ Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end Delete;
-------------
-------------
function Element (Container : Set; Key : Key_Type) return Element_Type is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type := Key_Keys.Find (Container.Content, Key);
begin
if Node = 0 then
end if;
declare
- N : Tree_Types.Nodes_Type renames Container.Nodes;
+ N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
begin
return N (Node).Element;
end;
-------------
procedure Exclude (Container : in out Set; Key : Key_Type) is
- X : constant Count_Type := Key_Keys.Find (Container, Key);
+ X : constant Count_Type := Key_Keys.Find (Container.Content, Key);
begin
if X /= 0 then
- Delete_Node_Sans_Free (Container, X);
- Formal_Ordered_Sets.Free (Container, X);
+ Delete_Node_Sans_Free (Container.Content, X);
+ Free (Container, X);
end if;
end Exclude;
----------
function Find (Container : Set; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type := Key_Keys.Find (Container.Content, Key);
begin
return (if Node = 0 then No_Element else (Node => Node));
end Find;
-----------
function Floor (Container : Set; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Keys.Floor (Container, Key);
+ Node : constant Count_Type := Key_Keys.Floor (Container.Content, Key);
begin
return (if Node = 0 then No_Element else (Node => Node));
end Floor;
"Position cursor has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Key");
declare
- N : Tree_Types.Nodes_Type renames Container.Nodes;
+ N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
begin
return Key (N (Position.Node).Element);
end;
Key : Key_Type;
New_Item : Element_Type)
is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type := Key_Keys.Find (Container.Content, Key);
begin
if not Has_Element (Container, (Node => Node)) then
raise Constraint_Error with
if Position.Node = 0 then
return False;
else
- return Container.Nodes (Position.Node).Has_Element;
+ return Container.Content.Nodes (Position.Node).Has_Element;
end if;
end Has_Element;
if not Inserted then
declare
- N : Tree_Types.Nodes_Type renames Container.Nodes;
+ N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
begin
N (Position.Node).Element := New_Item;
end;
Inserted : out Boolean)
is
begin
- Insert_Sans_Hint (Container, New_Item, Position.Node, Inserted);
+ Insert_Sans_Hint (Container.Content, New_Item, Position.Node, Inserted);
end Insert;
procedure Insert
----------------------
procedure Insert_Sans_Hint
- (Container : in out Set;
+ (Container : in out Tree_Types.Tree_Type;
New_Item : Element_Type;
Node : out Count_Type;
Inserted : out Boolean)
----------------------
procedure Insert_With_Hint
- (Dst_Set : in out Set;
+ (Dst_Set : in out Tree_Types.Tree_Type;
Dst_Hint : Count_Type;
Src_Node : Node_Type;
Dst_Node : out Count_Type)
procedure Intersection (Target : in out Set; Source : Set) is
begin
- Set_Ops.Set_Intersection (Target, Source);
+ Set_Ops.Set_Intersection (Target.Content, Source.Content);
end Intersection;
function Intersection (Left, Right : Set) return Set is
begin
if Left'Address = Right'Address then
- return Left.Copy;
+ return Copy (Left);
end if;
return S : Set (Count_Type'Min (Length (Left), Length (Right))) do
- Assign (S, Set_Ops.Set_Intersection (Left, Right));
+ Assign (S.Content,
+ Set_Ops.Set_Intersection (Left.Content, Right.Content));
end return;
end Intersection;
function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
begin
- return Set_Ops.Set_Subset (Subset, Of_Set => Of_Set);
+ return Set_Ops.Set_Subset (Subset.Content, Of_Set => Of_Set.Content);
end Is_Subset;
----------
begin
return (if Length (Container) = 0
then No_Element
- else (Node => Container.Last));
+ else (Node => Container.Content.Last));
end Last;
------------------
end if;
declare
- N : Tree_Types.Nodes_Type renames Container.Nodes;
+ N : Tree_Types.Nodes_Type renames Container.Content.Nodes;
begin
return N (Last (Container).Node).Element;
end;
function Length (Container : Set) return Count_Type is
begin
- return Container.Length;
+ return Container.Content.Length;
end Length;
----------
----------
procedure Move (Target : in out Set; Source : in out Set) is
- N : Tree_Types.Nodes_Type renames Source.Nodes;
+ N : Tree_Types.Nodes_Type renames Source.Content.Nodes;
X : Count_Type;
begin
Clear (Target);
loop
- X := Source.First;
+ X := Source.Content.First;
exit when X = 0;
Insert (Target, N (X).Element); -- optimize???
- Tree_Operations.Delete_Node_Sans_Free (Source, X);
- Formal_Ordered_Sets.Free (Source, X);
+ Tree_Operations.Delete_Node_Sans_Free (Source.Content, X);
+ Free (Source, X);
end loop;
end Move;
raise Constraint_Error;
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Next");
- return (Node => Tree_Operations.Next (Container, Position.Node));
+ return (Node => Tree_Operations.Next (Container.Content, Position.Node));
end Next;
procedure Next (Container : Set; Position : in out Cursor) is
function Overlap (Left, Right : Set) return Boolean is
begin
- return Set_Ops.Set_Overlap (Left, Right);
+ return Set_Ops.Set_Overlap (Left.Content, Right.Content);
end Overlap;
------------
raise Constraint_Error;
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Previous");
declare
Node : constant Count_Type :=
- Tree_Operations.Previous (Container, Position.Node);
+ Tree_Operations.Previous (Container.Content, Position.Node);
begin
return (if Node = 0 then No_Element else (Node => Node));
end;
-------------
procedure Replace (Container : in out Set; New_Item : Element_Type) is
- Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
+ Node : constant Count_Type :=
+ Element_Keys.Find (Container.Content, New_Item);
begin
if Node = 0 then
"attempt to replace element not in set";
end if;
- Container.Nodes (Node).Element := New_Item;
+ Container.Content.Nodes (Node).Element := New_Item;
end Replace;
---------------------
(Local_Insert_Post,
Local_Insert_Sans_Hint);
- NN : Tree_Types.Nodes_Type renames Tree.Nodes;
+ NN : Tree_Types.Nodes_Type renames Tree.Content.Nodes;
--------------
-- New_Node --
return;
end if;
- Hint := Element_Keys.Ceiling (Tree, Item);
+ Hint := Element_Keys.Ceiling (Tree.Content, Item);
if Hint = 0 then
null;
raise Program_Error with "attempt to replace existing element";
end if;
- Tree_Operations.Delete_Node_Sans_Free (Tree, Node);
+ Tree_Operations.Delete_Node_Sans_Free (Tree.Content, Node);
Local_Insert_With_Hint
- (Tree => Tree,
+ (Tree => Tree.Content,
Position => Hint,
Key => Item,
Node => Result,
"Position cursor has no element";
end if;
- pragma Assert (Vet (Container, Position.Node),
+ pragma Assert (Vet (Container.Content, Position.Node),
"bad cursor in Replace_Element");
Replace_Element (Container, Position.Node, New_Item);
procedure Symmetric_Difference (Target : in out Set; Source : Set) is
begin
- Set_Ops.Set_Symmetric_Difference (Target, Source);
+ Set_Ops.Set_Symmetric_Difference (Target.Content, Source.Content);
end Symmetric_Difference;
function Symmetric_Difference (Left, Right : Set) return Set is
end if;
if Length (Right) = 0 then
- return Left.Copy;
+ return Copy (Left);
end if;
if Length (Left) = 0 then
- return Right.Copy;
+ return Copy (Right);
end if;
return S : Set (Length (Left) + Length (Right)) do
- Assign (S, Set_Ops.Set_Symmetric_Difference (Left, Right));
+ Assign
+ (S.Content,
+ Set_Ops.Set_Symmetric_Difference (Left.Content, Right.Content));
end return;
end Symmetric_Difference;
Inserted : Boolean;
begin
return S : Set (Capacity => 1) do
- Insert_Sans_Hint (S, New_Item, Node, Inserted);
+ Insert_Sans_Hint (S.Content, New_Item, Node, Inserted);
pragma Assert (Inserted);
end return;
end To_Set;
procedure Union (Target : in out Set; Source : Set) is
begin
- Set_Ops.Set_Union (Target, Source);
+ Set_Ops.Set_Union (Target.Content, Source.Content);
end Union;
function Union (Left, Right : Set) return Set is
begin
if Left'Address = Right'Address then
- return Left.Copy;
+ return Copy (Left);
end if;
if Length (Left) = 0 then
- return Right.Copy;
+ return Copy (Right);
end if;
if Length (Right) = 0 then
- return Left.Copy;
+ return Copy (Left);
end if;
return S : Set (Length (Left) + Length (Right)) do
Position => Position)
and Positions (Container) = Positions (Container)'Old;
+ function Constant_Reference
+ (Container : aliased Set;
+ Position : Cursor) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Constant_Reference'Result.all =
+ E.Get (Elements (Container), P.Get (Positions (Container), Position));
+
procedure Move (Target : in out Set; Source : in out Set) with
Global => null,
Pre => Target.Capacity >= Length (Source),
type Node_Type is record
Has_Element : Boolean := False;
- Parent : Count_Type := 0;
- Left : Count_Type := 0;
- Right : Count_Type := 0;
- Color : Red_Black_Trees.Color_Type;
- Element : Element_Type;
+ Parent : Count_Type := 0;
+ Left : Count_Type := 0;
+ Right : Count_Type := 0;
+ Color : Red_Black_Trees.Color_Type;
+ Element : aliased Element_Type;
end record;
package Tree_Types is
new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
- type Set (Capacity : Count_Type) is
- new Tree_Types.Tree_Type (Capacity) with null record;
+ type Set (Capacity : Count_Type) is record
+ Content : Tree_Types.Tree_Type (Capacity);
+ end record;
use Red_Black_Trees;
return Get (Left) = Get (Right);
end "=";
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased Holder) return not null access constant Element_Type
+ is
+ begin
+ return Cast (Container'Address);
+ end Constant_Reference;
+
+ ---------
+ -- Get --
+ ---------
+
+ function Get (Container : Holder) return Element_Type is
+ begin
+ return Cast (Container'Address).all;
+ end Get;
+
---------------
-- Put_Image --
---------------
Array_After (S);
end Put_Image;
- ---------
- -- Get --
- ---------
+ ---------------
+ -- Reference --
+ ---------------
- function Get (Container : Holder) return Element_Type is
+ function Reference
+ (Container : not null access Holder) return not null access Element_Type
+ is
begin
- return Cast (Container'Address).all;
- end Get;
+ return Cast (Container.all'Address);
+ end Reference;
---------
-- Set --
procedure Set (Container : in out Holder; New_Item : Element_Type);
+ function Constant_Reference
+ (Container : aliased Holder) return not null access constant Element_Type;
+
+ function Reference
+ (Container : not null access Holder) return not null access Element_Type;
+
private
-- The implementation uses low-level tricks (Address clauses and unchecked
Container.Last := No_Index;
end Clear;
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : aliased Vector;
+ Index : Index_Type) return not null access constant Element_Type
+ is
+ begin
+ if Index > Container.Last then
+ raise Constraint_Error with "Index is out of range";
+ end if;
+
+ return Container.Elements (To_Array_Index (Index))'Access;
+ end Constant_Reference;
+
--------------
-- Contains --
--------------
end;
end Replace_Element;
+ ---------------
+ -- Reference --
+ ---------------
+
+ function Reference
+ (Container : not null access Vector;
+ Index : Index_Type) return not null access Element_Type
+ is
+ begin
+ if Index > Container.Last then
+ raise Constraint_Error with "Index is out of range";
+ end if;
+
+ return Container.Elements (To_Array_Index (Index))'Access;
+ end Reference;
+
----------------------
-- Reserve_Capacity --
----------------------
Right => Model (Container),
Position => Index);
+ function At_End (E : access constant Vector) return access constant Vector
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function At_End
+ (E : access constant Element_Type) return access constant Element_Type
+ is (E)
+ with Ghost,
+ Annotate => (GNATprove, At_End_Borrow);
+
+ function Constant_Reference
+ (Container : aliased Vector;
+ Index : Index_Type) return not null access constant Element_Type
+ with
+ Global => null,
+ Pre => Index in First_Index (Container) .. Last_Index (Container),
+ Post =>
+ Constant_Reference'Result.all = Element (Model (Container), Index);
+
+ function Reference
+ (Container : not null access Vector;
+ Index : Index_Type) return not null access Element_Type
+ with
+ Global => null,
+ Pre =>
+ Index in First_Index (Container.all) .. Last_Index (Container.all),
+ Post =>
+ Length (Container.all) = Length (At_End (Container).all)
+
+ -- Container will have Result.all at index Index
+
+ and At_End (Reference'Result).all =
+ Element (Model (At_End (Container).all), Index)
+
+ -- All other elements are preserved
+
+ and M.Equal_Except
+ (Left => Model (Container.all),
+ Right => Model (At_End (Container).all),
+ Position => Index);
+
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
pragma Inline (Contains);
subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
- type Elements_Array is array (Array_Index range <>) of Element_Type;
+ type Elements_Array is array (Array_Index range <>) of aliased Element_Type;
function "=" (L, R : Elements_Array) return Boolean is abstract;
type Vector (Capacity : Capacity_Range) is record
Global => null,
Pre => Has_Witness (Container, Witness);
+ function Copy_Key (Key : Key_Type) return Key_Type is (Key);
+ function Copy_Element (Item : Element_Type) return Element_Type is (Item);
+ -- Elements and Keys of maps are copied by numerous primitives in this
+ -- package. This function causes GNATprove to verify that such a copy is
+ -- valid (in particular, it does not break the ownership policy of SPARK,
+ -- i.e. it does not contain pointers that could be used to alias mutable
+ -- data).
+
---------------------------
-- Iteration Primitives --
---------------------------
and Right <= Union'Result
and Included_In_Union (Union'Result, Left, Right);
+ function Copy_Element (Item : Element_Type) return Element_Type is (Item);
+ -- Elements of containers are copied by numerous primitives in this
+ -- package. This function causes GNATprove to verify that such a copy is
+ -- valid (in particular, it does not break the ownership policy of SPARK,
+ -- i.e. it does not contain pointers that could be used to alias mutable
+ -- data).
+
---------------------------
-- Iteration Primitives --
---------------------------
Lst => Last (Remove'Result),
Offset => 1);
+ function Copy_Element (Item : Element_Type) return Element_Type is (Item);
+ -- Elements of containers are copied by numerous primitives in this
+ -- package. This function causes GNATprove to verify that such a copy is
+ -- valid (in particular, it does not break the ownership policy of SPARK,
+ -- i.e. it does not contain pointers that could be used to alias mutable
+ -- data).
+
---------------------------
-- Iteration Primitives --
---------------------------
projects / thirdparty / gcc.git / commitdiff
