Deep delta aggregates

[danhettena-nvidia]

Summary

Analogous to the TLA+ EXCEPT operator (see https://lamport.azurewebsites.net/tla/book-21-07-04.pdf, section 5.2), enhance Ada delta aggregates to support updates to components of components, components of components of components, etc.

The following example demonstrates the capability, but not necessarily the best language design choice for the syntax.

This hypothetical syntax (which, again, is not necessarily the best syntax; that should be debated):

base_expression with delta '(' choice_expression1 ')' '.' component_selector_name1 '(' choice_expression2 ')' '.' component_selector_name2 => expression

Would be equivalent to this:

base_expression with delta choice_expression1 => base_expression '(' choice_expression1 ')' with delta component_selector_name1 => base_expression (' choice_expression1 ')' '.' component_selector_name1 with delta choice_expression2 => base_expression (' choice_expression1 ')' '.' component_selector_name1 '(' choice_expression2 ')' **with delta component_selector_name2 => expression

Motivation

When using SPARK to specify procedures that modify just one state variable inside a nested data structure such as shown above, one delta aggregate expression is substantially easier to comprehend than a sequence of delta expressions.

Caveats and alternatives

(1) The syntax would need to be debated. In particular, my suggestion above to use parentheses to wrap choice expressions is suspect.

(2) I have not thought through whether all current features of delta aggregates fit neatly with the proposed feature. For example, I am unclear on whether a component_choice_list with multiple component_selector_names should be supported in combination with the proposed feature.

[sttaft]

This could have the advantage of helping to unify record and array delta aggregates, and include support for multi-dimensional arrays, which were omitted from the first version of array delta aggregates. The BNF for this could become:

delta_aggregate ::= (base_expression with delta delta_subcomponent_association_list)

delta_subcomponent_association_list ::= delta_subcomponent_association {, delta_subcomponent_association}

delta_subcomponent_association ::=
    delta_subcomponent_choice_list => expression
  | discrete_choice_list => expression
  | iterated_component_association

delta_subcomponent_choice_list ::= delta_subcomponent_choice {'|' delta_subcomponent_choice}

delta_subcomponent_choice ::=
   (expression {, expression})
  | component_selector_name
  | delta_subcomponent_choice (expression {, expression)
  | delta_subcomponent_choice . component_selector_name

The discrete_choice_list and iterated_component_association would only be usable for single-dimension arrays. The more general delta_subcomponent_choice-based syntax could be used for both arrays and records.

[yannickmoy]

@sttaft I guess you'll want to preserve the syntax with square brackets [..] for array delta aggregates, as this is currently allowed by the syntax of Ada 2022: http://www.ada-auth.org/standards/2xrm/html/RM-4-3-4.html

I agree that the syntax that you propose looks natural, and seems to solve the issue that was bothering @danhettena-nvidia