[RFC] constrained indefinite arrays

[jklmnn]

https://github.com/jklmnn/ada-spark-rfcs/blob/static_arrays/considered/definite_unconstrained_arrays.md

[raph-amiard]

Can you please add a (more thorough) example to your RFC ? Even though it's pretty simple, examples go a long way.

[raph-amiard]

A few more comments:

• WRT. naming, I think it needs to be clear that this feature is part of the same family as the Max_Size for tagged types. It's not really the case so far, so we need to unify the naming somehow
• It feels to me like being able to create singleton arrays rather than types might be explored too. WDYT ?

You say:

Whether the behaviour of arrays with this aspect is different from regular arrays

Clearly the answer is yes. It needs to, because even assigning an aggregate of the wrong size to a regular constrained array will trigger a C_E. As you can see from the internal discussion on W104-022, we will also probably need additional rules since the size of those arrays can change:

type Arr is array (1 .. 32) of Integer with Constrained;

Inst : Arr := (1, 2, 3, 4);

R : Integer renames Arr (4);

Inst := (1, 2);

--  ??? R

[jklmnn]

Clearly the answer is yes. It needs to, because even assigning an aggregate of the wrong size to a regular constrained array will trigger a C_E.

What would prevent us to do the same on a constrained array? Just because it would fit into the allocated memory doesn't mean that it cannot trigger a C_E. The features that are technically possible are a superset of what currently can be done with arrays. Nothing prevents us from saying we want to restrict that feature set to what is currently available.

My question is not intended to test the technical feasibility but rather if we want to have these improved features or not.

It feels to me like being able to create singleton arrays rather than types might be explored too. WDYT ?

What do you mean by that? Anonymous arrays? One intention of this feature is to use these arrays as return types in functions to avoid needing the secondary stack. I don't see how anonymous types would help here.

[raph-amiard]

What would prevent us to do the same on a constrained array? Just because it would fit into the allocated memory doesn't mean that it cannot trigger a C_E. The features that are technically possible are a superset of what currently can be done with arrays. Nothing prevents us from saying we want to restrict that feature set to what is currently available.

I think the answer is that it would make this new feature pretty useless. The whole point of having this is being able to treat this like a box to an array that you can modify, or at the very least set the length freely at initialization.

We also want some consistency with the other features we're going to link it with conceptually, namely Max_Size tagged types, and discriminated records with default values.

[jklmnn]

I think the answer is that it would make this new feature pretty useless. The whole point of having this is being able to treat this like a box to an array that you can modify, or at the very least set the length freely at initialization.

I think we're coming from different assumptions here. The intent of my initial draft was not to treat it like a box but explicitly treat it like a regular array. The usefulness of the feature is solely in its different behavior in terms of runtime support (namely that it doesn't require any secondary stack support).

[jklmnn]

I improved the example and added some clarifications about the behavior. I also renamed it to Definite Unconstrained Arrays.