Type inference in loops with immediate constants

Type inference in loops with immediate constants

[Guillaume Foliard]

Hi,

I'm currently chasing down a Constraint_Error exception and while I was
reading one loop statement I wondered about the type inference in such a
place. Here is the snippet :

---

Length : Positive; -- reminder : subtype Integer range 1 .. Integer'Last

for Index in 0 .. Length - 1 loop

---

Then what type Index should be ?

Positive ?

Obviously not, because of the 0, which is not a Positive, as a starting
value.

Integer ?

Is the compiler using the fact that a positive is derived from an universal
integer and thus decides to give the base type to the loop variable ?

-- 
Guillaume

Re: Type inference in loops with immediate constants

[Jeffrey Carter]

Guillaume Foliard wrote:
> 
> Length : Positive; -- reminder : subtype Integer range 1 .. Integer'Last
> 
> for Index in 0 .. Length - 1 loop
> 
> Then what type Index should be ?

Positive is a subtype of Integer, so any expressions including Length 
have type Integer, so Index has type Integer. A discrete range can be 
considered (informally; language lawyers will get more specific if you 
like, and sometimes even if you don't like :) an expression, so in

for Index in 0 .. Length loop

Index will also have type Integer. Finally, in a for loop, a numeric 
range with a universal type yields a loop constant with type Integer. In 
other words, given something like

for Index in 1 .. A'Length loop

Index has type Integer.

-- 
Jeff Carter
"When Roman engineers built a bridge, they had to stand under it
while the first legion marched across. If programmers today
worked under similar ground rules, they might well find
themselves getting much more interested in Ada!"
Robert Dewar

Re: Type inference in loops with immediate constants

[christoph.grein]

> Length : Positive; -- reminder : subtype Integer range 1 .. Integer'Last
>
> for Index in 0 .. Length - 1 loop
>
> ---
>
> Then what type Index should be ?
>
> Positive ?
>
> Obviously not, because of the 0, which is not a Positive, as a starting
> value.
>
> Integer ?
>
> Is the compiler using the fact that a positive is derived from an universal
> integer and thus decides to give the base type to the loop variable ?

Note that Positive is not a type, but a subtype of Integer. So Index is of type 
Integer with a constraint of 0 .. Length -1.