public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-1617] [Ada] Add new unbounded and indefinite formal doubly linked list
@ 2022-07-12 12:24 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-07-12 12:24 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:829b5a6075e63e84600b0eee5daebb3fab9aa491
commit r13-1617-g829b5a6075e63e84600b0eee5daebb3fab9aa491
Author: Julien Bortolussi <bortolussi@adacore.com>
Date: Thu May 19 15:49:03 2022 +0200
[Ada] Add new unbounded and indefinite formal doubly linked list
Before this patch, the only formal doubly linked lists were bounded and
definite. This means that it is necessary to provide their maximum
length or capacity at instantiation and that they can only be used with
definite element types.
The formal lists added by this patch are unbounded and indefinite.
Their length grows dynamically until Count_Type'Last. This makes them
easier to use but requires the use of dynamic allocation and controlled
types.
gcc/ada/
* libgnat/a-cfidll.adb, libgnat/a-cfidll.ads: Implementation
files of the formal unbounded indefinite list.
* Makefile.rtl, impunit.adb: Take into account the add of the
new files.
Diff:
---
gcc/ada/Makefile.rtl | 1 +
gcc/ada/impunit.adb | 1 +
gcc/ada/libgnat/a-cfidll.adb | 2054 ++++++++++++++++++++++++++++++++++++++++++
gcc/ada/libgnat/a-cfidll.ads | 1670 ++++++++++++++++++++++++++++++++++
4 files changed, 3726 insertions(+)
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index 3ae4e23d414..00137f20433 100644
--- a/gcc/ada/Makefile.rtl
+++ b/gcc/ada/Makefile.rtl
@@ -113,6 +113,7 @@ GNATRTL_NONTASKING_OBJS= \
a-cfdlli$(objext) \
a-cfhama$(objext) \
a-cfhase$(objext) \
+ a-cfidll$(objext) \
a-cfinve$(objext) \
a-cfinse$(objext) \
a-cforma$(objext) \
diff --git a/gcc/ada/impunit.adb b/gcc/ada/impunit.adb
index b6a7bdee510..343a9dbe8f9 100644
--- a/gcc/ada/impunit.adb
+++ b/gcc/ada/impunit.adb
@@ -605,6 +605,7 @@ package body Impunit is
-- GNAT Defined Additions to Ada 2012 --
----------------------------------------
+ ("a-cfidll", F), -- Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists
("a-cfinse", F), -- Ada.Containers.Functional_Infinite_Sequences
("a-cfinve", F), -- Ada.Containers.Formal_Indefinite_Vectors
("a-coboho", F), -- Ada.Containers.Bounded_Holders
diff --git a/gcc/ada/libgnat/a-cfidll.adb b/gcc/ada/libgnat/a-cfidll.adb
new file mode 100644
index 00000000000..17e48d29e65
--- /dev/null
+++ b/gcc/ada/libgnat/a-cfidll.adb
@@ -0,0 +1,2054 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- ADA.CONTAINERS.FORMAL_INDEFINITE_DOUBLY_LINKED_LISTS --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2022-2022, Free Software Foundation, Inc. --
+-- --
+-- This specification is derived from the Ada Reference Manual for use with --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the contents of the part following the private keyword. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+with Ada.Unchecked_Deallocation;
+
+with Ada.Containers.Stable_Sorting; use Ada.Containers.Stable_Sorting;
+
+with System; use type System.Address;
+
+with Ada.Numerics.Big_Numbers.Big_Integers;
+use Ada.Numerics.Big_Numbers.Big_Integers;
+
+package body Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists with
+ SPARK_Mode => Off
+is
+ -- Convert Count_Type to Big_Integer
+
+ package Conversions is new Signed_Conversions (Int => Count_Type);
+ use Conversions;
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ procedure Allocate
+ (Container : in out List;
+ New_Item : Element_Type;
+ New_Node : out Count_Type);
+
+ procedure Allocate
+ (Container : in out List;
+ New_Node : out Count_Type);
+
+ procedure Free (Container : in out List; X : Count_Type);
+
+ procedure Insert_Internal
+ (Container : in out List;
+ Before : Count_Type;
+ New_Node : Count_Type);
+
+ function Vet (L : List; Position : Cursor) return Boolean with Inline;
+
+ procedure Resize (Container : in out List) with
+ -- Add more room in the internal array
+
+ Global => null,
+ Pre => Container.Nodes = null
+ or else Length (Container) = Container.Nodes'Length,
+ Post => Model (Container) = Model (Container)'Old
+ and Positions (Container) = Positions (Container)'Old;
+
+ procedure Finalize_Element is new Ada.Unchecked_Deallocation
+ (Object => Element_Type,
+ Name => Element_Access);
+
+ procedure Finalize_Nodes is new Ada.Unchecked_Deallocation
+ (Object => Node_Array,
+ Name => Node_Array_Access);
+
+ ---------
+ -- "=" --
+ ---------
+
+ function "=" (Left : List; Right : List) return Boolean is
+ LI : Count_Type;
+ RI : Count_Type;
+
+ begin
+ if Left'Address = Right'Address then
+ return True;
+ end if;
+
+ if Left.Length /= Right.Length then
+ return False;
+ end if;
+
+ LI := Left.First;
+ RI := Right.First;
+ while LI /= 0 loop
+ if Left.Nodes (LI).Element.all /= Right.Nodes (RI).Element.all then
+ return False;
+ end if;
+
+ LI := Left.Nodes (LI).Next;
+ RI := Right.Nodes (RI).Next;
+ end loop;
+
+ return True;
+ end "=";
+
+ ------------
+ -- Adjust --
+ ------------
+
+ overriding procedure Adjust (Container : in out List) is
+ N_Src : Node_Array_Access renames Container.Nodes;
+ N_Tar : Node_Array_Access;
+
+ begin
+ if N_Src = null then
+ return;
+ end if;
+
+ if Container.Length = 0 then
+ Container.Nodes := null;
+ Container.Free := -1;
+ return;
+ end if;
+
+ N_Tar := new Node_Array (1 .. N_Src'Length);
+
+ for X in 1 .. Count_Type (N_Src'Length) loop
+ N_Tar (X) := N_Src (X);
+ if N_Src (X).Element /= null
+ then
+ N_Tar (X).Element := new Element_Type'(N_Src (X).Element.all);
+ end if;
+ end loop;
+
+ N_Src := N_Tar;
+
+ end Adjust;
+
+ --------------
+ -- Allocate --
+ --------------
+
+ procedure Allocate
+ (Container : in out List;
+ New_Node : out Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ if Container.Nodes = null
+ or else Length (Container) = Container.Nodes'Length
+ then
+ Resize (Container);
+ end if;
+
+ if Container.Free >= 0 then
+ New_Node := Container.Free;
+ Container.Free := N (New_Node).Next;
+ else
+ New_Node := abs Container.Free;
+ Container.Free := Container.Free - 1;
+ end if;
+
+ N (New_Node).Element := null;
+ end Allocate;
+
+ procedure Allocate
+ (Container : in out List;
+ New_Item : Element_Type;
+ New_Node : out Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ Allocate (Container, New_Node);
+
+ N (New_Node).Element := new Element_Type'(New_Item);
+ end Allocate;
+
+ ------------
+ -- Append --
+ ------------
+
+ procedure Append (Container : in out List; New_Item : Element_Type) is
+ begin
+ Insert (Container, No_Element, New_Item, 1);
+ end Append;
+
+ procedure Append
+ (Container : in out List;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ is
+ begin
+ Insert (Container, No_Element, New_Item, Count);
+ end Append;
+
+ ------------
+ -- Assign --
+ ------------
+
+ procedure Assign (Target : in out List; Source : List) is
+ N : Node_Array_Access renames Source.Nodes;
+ J : Count_Type;
+
+ begin
+ if Target'Address = Source'Address then
+ return;
+ end if;
+
+ Clear (Target);
+
+ J := Source.First;
+ while J /= 0 loop
+ Append (Target, N (J).Element.all);
+ J := N (J).Next;
+ end loop;
+ end Assign;
+
+ -----------
+ -- Clear --
+ -----------
+
+ procedure Clear (Container : in out List) is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if Container.Length = 0 then
+ pragma Assert (Container.First = 0);
+ pragma Assert (Container.Last = 0);
+ return;
+ end if;
+
+ pragma Assert (Container.First >= 1);
+ pragma Assert (Container.Last >= 1);
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ while Container.Length > 1 loop
+ X := Container.First;
+
+ Container.First := N (X).Next;
+ N (Container.First).Prev := 0;
+
+ Container.Length := Container.Length - 1;
+
+ Free (Container, X);
+ end loop;
+
+ X := Container.First;
+
+ Container.First := 0;
+ Container.Last := 0;
+ Container.Length := 0;
+
+ Free (Container, X);
+ end Clear;
+
+ ------------------------
+ -- Constant_Reference --
+ ------------------------
+
+ function Constant_Reference
+ (Container : 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;
+ end Constant_Reference;
+
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains
+ (Container : List;
+ Item : Element_Type) return Boolean
+ is
+ begin
+ return Find (Container, Item) /= No_Element;
+ end Contains;
+
+ ----------
+ -- Copy --
+ ----------
+
+ function Copy (Source : List) return List
+ is
+ N : Count_Type;
+ P : List;
+
+ begin
+ if Source.Nodes = null then
+ return P;
+ end if;
+
+ P.Nodes := new Node_Array (1 .. Source.Nodes'Length);
+
+ N := 1;
+ while N <= Source.Nodes'Length loop
+ P.Nodes (N).Prev := Source.Nodes (N).Prev;
+ P.Nodes (N).Next := Source.Nodes (N).Next;
+ if Source.Nodes (N).Element /= null then
+ P.Nodes (N).Element :=
+ new Element_Type'(Source.Nodes (N).Element.all);
+ end if;
+ N := N + 1;
+ end loop;
+
+ P.Free := Source.Free;
+ P.Length := Source.Length;
+ P.First := Source.First;
+ P.Last := Source.Last;
+
+ return P;
+ end Copy;
+
+ ------------
+ -- Delete --
+ ------------
+
+ procedure Delete (Container : in out List; Position : in out Cursor) is
+ begin
+ Delete
+ (Container => Container,
+ Position => Position,
+ Count => 1);
+ end Delete;
+
+ procedure Delete
+ (Container : in out List;
+ Position : in out Cursor;
+ Count : Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if not Has_Element (Container => Container,
+ Position => Position)
+ then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert (Vet (Container, Position), "bad cursor in Delete");
+ pragma Assert (Container.First >= 1);
+ pragma Assert (Container.Last >= 1);
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ if Position.Node = Container.First then
+ Delete_First (Container, Count);
+ Position := No_Element;
+ return;
+ end if;
+
+ if Count = 0 then
+ Position := No_Element;
+ return;
+ end if;
+
+ for Index in 1 .. Count loop
+ pragma Assert (Container.Length >= 2);
+
+ X := Position.Node;
+ Container.Length := Container.Length - 1;
+
+ if X = Container.Last then
+ Position := No_Element;
+
+ Container.Last := N (X).Prev;
+ N (Container.Last).Next := 0;
+
+ Free (Container, X);
+ return;
+ end if;
+
+ Position.Node := N (X).Next;
+ pragma Assert (N (Position.Node).Prev >= 0);
+
+ N (N (X).Next).Prev := N (X).Prev;
+ N (N (X).Prev).Next := N (X).Next;
+
+ Free (Container, X);
+ end loop;
+
+ Position := No_Element;
+ end Delete;
+
+ ------------------
+ -- Delete_First --
+ ------------------
+
+ procedure Delete_First (Container : in out List) is
+ begin
+ Delete_First
+ (Container => Container,
+ Count => 1);
+ end Delete_First;
+
+ procedure Delete_First (Container : in out List; Count : Count_Type) is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if Count >= Container.Length then
+ Clear (Container);
+ return;
+ end if;
+
+ if Count = 0 then
+ return;
+ end if;
+
+ for J in 1 .. Count loop
+ X := Container.First;
+ pragma Assert (N (N (X).Next).Prev = Container.First);
+
+ Container.First := N (X).Next;
+ N (Container.First).Prev := 0;
+
+ Container.Length := Container.Length - 1;
+
+ Free (Container, X);
+ end loop;
+ end Delete_First;
+
+ -----------------
+ -- Delete_Last --
+ -----------------
+
+ procedure Delete_Last (Container : in out List) is
+ begin
+ Delete_Last
+ (Container => Container,
+ Count => 1);
+ end Delete_Last;
+
+ procedure Delete_Last (Container : in out List; Count : Count_Type) is
+ N : Node_Array_Access renames Container.Nodes;
+ X : Count_Type;
+
+ begin
+ if Count >= Container.Length then
+ Clear (Container);
+ return;
+ end if;
+
+ if Count = 0 then
+ return;
+ end if;
+
+ for J in 1 .. Count loop
+ X := Container.Last;
+ pragma Assert (N (N (X).Prev).Next = Container.Last);
+
+ Container.Last := N (X).Prev;
+ N (Container.Last).Next := 0;
+
+ Container.Length := Container.Length - 1;
+
+ Free (Container, X);
+ end loop;
+ end Delete_Last;
+
+ -------------
+ -- Element --
+ -------------
+
+ function Element
+ (Container : List;
+ Position : Cursor) return 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.all;
+ end Element;
+
+ ----------------
+ -- Empty_List --
+ ----------------
+
+ function Empty_List return List is
+ ((Controlled with others => <>));
+
+ --------------
+ -- Finalize --
+ --------------
+
+ procedure Finalize (Container : in out List) is
+ X : Count_Type := Container.First;
+ N : Node_Array_Access renames Container.Nodes;
+ begin
+
+ if N = null then
+ return;
+ end if;
+
+ while X /= 0 loop
+ Finalize_Element (N (X).Element);
+ X := N (X).Next;
+ end loop;
+
+ Finalize_Nodes (N);
+
+ Container.Free := 0;
+ Container.Last := 0;
+ Container.First := 0;
+ Container.Length := 0;
+ end Finalize;
+
+ ----------
+ -- Find --
+ ----------
+
+ function Find
+ (Container : List;
+ Item : Element_Type;
+ Position : Cursor := No_Element) return Cursor
+ is
+ From : Count_Type := Position.Node;
+
+ begin
+ if From = 0 and Container.Length = 0 then
+ return No_Element;
+ end if;
+
+ if From = 0 then
+ From := Container.First;
+ end if;
+
+ if Position.Node /= 0 and then not Has_Element (Container, Position) then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ while From /= 0 loop
+ if Container.Nodes (From).Element.all = Item then
+ return (Node => From);
+ end if;
+
+ From := Container.Nodes (From).Next;
+ end loop;
+
+ return No_Element;
+ end Find;
+
+ -----------
+ -- First --
+ -----------
+
+ function First (Container : List) return Cursor is
+ begin
+ if Container.First = 0 then
+ return No_Element;
+ end if;
+
+ return (Node => Container.First);
+ end First;
+
+ -------------------
+ -- First_Element --
+ -------------------
+
+ function First_Element (Container : List) return Element_Type is
+ F : constant Count_Type := Container.First;
+ begin
+ if F = 0 then
+ raise Constraint_Error with "list is empty";
+ else
+ return Container.Nodes (F).Element.all;
+ end if;
+ end First_Element;
+
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ ----------------------------
+ -- Lift_Abstraction_Level --
+ ----------------------------
+
+ procedure Lift_Abstraction_Level (Container : List) is null;
+
+ -------------------------
+ -- M_Elements_In_Union --
+ -------------------------
+
+ function M_Elements_In_Union
+ (Container : M.Sequence;
+ Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ is
+ Elem : Element_Type;
+
+ begin
+ for Index in 1 .. M.Length (Container) loop
+ Elem := Element (Container, Index);
+
+ if not M.Contains (Left, 1, M.Length (Left), Elem)
+ and then not M.Contains (Right, 1, M.Length (Right), Elem)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end M_Elements_In_Union;
+
+ -------------------------
+ -- M_Elements_Included --
+ -------------------------
+
+ function M_Elements_Included
+ (Left : M.Sequence;
+ L_Fst : Positive_Count_Type := 1;
+ L_Lst : Count_Type;
+ Right : M.Sequence;
+ R_Fst : Positive_Count_Type := 1;
+ R_Lst : Count_Type) return Boolean
+ is
+ begin
+ for I in L_Fst .. L_Lst loop
+ declare
+ Found : Boolean := False;
+ J : Count_Type := R_Fst - 1;
+
+ begin
+ while not Found and J < R_Lst loop
+ J := J + 1;
+ if Element (Left, I) = Element (Right, J) then
+ Found := True;
+ end if;
+ end loop;
+
+ if not Found then
+ return False;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end M_Elements_Included;
+
+ -------------------------
+ -- M_Elements_Reversed --
+ -------------------------
+
+ function M_Elements_Reversed
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ is
+ L : constant Count_Type := M.Length (Left);
+
+ begin
+ if L /= M.Length (Right) then
+ return False;
+ end if;
+
+ for I in 1 .. L loop
+ if Element (Left, I) /= Element (Right, L - I + 1) then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end M_Elements_Reversed;
+
+ ------------------------
+ -- M_Elements_Swapped --
+ ------------------------
+
+ function M_Elements_Swapped
+ (Left : M.Sequence;
+ Right : M.Sequence;
+ X : Positive_Count_Type;
+ Y : Positive_Count_Type) return Boolean
+ is
+ begin
+ if M.Length (Left) /= M.Length (Right)
+ or else Element (Left, X) /= Element (Right, Y)
+ or else Element (Left, Y) /= Element (Right, X)
+ then
+ return False;
+ end if;
+
+ for I in 1 .. M.Length (Left) loop
+ if I /= X and then I /= Y
+ and then Element (Left, I) /= Element (Right, I)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end M_Elements_Swapped;
+
+ -----------
+ -- Model --
+ -----------
+
+ function Model (Container : List) return M.Sequence is
+ Position : Count_Type := Container.First;
+ R : M.Sequence;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := M.Add (R, Container.Nodes (Position).Element.all);
+ Position := Container.Nodes (Position).Next;
+ end loop;
+
+ return R;
+ end Model;
+
+ -----------------------
+ -- Mapping_Preserved --
+ -----------------------
+
+ function Mapping_Preserved
+ (M_Left : M.Sequence;
+ M_Right : M.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ is
+ begin
+ for C of P_Left loop
+ if not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > M.Length (M_Left)
+ or else P.Get (P_Right, C) > M.Length (M_Right)
+ or else M.Get (M_Left, P.Get (P_Left, C)) /=
+ M.Get (M_Right, P.Get (P_Right, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ for C of P_Right loop
+ if not P.Has_Key (P_Left, C) then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Mapping_Preserved;
+
+ -------------------------
+ -- P_Positions_Shifted --
+ -------------------------
+
+ function P_Positions_Shifted
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ is
+ begin
+ for Cu of Small loop
+ if not P.Has_Key (Big, Cu) then
+ return False;
+ end if;
+ end loop;
+
+ for Cu of Big loop
+ declare
+ Pos : constant Positive_Count_Type := P.Get (Big, Cu);
+
+ begin
+ if Pos < Cut then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu)
+ then
+ return False;
+ end if;
+
+ elsif Pos >= Cut + Count then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu) + Count
+ then
+ return False;
+ end if;
+
+ else
+ if P.Has_Key (Small, Cu) then
+ return False;
+ end if;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end P_Positions_Shifted;
+
+ -------------------------
+ -- P_Positions_Swapped --
+ -------------------------
+
+ function P_Positions_Swapped
+ (Left : P.Map;
+ Right : P.Map;
+ X : Cursor;
+ Y : Cursor) return Boolean
+ is
+ begin
+ if not P.Has_Key (Left, X)
+ or not P.Has_Key (Left, Y)
+ or not P.Has_Key (Right, X)
+ or not P.Has_Key (Right, Y)
+ then
+ return False;
+ end if;
+
+ if P.Get (Left, X) /= P.Get (Right, Y)
+ or P.Get (Left, Y) /= P.Get (Right, X)
+ then
+ return False;
+ end if;
+
+ for C of Left loop
+ if not P.Has_Key (Right, C) then
+ return False;
+ end if;
+ end loop;
+
+ for C of Right loop
+ if not P.Has_Key (Left, C)
+ or else (C /= X
+ and C /= Y
+ and P.Get (Left, C) /= P.Get (Right, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end P_Positions_Swapped;
+
+ ---------------------------
+ -- P_Positions_Truncated --
+ ---------------------------
+
+ function P_Positions_Truncated
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ is
+ begin
+ for Cu of Small loop
+ if not P.Has_Key (Big, Cu) then
+ return False;
+ end if;
+ end loop;
+
+ for Cu of Big loop
+ declare
+ Pos : constant Positive_Count_Type := P.Get (Big, Cu);
+
+ begin
+ if Pos < Cut then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu)
+ then
+ return False;
+ end if;
+
+ elsif Pos >= Cut + Count then
+ return False;
+
+ elsif P.Has_Key (Small, Cu) then
+ return False;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end P_Positions_Truncated;
+
+ ---------------
+ -- Positions --
+ ---------------
+
+ function Positions (Container : List) return P.Map is
+ I : Count_Type := 1;
+ Position : Count_Type := Container.First;
+ R : P.Map;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := P.Add (R, (Node => Position), I);
+ pragma Assert (P.Length (R) = To_Big_Integer (I));
+ Position := Container.Nodes (Position).Next;
+ I := I + 1;
+ end loop;
+
+ return R;
+ end Positions;
+
+ end Formal_Model;
+
+ ----------
+ -- Free --
+ ----------
+
+ procedure Free (Container : in out List; X : Count_Type) is
+ pragma Assert (X > 0);
+ pragma Assert (X <= Container.Nodes'Length);
+
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ N (X).Prev := -1; -- Node is deallocated (not on active list)
+
+ if N (X).Element /= null then
+ Finalize_Element (N (X).Element);
+ end if;
+
+ if Container.Free >= 0 then
+ N (X).Next := Container.Free;
+ Container.Free := X;
+ elsif X + 1 = abs Container.Free then
+ N (X).Next := 0; -- Not strictly necessary, but marginally safer
+ Container.Free := Container.Free + 1;
+ else
+ Container.Free := abs Container.Free;
+
+ for J in Container.Free .. Container.Nodes'Length loop
+ N (J).Next := J + 1;
+ end loop;
+
+ N (Container.Nodes'Length).Next := 0;
+
+ N (X).Next := Container.Free;
+ Container.Free := X;
+ end if;
+ end Free;
+
+ ---------------------
+ -- Generic_Sorting --
+ ---------------------
+
+ package body Generic_Sorting with SPARK_Mode => Off is
+
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -----------------------
+ -- M_Elements_Sorted --
+ -----------------------
+
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean is
+ begin
+ if M.Length (Container) = 0 then
+ return True;
+ end if;
+
+ declare
+ E1 : Element_Type := Element (Container, 1);
+
+ begin
+ for I in 2 .. M.Length (Container) loop
+ declare
+ E2 : constant Element_Type := Element (Container, I);
+
+ begin
+ if E2 < E1 then
+ return False;
+ end if;
+
+ E1 := E2;
+ end;
+ end loop;
+ end;
+
+ return True;
+ end M_Elements_Sorted;
+
+ end Formal_Model;
+
+ ---------------
+ -- Is_Sorted --
+ ---------------
+
+ function Is_Sorted (Container : List) return Boolean is
+ Nodes : Node_Array_Access renames Container.Nodes;
+ Node : Count_Type := Container.First;
+
+ begin
+ for J in 2 .. Container.Length loop
+ if Nodes (Nodes (Node).Next).Element.all < Nodes (Node).Element.all
+ then
+ return False;
+ else
+ Node := Nodes (Node).Next;
+ end if;
+ end loop;
+
+ return True;
+ end Is_Sorted;
+
+ -----------
+ -- Merge --
+ -----------
+
+ procedure Merge (Target : in out List; Source : in out List) is
+ LN : Node_Array_Access renames Target.Nodes;
+ RN : Node_Array_Access renames Source.Nodes;
+ LI : Cursor;
+ RI : Cursor;
+
+ begin
+ if Target'Address = Source'Address then
+ raise Program_Error with "Target and Source denote same container";
+ end if;
+
+ LI := First (Target);
+ RI := First (Source);
+ while RI.Node /= 0 loop
+ pragma Assert
+ (RN (RI.Node).Next = 0
+ or else not (RN (RN (RI.Node).Next).Element.all <
+ RN (RI.Node).Element.all));
+
+ if LI.Node = 0 then
+ Splice (Target, No_Element, Source);
+ return;
+ end if;
+
+ pragma Assert
+ (LN (LI.Node).Next = 0
+ or else not (LN (LN (LI.Node).Next).Element.all <
+ LN (LI.Node).Element.all));
+
+ if RN (RI.Node).Element.all < LN (LI.Node).Element.all then
+ declare
+ RJ : Cursor := RI;
+ pragma Warnings (Off, RJ);
+ begin
+ RI.Node := RN (RI.Node).Next;
+ Splice (Target, LI, Source, RJ);
+ end;
+
+ else
+ LI.Node := LN (LI.Node).Next;
+ end if;
+ end loop;
+ end Merge;
+
+ ----------
+ -- Sort --
+ ----------
+
+ procedure Sort (Container : in out List) is
+ N : Node_Array_Access renames Container.Nodes;
+ begin
+ if Container.Length <= 1 then
+ return;
+ end if;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ declare
+ package Descriptors is new List_Descriptors
+ (Node_Ref => Count_Type, Nil => 0);
+ use Descriptors;
+
+ function Next (Idx : Count_Type) return Count_Type is
+ (N (Idx).Next);
+ procedure Set_Next (Idx : Count_Type; Next : Count_Type)
+ with Inline;
+ procedure Set_Prev (Idx : Count_Type; Prev : Count_Type)
+ with Inline;
+ function "<" (L, R : Count_Type) return Boolean is
+ (N (L).Element.all < N (R).Element.all);
+ procedure Update_Container (List : List_Descriptor) with Inline;
+
+ procedure Set_Next (Idx : Count_Type; Next : Count_Type) is
+ begin
+ N (Idx).Next := Next;
+ end Set_Next;
+
+ procedure Set_Prev (Idx : Count_Type; Prev : Count_Type) is
+ begin
+ N (Idx).Prev := Prev;
+ end Set_Prev;
+
+ procedure Update_Container (List : List_Descriptor) is
+ begin
+ Container.First := List.First;
+ Container.Last := List.Last;
+ Container.Length := List.Length;
+ end Update_Container;
+
+ procedure Sort_List is new Doubly_Linked_List_Sort;
+ begin
+ Sort_List (List_Descriptor'(First => Container.First,
+ Last => Container.Last,
+ Length => Container.Length));
+ end;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+ end Sort;
+
+ end Generic_Sorting;
+
+ -----------------
+ -- Has_Element --
+ -----------------
+
+ function Has_Element (Container : List; Position : Cursor) return Boolean is
+ begin
+ if Position.Node = 0 then
+ return False;
+ end if;
+
+ return Container.Nodes (Position.Node).Prev /= -1;
+ end Has_Element;
+
+ ------------
+ -- Insert --
+ ------------
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Position : out Cursor;
+ Count : Count_Type)
+ is
+ J : Count_Type;
+
+ begin
+ if Before.Node /= 0 then
+ pragma Assert (Vet (Container, Before), "bad cursor in Insert");
+ end if;
+
+ if Count = 0 then
+ Position := Before;
+ return;
+ end if;
+ Allocate (Container, New_Item, New_Node => J);
+ Insert_Internal (Container, Before.Node, New_Node => J);
+ Position := (Node => J);
+
+ for Index in 2 .. Count loop
+ Allocate (Container, New_Item, New_Node => J);
+ Insert_Internal (Container, Before.Node, New_Node => J);
+ end loop;
+ end Insert;
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Position : out Cursor)
+ is
+ begin
+ Insert
+ (Container => Container,
+ Before => Before,
+ New_Item => New_Item,
+ Position => Position,
+ Count => 1);
+ end Insert;
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ is
+ Position : Cursor;
+
+ begin
+ Insert (Container, Before, New_Item, Position, Count);
+ end Insert;
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type)
+ is
+ Position : Cursor;
+
+ begin
+ Insert (Container, Before, New_Item, Position, 1);
+ end Insert;
+
+ ---------------------
+ -- Insert_Internal --
+ ---------------------
+
+ procedure Insert_Internal
+ (Container : in out List;
+ Before : Count_Type;
+ New_Node : Count_Type)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ if Container.Length = 0 then
+ pragma Assert (Before = 0);
+ pragma Assert (Container.First = 0);
+ pragma Assert (Container.Last = 0);
+
+ Container.First := New_Node;
+ Container.Last := New_Node;
+
+ N (Container.First).Prev := 0;
+ N (Container.Last).Next := 0;
+
+ elsif Before = 0 then
+ pragma Assert (N (Container.Last).Next = 0);
+
+ N (Container.Last).Next := New_Node;
+ N (New_Node).Prev := Container.Last;
+
+ Container.Last := New_Node;
+ N (Container.Last).Next := 0;
+
+ elsif Before = Container.First then
+ pragma Assert (N (Container.First).Prev = 0);
+
+ N (Container.First).Prev := New_Node;
+ N (New_Node).Next := Container.First;
+
+ Container.First := New_Node;
+ N (Container.First).Prev := 0;
+
+ else
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ N (New_Node).Next := Before;
+ N (New_Node).Prev := N (Before).Prev;
+
+ N (N (Before).Prev).Next := New_Node;
+ N (Before).Prev := New_Node;
+ end if;
+ Container.Length := Container.Length + 1;
+ end Insert_Internal;
+
+ --------------
+ -- Is_Empty --
+ --------------
+
+ function Is_Empty (Container : List) return Boolean is
+ begin
+ return Length (Container) = 0;
+ end Is_Empty;
+
+ ----------
+ -- Last --
+ ----------
+
+ function Last (Container : List) return Cursor is
+ begin
+ if Container.Last = 0 then
+ return No_Element;
+ end if;
+
+ return (Node => Container.Last);
+ end Last;
+
+ ------------------
+ -- Last_Element --
+ ------------------
+
+ function Last_Element (Container : List) return Element_Type is
+ L : constant Count_Type := Container.Last;
+
+ begin
+ if L = 0 then
+ raise Constraint_Error with "list is empty";
+ else
+ return Container.Nodes (L).Element.all;
+ end if;
+ end Last_Element;
+
+ ------------
+ -- Length --
+ ------------
+
+ function Length (Container : List) return Count_Type is
+ begin
+ return Container.Length;
+ end Length;
+
+ ----------
+ -- Move --
+ ----------
+
+ procedure Move (Target : in out List; Source : in out List) is
+ N : Node_Array_Access renames Source.Nodes;
+
+ procedure Finalize_Node_Array is new Ada.Unchecked_Deallocation
+ (Object => Node_Array,
+ Name => Node_Array_Access);
+
+ begin
+ if Target'Address = Source'Address then
+ return;
+ end if;
+
+ Clear (Target);
+
+ if Source.Length = 0 then
+ return;
+ end if;
+
+ -- Make sure that Target is large enough
+
+ if Target.Nodes = null
+ or else Target.Nodes'Length < Source.Length
+ then
+ if Target.Nodes /= null then
+ Finalize_Node_Array (Target.Nodes);
+ end if;
+ Target.Nodes := new Node_Array (1 .. Source.Length);
+ end if;
+
+ -- Copy first element from Source to Target
+
+ Target.First := 1;
+
+ Target.Nodes (1).Prev := 0;
+ Target.Nodes (1).Element := N (Source.First).Element;
+ N (Source.First).Element := null;
+
+ -- Copy the other elements
+
+ declare
+ X_Src : Count_Type := N (Source.First).Next;
+ X_Tar : Count_Type := 2;
+
+ begin
+ while X_Src /= 0 loop
+ Target.Nodes (X_Tar).Prev := X_Tar - 1;
+ Target.Nodes (X_Tar - 1).Next := X_Tar;
+
+ Target.Nodes (X_Tar).Element := N (X_Src).Element;
+ N (X_Src).Element := null;
+
+ X_Src := N (X_Src).Next;
+ X_Tar := X_Tar + 1;
+ end loop;
+ end;
+
+ Target.Last := Source.Length;
+ Target.Length := Source.Length;
+ Target.Nodes (Target.Last).Next := 0;
+
+ -- Set up the free list
+
+ Target.Free := -Source.Length - 1;
+
+ -- It is possible to Clear Source because the Element accesses were
+ -- set to null.
+
+ Clear (Source);
+ end Move;
+
+ ----------
+ -- Next --
+ ----------
+
+ procedure Next (Container : List; Position : in out Cursor) is
+ begin
+ Position := Next (Container, Position);
+ end Next;
+
+ function Next (Container : List; Position : Cursor) return Cursor is
+ begin
+ if Position.Node = 0 then
+ return No_Element;
+ end if;
+
+ if not Has_Element (Container, Position) then
+ raise Program_Error with "Position cursor has no element";
+ end if;
+
+ return (Node => Container.Nodes (Position.Node).Next);
+ end Next;
+
+ -------------
+ -- Prepend --
+ -------------
+
+ procedure Prepend (Container : in out List; New_Item : Element_Type) is
+ begin
+ Insert (Container, First (Container), New_Item, 1);
+ end Prepend;
+
+ procedure Prepend
+ (Container : in out List;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ is
+ begin
+ Insert (Container, First (Container), New_Item, Count);
+ end Prepend;
+
+ --------------
+ -- Previous --
+ --------------
+
+ procedure Previous (Container : List; Position : in out Cursor) is
+ begin
+ Position := Previous (Container, Position);
+ end Previous;
+
+ function Previous (Container : List; Position : Cursor) return Cursor is
+ begin
+ if Position.Node = 0 then
+ return No_Element;
+ end if;
+
+ if not Has_Element (Container, Position) then
+ raise Program_Error with "Position cursor has no element";
+ end if;
+
+ 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;
+ end Reference;
+
+ ---------------------
+ -- Replace_Element --
+ ---------------------
+
+ procedure Replace_Element
+ (Container : in out List;
+ Position : Cursor;
+ New_Item : 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 Replace_Element");
+
+ Finalize_Element (Container.Nodes (Position.Node).Element);
+ Container.Nodes (Position.Node).Element := new Element_Type'(New_Item);
+ end Replace_Element;
+
+ ------------
+ -- Resize --
+ ------------
+
+ procedure Resize (Container : in out List) is
+ Min_Size : constant Count_Type := 100;
+ begin
+ if Container.Nodes = null then
+ Container.Nodes := new Node_Array (1 .. Min_Size);
+ Container.First := 0;
+ Container.Last := 0;
+ Container.Length := 0;
+ Container.Free := -1;
+
+ return;
+ end if;
+
+ if Container.Length /= Container.Nodes'Length then
+ raise Program_Error with "List must be at size max to resize";
+ end if;
+
+ declare
+ procedure Finalize_Node_Array is new Ada.Unchecked_Deallocation
+ (Object => Node_Array,
+ Name => Node_Array_Access);
+
+ New_Size : constant Count_Type :=
+ (if Container.Nodes'Length > Count_Type'Last / 2
+ then Count_Type'Last
+ else 2 * Container.Nodes'Length);
+ New_Nodes : Node_Array_Access;
+
+ begin
+ New_Nodes :=
+ new Node_Array (1 .. Count_Type'Max (New_Size, Min_Size));
+
+ New_Nodes (1 .. Container.Nodes'Length) :=
+ Container.Nodes (1 .. Container.Nodes'Length);
+
+ Container.Free := -Container.Nodes'Length - 1;
+
+ Finalize_Node_Array (Container.Nodes);
+ Container.Nodes := New_Nodes;
+ end;
+ end Resize;
+
+ ----------------------
+ -- Reverse_Elements --
+ ----------------------
+
+ procedure Reverse_Elements (Container : in out List) is
+ N : Node_Array_Access renames Container.Nodes;
+ I : Count_Type := Container.First;
+ J : Count_Type := Container.Last;
+
+ procedure Swap (L : Count_Type; R : Count_Type);
+
+ ----------
+ -- Swap --
+ ----------
+
+ procedure Swap (L : Count_Type; R : Count_Type) is
+ LN : constant Count_Type := N (L).Next;
+ LP : constant Count_Type := N (L).Prev;
+
+ RN : constant Count_Type := N (R).Next;
+ RP : constant Count_Type := N (R).Prev;
+
+ begin
+ if LP /= 0 then
+ N (LP).Next := R;
+ end if;
+
+ if RN /= 0 then
+ N (RN).Prev := L;
+ end if;
+
+ N (L).Next := RN;
+ N (R).Prev := LP;
+
+ if LN = R then
+ pragma Assert (RP = L);
+
+ N (L).Prev := R;
+ N (R).Next := L;
+
+ else
+ N (L).Prev := RP;
+ N (RP).Next := L;
+
+ N (R).Next := LN;
+ N (LN).Prev := R;
+ end if;
+ end Swap;
+
+ -- Start of processing for Reverse_Elements
+
+ begin
+ if Container.Length <= 1 then
+ return;
+ end if;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+
+ Container.First := J;
+ Container.Last := I;
+ loop
+ Swap (L => I, R => J);
+
+ J := N (J).Next;
+ exit when I = J;
+
+ I := N (I).Prev;
+ exit when I = J;
+
+ Swap (L => J, R => I);
+
+ I := N (I).Next;
+ exit when I = J;
+
+ J := N (J).Prev;
+ exit when I = J;
+ end loop;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+ end Reverse_Elements;
+
+ ------------------
+ -- Reverse_Find --
+ ------------------
+
+ function Reverse_Find
+ (Container : List;
+ Item : Element_Type;
+ Position : Cursor := No_Element) return Cursor
+ is
+ CFirst : Count_Type := Position.Node;
+
+ begin
+ if CFirst = 0 then
+ CFirst := Container.Last;
+ end if;
+
+ if Container.Length = 0 then
+ return No_Element;
+ else
+ while CFirst /= 0 loop
+ if Container.Nodes (CFirst).Element.all = Item then
+ return (Node => CFirst);
+ else
+ CFirst := Container.Nodes (CFirst).Prev;
+ end if;
+ end loop;
+
+ return No_Element;
+ end if;
+ end Reverse_Find;
+
+ ------------
+ -- Splice --
+ ------------
+
+ procedure Splice
+ (Target : in out List;
+ Before : Cursor;
+ Source : in out List)
+ is
+ SN : Node_Array_Access renames Source.Nodes;
+ TN : Node_Array_Access renames Target.Nodes;
+
+ begin
+ if Target'Address = Source'Address then
+ raise Program_Error with "Target and Source denote same container";
+ end if;
+
+ if Before.Node /= 0 then
+ pragma Assert (Vet (Target, Before), "bad cursor in Splice");
+ end if;
+
+ if Is_Empty (Source) then
+ return;
+ end if;
+
+ pragma Assert (SN (Source.First).Prev = 0);
+ pragma Assert (SN (Source.Last).Next = 0);
+
+ declare
+ X : Count_Type;
+
+ begin
+ while not Is_Empty (Source) loop
+ Allocate (Target, X);
+
+ TN (X).Element := SN (Source.Last).Element;
+
+ -- Insert the new node in Target
+
+ Insert_Internal (Target, Before.Node, X);
+
+ -- Free the last node of Source
+
+ SN (Source.Last).Element := null;
+ Delete_Last (Source);
+ end loop;
+ end;
+
+ end Splice;
+
+ procedure Splice
+ (Target : in out List;
+ Before : Cursor;
+ Source : in out List;
+ Position : in out Cursor)
+ is
+ begin
+ if Target'Address = Source'Address then
+ raise Program_Error with "Target and Source denote same container";
+ end if;
+
+ if Position.Node = 0 then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert (Vet (Source, Position), "bad Position cursor in Splice");
+
+ declare
+ X : Count_Type;
+
+ begin
+ Allocate (Target, X);
+
+ Target.Nodes (X).Element := Source.Nodes (Position.Node).Element;
+
+ -- Insert the new node in Target
+
+ Insert_Internal (Target, Before.Node, X);
+
+ -- Free the node at position Position in Source
+
+ Source.Nodes (Position.Node).Element := null;
+ Delete (Source, Position);
+
+ Position := (Node => X);
+ end;
+ end Splice;
+
+ procedure Splice
+ (Container : in out List;
+ Before : Cursor;
+ Position : Cursor)
+ is
+ N : Node_Array_Access renames Container.Nodes;
+
+ begin
+ if Before.Node /= 0 then
+ pragma Assert
+ (Vet (Container, Before), "bad Before cursor in Splice");
+ end if;
+
+ if Position.Node = 0 then
+ raise Constraint_Error with "Position cursor has no element";
+ end if;
+
+ pragma Assert
+ (Vet (Container, Position), "bad Position cursor in Splice");
+
+ if Position.Node = Before.Node
+ or else N (Position.Node).Next = Before.Node
+ then
+ return;
+ end if;
+
+ pragma Assert (Container.Length >= 2);
+
+ if Before.Node = 0 then
+ pragma Assert (Position.Node /= Container.Last);
+
+ if Position.Node = Container.First then
+ Container.First := N (Position.Node).Next;
+ N (Container.First).Prev := 0;
+
+ else
+ N (N (Position.Node).Prev).Next := N (Position.Node).Next;
+ N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
+ end if;
+
+ N (Container.Last).Next := Position.Node;
+ N (Position.Node).Prev := Container.Last;
+
+ Container.Last := Position.Node;
+ N (Container.Last).Next := 0;
+
+ return;
+ end if;
+
+ if Before.Node = Container.First then
+ pragma Assert (Position.Node /= Container.First);
+
+ if Position.Node = Container.Last then
+ Container.Last := N (Position.Node).Prev;
+ N (Container.Last).Next := 0;
+
+ else
+ N (N (Position.Node).Prev).Next := N (Position.Node).Next;
+ N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
+ end if;
+
+ N (Container.First).Prev := Position.Node;
+ N (Position.Node).Next := Container.First;
+
+ Container.First := Position.Node;
+ N (Container.First).Prev := 0;
+
+ return;
+ end if;
+
+ if Position.Node = Container.First then
+ Container.First := N (Position.Node).Next;
+ N (Container.First).Prev := 0;
+
+ elsif Position.Node = Container.Last then
+ Container.Last := N (Position.Node).Prev;
+ N (Container.Last).Next := 0;
+
+ else
+ N (N (Position.Node).Prev).Next := N (Position.Node).Next;
+ N (N (Position.Node).Next).Prev := N (Position.Node).Prev;
+ end if;
+
+ N (N (Before.Node).Prev).Next := Position.Node;
+ N (Position.Node).Prev := N (Before.Node).Prev;
+
+ N (Before.Node).Prev := Position.Node;
+ N (Position.Node).Next := Before.Node;
+
+ pragma Assert (N (Container.First).Prev = 0);
+ pragma Assert (N (Container.Last).Next = 0);
+ end Splice;
+
+ ----------
+ -- Swap --
+ ----------
+
+ procedure Swap
+ (Container : in out List;
+ I : Cursor;
+ J : Cursor)
+ is
+ begin
+ if I.Node = 0 then
+ raise Constraint_Error with "I cursor has no element";
+ end if;
+
+ if J.Node = 0 then
+ raise Constraint_Error with "J cursor has no element";
+ end if;
+
+ if I.Node = J.Node then
+ return;
+ end if;
+
+ pragma Assert (Vet (Container, I), "bad I cursor in Swap");
+ pragma Assert (Vet (Container, J), "bad J cursor in Swap");
+
+ declare
+ NN : Node_Array_Access renames Container.Nodes;
+ NI : Node_Type renames NN (I.Node);
+ NJ : Node_Type renames NN (J.Node);
+
+ EI_Copy : constant Element_Access := NI.Element;
+
+ begin
+ NI.Element := NJ.Element;
+ NJ.Element := EI_Copy;
+ end;
+ end Swap;
+
+ ----------------
+ -- Swap_Links --
+ ----------------
+
+ procedure Swap_Links
+ (Container : in out List;
+ I : Cursor;
+ J : Cursor)
+ is
+ I_Next : Cursor;
+ J_Next : Cursor;
+
+ begin
+ if I.Node = 0 then
+ raise Constraint_Error with "I cursor has no element";
+ end if;
+
+ if J.Node = 0 then
+ raise Constraint_Error with "J cursor has no element";
+ end if;
+
+ if I.Node = J.Node then
+ return;
+ end if;
+
+ pragma Assert (Vet (Container, I), "bad I cursor in Swap_Links");
+ pragma Assert (Vet (Container, J), "bad J cursor in Swap_Links");
+
+ I_Next := Next (Container, I);
+
+ if I_Next = J then
+ Splice (Container, Before => I, Position => J);
+
+ else
+ J_Next := Next (Container, J);
+
+ if J_Next = I then
+ Splice (Container, Before => J, Position => I);
+
+ else
+ pragma Assert (Container.Length >= 3);
+ Splice (Container, Before => I_Next, Position => J);
+ Splice (Container, Before => J_Next, Position => I);
+ end if;
+ end if;
+ end Swap_Links;
+
+ ---------
+ -- Vet --
+ ---------
+
+ function Vet (L : List; Position : Cursor) return Boolean is
+ N : Node_Array_Access renames L.Nodes;
+ begin
+ if not Container_Checks'Enabled then
+ return True;
+ end if;
+
+ if L.Length = 0 then
+ return False;
+ end if;
+
+ if L.First = 0 then
+ return False;
+ end if;
+
+ if L.Last = 0 then
+ return False;
+ end if;
+
+ if Position.Node > L.Nodes'Length then
+ return False;
+ end if;
+
+ if N (Position.Node).Prev < 0
+ or else N (Position.Node).Prev > L.Nodes'Length
+ then
+ return False;
+ end if;
+
+ if N (Position.Node).Next > L.Nodes'Length then
+ return False;
+ end if;
+
+ if N (L.First).Prev /= 0 then
+ return False;
+ end if;
+
+ if N (L.Last).Next /= 0 then
+ return False;
+ end if;
+
+ if N (Position.Node).Prev = 0 and then Position.Node /= L.First then
+ return False;
+ end if;
+
+ if N (Position.Node).Next = 0 and then Position.Node /= L.Last then
+ return False;
+ end if;
+
+ if L.Length = 1 then
+ return L.First = L.Last;
+ end if;
+
+ if L.First = L.Last then
+ return False;
+ end if;
+
+ if N (L.First).Next = 0 then
+ return False;
+ end if;
+
+ if N (L.Last).Prev = 0 then
+ return False;
+ end if;
+
+ if N (N (L.First).Next).Prev /= L.First then
+ return False;
+ end if;
+
+ if N (N (L.Last).Prev).Next /= L.Last then
+ return False;
+ end if;
+
+ if L.Length = 2 then
+ if N (L.First).Next /= L.Last then
+ return False;
+ end if;
+
+ if N (L.Last).Prev /= L.First then
+ return False;
+ end if;
+
+ return True;
+ end if;
+
+ if N (L.First).Next = L.Last then
+ return False;
+ end if;
+
+ if N (L.Last).Prev = L.First then
+ return False;
+ end if;
+
+ if Position.Node = L.First then
+ return True;
+ end if;
+
+ if Position.Node = L.Last then
+ return True;
+ end if;
+
+ if N (Position.Node).Next = 0 then
+ return False;
+ end if;
+
+ if N (Position.Node).Prev = 0 then
+ return False;
+ end if;
+
+ if N (N (Position.Node).Next).Prev /= Position.Node then
+ return False;
+ end if;
+
+ if N (N (Position.Node).Prev).Next /= Position.Node then
+ return False;
+ end if;
+
+ if L.Length = 3 then
+ if N (L.First).Next /= Position.Node then
+ return False;
+ end if;
+
+ if N (L.Last).Prev /= Position.Node then
+ return False;
+ end if;
+ end if;
+
+ return True;
+ end Vet;
+
+end Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists;
diff --git a/gcc/ada/libgnat/a-cfidll.ads b/gcc/ada/libgnat/a-cfidll.ads
new file mode 100644
index 00000000000..c4d244a30b0
--- /dev/null
+++ b/gcc/ada/libgnat/a-cfidll.ads
@@ -0,0 +1,1670 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT LIBRARY COMPONENTS --
+-- --
+-- ADA.CONTAINERS.FORMAL_INDEFINITE_DOUBLY_LINKED_LISTS --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2022-2022, Free Software Foundation, Inc. --
+-- --
+-- This specification is derived from the Ada Reference Manual for use with --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the contents of the part following the private keyword. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+------------------------------------------------------------------------------
+
+with Ada.Containers.Functional_Vectors;
+with Ada.Containers.Functional_Maps;
+private with Ada.Finalization;
+
+generic
+ type Element_Type is private;
+ with function "=" (Left, Right : Element_Type) return Boolean is <>;
+
+package Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists with
+ SPARK_Mode
+is
+ -- Contracts in this unit are meant for analysis only, not for run-time
+ -- checking.
+
+ pragma Assertion_Policy (Pre => Ignore);
+ pragma Assertion_Policy (Post => Ignore);
+ pragma Assertion_Policy (Contract_Cases => Ignore);
+ pragma Annotate (CodePeer, Skip_Analysis);
+
+ type List is private with
+ Iterable => (First => First,
+ Next => Next,
+ Has_Element => Has_Element,
+ Element => Element),
+ Default_Initial_Condition => Is_Empty (List);
+
+ type Cursor is record
+ Node : Count_Type := 0;
+ end record;
+
+ No_Element : constant Cursor := Cursor'(Node => 0);
+
+ function Length (Container : List) return Count_Type with
+ Global => null;
+
+ function Empty_List return List with
+ Global => null,
+ Post => Length (Empty_List'Result) = 0;
+
+ pragma Unevaluated_Use_Of_Old (Allow);
+
+ package Formal_Model with Ghost is
+ subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+ package M is new Ada.Containers.Functional_Vectors
+ (Index_Type => Positive_Count_Type,
+ Element_Type => Element_Type);
+
+ function "="
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean renames M."=";
+
+ function "<"
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean renames M."<";
+
+ function "<="
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean renames M."<=";
+
+ function M_Elements_In_Union
+ (Container : M.Sequence;
+ Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ -- The elements of Container are contained in either Left or Right
+ with
+ Global => null,
+ Post =>
+ M_Elements_In_Union'Result =
+ (for all I in 1 .. M.Length (Container) =>
+ (for some J in 1 .. M.Length (Left) =>
+ Element (Container, I) = Element (Left, J))
+ or (for some J in 1 .. M.Length (Right) =>
+ Element (Container, I) = Element (Right, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
+
+ function M_Elements_Included
+ (Left : M.Sequence;
+ L_Fst : Positive_Count_Type := 1;
+ L_Lst : Count_Type;
+ Right : M.Sequence;
+ R_Fst : Positive_Count_Type := 1;
+ R_Lst : Count_Type) return Boolean
+ -- The elements of the slice from L_Fst to L_Lst in Left are contained
+ -- in the slide from R_Fst to R_Lst in Right.
+ with
+ Global => null,
+ Pre => L_Lst <= M.Length (Left) and R_Lst <= M.Length (Right),
+ Post =>
+ M_Elements_Included'Result =
+ (for all I in L_Fst .. L_Lst =>
+ (for some J in R_Fst .. R_Lst =>
+ Element (Left, I) = Element (Right, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
+
+ function M_Elements_Reversed
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ -- Right is Left in reverse order
+ with
+ Global => null,
+ Post =>
+ M_Elements_Reversed'Result =
+ (M.Length (Left) = M.Length (Right)
+ and (for all I in 1 .. M.Length (Left) =>
+ Element (Left, I) =
+ Element (Right, M.Length (Left) - I + 1))
+ and (for all I in 1 .. M.Length (Left) =>
+ Element (Right, I) =
+ Element (Left, M.Length (Left) - I + 1)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
+
+ function M_Elements_Swapped
+ (Left : M.Sequence;
+ Right : M.Sequence;
+ X : Positive_Count_Type;
+ Y : Positive_Count_Type) return Boolean
+ -- Elements stored at X and Y are reversed in Left and Right
+ with
+ Global => null,
+ Pre => X <= M.Length (Left) and Y <= M.Length (Left),
+ Post =>
+ M_Elements_Swapped'Result =
+ (M.Length (Left) = M.Length (Right)
+ and Element (Left, X) = Element (Right, Y)
+ and Element (Left, Y) = Element (Right, X)
+ and M.Equal_Except (Left, Right, X, Y));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
+
+ package P is new Ada.Containers.Functional_Maps
+ (Key_Type => Cursor,
+ Element_Type => Positive_Count_Type,
+ Equivalent_Keys => "=",
+ Enable_Handling_Of_Equivalence => False);
+
+ function "="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."=";
+
+ function "<="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."<=";
+
+ function P_Positions_Shifted
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ with
+ Global => null,
+ Post =>
+ P_Positions_Shifted'Result =
+
+ -- Big contains all cursors of Small
+
+ (P.Keys_Included (Small, Big)
+
+ -- Cursors located before Cut are not moved, cursors located
+ -- after are shifted by Count.
+
+ and (for all I of Small =>
+ (if P.Get (Small, I) < Cut then
+ P.Get (Big, I) = P.Get (Small, I)
+ else
+ P.Get (Big, I) - Count = P.Get (Small, I)))
+
+ -- New cursors of Big (if any) are between Cut and Cut - 1 +
+ -- Count.
+
+ and (for all I of Big =>
+ P.Has_Key (Small, I)
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
+
+ function P_Positions_Swapped
+ (Left : P.Map;
+ Right : P.Map;
+ X : Cursor;
+ Y : Cursor) return Boolean
+ -- Left and Right contain the same cursors, but the positions of X and Y
+ -- are reversed.
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ P_Positions_Swapped'Result =
+ (P.Same_Keys (Left, Right)
+ and P.Elements_Equal_Except (Left, Right, X, Y)
+ and P.Has_Key (Left, X)
+ and P.Has_Key (Left, Y)
+ and P.Get (Left, X) = P.Get (Right, Y)
+ and P.Get (Left, Y) = P.Get (Right, X));
+
+ function P_Positions_Truncated
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ P_Positions_Truncated'Result =
+
+ -- Big contains all cursors of Small at the same position
+
+ (Small <= Big
+
+ -- New cursors of Big (if any) are between Cut and Cut - 1 +
+ -- Count.
+
+ and (for all I of Big =>
+ P.Has_Key (Small, I)
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
+
+ function Mapping_Preserved
+ (M_Left : M.Sequence;
+ M_Right : M.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ (if Mapping_Preserved'Result then
+
+ -- Left and Right contain the same cursors
+
+ P.Same_Keys (P_Left, P_Right)
+
+ -- Mappings from cursors to elements induced by M_Left, P_Left
+ -- and M_Right, P_Right are the same.
+
+ and (for all C of P_Left =>
+ M.Get (M_Left, P.Get (P_Left, C)) =
+ M.Get (M_Right, P.Get (P_Right, C))));
+
+ function Model (Container : List) return M.Sequence with
+ -- The high-level model of a list is a sequence of elements. Cursors are
+ -- not represented in this model.
+
+ Ghost,
+ Global => null,
+ Post => M.Length (Model'Result) = Length (Container);
+ pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Model);
+
+ function Positions (Container : List) return P.Map with
+ -- The Positions map is used to model cursors. It only contains valid
+ -- cursors and map them to their position in the container.
+
+ Ghost,
+ Global => null,
+ Post =>
+ not P.Has_Key (Positions'Result, No_Element)
+
+ -- Positions of cursors are smaller than the container's length
+
+ and then
+ (for all I of Positions'Result =>
+ P.Get (Positions'Result, I) in 1 .. Length (Container)
+
+ -- No two cursors have the same position. Note that we do not
+ -- state that there is a cursor in the map for each position, as
+ -- it is rarely needed.
+
+ and then
+ (for all J of Positions'Result =>
+ (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
+ then I = J)));
+
+ procedure Lift_Abstraction_Level (Container : List) with
+ -- Lift_Abstraction_Level is a ghost procedure that does nothing but
+ -- assume that we can access to the same elements by iterating over
+ -- positions or cursors.
+ -- This information is not generally useful except when switching from
+ -- a low-level cursor-aware view of a container to a high-level
+ -- position-based view.
+
+ Ghost,
+ Global => null,
+ Post =>
+ (for all Elt of Model (Container) =>
+ (for some I of Positions (Container) =>
+ M.Get (Model (Container), P.Get (Positions (Container), I)) =
+ Elt));
+
+ function Element
+ (S : M.Sequence;
+ I : Count_Type) return Element_Type renames M.Get;
+ -- To improve readability of contracts, we rename the function used to
+ -- access an element in the model to Element.
+
+ end Formal_Model;
+ use Formal_Model;
+
+ function "=" (Left, Right : List) return Boolean with
+ Global => null,
+ Post => "="'Result = (Model (Left) = Model (Right));
+
+ function Is_Empty (Container : List) return Boolean with
+ Global => null,
+ Post => Is_Empty'Result = (Length (Container) = 0);
+
+ procedure Clear (Container : in out List) with
+ Global => null,
+ Post => Length (Container) = 0;
+
+ procedure Assign (Target : in out List; Source : List) with
+ Global => null,
+ Post => Model (Target) = Model (Source);
+
+ function Copy (Source : List) return List with
+ Global => null,
+ Post =>
+ Model (Copy'Result) = Model (Source)
+ and Positions (Copy'Result) = Positions (Source);
+
+ function Element
+ (Container : List;
+ Position : Cursor) return Element_Type
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Element'Result =
+ Element (Model (Container), P.Get (Positions (Container), Position));
+ pragma Annotate (GNATprove, Inline_For_Proof, Element);
+
+ procedure Replace_Element
+ (Container : in out List;
+ Position : Cursor;
+ New_Item : Element_Type)
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Length (Container) = Length (Container)'Old
+
+ -- Cursors are preserved
+
+ and Positions (Container)'Old = Positions (Container)
+
+ -- The element at the position of Position in Container is New_Item
+
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container), Position)) = New_Item
+
+ -- Other elements are preserved
+
+ and M.Equal_Except
+ (Model (Container)'Old,
+ 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 : 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,
+ Post => Model (Target) = Model (Source'Old) and Length (Source) = 0;
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type)
+ with
+ Global => null,
+ Pre =>
+ Length (Container) < Count_Type'Last
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
+ Post => Length (Container) = Length (Container)'Old + 1,
+ Contract_Cases =>
+ (Before = No_Element =>
+
+ -- Positions contains a new mapping from the last cursor of
+ -- Container to its length.
+
+ P.Get (Positions (Container), Last (Container)) = Length (Container)
+
+ -- Other cursors come from Container'Old
+
+ and P.Keys_Included_Except
+ (Left => Positions (Container),
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container))
+
+ -- Cursors of Container'Old keep the same position
+
+ and Positions (Container)'Old <= Positions (Container)
+
+ -- Model contains a new element New_Item at the end
+
+ and Element (Model (Container), Length (Container)) = New_Item
+
+ -- Elements of Container'Old are preserved
+
+ and Model (Container)'Old <= Model (Container),
+
+ others =>
+
+ -- The elements of Container located before Before are preserved
+
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1)
+
+ -- Other elements are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst => Length (Container)'Old,
+ Offset => 1)
+
+ -- New_Item is stored at the previous position of Before in
+ -- Container.
+
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container)'Old, Before)) = New_Item
+
+ -- A new cursor has been inserted at position Before in Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container)'Old, Before)));
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ with
+ Global => null,
+ Pre =>
+ Length (Container) <= Count_Type'Last - Count
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
+ Post => Length (Container) = Length (Container)'Old + Count,
+ Contract_Cases =>
+ (Before = No_Element =>
+
+ -- The elements of Container are preserved
+
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old)
+
+ -- Container contains Count times New_Item at the end
+
+ and (if Count > 0 then
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item))
+
+ -- Count cursors have been inserted at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => Length (Container)'Old + 1,
+ Count => Count),
+
+ others =>
+
+ -- The elements of Container located before Before are preserved
+
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1)
+
+ -- Other elements are shifted by Count
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst => Length (Container)'Old,
+ Offset => Count)
+
+ -- Container contains Count times New_Item after position Before
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst =>
+ P.Get (Positions (Container)'Old, Before) - 1 + Count,
+ Item => New_Item)
+
+ -- Count cursors have been inserted at position Before in
+ -- Container.
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container)'Old, Before),
+ Count => Count));
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Position : out Cursor)
+ with
+ Global => null,
+ Pre =>
+ Length (Container) < Count_Type'Last
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
+
+ -- Positions is valid in Container and it is located either before
+ -- Before if it is valid in Container or at the end if it is
+ -- No_Element.
+
+ and P.Has_Key (Positions (Container), Position)
+ and (if Before = No_Element then
+ P.Get (Positions (Container), Position) = Length (Container)
+ else
+ P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container)'Old, Before))
+
+ -- The elements of Container located before Position are preserved
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
+
+ -- Other elements are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst => Length (Container)'Old,
+ Offset => 1)
+
+ -- New_Item is stored at Position in Container
+
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container), Position)) = New_Item
+
+ -- A new cursor has been inserted at position Position in Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container), Position));
+
+ procedure Insert
+ (Container : in out List;
+ Before : Cursor;
+ New_Item : Element_Type;
+ Position : out Cursor;
+ Count : Count_Type)
+ with
+ Global => null,
+ Pre =>
+ Length (Container) <= Count_Type'Last - Count
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element),
+ Post => Length (Container) = Length (Container)'Old + Count,
+ Contract_Cases =>
+ (Count = 0 =>
+ Position = Before
+ and Model (Container) = Model (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ others =>
+
+ -- Positions is valid in Container and it is located either before
+ -- Before if it is valid in Container or at the end if it is
+ -- No_Element.
+
+ P.Has_Key (Positions (Container), Position)
+ and (if Before = No_Element then
+ P.Get (Positions (Container), Position) =
+ Length (Container)'Old + 1
+ else
+ P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container)'Old, Before))
+
+ -- The elements of Container located before Position are preserved
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
+
+ -- Other elements are shifted by Count
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst => Length (Container)'Old,
+ Offset => Count)
+
+ -- Container contains Count times New_Item after position Position
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst =>
+ P.Get (Positions (Container), Position) - 1 + Count,
+ Item => New_Item)
+
+ -- Count cursor have been inserted at Position in Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container), Position),
+ Count => Count));
+
+ procedure Prepend (Container : in out List; New_Item : Element_Type) with
+ Global => null,
+ Pre => Length (Container) < Count_Type'Last,
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
+
+ -- Elements are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old,
+ Offset => 1)
+
+ -- New_Item is the first element of Container
+
+ and Element (Model (Container), 1) = New_Item
+
+ -- A new cursor has been inserted at the beginning of Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => 1);
+
+ procedure Prepend
+ (Container : in out List;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ with
+ Global => null,
+ Pre => Length (Container) <= Count_Type'Last - Count,
+ Post =>
+ Length (Container) = Length (Container)'Old + Count
+
+ -- Elements are shifted by Count
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old,
+ Offset => Count)
+
+ -- Container starts with Count times New_Item
+
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => 1,
+ Lst => Count,
+ Item => New_Item)
+
+ -- Count cursors have been inserted at the beginning of Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => 1,
+ Count => Count);
+
+ procedure Append (Container : in out List; New_Item : Element_Type) with
+ Global => null,
+ Pre => Length (Container) < Count_Type'Last,
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
+
+ -- Positions contains a new mapping from the last cursor of Container
+ -- to its length.
+
+ and P.Get (Positions (Container), Last (Container)) =
+ Length (Container)
+
+ -- Other cursors come from Container'Old
+
+ and P.Keys_Included_Except
+ (Left => Positions (Container),
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container))
+
+ -- Cursors of Container'Old keep the same position
+
+ and Positions (Container)'Old <= Positions (Container)
+
+ -- Model contains a new element New_Item at the end
+
+ and Element (Model (Container), Length (Container)) = New_Item
+
+ -- Elements of Container'Old are preserved
+
+ and Model (Container)'Old <= Model (Container);
+
+ procedure Append
+ (Container : in out List;
+ New_Item : Element_Type;
+ Count : Count_Type)
+ with
+ Global => null,
+ Pre => Length (Container) <= Count_Type'Last - Count,
+ Post =>
+ Length (Container) = Length (Container)'Old + Count
+
+ -- The elements of Container are preserved
+
+ and Model (Container)'Old <= Model (Container)
+
+ -- Container contains Count times New_Item at the end
+
+ and (if Count > 0 then
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item))
+
+ -- Count cursors have been inserted at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => Length (Container)'Old + 1,
+ Count => Count);
+
+ procedure Delete (Container : in out List; Position : in out Cursor) with
+ Global => null,
+ Depends => (Container =>+ Position, Position => null),
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Position is set to No_Element
+
+ and Position = No_Element
+
+ -- The elements of Container located before Position are preserved.
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
+
+ -- The elements located after Position are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Container),
+ Right => Model (Container)'Old,
+ Fst => P.Get (Positions (Container)'Old, Position'Old),
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- Position has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old));
+
+ procedure Delete
+ (Container : in out List;
+ Position : in out Cursor;
+ Count : Count_Type)
+ with
+ Global => null,
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Length (Container) in
+ Length (Container)'Old - Count .. Length (Container)'Old
+
+ -- Position is set to No_Element
+
+ and Position = No_Element
+
+ -- The elements of Container located before Position are preserved.
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1),
+
+ Contract_Cases =>
+
+ -- All the elements after Position have been erased
+
+ (Length (Container) - Count < P.Get (Positions (Container), Position) =>
+ Length (Container) =
+ P.Get (Positions (Container)'Old, Position'Old) - 1
+
+ -- At most Count cursors have been removed at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old),
+ Count => Count),
+
+ others =>
+ Length (Container) = Length (Container)'Old - Count
+
+ -- Other elements are shifted by Count
+
+ and M.Range_Shifted
+ (Left => Model (Container),
+ Right => Model (Container)'Old,
+ Fst => P.Get (Positions (Container)'Old, Position'Old),
+ Lst => Length (Container),
+ Offset => Count)
+
+ -- Count cursors have been removed from Container at Position
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old),
+ Count => Count));
+
+ procedure Delete_First (Container : in out List) with
+ Global => null,
+ Pre => not Is_Empty (Container),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- The elements of Container are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Container),
+ Right => Model (Container)'Old,
+ Fst => 1,
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- The first cursor of Container has been removed
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => 1);
+
+ procedure Delete_First (Container : in out List; Count : Count_Type) with
+ Global => null,
+ Contract_Cases =>
+
+ -- All the elements of Container have been erased
+
+ (Length (Container) <= Count =>
+ Length (Container) = 0,
+
+ others =>
+ Length (Container) = Length (Container)'Old - Count
+
+ -- Elements of Container are shifted by Count
+
+ and M.Range_Shifted
+ (Left => Model (Container),
+ Right => Model (Container)'Old,
+ Fst => 1,
+ Lst => Length (Container),
+ Offset => Count)
+
+ -- The first Count cursors have been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => 1,
+ Count => Count));
+
+ procedure Delete_Last (Container : in out List) with
+ Global => null,
+ Pre => not Is_Empty (Container),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- The elements of Container are preserved
+
+ and Model (Container) <= Model (Container)'Old
+
+ -- The last cursor of Container has been removed
+
+ and not P.Has_Key (Positions (Container), Last (Container)'Old)
+
+ -- Other cursors are still valid
+
+ and P.Keys_Included_Except
+ (Left => Positions (Container)'Old,
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container)'Old)
+
+ -- The positions of other cursors are preserved
+
+ and Positions (Container) <= Positions (Container)'Old;
+
+ procedure Delete_Last (Container : in out List; Count : Count_Type) with
+ Global => null,
+ Contract_Cases =>
+
+ -- All the elements of Container have been erased
+
+ (Length (Container) <= Count =>
+ Length (Container) = 0,
+
+ others =>
+ Length (Container) = Length (Container)'Old - Count
+
+ -- The elements of Container are preserved
+
+ and Model (Container) <= Model (Container)'Old
+
+ -- At most Count cursors have been removed at the end of Container
+
+ and P_Positions_Truncated
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => Length (Container) + 1,
+ Count => Count));
+
+ procedure Reverse_Elements (Container : in out List) with
+ Global => null,
+ Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
+
+ procedure Swap
+ (Container : in out List;
+ I : Cursor;
+ J : Cursor)
+ with
+ Global => null,
+ Pre => Has_Element (Container, I) and then Has_Element (Container, J),
+ Post =>
+ M_Elements_Swapped
+ (Model (Container)'Old,
+ Model (Container),
+ X => P.Get (Positions (Container)'Old, I),
+ Y => P.Get (Positions (Container)'Old, J))
+
+ and Positions (Container) = Positions (Container)'Old;
+
+ procedure Swap_Links
+ (Container : in out List;
+ I : Cursor;
+ J : Cursor)
+ with
+ Global => null,
+ Pre => Has_Element (Container, I) and then Has_Element (Container, J),
+ Post =>
+ M_Elements_Swapped
+ (Model (Container'Old),
+ Model (Container),
+ X => P.Get (Positions (Container)'Old, I),
+ Y => P.Get (Positions (Container)'Old, J))
+ and P_Positions_Swapped
+ (Positions (Container)'Old, Positions (Container), I, J);
+
+ procedure Splice
+ (Target : in out List;
+ Before : Cursor;
+ Source : in out List)
+ -- Target and Source should not be aliased
+ with
+ Global => null,
+ Pre =>
+ Length (Source) <= Count_Type'Last - Length (Target)
+ and then (Has_Element (Target, Before) or else Before = No_Element),
+ Post =>
+ Length (Source) = 0
+ and Length (Target) = Length (Target)'Old + Length (Source)'Old,
+ Contract_Cases =>
+ (Before = No_Element =>
+
+ -- The elements of Target are preserved
+
+ M.Range_Equal
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => Length (Target)'Old)
+
+ -- The elements of Source are appended to target, the order is not
+ -- specified.
+
+ and M_Elements_Included
+ (Left => Model (Source)'Old,
+ L_Lst => Length (Source)'Old,
+ Right => Model (Target),
+ R_Fst => Length (Target)'Old + 1,
+ R_Lst => Length (Target))
+
+ and M_Elements_Included
+ (Left => Model (Target),
+ L_Fst => Length (Target)'Old + 1,
+ L_Lst => Length (Target),
+ Right => Model (Source)'Old,
+ R_Lst => Length (Source)'Old)
+
+ -- Cursors have been inserted at the end of Target
+
+ and P_Positions_Truncated
+ (Positions (Target)'Old,
+ Positions (Target),
+ Cut => Length (Target)'Old + 1,
+ Count => Length (Source)'Old),
+
+ others =>
+
+ -- The elements of Target located before Before are preserved
+
+ M.Range_Equal
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => P.Get (Positions (Target)'Old, Before) - 1)
+
+ -- The elements of Source are inserted before Before, the order is
+ -- not specified.
+
+ and M_Elements_Included
+ (Left => Model (Source)'Old,
+ L_Lst => Length (Source)'Old,
+ Right => Model (Target),
+ R_Fst => P.Get (Positions (Target)'Old, Before),
+ R_Lst =>
+ P.Get (Positions (Target)'Old, Before) - 1 +
+ Length (Source)'Old)
+
+ and M_Elements_Included
+ (Left => Model (Target),
+ L_Fst => P.Get (Positions (Target)'Old, Before),
+ L_Lst =>
+ P.Get (Positions (Target)'Old, Before) - 1 +
+ Length (Source)'Old,
+ Right => Model (Source)'Old,
+ R_Lst => Length (Source)'Old)
+
+ -- Other elements are shifted by the length of Source
+
+ and M.Range_Shifted
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => P.Get (Positions (Target)'Old, Before),
+ Lst => Length (Target)'Old,
+ Offset => Length (Source)'Old)
+
+ -- Cursors have been inserted at position Before in Target
+
+ and P_Positions_Shifted
+ (Positions (Target)'Old,
+ Positions (Target),
+ Cut => P.Get (Positions (Target)'Old, Before),
+ Count => Length (Source)'Old));
+
+ procedure Splice
+ (Target : in out List;
+ Before : Cursor;
+ Source : in out List;
+ Position : in out Cursor)
+ -- Target and Source should not be aliased
+ with
+ Global => null,
+ Pre =>
+ (Has_Element (Target, Before) or else Before = No_Element)
+ and then Has_Element (Source, Position)
+ and then Length (Target) < Count_Type'Last,
+ Post =>
+ Length (Target) = Length (Target)'Old + 1
+ and Length (Source) = Length (Source)'Old - 1
+
+ -- The elements of Source located before Position are preserved
+
+ and M.Range_Equal
+ (Left => Model (Source)'Old,
+ Right => Model (Source),
+ Fst => 1,
+ Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
+
+ -- The elements located after Position are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Source)'Old,
+ Right => Model (Source),
+ Fst => P.Get (Positions (Source)'Old, Position'Old) + 1,
+ Lst => Length (Source)'Old,
+ Offset => -1)
+
+ -- Position has been removed from Source
+
+ and P_Positions_Shifted
+ (Positions (Source),
+ Positions (Source)'Old,
+ Cut => P.Get (Positions (Source)'Old, Position'Old))
+
+ -- Positions is valid in Target and it is located either before
+ -- Before if it is valid in Target or at the end if it is No_Element.
+
+ and P.Has_Key (Positions (Target), Position)
+ and (if Before = No_Element then
+ P.Get (Positions (Target), Position) = Length (Target)
+ else
+ P.Get (Positions (Target), Position) =
+ P.Get (Positions (Target)'Old, Before))
+
+ -- The elements of Target located before Position are preserved
+
+ and M.Range_Equal
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => P.Get (Positions (Target), Position) - 1)
+
+ -- Other elements are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => P.Get (Positions (Target), Position),
+ Lst => Length (Target)'Old,
+ Offset => 1)
+
+ -- The element located at Position in Source is moved to Target
+
+ and Element (Model (Target),
+ P.Get (Positions (Target), Position)) =
+ Element (Model (Source)'Old,
+ P.Get (Positions (Source)'Old, Position'Old))
+
+ -- A new cursor has been inserted at position Position in Target
+
+ and P_Positions_Shifted
+ (Positions (Target)'Old,
+ Positions (Target),
+ Cut => P.Get (Positions (Target), Position));
+
+ procedure Splice
+ (Container : in out List;
+ Before : Cursor;
+ Position : Cursor)
+ with
+ Global => null,
+ Pre =>
+ (Has_Element (Container, Before) or else Before = No_Element)
+ and then Has_Element (Container, Position),
+ Post => Length (Container) = Length (Container)'Old,
+ Contract_Cases =>
+ (Before = Position =>
+ Model (Container) = Model (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ Before = No_Element =>
+
+ -- The elements located before Position are preserved
+
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position) - 1)
+
+ -- The elements located after Position are shifted by 1
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Position) + 1,
+ Lst => Length (Container)'Old,
+ Offset => -1)
+
+ -- The last element of Container is the one that was previously at
+ -- Position.
+
+ and Element (Model (Container),
+ Length (Container)) =
+ Element (Model (Container)'Old,
+ P.Get (Positions (Container)'Old, Position))
+
+ -- Cursors from Container continue designating the same elements
+
+ and Mapping_Preserved
+ (M_Left => Model (Container)'Old,
+ M_Right => Model (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container)),
+
+ others =>
+
+ -- The elements located before Position and Before are preserved
+
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst =>
+ Count_Type'Min
+ (P.Get (Positions (Container)'Old, Position) - 1,
+ P.Get (Positions (Container)'Old, Before) - 1))
+
+ -- The elements located after Position and Before are preserved
+
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst =>
+ Count_Type'Max
+ (P.Get (Positions (Container)'Old, Position) + 1,
+ P.Get (Positions (Container)'Old, Before) + 1),
+ Lst => Length (Container))
+
+ -- The elements located after Before and before Position are
+ -- shifted by 1 to the right.
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before) + 1,
+ Lst => P.Get (Positions (Container)'Old, Position) - 1,
+ Offset => 1)
+
+ -- The elements located after Position and before Before are
+ -- shifted by 1 to the left.
+
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Position) + 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1,
+ Offset => -1)
+
+ -- The element previously at Position is now before Before
+
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container)'Old, Before)) =
+ Element
+ (Model (Container)'Old,
+ P.Get (Positions (Container)'Old, Position))
+
+ -- Cursors from Container continue designating the same elements
+
+ and Mapping_Preserved
+ (M_Left => Model (Container)'Old,
+ M_Right => Model (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container)));
+
+ function First (Container : List) return Cursor with
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 =>
+ First'Result = No_Element,
+
+ others =>
+ Has_Element (Container, First'Result)
+ and P.Get (Positions (Container), First'Result) = 1);
+
+ function First_Element (Container : List) return Element_Type with
+ Global => null,
+ Pre => not Is_Empty (Container),
+ Post => First_Element'Result = M.Get (Model (Container), 1);
+
+ function Last (Container : List) return Cursor with
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 =>
+ Last'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Last'Result)
+ and P.Get (Positions (Container), Last'Result) =
+ Length (Container));
+
+ function Last_Element (Container : List) return Element_Type with
+ Global => null,
+ Pre => not Is_Empty (Container),
+ Post =>
+ Last_Element'Result = M.Get (Model (Container), Length (Container));
+
+ function Next (Container : List; Position : Cursor) return Cursor with
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Next'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Next'Result)
+ and then P.Get (Positions (Container), Next'Result) =
+ P.Get (Positions (Container), Position) + 1);
+
+ procedure Next (Container : List; Position : in out Cursor) with
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Position = No_Element,
+
+ others =>
+ Has_Element (Container, Position)
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) + 1);
+
+ function Previous (Container : List; Position : Cursor) return Cursor with
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = 1
+ =>
+ Previous'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Previous'Result)
+ and then P.Get (Positions (Container), Previous'Result) =
+ P.Get (Positions (Container), Position) - 1);
+
+ procedure Previous (Container : List; Position : in out Cursor) with
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = 1
+ =>
+ Position = No_Element,
+
+ others =>
+ Has_Element (Container, Position)
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) - 1);
+
+ function Find
+ (Container : List;
+ Item : Element_Type;
+ Position : Cursor := No_Element) return Cursor
+ with
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+
+ -- If Item is not contained in Container after Position, Find returns
+ -- No_Element.
+
+ (not M.Contains
+ (Container => Model (Container),
+ Fst =>
+ (if Position = No_Element then
+ 1
+ else
+ P.Get (Positions (Container), Position)),
+ Lst => Length (Container),
+ Item => Item)
+ =>
+ Find'Result = No_Element,
+
+ -- Otherwise, Find returns a valid cursor in Container
+
+ others =>
+ P.Has_Key (Positions (Container), Find'Result)
+
+ -- The element designated by the result of Find is Item
+
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container), Find'Result)) = Item
+
+ -- The result of Find is located after Position
+
+ and (if Position /= No_Element then
+ P.Get (Positions (Container), Find'Result) >=
+ P.Get (Positions (Container), Position))
+
+ -- It is the first occurrence of Item in this slice
+
+ and not M.Contains
+ (Container => Model (Container),
+ Fst =>
+ (if Position = No_Element then
+ 1
+ else
+ P.Get (Positions (Container), Position)),
+ Lst =>
+ P.Get (Positions (Container), Find'Result) - 1,
+ Item => Item));
+
+ function Reverse_Find
+ (Container : List;
+ Item : Element_Type;
+ Position : Cursor := No_Element) return Cursor
+ with
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+
+ -- If Item is not contained in Container before Position, Find returns
+ -- No_Element.
+
+ (not M.Contains
+ (Container => Model (Container),
+ Fst => 1,
+ Lst =>
+ (if Position = No_Element then
+ Length (Container)
+ else
+ P.Get (Positions (Container), Position)),
+ Item => Item)
+ =>
+ Reverse_Find'Result = No_Element,
+
+ -- Otherwise, Find returns a valid cursor in Container
+
+ others =>
+ P.Has_Key (Positions (Container), Reverse_Find'Result)
+
+ -- The element designated by the result of Find is Item
+
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container), Reverse_Find'Result)) = Item
+
+ -- The result of Find is located before Position
+
+ and (if Position /= No_Element then
+ P.Get (Positions (Container), Reverse_Find'Result) <=
+ P.Get (Positions (Container), Position))
+
+ -- It is the last occurrence of Item in this slice
+
+ and not M.Contains
+ (Container => Model (Container),
+ Fst =>
+ P.Get (Positions (Container),
+ Reverse_Find'Result) + 1,
+ Lst =>
+ (if Position = No_Element then
+ Length (Container)
+ else
+ P.Get (Positions (Container), Position)),
+ Item => Item));
+
+ function Contains
+ (Container : List;
+ Item : Element_Type) return Boolean
+ with
+ Global => null,
+ Post =>
+ Contains'Result = M.Contains (Container => Model (Container),
+ Fst => 1,
+ Lst => Length (Container),
+ Item => Item);
+
+ function Has_Element
+ (Container : List;
+ Position : Cursor) return Boolean
+ with
+ Global => null,
+ Post =>
+ Has_Element'Result = P.Has_Key (Positions (Container), Position);
+ pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
+
+ generic
+ with function "<" (Left, Right : Element_Type) return Boolean is <>;
+
+ package Generic_Sorting with SPARK_Mode is
+
+ package Formal_Model with Ghost is
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean
+ with
+ Global => null,
+ Post =>
+ M_Elements_Sorted'Result =
+ (for all I in 1 .. M.Length (Container) =>
+ (for all J in I .. M.Length (Container) =>
+ not (Element (Container, J) < Element (Container, I))));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
+
+ end Formal_Model;
+ use Formal_Model;
+
+ function Is_Sorted (Container : List) return Boolean with
+ Global => null,
+ Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
+
+ procedure Sort (Container : in out List) with
+ Global => null,
+ Post =>
+ Length (Container) = Length (Container)'Old
+ and M_Elements_Sorted (Model (Container))
+ and M_Elements_Included
+ (Left => Model (Container)'Old,
+ L_Lst => Length (Container),
+ Right => Model (Container),
+ R_Lst => Length (Container))
+ and M_Elements_Included
+ (Left => Model (Container),
+ L_Lst => Length (Container),
+ Right => Model (Container)'Old,
+ R_Lst => Length (Container));
+
+ procedure Merge (Target : in out List; Source : in out List) with
+ -- Target and Source should not be aliased
+ Global => null,
+ Pre => Length (Target) <= Count_Type'Last - Length (Source),
+ Post =>
+ Length (Target) = Length (Target)'Old + Length (Source)'Old
+ and Length (Source) = 0
+ and (if M_Elements_Sorted (Model (Target)'Old)
+ and M_Elements_Sorted (Model (Source)'Old)
+ then
+ M_Elements_Sorted (Model (Target)))
+ and M_Elements_Included
+ (Left => Model (Target)'Old,
+ L_Lst => Length (Target)'Old,
+ Right => Model (Target),
+ R_Lst => Length (Target))
+ and M_Elements_Included
+ (Left => Model (Source)'Old,
+ L_Lst => Length (Source)'Old,
+ Right => Model (Target),
+ R_Lst => Length (Target))
+ and M_Elements_In_Union
+ (Model (Target),
+ Model (Source)'Old,
+ Model (Target)'Old);
+ end Generic_Sorting;
+
+private
+ pragma SPARK_Mode (Off);
+
+ use Ada.Finalization;
+
+ type Element_Access is access all Element_Type;
+
+ type Node_Type is record
+ Prev : Count_Type'Base := -1;
+ Next : Count_Type := 0;
+ Element : Element_Access := null;
+ end record;
+
+ type Node_Access is access all Node_Type;
+
+ function "=" (L, R : Node_Type) return Boolean is abstract;
+
+ type Node_Array is array (Count_Type range <>) of Node_Type;
+ function "=" (L, R : Node_Array) return Boolean is abstract;
+
+ type Node_Array_Access is access all Node_Array;
+
+ type List is new Controlled with record
+ Free : Count_Type'Base := -1;
+ Length : Count_Type := 0;
+ First : Count_Type := 0;
+ Last : Count_Type := 0;
+ Nodes : Node_Array_Access := null;
+ end record;
+
+ overriding procedure Finalize (Container : in out List);
+ overriding procedure Adjust (Container : in out List);
+end Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-07-12 12:24 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-07-12 12:24 [gcc r13-1617] [Ada] Add new unbounded and indefinite formal doubly linked list Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).