[feature] Refer to the loop index in a *for .. of* loop

[clairedross]

Summary

A new attribute, possibly called Loop_Index, could be defined for the parameter of a for .. of loop to get the underlying index/cursor. Ideally, this would work both for loops over arrays, and loops using the Iterable aspect.

   procedure Do_Loop_1 (A : in out My_Array) is
   begin
      for E of A loop
         E := E + 1;
         pragma Loop_Invariant
           (for all K in A'First .. E'Loop_Index => A (I) = A'Loop_Entry (I) + 1);
      end loop;
   end Do_Loop_1;

   procedure Do_Loop_2 (S : in out My_Sequence) is
      C : Big_Natural := 0;
   begin
      for E of S loop
         if E = 0 then
           C := C + 1;
         end if;
         pragma Loop_Invariant (C <= E'Loop_Index);
      end loop;
   end Do_Loop_2;

Motivation

Currently, it is not possible to use for .. of loops in SPARK most of the time, as loop invariants generally need to refer to the underlying loop index/cursor etc. This is a shame as arguably for .. of loops are easier to read for programmers.

Caveats and alternatives

TBD

[raph-amiard]

I think this looks very reasonable. It's a bit frustrating to not be able to do a more elegant thing involving possibly tuples and unpacking, as it is done in many other languages.

I'm not sure it would be reasonable in Ada just because the involved effort is much larger, but I think it would be good to exhaust other ways (on paper of course), to justify that this is the best one for us.

[mosteo]

I seem to remember a syntactic sugar AI proposal in which you did

for (Key, Value) in Collection.Iterate loop

where Iterate is the already existing subprogram in e.g. standard Maps.

[clairedross]

I seem to remember a syntactic sugar AI proposal in which you did

for (Key, Value) in Collection.Iterate loop
where Iterate is the already existing subprogram in e.g. standard Maps.

Yes, it is the kind of alternative @raph-amiard is referring to above I think. I suspect it might be more complicated to support due to the problem of typing the pair in particular. Basically, it would require adding a new syntax in Ada whereas the syntax proposed in the RFC has the advantage of only needing a new attribute. It is more common as an extension.

[sttaft]

I seem to remember a syntactic sugar AI proposal in which you did

for (Key, Value) in Collection.Iterate loop

where Iterate is the already existing subprogram in e.g. standard Maps.

This syntax is consistent with the Ada 2022 syntax for Procedural Iterators, so would seem worth further investigation. See RM 5.5.3, with example:

for (Name, Val) of Ada.Environment_Variables.Iterate(<>) loop
   --  "(<>)" is optional because it is the last parameter
   Put_Line (Name & " => " & Val);
end loop;

[clairedross]

Are procedural iterators already supported in GNAT? If so, I have no strong preference either ways.

[sttaft]

Are procedural iterators already supported in GNAT? If so, I have no strong preference either ways.

I don't believe they have been implemented yet, but this might be the impetus they need.
-Tuck