diff --git a/rfc-template.md b/rfc-template.md deleted file mode 100644 index 32efa48a..00000000 --- a/rfc-template.md +++ /dev/null @@ -1,122 +0,0 @@ -- Feature Name: (fill me in with a unique ident, my_awesome_feature) -- Start Date: (fill me in with today's date, YYYY-MM-DD) -- RFC PR: (leave this empty) -- RFC Issue: (leave this empty) - -Summary -======= - -One paragraph explanation of the feature. - -Motivation -========== - -Why are we doing this? What use cases does it support? What is the expected -outcome? - -Guide-level explanation -======================= - -Explain the proposal as if it was already included in the language and you were -teaching it to another Ada/SPARK programmer. That generally means: - -- Introducing new named concepts. - -- Explaining the feature largely in terms of examples. - -- Explaining how Ada/SPARK programmers should *think* about the feature, and - how it should impact the way they use it. It should explain the impact as - concretely as possible. - -- If applicable, provide sample error messages, deprecation warnings, or - migration guidance. - -For implementation-oriented RFCs (e.g. for RFCS that have no or little -user-facing impact), this section should focus on how compiler contributors -should think about the change, and give examples of its concrete impact. - -For "bug-fixes" RFCs, this section should explain briefly the bug and why it -matters. - -Reference-level explanation -=========================== - -This is the technical portion of the RFC. Explain the design in sufficient -detail that: - -- Its interaction with other features is clear. -- It is reasonably clear how the feature would be implemented. -- Corner cases are dissected by example. - -The section should return to the examples given in the previous section, and -explain more fully how the detailed proposal makes those examples work. - -Rationale and alternatives -========================== - -- Why is this design the best in the space of possible designs? -- What other designs have been considered and what is the rationale for not - choosing them? -- What is the impact of not doing this? -- How does this feature meshes with the general philosophy of the languages ? - -Drawbacks -========= - -Why should we *not* do this? - -Prior art -========= - -Discuss prior art, both the good and the bad, in relation to this proposal. - -- For language, library, and compiler proposals: Does this feature exist in - other programming languages and what experience have their community had? - -- Papers: Are there any published papers or great posts that discuss this? If - you have some relevant papers to refer to, this can serve as a more detailed - theoretical background. - -This section is intended to encourage you as an author to think about the -lessons from other languages, provide readers of your RFC with a fuller -picture. - -If there is no prior art, that is fine - your ideas are interesting to us -whether they are brand new or if it is an adaptation from other languages. - -Note that while precedent set by other languages is some motivation, it does -not on its own motivate an RFC. - -Unresolved questions -==================== - -- What parts of the design do you expect to resolve through the RFC process - before this gets merged? - -- What parts of the design do you expect to resolve through the implementation - of this feature before stabilization? - -- What related issues do you consider out of scope for this RFC that could be - addressed in the future independently of the solution that comes out of this - RFC? - -Future possibilities -==================== - -Think about what the natural extension and evolution of your proposal would -be and how it would affect the language and project as a whole in a holistic -way. Try to use this section as a tool to more fully consider all possible -interactions with the project and language in your proposal. -Also consider how the this all fits into the roadmap for the project -and of the relevant sub-team. - -This is also a good place to "dump ideas", if they are out of scope for the -RFC you are writing but otherwise related. - -If you have tried and cannot think of any future possibilities, -you may simply state that you cannot think of anything. - -Note that having something written down in the future-possibilities section -is not a reason to accept the current or a future RFC; such notes should be -in the section on motivation or rationale in this or subsequent RFCs. -The section merely provides additional information. diff --git a/topic/rfc-deep-delta-aggregates.md b/topic/rfc-deep-delta-aggregates.md new file mode 100644 index 00000000..3fa15ebf --- /dev/null +++ b/topic/rfc-deep-delta-aggregates.md @@ -0,0 +1,168 @@ +- Feature Name: Deep Delta Aggregates +- Start Date: 2021-10-07 +- RFC PR: (leave this empty) +- RFC Issue: (leave this empty) + +Summary +======= + +Delta aggregates should allow the update of individual subcomponents rather than only entire components + +Motivation +========== + +Early users of delta aggregates, and users of the former 'Update feature of SPARK +have noticed a periodic need to update an individual subcomponent (e.g. X.A.B) rather +than an entire component (e.g. X.A). This can be accomplished by a series of +nested delta aggregates, but it seems more straightforward to support a syntax +that allows the direct update of an individual subcomponent of an enclosing object. + +Guide-level explanation +======================= + +Delta aggregates allow the construction of a new object of a composite type +by taking a base object, and specifying new values for some of the components. +This proposal would allow the specification of a new value for a subcomponent, +rather than an entire component, using a generalization of the current +syntax, such as: + + (X with delta A.B => 42) + +This would be approximately equivalent to: + + (X with delta A => (X.A with delta B => 42)) + +but would presumably involve fewer copies. + +More generally a delta aggregate can be seen as equivalent to the creation of a copy +of the base object, and then a sequence of assignments to some of the *components* +of the copy. This feature generalizes that to be a sequence of assignments +to some of the *subcomponents* of the copy. + +This generalization also permits a more general notation for updating +subcomponents of arrays, including multi-dimensional arrays: + + (A with delta B.C(1,2) => 5, D(3,True) => 7) + +or for the case where the base object is itself an array: + + [O with delta (6).G => 11, 5 => (G => 3, H => 4), for I in 2..4 => (G => 7, H => I*2)] + +including a multi-dimensional case: + + [M with delta (1, 3) => 77, (2, 5) => 88] + +Reference-level explanation +=========================== + +The syntax for delta_aggregate (see RM 4.3.4) is revised as follows: + +``` +delta_aggregate ::= record_delta_aggregate | array_delta_aggregate + +record_delta_aggregate ::= + ( base_expression with delta record_subcomponent_association_list ) + +record_subcomponent_association_list ::= + record_subcomponent_association {, record_subcomponent_association} + +record_subcomponent_association ::= + record_subcomponent_choice_list => expression + +record_subcomponent_choice_list ::= + record_subcomponent_choice {'|' record_subcomponent_choice} + +record_subcomponent_choice ::= + component_selector_name + | record_subcomponent_choice (expression {, expression) + | record_subcomponent_choice . component_selector_name + +array_delta_aggregate ::= + ( base_expression with delta array_subcomponent_association_list ) + | '[' base_expression with delta array_subcomponent_association_list ']' + +array_subcomponent_association_list ::= + array_subcomponent_association {, array_subcomponent_association} + +array_subcomponent_association ::= + discrete_choice_list => expression + | iterated_component_association + | array_subcomponent_choice_list => expression + +array_subcomponent_choice_list ::= + array_subcomponent_choice {'|' array_subcomponent_choice} + +array_subcomponent_choice ::= + ( expression {, expression} ) + | array_subcomponent_choice (expression {, expression) + | array_subcomponent_choice . component_selector_name +``` + +This revised syntax is a superset of the existing delta_aggregate syntax. +It provides for multi-dimensional arrays, and for subcomponent selection, +to support updates to the components of both nested arrays and nested records. + +This legality rule from RM 4.3.1(16/5): +> For a record_delta_aggregate, each component_selector_name of each component_choice_list shall denote a distinct nondiscriminant component of the type of the aggregate + +is removed, and a new legality rule in RM 4.3.4 is added: +> For a record_delta_aggregate, no two record_subcomponent_choices that consist of only component_selector_names, shall be the same sequence of selector_names. + +In addition, the dynamic semantics of RM 4.3.4(15/5-21/5) are changed as follows: + +>For a delta_aggregate, for each discrete_choice or each subcomponent associated with a record_ or array_subcomponent_association (in the order given in the enclosing discrete_choice_list or subcomponent_association_list, respectively): +> * if the associated subcomponent belongs to a variant, a check is made that the values of the governing discriminants are such that the anonymous object has this component. The exception Constraint_Error is raised if this check fails. +> * if the associated subcomponent is a subcomponent of an array, then for each represented index value (in ascending order, if the discrete_choice represents a range): +> * the index value is converted to the index type of the array type. +> * a check is made that the index value belongs to the index range of the corresponding array part of the anonymous object; Constraint_Error is raised if this check fails. +> * the expression of the record_ or array_subcomponent_association is evaluated, converted to the nominal subtype of the associated subcomponent, and assigned to the corresponding subcomponent of the anonymous object. + +Rationale and alternatives +========================== + +This is a generalization of the existing delta_aggregate syntax, and in fact unifies record and array +delta aggregates to some degree, while preserving the ability to identify array components simply by their index value if desired. +Note that there is syntactic ambiguity for single-dimensional arrays, since the choices in a discrete choice list may individually be parenthesized, as in: + + [X with delta (1)|(2)|(3) => 55] + +This is a benign syntactic ambiguity, since the semantics are the same. It would be possible to eliminate this ambiguity with a more +complex BNF, but that would probably not increase understandability. + +Drawbacks +========= + +This clearly adds complexity to delta aggregates, but seems like an "intuitive" extension if the programmer +makes the connection to a series of assignments to subcomponents. + +Prior art +========= + +Not sure what are the other languages that provide this capability, though it has been indicated +that the TLA+ "EXCEPT" operator has this feature. + +Unresolved questions +==================== + +It has been indicated that SPARK may have some trouble with transforming this feature to Why3. + +Future possibilities +==================== + +This could conceivably be generalized to allow operations other than assignments to be applied +to the "anonymous object" that is a copy of the base object, thereby generalizing it to work +on private types. E.g.: + + (Empty_Stack with delta Push(5), Push(7)) + +being defined as equivalent to: + +``` + X : Stack_Type := Empty_Stack; + begin + X.Push(5); + X.Push(7); + return X; +``` + +At some point it might make better sense to declare a ghost function to do this, presuming it can be inlined for proof.