Re: Brain bug or GNAT bug?

["(see below)" <yaldnif.w@blueyonder.co.uk>]

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