Brain bug or GNAT bug?

Brain bug or GNAT bug?

[(see below)]

Using GNAT GPL 2006 (PPC/Darwin), I instantiate:

   generic
   
      type modular is mod <>;
   
   package try is
   
      type DT1 (the_size : modular)  is limited private;
   
   -- subtype bounded is modular;
      subtype bounded is modular range 1..9;
      type DT2 (the_size : bounded)  is limited private;
   --                         |
   -- >>> subtype must be compatible with parent discriminant
   
      function is_empty (the_data : DT2) return Boolean;
   
   private
   
      type a_thing is null record;
      type a_ptr   is access a_thing;
      
      type a_ptr_array is array (modular range <>) of a_ptr;
   
      type DT1 (the_size : modular) is
         record
            things : a_ptr_array (1 .. the_size);
         end record;
   
      type DT2 (the_size : bounded)  is new DT1(the_size);
   
   end try;

and I get the error message commented-out at line 11.

If I substitute the declaration at line 9 for that at line 10,
the test program compiles and runs correctly.

Am I blundering here, or is this a GNAT bug?

-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk

Re: Brain bug or GNAT bug?

[Ludovic Brenta]

"(see below)" writes:

> Using GNAT GPL 2006 (PPC/Darwin), I instantiate:
>
>    generic
>    
>       type modular is mod <>;
>    
>    package try is
>    
>       type DT1 (the_size : modular)  is limited private;
>    
>    -- subtype bounded is modular;
>       subtype bounded is modular range 1..9;
>       type DT2 (the_size : bounded)  is limited private;
>    --                         |
>    -- >>> subtype must be compatible with parent discriminant
>
>       function is_empty (the_data : DT2) return Boolean;
>    
>    private
>    
>       type a_thing is null record;
>       type a_ptr   is access a_thing;
>       
>       type a_ptr_array is array (modular range <>) of a_ptr;
>    
>       type DT1 (the_size : modular) is
>          record
>             things : a_ptr_array (1 .. the_size);
>          end record;
>    
>       type DT2 (the_size : bounded)  is new DT1(the_size);
>
>    end try;
>
> and I get the error message commented-out at line 11.
>
> If I substitute the declaration at line 9 for that at line 10,
> the test program compiles and runs correctly.
>
> Am I blundering here, or is this a GNAT bug?

Per ARM 3.7(15), the types of DT1.the_size and DT2.the_size must be
statically compatible.  In other words, you must guarantee at compile
time that "the_size" is in the range of type "modular".  Because
modular's range is not known at compile time but bounded's is, no such
guarantee exists.

If you remove the "range" constraint on subtype "bounded", then the
range for "bounded" and the range of "modular" are known at compile
time to be identical, so all is well.

What are ou trying to achieve?

-- 
Ludovic Brenta.

Re: Brain bug or GNAT bug?

[(see below)]

On 1/3/07 00:11, in article 87irdlx1ol.fsf@ludovic-brenta.org, "Ludovic
Brenta" <ludovic@ludovic-brenta.org> wrote:

>>    generic 
>>       type modular is mod <>;
>>    package try is
>>    
>>       type DT1 (the_size : modular)  is limited private;
>>    
>>    -- subtype bounded is modular;
>>       subtype bounded is modular range 1..9;
>>       type DT2 (the_size : bounded)  is limited private;
>>    --                         |
>>    -- >>> subtype must be compatible with parent discriminant
>> 
>>       function is_empty (the_data : DT2) return Boolean;
>>    
>>    private  
>>       type a_thing is null record;
>>       type a_ptr   is access a_thing;
>>       type a_ptr_array is array (modular range <>) of a_ptr;
>>    
>>       type DT1 (the_size : modular) is
>>          record
>>             things : a_ptr_array (1 .. the_size);
>>          end record;
>>    
>>       type DT2 (the_size : bounded)  is new DT1(the_size);
>>    end try;
>> 
>> and I get the error message commented-out at line 11.
>> 
>> If I substitute the declaration at line 9 for that at line 10,
>> the test program compiles and runs correctly.
>> 
>> Am I blundering here, or is this a GNAT bug?
> 
> Per ARM 3.7(15), the types of DT1.the_size and DT2.the_size must be
> statically compatible.  In other words, you must guarantee at compile
> time that "the_size" is in the range of type "modular".  Because
> modular's range is not known at compile time but bounded's is, no such
> guarantee exists.
> 
> If you remove the "range" constraint on subtype "bounded", then the
> range for "bounded" and the range of "modular" are known at compile
> time to be identical, so all is well.

But if the declaration of bounded compiles,
the range of bounded must be a subset of the range of modular,
so DT2.the_size must be in the range of modular.
The rule at ARM 3.7(15) seems overly restrictive.

> What are ou trying to achieve?

Implement DT2 as a derivation of DT1 with guaranteed bounds on its size
(in the actual s/w, the bounds are also generic parameters,
and DT1 is actually declared in a distinct, with-ed package).

At the moment bounds checking for DT2 has to be done by a runtime
check on use of DT2 objects.

I can't help feeling the type system should be able to catch a misuse,
at the point of declaration of a DT2 object,
but there does not seem any way to do that, thanks to ARM 3.7(15).

-- 
Bill Findlay
<surname><forename> chez blueyonder.co.uk

Re: Brain bug or GNAT bug?

[Jeffrey R. Carter]

(see below) wrote:
> 
>>>    generic 
>>>       type modular is mod <>;
>>>    package try is
>>>    
>>>       type DT1 (the_size : modular)  is limited private;
>>>    
>>>    -- subtype bounded is modular;
>>>       subtype bounded is modular range 1..9;

> But if the declaration of bounded compiles,
> the range of bounded must be a subset of the range of modular,
> so DT2.the_size must be in the range of modular.
> The rule at ARM 3.7(15) seems overly restrictive.

Consider:

with Ada.Command_Line;

procedure Modular_Subtype is
    type Modular is mod 2 ** 32;

    Low  : constant Modular :=
       Modular'Value (Ada.Command_Line.Argument (1) );
    High : constant Modular :=
       Modular'Value (Ada.Command_Line.Argument (2) );

    subtype Mod_Sub is Modular range Low .. High;

    generic -- Modular_Parameter
       type Modular is mod <>;
    package Modular_Parameter is
       subtype Bounded is Modular range 1 .. 9; -- Line 16
    end Modular_Parameter;

    package Instantiation is new Modular_Parameter (Modular => Mod_Sub);
begin -- Modular_Subtype
    null;
end Modular_Subtype;

This compiles (with a warning that Instantiation is not referenced). 
Since the instantiation cannot be checked during compilation, it is 
checked at run time. Here's a sample run:

D:\Code>modular_subtype 10 24

raised CONSTRAINT_ERROR : modular_subtype.adb:16 range check failed

Here's another:

D:\Code>modular_subtype 0 10

D:\Code>

-- 
Jeff Carter
"I unclog my nose towards you."
Monty Python & the Holy Grail
11

Re: Brain bug or GNAT bug?

[Ludovic Brenta]

(see below) writes:
> Ludovic Brenta writes:
>> Per ARM 3.7(15), the types of DT1.the_size and DT2.the_size must be
>> statically compatible.  In other words, you must guarantee at compile
>> time that "the_size" is in the range of type "modular".  Because
>> modular's range is not known at compile time but bounded's is, no such
>> guarantee exists.
>> 
>> If you remove the "range" constraint on subtype "bounded", then the
>> range for "bounded" and the range of "modular" are known at compile
>> time to be identical, so all is well.
>
> But if the declaration of bounded compiles,
> the range of bounded must be a subset of the range of modular,

The compiler doesn't know that, so inserts run-time checks as aptly
illustrated by Jeffrey Carter.

> so DT2.the_size must be in the range of modular.
> The rule at ARM 3.7(15) seems overly restrictive.

The rule implies there must be no run-time checks.  I don't think this
is overly restrictive, since this is exactly what you want as you
explained below.

>> What are ou trying to achieve?
>
> Implement DT2 as a derivation of DT1 with guaranteed bounds on its
> size (in the actual s/w, the bounds are also generic parameters, and
> DT1 is actually declared in a distinct, with-ed package).

Consider that it must be possible to convert explicitly between
related types, i.e. from DT1 to DT2 and back.  What happens if you
want to convert from a DT1 object with unknown bounds to a DT2 with
"guaranteed" but different bounds?  Remember that generic formal
objects are never considered static inside the generic, even if the
actuals for some instantiations happen to be static.

> At the moment bounds checking for DT2 has to be done by a runtime
> check on use of DT2 objects.

Yes, but even with your solution, this is still a run-time check, and
that's illegal for a discriminant used to constrain a parent type.

> I can't help feeling the type system should be able to catch a
> misuse, at the point of declaration of a DT2 object, but there does
> not seem any way to do that, thanks to ARM 3.7(15).

So long as the bounds of DT1 are unknown at compile time, there will
be a run-time check somewhere.  You can make that implicit or
explicit.

I think a possible solution is to not declare DT2 as derived from DT1.
Make the two types independent, and write a conversion function that
takes into account the possible difference in bounds.  For example, it
would convert a DT1 object with unknown bounds into one *or more* DT2
objects with guaranteed bounds.  Actually, make that *zero* or more
DT2 objects.

-- 
Ludovic Brenta.