[feature] Proposal for a ghost Loop_Index attribute

[tonunaks]

Summary

This RFC introduces a new ghost attribute, called Loop_Index,
that can be applied to the loop parameter of a generalized iterator to get the
underlying index or cursor.

Motivation

Currently, it is often not possible to use array component iterators and
container element iterators in loops in SPARK as loop invariants generally need
to refer to the underlying loop index or cursor.
It would be possible to use the ghost attribute Loop_Index inside the pragma
Loop_Invariant or Loop_Variant of loops with array component iterators
or container element iterators, making it possible to use this pattern in SPARK.
This feature should work both for array component iterators and for container
element iterators based on the Iterable aspect.
It should be executable when ghost code is enabled.

Caveats and alternatives

TBD

[sttaft]

The attribute name "Loop_Index" might be confusing. I would suggest "Component_Index" as being a bit clearer, since the prefix is denoting a component of the array or the container, and the user wants the associated "index" into the array or container.

For example:

      for E of Arr loop
          Put_Line ("A component with value " & E'Image &
             " was found at location " & E'Component_Index'Image);
      end loop;

For multidimensional arrays, it would be consistent to use E'Component_Index(N) where N is the dimension, similar to Arr'Range(N).

I see this as a generally useful feature, given that Ada iterators only provide the component and not the index. There have been other requests for being able to get the component's index, and this seems like a simple way to do so without defining a new syntactic variant of loop iterators.

[Nikokrock]

Cursor is probably a better word than Index. Why not introduce a syntax like this:

for Cursor, Element of Arr loop
    [...]
end loop

If necessary an optional function could declared as an aspect in order to be able to transform the Cursor in something else (might be handy for example for hash maps to just return the key rather than the cursor)

[sttaft]

Cursor is probably a better word than Index.

There is now an ARG issue discussing this idea, using the attribute name Component_Index. See Ada-Rapporteur-Group/User-Community-Input#145

Why not introduce a syntax like this:

for Cursor, Element of Arr loop
    [...]
end loop

We considered this during Ada 2022. We considered a syntax such as:

for [Key => Value] of Arr loop

We also suggested using the Procedural Iterator for this purpose, as illustrated in RM 5.5.3(35/5):

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

If necessary an optional function could declared as an aspect in order to be able to transform the Cursor in something else (might be handy for example for hash maps to just return the key rather than the cursor)

Agreed. There would probably need to be an additional aspect to specify what function of the Cursor would return the Component_Index/Cursor/Key.

[clairedross]

I understand the interest in having a nice syntax, but ideally, the development effort should remain consistent with the scope of the feature. This is in no way a proposal for a new syntax for loops that would allow quick access to both the element and the cursor. It is a minor enhancement to allow users to use loops on array components (and containers) in SPARK.

[Nikokrock]

I understand but the current proposed use of an attribute of the element attach "loop property" to the returned element which is a bit weird from my point of view.

[clairedross]

I am happy with other ideas, but let's not make this anything more than it is, or we risk simply never getting to do it.