From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!newsfeed.xs3.de!io.xs3.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Is there a reason System.Storage_Pools isn't Pure?
Date: Wed, 19 Apr 2017 15:36:26 -0500
Organization: JSA Research & Innovation
Message-ID: <od8hob$n82$1@franka.jacob-sparre.dk>
References: <178b6fbc-229b-49fc-8ffb-a5797bfc335f@googlegroups.com>
 <od5m40$tnu$1@franka.jacob-sparre.dk>
 <61e151c1-9fe6-4d32-8f13-d425bc41a616@googlegroups.com>
NNTP-Posting-Host: rrsoftware.com
X-Trace: franka.jacob-sparre.dk 1492634187 23810 24.196.82.226 (19 Apr 2017
 20:36:27 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Wed, 19 Apr 2017 20:36:27 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Xref: news.eternal-september.org comp.lang.ada:46599
Date: 2017-04-19T15:36:26-05:00
List-Id: <comp.lang.ada>

"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.