SPARK and Indefinite_Holders

General
1

I was thinking to move some of my code to Spark. But I use Ada.Containers.Indefinite_Holders a lot, and I can’t find an equivalent in Sparklib.
Am I missing something?

2

Afaik, SPARKlib tries to mimic the functionality of parts of the Ada Standard Library. So I suppose it should work OOTB. Nonetheless, there may be a performance hit or some functionality may be limited, but I believe it can be worth a try!

A quick search and replace could work or maybe even a renames?

Best regards,
Fer

3

I don’t know spark well, but there are some formal vectors. An indefinite_holder is just a 1 element vector notionally, so maybe you can make a quick wrapper around a vector that looks like an indefinite_holder and be ok?

Again I don’t know spark, but if I were to do it in plain Ada, I could do something like this (and just add functionality I need as I go):

   generic
      type Element_Type(<>) is private;
   package Indefinite_Holders is

      package Core is new Ada.Containers.Indefinite_Vectors
         (Index_Type   => Positive,
          Element_Type => Element_Type);
      
      subtype Reference_Type is Core.Reference_Type;
      subtype Constant_Reference_Type is Core.Constant_Reference_Type;

      type Holder is private;
      
      function Reference(Self : aliased in out Holder) return Reference_Type;
      function Constant_Reference(Self : aliased Holder) return Constant_Reference_Type;
      
      function To_Holder (New_Item : Element_Type) return Holder;
      function Element(Self : Holder) return Element_Type;
      procedure Replace_Element(Self : in out Holder; New_Item : Element_Type);

   private

      type Holder is new Core.Vector with null record;

      function Reference(Self : aliased in out Holder) return Reference_Type is
         (Self.Reference(1));
      function Constant_Reference(Self : aliased Holder) return Constant_Reference_Type is
         (Self.Constant_Reference(1));
      function To_Holder (New_Item : Element_Type) return Holder is
         (To_Vector(New_Item,1));
      function Element(Self : Holder) return Element_Type is
         (Self.Element(1));

   end Indefinite_Holders;

   package body Indefinite_Holders is

      procedure Replace_Element(Self : in out Holder; New_Item : Element_Type) is
      begin
         if Self.Is_Empty then
            Self.Append(New_Item);
         else
            Self.Replace_Element(1, New_Item);
         end if;
      end Replace_Element;

   end Indefinite_Holders;

You could maybe play with this and use SPARK.Formal_Containers.Unbounded_Vectors (instead of my indefinite_vectors example)?

4

Thanks. Using a formal unbounded vector behind the hood seems a good starting point. I will try to do that. Still I don’t understand why it is not in Sparklib as it seems to be the only missing container type.

5

I’m not sure honestly. It seems like a nobrainer to me to have them, but I’m not super smart in SPARK, so maybe I am not thinking of an issue, but it is puzzling to me.

6

If you’re not using indefinite-types, using unconstrained arrays:

Generic
  Type Element is limited private;
Package Generic_Holder is
  Type Holder(<>) is private;
  -- Interface-subprograms.

  Empty_Holder : Constant Holder;
Private

   Subtype Index is Boolean True..True;
   Type Holder is array(Index range <>) of Element;

  Empty_Holder : Constant Holder:= ( True..False => <> );
End Generic_Holder;

The idea here: you can have a holder with an element (an array of length-1), or an empty holder (array of length-0). Note that Function Has_Element(Object : Holder) return Boolean now becomes (Object'Length in Positive);

7

Just note that if you used the unconstrained array method that you have some considerations:

  • It will be on the stack (vs the heap in Vector’s case) so large objects may be undesirable to use
  • Once you initialize a holder (based on an unconstrained array) to Empty_Holder , you cannot change it later (vs being able to freely change it in the Vector implementation). Similarly you cannot change an non empty back to empty.

None of these are bad things in general (I prefer stack to heap personally, but sometimes you need the heap), but things to keep in mind.