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

[Shark8 <onewingedshark@gmail.com>]

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;