Re: Is there a reason System.Storage_Pools isn't Pure?

["Randy Brukardt" <randy@rrsoftware.com>]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:61e151c1-9fe6-4d32-8f13-d425bc41a616@googlegroups.com...
...
> What about a usable-for-anything holder? (In particular, I think that 
> Ada.Containers.Indefinite_Holders ought to be less restrictive than they 
> are.) We could have a Pure Indefinite_Holder with:
>
>    Generic
>      Type Element_Type(<>) is limited private;
>      -- Pure storage-pool as a parameter? a dependency?
>    Package Example with Pure, Spark_Mode => On is
>      Type Holder is private;
>      Function Has_Element( Container : Holder ) return Boolean;
>      Function Element( Container : Holder ) return Element_Type
>        with Pre => Has_Element( Container );
>      Procedure Clear( Container : in out Holder )
>        with Post => not Has_Element( Container );
>    Private
>      Pragma SPARK_Mode( Off );
>
>      Type is access Element_Type
>        with Storage_Size => 0; -- Pure pool storage to allow non-zero?
>
>      Function Has_Element( Container : Holder ) return Boolean is
>        (Container /= Null);
>      Function Has_Element( Container : Holder ) return Boolean is
>        (Container.All);
>    End Example;
>
> Or am I misunderstanding?

Your spec here doesn't have any way to put an element into the holder. And 
that's where the trouble comes (especially for limited types!). Perhaps you 
can figure it out (I haven't been able to). As it stands, your holder 
objects would have to have Has_Element = False. Not very useful. ;-)

                              Randy.