a-cofuba.ads (Add): Take as an additional input parameter the position where the element should be...

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cofuba.ads (Add): Take as an additional input parameter
	the position where the element should be inserted.
	(Remove): New function that removes an element from the container.
	* a-cofuma.ads (Add): Adapt to the new API of Base.Add.
	* a-cofuse.ads (Add): Adapt to the new API of Base.Add.
	(Remove): New function that removes an element from a set.
	* a-cofuve.ads (Add): Adapt to the new API of Base.Add.
	(Remove): New function that removes an element from a sequence.
	(Insert): New function that adds anywhere in a sequence.

From-SVN: r247297

9 files changed, 227 insertions, 105 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 91c78f8..f6bf798 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,15 @@
+2017-04-27  Claire Dross  <dross@adacore.com>
+
+	* a-cofuba.ads (Add): Take as an additional input parameter
+	the position where the element should be inserted.
+	(Remove): New function that removes an element from the container.
+	* a-cofuma.ads (Add): Adapt to the new API of Base.Add.
+	* a-cofuse.ads (Add): Adapt to the new API of Base.Add.
+	(Remove): New function that removes an element from a set.
+	* a-cofuve.ads (Add): Adapt to the new API of Base.Add.
+	(Remove): New function that removes an element from a sequence.
+	(Insert): New function that adds anywhere in a sequence.
+
 2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* checks.adb (Generate_Range_Check): Revert previous change.
diff --git a/gcc/ada/a-cofuba.adb b/gcc/ada/a-cofuba.adb
index dd29eea..63ebc5f 100644
--- a/gcc/ada/a-cofuba.adb
+++ b/gcc/ada/a-cofuba.adb
@@ -33,21 +33,17 @@ pragma Ada_2012;
 
 package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
 
-   pragma Assertion_Policy
-      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
-
    function To_Count (Idx : Extended_Index) return Count_Type
    is (Count_Type
-       (Extended_Index'Pos (Idx)
-        - Extended_Index'Pos (Extended_Index'First)));
+         (Extended_Index'Pos (Idx)
+            - Extended_Index'Pos (Extended_Index'First)));
    function To_Index (Position : Count_Type) return Extended_Index
    is (Extended_Index'Val
-       (Position
-        + Extended_Index'Pos (Extended_Index'First)));
+         (Position + Extended_Index'Pos (Extended_Index'First)));
    --  Conversion functions between Index_Type and Count_Type
 
    function Find (C : Container; E : access Element_Type) return Count_Type;
-   --  Search a container C for an element equal to E.all, return the
+   --  Search a container C for an element equal to E.all, returning the
    --  position in the underlying array.
 
    ---------
@@ -86,11 +82,24 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
    -- Add --
    ---------
 
-   function Add (C : Container; E : Element_Type) return Container is
+   function Add
+     (C : Container;
+      I : Index_Type;
+      E : Element_Type) return Container
+   is
+      A : constant Element_Array_Access :=
+            new Element_Array'(1 .. C.Elements'Last + 1 => <>);
+      P : Count_Type := 0;
    begin
-      return Container'(Elements =>
-                           new Element_Array'
-                          (C.Elements.all & new Element_Type'(E)));
+      for J in 1 .. C.Elements'Last + 1 loop
+         if J /= To_Count (I) then
+            P := P + 1;
+            A (J) := C.Elements (P);
+         else
+            A (J) := new Element_Type'(E);
+         end if;
+      end loop;
+      return Container'(Elements => A);
    end Add;
 
    ----------
@@ -123,7 +132,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
 
    function Intersection (C1, C2 : Container) return Container is
       A : constant Element_Array_Access :=
-        new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>);
+            new Element_Array'(1 .. Num_Overlaps (C1, C2) => <>);
       P : Count_Type := 0;
    begin
       for I in C1.Elements'Range loop
@@ -139,8 +148,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
    -- Length --
    ------------
 
-   function Length (C : Container) return Count_Type is
-     (C.Elements'Length);
+   function Length (C : Container) return Count_Type is (C.Elements'Length);
 
    ---------------------
    -- Num_Overlaps --
@@ -157,6 +165,24 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
       return P;
    end Num_Overlaps;
 
+   ------------
+   -- Remove --
+   ------------
+
+   function Remove (C : Container; I : Index_Type) return Container is
+      A : constant Element_Array_Access :=
+            new Element_Array'(1 .. C.Elements'Last - 1 => <>);
+      P : Count_Type := 0;
+   begin
+      for J in C.Elements'Range loop
+         if J /= To_Count (I) then
+            P := P + 1;
+            A (P) := C.Elements (J);
+         end if;
+      end loop;
+      return Container'(Elements => A);
+   end Remove;
+
    ---------
    -- Set --
    ---------
@@ -165,7 +191,7 @@ package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
                  return Container
    is
       Result : constant Container :=
-        Container'(Elements => new Element_Array'(C.Elements.all));
+                 Container'(Elements => new Element_Array'(C.Elements.all));
    begin
       Result.Elements (To_Count (I)) := new Element_Type'(E);
       return Result;
diff --git a/gcc/ada/a-cofuba.ads b/gcc/ada/a-cofuba.ads
index 6bcea9d..e176071 100644
--- a/gcc/ada/a-cofuba.ads
+++ b/gcc/ada/a-cofuba.ads
@@ -28,16 +28,16 @@
 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
---  Functional containers are neither controlled nor limited. This is safe as
---  no primitives is provided to modify them.
+--  Functional containers are neither controlled nor limited. This is safe, as
+--  no primitives are provided to modify them.
 --  Memory allocated inside functional containers is never reclaimed.
 
 pragma Ada_2012;
 
 private generic
    type Index_Type is (<>);
-   --  To avoid Constraint_Error being raised at runtime, Index_Type'Base
-   --  should have at least one more element at the left than Index_Type.
+   --  To avoid Constraint_Error being raised at run time, Index_Type'Base
+   --  should have at least one more element at the low end than Index_Type.
 
    type Element_Type (<>) is private;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
@@ -52,22 +52,28 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is
    --  Return True if C1 and C2 contain the same elements at the same position
 
    function Length (C : Container) return Count_Type;
-   --  Number of elements stored in C.
+   --  Number of elements stored in C
 
    function Get (C : Container; I : Index_Type) return Element_Type;
-   --  Access to the element at index I in C.
+   --  Access to the element at index I in C
 
    function Set (C : Container; I : Index_Type; E : Element_Type)
                  return Container;
    --  Return a new container which is equal to C except for the element at
-   --  index I which is set to E.
+   --  index I, which is set to E.
 
-   function Add (C : Container; E : Element_Type) return Container;
-   --  Return a new container which is C appended with E.
+   function Add
+     (C : Container;
+      I : Index_Type;
+      E : Element_Type) return Container;
+   --  Return a new container that is C with E inserted at index I
+
+   function Remove (C : Container; I : Index_Type) return Container;
+   --  Return a new container that is C without the element at index I
 
    function Find (C : Container; E : Element_Type) return Extended_Index;
-   --  Return the first index for which the element stored in C is I.
-   --  If there are no such indexes, return Extended_Index'First.
+   --  Return the first index for which the element stored in C is I. If there
+   --  are no such indexes, return Extended_Index'First.
 
    --------------------
    -- Set Operations --
@@ -77,7 +83,7 @@ package Ada.Containers.Functional_Base with SPARK_Mode => Off is
    --  Return True if every element of C1 is in C2
 
    function Num_Overlaps (C1, C2 : Container) return Count_Type;
-   --  Return the number of elements that are both in
+   --  Return the number of elements that are in both C1 and C2
 
    function Union (C1, C2 : Container) return Container;
    --  Return a container which is C1 plus all the elements of C2 that are not
@@ -92,13 +98,17 @@ private
    subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
 
    type Element_Access is access all Element_Type;
+
    type Element_Array is
      array (Positive_Count_Type range <>) of Element_Access;
+
    type Element_Array_Access is not null access Element_Array;
+
    Empty_Element_Array_Access : constant Element_Array_Access :=
      new Element_Array'(1 .. 0 => null);
 
    type Container is record
       Elements : Element_Array_Access := Empty_Element_Array_Access;
    end record;
+
 end Ada.Containers.Functional_Base;
diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb
index 9367bae..742320c 100644
--- a/gcc/ada/a-cofuma.adb
+++ b/gcc/ada/a-cofuma.adb
@@ -34,9 +34,6 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
    use Key_Containers;
    use Element_Containers;
 
-   pragma Assertion_Policy
-      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
-
    ---------
    -- "=" --
    ---------
@@ -69,8 +66,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
    function Add (M : Map; K : Key_Type; E : Element_Type) return Map is
    begin
       return
-        (Keys     => Add (M.Keys, K),
-         Elements => Add (M.Elements, E));
+        (Keys     => Add (M.Keys, Length (M.Keys) + 1, K),
+         Elements => Add (M.Elements, Length (M.Elements) + 1, E));
    end Add;
 
    ---------
diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads
index 23fb45c..960264c 100644
--- a/gcc/ada/a-cofuma.ads
+++ b/gcc/ada/a-cofuma.ads
@@ -39,6 +39,8 @@ generic
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 package Ada.Containers.Functional_Maps with SPARK_Mode is
 
+   pragma Assertion_Policy (Post => Ignore);
+
    type Map is private with
      Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
      Iterable                  => (First       => Iter_First,
@@ -46,10 +48,10 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
                                    Has_Element => Iter_Has_Element,
                                    Element     => Iter_Element);
    --  Maps are empty when default initialized.
-   --  For in quantification over maps should not be used.
-   --  For of quantification over maps iterates over keys.
+   --  "For in" quantification over maps should not be used.
+   --  "For of" quantification over maps iterates over keys.
 
-   --  Maps are axiomatized using Mem and Get encoding respectively the
+   --  Maps are axiomatized using Mem and Get, encoding respectively the
    --  presence of a key in a map and an accessor to elements associated to its
    --  keys. The length of a map is also added to protect Add against overflows
    --  but it is not actually modeled.
@@ -64,7 +66,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
      Global => null;
 
    function "<=" (M1, M2 : Map) return Boolean with
-   --  Map inclusion.
+   --  Map inclusion
 
      Global => null,
      Post   => "<="'Result =
@@ -72,25 +74,23 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
         and then Get (M2, K) = Get (M1, K));
 
    function "=" (M1, M2 : Map) return Boolean with
-   --  Extensional equality over maps.
+   --  Extensional equality over maps
 
      Global => null,
      Post   => "="'Result =
-       ((for all K of M1 => Mem (M2, K)
-        and then Get (M2, K) = Get (M1, K))
-        and (for all K of M2 => Mem (M1, K)));
+       ((for all K of M1 => Mem (M2, K) and then Get (M2, K) = Get (M1, K))
+          and (for all K of M2 => Mem (M1, K)));
 
    pragma Warnings (Off, "unused variable ""K""");
    function Is_Empty (M : Map) return Boolean with
-   --  A map is empty if it contains no key.
-
+   --  A map is empty if it contains no key
      Global => null,
      Post   => Is_Empty'Result = (for all K of M => False);
    pragma Warnings (On, "unused variable ""K""");
 
    function Is_Add
      (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean
-   --  Returns True if Result is M augmented with the mapping K -> E.
+   --  Returns True if Result is M augmented with the mapping K -> E
 
    with
      Global => null,
@@ -115,7 +115,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
 
    function Is_Set
      (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean
-   --  Returns True if Result is M where the element associated to K has been
+   --  Returns True if Result is M, where the element associated to K has been
    --  replaced by E.
 
    with
@@ -130,7 +130,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
           and then (for all K of Result => Mem (M, K)));
 
    function Set (M : Map; K : Key_Type; E : Element_Type) return Map with
-   --  Returns M where the element associated to K has been replaced by E.
+   --  Returns M, where the element associated to K has been replaced by E.
    --  Is_Set (M, K, E, Result) should be used instead of
    --  Result = Set (M, K, E) whenever possible both for execution and for
    --  proof.
@@ -157,7 +157,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
      Global => null,
      Pre    => Iter_Has_Element (M, K);
    pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem);
+
 private
+
    pragma SPARK_Mode (Off);
 
    function "="  (Left, Right : Key_Type) return Boolean
@@ -190,4 +192,5 @@ private
 
    function Iter_Element (M : Map; K : Private_Key) return Key_Type is
      (Key_Containers.Get (M.Keys, Count_Type (K)));
+
 end Ada.Containers.Functional_Maps;
diff --git a/gcc/ada/a-cofuse.adb b/gcc/ada/a-cofuse.adb
index 21417b2..8a3d08d 100644
--- a/gcc/ada/a-cofuse.adb
+++ b/gcc/ada/a-cofuse.adb
@@ -34,9 +34,6 @@ pragma Ada_2012;
 package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
    use Containers;
 
-   pragma Assertion_Policy
-      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
-
    ---------
    -- "=" --
    ---------
@@ -55,27 +52,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
    ---------
 
    function Add (S : Set; E : Element_Type) return Set is
-     (Content => Add (S.Content, E));
-
-   ------------
-   -- Length --
-   ------------
-
-   function Length (S : Set) return Count_Type is (Length (S.Content));
-
-   ---------
-   -- Mem --
-   ---------
-
-   function Mem (S : Set; E : Element_Type) return Boolean is
-      (Find (S.Content, E) > 0);
-
-   ------------------
-   -- Num_Overlaps --
-   ------------------
-
-   function Num_Overlaps (S1, S2 : Set) return Count_Type is
-      (Num_Overlaps (S1.Content, S2.Content));
+     (Content => Add (S.Content, Length (S.Content) + 1, E));
 
    ------------------
    -- Intersection --
@@ -119,6 +96,33 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
       and (for all E of S1 => Mem (Result, E))
       and (for all E of S2 => Mem (Result, E)));
 
+   ------------
+   -- Length --
+   ------------
+
+   function Length (S : Set) return Count_Type is (Length (S.Content));
+
+   ---------
+   -- Mem --
+   ---------
+
+   function Mem (S : Set; E : Element_Type) return Boolean is
+      (Find (S.Content, E) > 0);
+
+   ------------------
+   -- Num_Overlaps --
+   ------------------
+
+   function Num_Overlaps (S1, S2 : Set) return Count_Type is
+      (Num_Overlaps (S1.Content, S2.Content));
+
+   ------------
+   -- Remove --
+   ------------
+
+   function Remove (S : Set; E : Element_Type) return Set is
+     (Content => Remove (S.Content, Find (S.Content, E)));
+
    -----------
    -- Union --
    -----------
diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads
index cbc03fa..6f4dc98 100644
--- a/gcc/ada/a-cofuse.ads
+++ b/gcc/ada/a-cofuse.ads
@@ -37,6 +37,8 @@ generic
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 package Ada.Containers.Functional_Sets with SPARK_Mode is
 
+   pragma Assertion_Policy (Post => Ignore);
+
    type Set is private with
      Default_Initial_Condition => Is_Empty (Set) and Length (Set) = 0,
      Iterable                  => (First       => Iter_First,
@@ -44,11 +46,11 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
                                    Has_Element => Iter_Has_Element,
                                    Element     => Iter_Element);
    --  Sets are empty when default initialized.
-   --  For in quantification over sets should not be used.
-   --  For of quantification over sets iterates over elements.
+   --  "For in" quantification over sets should not be used.
+   --  "For of" quantification over sets iterates over elements.
 
-   --  Sets are axiomatized using Mem which encodes whether an element is
-   --  contained in a set.  The length of a set is also added to protect Add
+   --  Sets are axiomatized using Mem, which encodes whether an element is
+   --  contained in a set. The length of a set is also added to protect Add
    --  against overflows but it is not actually modeled.
 
    function Mem (S : Set; E : Element_Type) return Boolean with
@@ -58,13 +60,13 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
      Global => null;
 
    function "<=" (S1, S2 : Set) return Boolean with
-   --  Set inclusion.
+   --  Set inclusion
 
      Global => null,
      Post   => "<="'Result = (for all E of S1 => Mem (S2, E));
 
    function "=" (S1, S2 : Set) return Boolean with
-   --  Extensional equality over sets.
+   --  Extensional equality over sets
 
      Global => null,
      Post   =>
@@ -73,14 +75,14 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
 
    pragma Warnings (Off, "unused variable ""E""");
    function Is_Empty (S : Set) return Boolean with
-   --  A set is empty if it contains no element.
+   --  A set is empty if it contains no element
 
      Global => null,
      Post   => Is_Empty'Result = (for all E of S => False);
    pragma Warnings (On, "unused variable ""E""");
 
    function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean
-   --  Returns True if Result is S augmented with E.
+   --  Returns True if Result is S augmented with E
 
    with
      Global => null,
@@ -99,8 +101,18 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
      Post   => Length (Add'Result) = Length (S) + 1
      and Is_Add (S, E, Add'Result);
 
+   function Remove (S : Set; E : Element_Type) return Set with
+   --  Returns S without E.
+   --  Is_Add (Result, E, S) should be used instead of Result = Remove (S, E)
+   --  whenever possible both for execution and for proof.
+
+     Global => null,
+     Pre    => Mem (S, E),
+     Post   => Length (Remove'Result) = Length (S) - 1
+     and Is_Add (Remove'Result, E, S);
+
    function Is_Intersection (S1, S2, Result : Set) return Boolean with
-   --  Returns True if Result is the intersection of S1 and S2.
+   --  Returns True if Result is the intersection of S1 and S2
 
      Global => null,
      Post   => Is_Intersection'Result =
@@ -110,7 +122,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
                (if Mem (S2, E) then Mem (Result, E))));
 
    function Num_Overlaps (S1, S2 : Set) return Count_Type with
-   --  Number of elements that are both in S1 and S2.
+   --  Number of elements that are both in S1 and S2
 
      Global => null,
      Post   => Num_Overlaps'Result <= Length (S1)
@@ -129,7 +141,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
      and Is_Intersection (S1, S2, Intersection'Result);
 
    function Is_Union (S1, S2, Result : Set) return Boolean with
-   --  Returns True if Result is the union of S1 and S2.
+   --  Returns True if Result is the union of S1 and S2
 
      Global => null,
      Post   => Is_Union'Result =
@@ -167,7 +179,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
      Global => null,
      Pre    => Iter_Has_Element (S, K);
    pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem);
+
 private
+
    pragma SPARK_Mode (Off);
 
    subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
@@ -192,4 +206,5 @@ private
 
    function Iter_Element (S : Set; K : Private_Key) return Element_Type is
      (Containers.Get (S.Content, Count_Type (K)));
+
 end Ada.Containers.Functional_Sets;
diff --git a/gcc/ada/a-cofuve.adb b/gcc/ada/a-cofuve.adb
index 6f4f2b1..04c7909 100644
--- a/gcc/ada/a-cofuve.adb
+++ b/gcc/ada/a-cofuve.adb
@@ -33,9 +33,6 @@ pragma Ada_2012;
 package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
    use Containers;
 
-   pragma Assertion_Policy
-      (Pre => Suppressible, Ghost => Suppressible, Post => Ignore);
-
    ---------
    -- "=" --
    ---------
@@ -66,7 +63,11 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
    ---------
 
    function Add (S : Sequence; E : Element_Type) return Sequence is
-     (Content => Add (S.Content, E));
+     (Content => Add (S.Content,
+                      Index_Type'Val
+                        (Index_Type'Pos (Index_Type'First) +
+                             Length (S.Content)),
+                      E));
 
    ---------
    -- Get --
@@ -76,6 +77,16 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
      (Get (S.Content, N));
 
    ------------
+   -- Insert --
+   ------------
+
+   function Insert
+     (S : Sequence;
+      N : Index_Type;
+      E : Element_Type) return Sequence is
+     (Content => Add (S.Content, N, E));
+
+   ------------
    -- Is_Add --
    ------------
 
@@ -123,6 +134,13 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
    function Length (S : Sequence) return Count_Type is
      (Length (S.Content));
 
+   ------------
+   -- Remove --
+   ------------
+
+   function Remove (S : Sequence; N : Index_Type) return Sequence is
+     (Content => Remove (S.Content, N));
+
    ---------
    -- Set --
    ---------
diff --git a/gcc/ada/a-cofuve.ads b/gcc/ada/a-cofuve.ads
index 9d990a9..13c047e 100644
--- a/gcc/ada/a-cofuve.ads
+++ b/gcc/ada/a-cofuve.ads
@@ -34,18 +34,20 @@ private with Ada.Containers.Functional_Base;
 
 generic
    type Index_Type is (<>);
-   --  To avoid Constraint_Error being raised at runtime, Index_Type'Base
-   --  should have at least one more element at the left than Index_Type.
+   --  To avoid Constraint_Error being raised at run time, Index_Type'Base
+   --  should have at least one more element at the low end than Index_Type.
 
    type Element_Type (<>) is private;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 package Ada.Containers.Functional_Vectors with SPARK_Mode is
 
+   pragma Assertion_Policy (Post => Ignore);
+
    subtype Extended_Index is Index_Type'Base range
      Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
-   --  Index_Type with one more element to the left.
+   --  Index_Type with one more element at the low end of the range.
    --  This type is never used but it forces GNATprove to check that there is
-   --  room for one more element at the left of Index_Type.
+   --  room for one more element at the low end of Index_Type.
 
    type Sequence is private
      with Default_Initial_Condition => Length (Sequence) = 0,
@@ -55,9 +57,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
                   Element     => Get);
    --  Sequences are empty when default initialized.
    --  Quantification over sequences can be done using the regular
-   --  quantification over its range or directky on its elements using for of.
+   --  quantification over its range or directly on its elements with "for of".
 
-   --  Sequences are axiomatized using Length and Get providing respectively
+   --  Sequences are axiomatized using Length and Get, providing respectively
    --  the length of a sequence and an accessor to its Nth element:
 
    function Length (S : Sequence) return Count_Type with
@@ -73,14 +75,14 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
    function First return Extended_Index is (Index_Type'First);
 
    function Get (S : Sequence; N : Extended_Index) return Element_Type
-   --  Get ranges over Extended_Index so that it can be used for iteration.
+   --  Get ranges over Extended_Index so that it can be used for iteration
 
    with
      Global => null,
      Pre    => N in Index_Type'First .. Last (S);
 
    function "=" (S1, S2 : Sequence) return Boolean with
-   --  Extensional equality over sequences.
+   --  Extensional equality over sequences
 
      Global => null,
      Post   => "="'Result =
@@ -109,22 +111,22 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
    function Is_Set
      (S : Sequence; N : Index_Type; E : Element_Type; Result : Sequence)
       return Boolean
-   --  Returns True if Result is S where the Nth element has been replaced by
+   --  Returns True if Result is S, where the Nth element has been replaced by
    --  E.
 
    with
      Global => null,
        Post   => Is_Set'Result =
          (N in Index_Type'First .. Last (S)
-          and then Length (Result) = Length (S)
-          and then Get (Result, N) = E
-          and then (for all M in Index_Type'First .. Last (S) =>
-              (if M /= N then Get (Result, M) = Get (S, M))));
+           and then Length (Result) = Length (S)
+           and then Get (Result, N) = E
+           and then (for all M in Index_Type'First .. Last (S) =>
+                       (if M /= N then Get (Result, M) = Get (S, M))));
 
    function Set
      (S : Sequence; N : Index_Type; E : Element_Type) return Sequence
-   --  Returns S where the Nth element has been replaced by E.
-   --  Is_Set (S, N, E, Result) should be instead of than
+   --  Returns S, where the Nth element has been replaced by E.
+   --  Is_Set (S, N, E, Result) should be used instead of
    --  Result = Set (S, N, E) whenever possible both for execution and for
    --  proof.
 
@@ -135,15 +137,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
 
    function Is_Add
      (S : Sequence; E : Element_Type; Result : Sequence) return Boolean
-   --  Returns True if Result is S appended with E.
+   --  Returns True if Result is S appended with E
 
    with
      Global => null,
      Post   => Is_Add'Result =
          (Length (Result) = Length (S) + 1
-          and then Get (Result, Last (Result)) = E
-          and then (for all M in Index_Type'First .. Last (S) =>
-              Get (Result, M) = Get (S, M)));
+           and then Get (Result, Last (Result)) = E
+           and then (for all M in Index_Type'First .. Last (S) =>
+                       Get (Result, M) = Get (S, M)));
 
    function Add (S : Sequence; E : Element_Type) return Sequence with
    --  Returns S appended with E.
@@ -154,6 +156,39 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
      Pre    => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last,
      Post   => Is_Add (S, E, Add'Result);
 
+   function Insert
+     (S : Sequence;
+      N : Index_Type;
+      E : Element_Type) return Sequence
+   with
+   --  Returns S with E inserted at index I
+
+     Global => null,
+     Pre    => Length (S) < Count_Type'Last and then Last (S) < Index_Type'Last
+     and then N <= Extended_Index'Succ (Last (S)),
+     Post   => Length (Insert'Result) = Length (S) + 1
+     and then Get (Insert'Result, N) = E
+     and then (for all M in Index_Type'First .. Extended_Index'Pred (N) =>
+                   Get (Insert'Result, M) = Get (S, M))
+     and then (for all M in Extended_Index'Succ (N) .. Last (Insert'Result) =>
+                   Get (Insert'Result, M) = Get (S, Extended_Index'Pred (M)))
+     and then (for all M in N .. Last (S) =>
+                   Get (Insert'Result, Extended_Index'Succ (M)) = Get (S, M));
+
+   function Remove (S : Sequence; N : Index_Type) return Sequence with
+   --  Returns S without the element at index N
+
+     Global => null,
+     Pre    => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last
+     and N in Index_Type'First .. Last (S),
+     Post   => Length (Remove'Result) = Length (S) - 1
+     and then (for all M in Index_Type'First .. Extended_Index'Pred (N) =>
+                   Get (Remove'Result, M) = Get (S, M))
+     and then (for all M in N .. Last (Remove'Result) =>
+                   Get (Remove'Result, M) = Get (S, Extended_Index'Succ (M)))
+     and then (for all M in Extended_Index'Succ (N) .. Last (S) =>
+                   Get (Remove'Result, Extended_Index'Pred (M)) = Get (S, M));
+
    ---------------------------
    --  Iteration Primitives --
    ---------------------------
@@ -172,6 +207,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
      Pre    => Iter_Has_Element (S, I);
 
 private
+
    pragma SPARK_Mode (Off);
 
    package Containers is new Ada.Containers.Functional_Base
@@ -194,5 +230,6 @@ private
    is
      (I in Index_Type'First ..
         (Index_Type'Val
-             ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))));
+           ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))));
+
 end Ada.Containers.Functional_Vectors;