What does "for I: some_type loop" do

[evanescente-ondine]

Hi, I found this construct that I didn’t know existed in Ada:

for I : Character loop
	put_line ("a");
--	put_line (I'Image);
end loop;

I knew you could indicate the subtype but now without the “in” or “of” part. Then I thought it would be identical to “for I in Character”… but no, you can’t access I from within and it in fact doesn’t do anything, it’s equal to a plain “loop”. Looks one hell of a blunder that should go away from the language. Either make it synonymous with “in …” or remove it…

[Nordic_Dogsledding]

This is not RM syntax; must be an AdaCore invention. See RM 5.5.

[evanescente-ondine]

Well I did and found the syntax element called multiple references to iterator_specification, so I thought it was it, but I see now 5.5.2 explains it. Weird, usually gnat’s extensions are somewhat functional, this one looks like a glitch. The expression version only creates bug so I can’t really compare. It seems to function only in contracts ? You can find it in spark 2014 guide:

(for all I : Positive =>
   (if I in 1 .. Length (Model (Init'Result)) then
      Get (Model (Init'Result), I) = E));

While here B: boolean := (for all I : Character => (if I in 'a'..'b' then I = I)); says “I in undefined”, while not mentioning the index makes it crash: try put B: boolean := (for some E: Char => Char'('d') = Char'('d')); anywhere.

[OneWingedShark]

@evanescente-ondine

for I : Character loop
	put_line ("a");
--	put_line (I'Image);
end loop;

This is the same as saying:
For C in Character'Range loop.

EDIT: I may be misremembering; there is a form where the subtype indication is given in the for loop… something like For X in Character : range 1..3 loop, or something similar. (I haven’t used this form much; I haven’t needed it, but I remember it.)`

[sttaft]

I don’t know what compiler you are using, but that is not legal Ada (I sometimes call such things “Aint’a” ;-). You are allowed to give a subtype for the loop parameter, but you still need to follow it with either “in <discrete_range>” or “of ”.

[evanescente-ondine]

Yes, I know this makes no sense. Don’t blame me, I use gnat_native_14.2.1_06bb3d, straight from alire. I didn’t come up with it, the Spark user guide did, in the link I gave. Try it on compiler explorer. Unfortunately it includes only versions of gnat.

[zertovitch]

procedure Hello is
begin
  for c : Character loop
    null;
    --  if c = ' ' then null; else null; end if;  --  Error: "c" is undefined
  end loop;
end Hello;

The above compiles with:

• gcc version 6.3.1 20170510 (for GNAT GPL 2017 20170515) (GCC)
• gcc version 10.3.1 20210520 (for GNAT Community 2021 20210519) (GCC)

Interesting!..

With an old Ada 95 GNAT:

• gcc version 2.8.1 (GNAT 3.15p)

I get: hello.adb:3:08: missing “in”

[zertovitch]

@OneWingedShark

EDIT: I may be misremembering; there is a form where the subtype indication is given in the for loop… something like For X in Character : range 1..3 loop, or something similar. (I haven’t used this form much; I haven’t needed it, but I remember it.)`

Probably you mean for c in Character range 'a' .. 'b' loop.
Regarding characters specifically, it is practical if you prefer using Wide_Character for instance.

You can also write for c in Wide_Character'('a') .. 'b' loop
I like this form less.

[JC001]

@zertovitch

@OneWingedShark

EDIT: I may be misremembering; there is a form where the subtype indication is given in the for loop… something like For X in Character : range 1..3 loop, or something similar. (I haven’t used this form much; I haven’t needed it, but I remember it.)`

Probably you mean for c in Character range 'a' .. 'b' loop.

ISO/IEC 8652: 2023 added

for C : Character in 'a' .. 'b' loop

and

for C : Character of Digit loop

Since the reported construct is not valid Ada and compiles with many versions of GNAT (including 14.2.0 and Godbolt “trunk”) without specifying the use of GNAT extensions, this is a compiler error. Probably its use in the SPARK guide is also an error.

[evanescente-ondine]

An error also in Gnatprove ! I’ll redact a bug report and ask the spark team. Also I don’t know where you got

for C : Character in 'a' .. 'b' loop

but it’s currently invalid:

main.adb:11:17: error: subtype indication is only legal on an element iterator
main.adb:11:27: error: extra “in” ignored

[ksson]

Those snippets in the SPARK UG aren’t supposed to be real code, but logical formulas, so a non-Ada syntax was deliberately chosen. I understand how it can be confusing. We will see if we can improve this part of the manual.

[JC001]

@evanescente-ondine

Also I don’t know where you got

for C : Character in 'a' .. 'b' loop

Sorry, you’re right. With a subtype and in, you have to give an iterator name:

for C : Character in Iterator loop

[evanescente-ondine]

So it’s not “real code”, huh ? Or is it valid only in contracts ? Yes, confusing it is… But forget the UG, why does GNAT not scream ?

[ksson]

It’s not valid code, and not valid in contracts. It’s just there to illustrate what happens in the tool internally.
The fact that GNAT (half) accepts the syntax is a bug.

[Irvise]

Reading http://www.ada-auth.org/standards/22over/Ada2022-Overview.pdf

I found in section 4.3:

4.3 Use subtype_indication in generalized iterators
Ada 2012 added the ability to simplify:

Vec : Int_Vectors.Vector;
...
for I in Vec.Iterate loop
Vec(I) := Vec(I) + 1;
end loop;

to:

Vec : Int_Vectors.Vector;
...
for E : T of Vec loop
E := E + 1;
end loop;

where the optional : T acts as a comment to the reader that the subtype of element E is T (and the
compiler verifies this comment). Use subtype_indication in generalized iterators (AI12-0156) allows an
optional subtype indication – though of the cursor not the element – to be given for the original in form of
a for loop (see RM 5.5.2), i.e.:

for I : Index in Vec.Iterate loop
Vec(I) := Vec(I) + 1;
end loop;

where Index is the subtype of the loop parameter.

So maybe it is somewhat correct?