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,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.107.11.219 with SMTP id 88mr2771342iol.9.1492647177280;
        Wed, 19 Apr 2017 17:12:57 -0700 (PDT)
X-Received: by 10.157.68.144 with SMTP id v16mr118596ote.12.1492647177219;
 Wed, 19 Apr 2017 17:12:57 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!t52no2085461qtb.0!news-out.google.com!y33ni726qty.1!nntp.google.com!c45no3913680qtb.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Wed, 19 Apr 2017 17:12:56 -0700 (PDT)
In-Reply-To: <od8hob$n82$1@franka.jacob-sparre.dk>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=50.130.162.123;
 posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC
NNTP-Posting-Host: 50.130.162.123
References: <178b6fbc-229b-49fc-8ffb-a5797bfc335f@googlegroups.com>
 <od5m40$tnu$1@franka.jacob-sparre.dk>
 <61e151c1-9fe6-4d32-8f13-d425bc41a616@googlegroups.com>
 <od8hob$n82$1@franka.jacob-sparre.dk>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <a498c0f6-11ae-4050-ade0-bc35c686dc1c@googlegroups.com>
Subject: Re: Is there a reason System.Storage_Pools isn't Pure?
From: Shark8 <onewingedshark@gmail.com>
Injection-Date: Thu, 20 Apr 2017 00:12:57 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:46604
Date: 2017-04-19T17:12:56-07:00
List-Id: <comp.lang.ada>

On Wednesday, April 19, 2017 at 2:36:28 PM UTC-6, Randy Brukardt wrote:
> 
> 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.

I should have known better than to type it on-the-fly.
Here's a different spec that actually does compile under GNAT, even though [AFACT] it shouldn't:

Pragma Ada_2012;
Pragma Assertion_Policy( Check );
Pragma SPARK_Mode( On );

Generic
    Type Element_Type(<>) is limited private;
Package Forth.Pure_Types.Pure_Holders with Pure, SPARK_Mode => On is
    Pragma Pure(Forth.Pure_Types.Pure_Holders);

    Type Holder is private;

    Function Has_Element (Container : Holder) return Boolean
      with Inline;

    Procedure Clear (Container : in out Holder)
      with Inline;

    Function Element (Container : Holder) return Element_Type
      with Inline,
	Pre     => Has_Element(Container)
		   or else raise Constraint_Error with "Container is empty.";

    Function To_Holder (Item : Element_Type) return Holder
      with Inline,
	Post    => Has_Element(To_Holder'Result);

    Procedure Replace_Element(Container : in out Holder; Item : Element_Type)
      with Inline;


Private
--      Pragma SPARK_Mode( OFF );

    Type Holder is access all Element_Type;
--      with Storage_Size => 0;

End Forth.Pure_Types.Pure_Holders;

---------------------------------------------------------------

Pragma Ada_2012;
Pragma Assertion_Policy( Check );

Package Body Forth.Pure_Types.Pure_Holders is

    Function Has_Element (Container : Holder) return Boolean is
      (Container /= Null);

    Procedure Clear (Container : in out Holder) is
	Procedure Unchecked_Deallocation(X : in out Holder)
	  with Import, Convention => Intrinsic;
    Begin
	Unchecked_Deallocation( Container );
    End Clear;

    Function Element (Container : Holder) return Element_Type is
      ( Container.All );

    Function To_Holder (Item : Element_Type) return Holder is
      ( New Element_Type'(Item) );

    Procedure Replace_Element(Container : in out Holder; Item : Element_Type) is
    Begin
	Clear( Container );
	Container:= To_Holder( Item );
    End Replace_Element;

End Forth.Pure_Types.Pure_Holders;

--------------

I've already got a Pure version of Storage_Pools (and Subpools) compiling too. (!) -- Of course I can't use an instance of them in a pure unit



----------------

Pragma Ada_2012;
Pragma Assertion_Policy( Check );

With
System.Storage_Pools;

Generic
    Type K(<>) is limited private;
    Pool : in out System.Storage_Pools.Root_Storage_Pool'Class;
Package Pool_Test with Pure is
    
    Type J is access all K
      with Storage_Pool => Pool;
    
End Pool_Test;