CVS difference for ai12s/ai12-0127-1.txt

Differences between 1.6 and version 1.7
Log of other versions for file ai12s/ai12-0127-1.txt

--- ai12s/ai12-0127-1.txt	2016/07/12 02:36:46	1.6
+++ ai12s/ai12-0127-1.txt	2016/10/03 04:58:43	1.7
@@ -1,4 +1,8 @@
-!standard A.3.4                                     16-06-07    AI12-0127-1/03
+!standard 4.3(2)                                    16-09-29    AI12-0127-1/04
+!standard 4.3(4)
+!standard 4.3.3(3)
+!standard 4.3.4(0)
+!standard 7.5(2.10/3)
 !class Amendment 14-08-21
 !status work item 14-08-21
 !status received 14-07-14
@@ -93,31 +97,18 @@
 
 4.3.4 Delta Aggregates
 
-A (record, array, multidimensional) delta aggregate yields a
-composite value resulting from copying another value of the same type and
-then subsequently assigning to some (but typically not all) components of
-the copy.
+A (record or array) delta aggregate yields a composite value resulting from
+copying another value of the same type and then subsequently assigning to
+some (but typically not all) components of the copy.
 
 Syntax
 
   delta_aggregate ::= (*base_*expression with delta delta_aggregate_association)
 
   delta_aggregate_association ::=
-    record_component_association_list                 |
-    array_component_association_list                  |
-    multidimensional_array_component_association_list
+    record_component_association_list |
+    array_component_association_list
 
-  multidimensional_array_component_association_list ::=
-    multidimensional_array_component_association
-    {, multidimensional_array_component_association}
-
-  multidimensional_array_component_association ::=
-    index_tuple_list => expression
-
-  index_tuple_list ::= index_tuple { | index_tuple }
-
-  index_tuple ::= ( expression, expression {, expression} )
-
 Name Resolution Rules
 
 The expected type for a delta_aggregate shall be a single array type, record
@@ -126,25 +117,19 @@
 
 The expected type for expression in a delta_aggregate depends on which form
 of delta_aggregate_association is used: a record type for
-record_component_association_list, and an array type for
-array_component_association_list or
-multidimensional_array_component_association_list.
+record_component_association_list, and a one-dimensional array type for
+array_component_association_list.
+
+For record delta aggregates, the expected type and applicable index constraint
+of the expression in each record_component_association is defined as for a
+record_component_association occurring within a record aggregate.
 
-For record delta aggregates, the expected type and applicable index
-constraint of the expression in each record_component_association is
-defined as for a record_component_association occurring within a record
-aggregate.
-
-For array delta aggregates, the expected type for each discrete_choice in
-an array_component_association is the index type of type of the delta
-aggregate. For a multidimensional delta aggregate, the expected type for
-each expression in index_tuple is the corresponding index type of the type
-of the delta aggregate.
+For array delta aggregates, the expected type for each discrete_choice in an
+array_component_association is the index type of type of the delta aggregate.
 
 The expected type and applicable index constraint of the expression in
-array_component_association or multidimensional_array_component_association
-is defined as for an array_component_association occurring within an array
-aggregate of the type of the delta aggregate.
+array_component_association is defined as for an array_component_association
+occurring within an array aggregate of the type of the delta aggregate.
 
 Legality rules
 
@@ -163,17 +148,10 @@
 the box symbol <>, and the discrete_choice shall not be others.
 
 For an array delta aggregate, the dimensionality of the type of the delta
-aggregate shall be 1; for a multidimensional delta aggregate the
-dimensionality of the type of the delta aggregate shall more than 1.
+aggregate shall be 1.
 
-For a multidimensional delta aggregate, the length of each
-index_tuple shall equal the dimensionality of the type of the delta
-aggregate.
-
-For a delta aggregate the expression in a record_component_association, a
-array_component_association, or a
-multidimensional_array_component_association shall not be of a limited
-type.
+For a delta aggregate the expression in a record_component_association or a
+array_component_association shall not be of a limited type.
 
 Dynamic Semantics
 
@@ -190,12 +168,12 @@
 operation. As with any aggregate, evaluation of a delta aggregate then
 denotes the associated anonymous object.
 
-Ramification: As with 'Old, this means that the underlying tag (if any)
+AARM Ramification: As with 'Old, this means that the underlying tag (if any)
 associated with the delta aggregate is that of the expression in
 delta_aggregate and not that of the nominal type of the expression in
 delta_aggregate.
 
-To be honest: the anonymous object associated with the evaluation of a
+AARM To be honest: the anonymous object associated with the evaluation of a
 delta aggregate begins its life as a variable, not a constant (Ada RM 3.3
 notwithstanding). This must be the case because the object is initialized
 and then subsequently modified. After evaluation of the delta aggregate is
@@ -205,28 +183,21 @@
 via "build in place".
 
 For a record delta aggregate, the order of the subsequent assignments is
-unspecified. For a delta aggregate of a (one-dimensional or
-multi-dimensional) array type, the subsequent assignments (including all
-associated expression evaluations) are performed in the order in which the
-array_component_association_list or
-multidimensional_array_component_association_list is given; within a single
-array_component_association, in the order of the discrete_choice_list; and
-within the range of a single discrete_choice, in ascending order.
-
-The expressions within an index_tuple are evaluated in an arbitrary order.
-For each assignment to a component, the the target component name
-(including the evaluation of any index expressions) and expression to be
-assigned are evaluated in an arbitrary order.
+unspecified. For an array delta aggregate, the subsequent assignments
+(including all associated expression evaluations) are performed in the
+order in which the array_component_association_list is given; within a
+single array_component_association, in the order of the discrete_choice_list;
+and within the range of a single discrete_choice, in ascending order.
 
 Examples
 
-  Post => X = (X'Old with delta Foo => 12, Bar | Baz => 42)
+  Post => D = (D'Old with delta Day => 12)
   --  Use in a postcondition.
 
-  N := (Merge (A, B) with delta Relevant => True)
+  N := (Min_Cell (L) with delta Value => 42);
   --  Expression can be more than just an a simple object reference.
 
-  R := ((R with delta F1 => False) with delta F2 => True);
+  R := ((D with delta Day => 12) with delta Day => 42);
   --  These aggregates can be nested arbitrarily.
 
   function Translate (P : Point'Class; X, Y : Float) return Point'Class
@@ -237,38 +208,9 @@
   Post => V = (V'Old with delta A .. B => 42, V'First => 0);
   --  Example of an array delta aggregate.
 
-  A1 := ((1, 2, 3) with delta F (X) => Y);
+  A1 := ((1, 2, 3) with delta Integer (Random * 3.0) => Y);
   --  Combining an aggregate with a delta aggregate
 
-  A2 := ((True => 1, False => 2) with delta
-           (for all I in Integer range X .. Y => G (I)) => 3,
-           (R with delta Field => True).Field           => 4);
-  --  When the index type is Boolean, this can get very interesting. Also
-  --  note that we can access components of a delta aggregate.
-
-  Null_Node_Attributes : constant V_Attributes :=
-    (Null_Attributes with delta Is_Null_Node    => True,
-                                Is_Program_Node => True);
-  --  This is an example from the SPARK 2014 source code, where we define a
-  --  similar (but slightly different) constant to a huge record in a
-  --  compact way.
-
-  A := (A with delta (1, 1, 1) | (2, 2, 2) => 1);
-  --  Simple example of a multidimensional array delta aggregate.
-
-  R : constant Partially_Limited := (Constructor with delta
-                                       Non_Limited_Field => 123);
-  --  Example where we update non-limited components of a record with at
-  --  least one limited component.
-
-  function F (R : T) return Int is
-     function Do_Dispatch (R : T) return Int is (Dispatching_Op (T'Class (R)));
-  begin
-     return Do_Dispatch (R with delta X => 1);
-  end F;
-  -- Calls the same procedure as Do_Dispatch (R) since the underlying tag
-  -- will not have changed.
-
 Add after 7.5(2.10/3):
 
 * the expression of a delta_aggregate (see 4.3.4)
@@ -284,82 +226,6 @@
 resolution, and the like to apply. Additionally, by using aggregate notation,
 we can reuse some of the existing definitions for aggregate elements.
 
----
-
-Ranges in multidimensional updates
-----------------------------------
-
-This is a optional proposal to allow more helpful (but slightly more complex)
-multidimensional delta aggregates. It is presented as a modification to the
-above !wording section.
-
-
-4.3.4 Delta Aggregates
-
-Syntax
-
--- e discrete_choice_list instead of expression:
-
-  index_tuple ::= ( discrete_choice_list {, discrete_choice_list} )
-
-Name Resulution Rules
-
--- to:
-
-For array delta aggregates, the expected type for each discrete_choice in
-an array_component_association is the index type of type of the delta
-aggregate. For a multidimensional delta aggregate, the expected type for
-each discrete_choice in index_tuple is the corresponding index type of the
-type of the delta aggregate.
-
-Legality Rules
-
--- h (yes, this adds back "others").
-
-For an array delta aggregate, the array_component_association shall not use
-the box symbol <>. For an array or multidimensional delta aggregate the
-discrete_choice shall not be others.
-
-Dynamic Semantics
-
--- to:
-
-The discrete_choices within an index_tuple are evaluated in an arbitrary
-order. For each assignment to a component, the the target component name
-(including the evaluation of any index expressions) and expression to be
-assigned are evaluated in an arbitrary order.
-
--- 
-
-For a multidimensional delta aggregate the expression is assigned to any
-combination of indicies that any of the discrete_choice_lists cover (see
-3.8.1). [You can think of this as nested iteration. For a 2D array we
-iterate over all values covered by the first discrete_choice_list, and
-inside this loop we iterate over all values covered by the second.]
-
-Examples
-
--- le:
-
-   procedure Censor (P           : in out Picture_T;
-                     Left, Right : X_Coord;
-                     Top, Bottom : Y_Coord)
-   with Pre => Left in P'Range (1) and Right in P'Range (1) and
-               Left in P'Range (2) and Right in P'Range (2),
-        Post => (P'Old with delta (Left .. Right, Top .. Bottom) => Black);
-
-   -- Example of a 2D delta aggregate using ranges, which is equivalent to
-   -- this much more verbose contract:
-   --   Post => (for all X in X_Coord range P'First (1) .. P'Last (1) =>
-   --             (for all Y in Y_Coord range P'First (2) .. P'Last (2) =>
-   --               (if X in L .. R and Y in T .. B
-   --                then P (X) (Y) = Black
-   --                else P (X) (Y) = P'Old (X) (Y))));
-
-   P := (Old_Picture with delta (P'First(1) | P'Last(1), P'Range(2)) => Black,
-                                (P'Range(1), P'First(2) | P'Last(2)) => Black);
-   --  Draw a 1px black border around a picture
-
 Discriminants
 -------------
 Should we allow discriminants in record updates? The would have to be
@@ -1283,5 +1149,257 @@
 The Java stream approach seems to be very flexible and powerful for
 expression, but the Ada take on this would be better for Ada if it can make
 it mechanism look more like a loop. 
+
+****************************************************************
+
+From: Florian Schnada
+Sent: Thursday, September 29, 2016  9:16 AM
+
+This is my attempt at implementing everything that was discussed and recorded
+in the minutes (btw, thanks Randy for these, they are excellent!). I have also
+attached a patch for the text file version. This may be more convenient for
+you to apply. YMMV.
+
+[Following was version /04 of the AI.]
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, September 29, 2016  4:29 PM
+
+Excellent write-up!  One question about array delta aggregates: the text
+suggests that each delta is a modification of a single component, but
+discrete_choices include ranges and subtype indications, which imply slice
+assignments. Are such choices excluded, or should the text mention indexed
+components and slices as legal targets of a delta assignment?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, September 29, 2016  4:51 PM
+
+I haven't read Florian's write up yet, but discrete range choices and the like
+of aggregates are modeled as a loop in the language semantics -- the component
+value is evaluated and assigned for each value of the range (in an unspecified
+order).
+
+I would have expected Florian's write-up to keep the semantics of each kind of
+choice the same, so that there is as little new complication as possible.
+(I'm sure he doesn't want to redescribe the various kinds of array choices and
+their semantics.)
+
+Ergo, there are no "slice assignments"; it's just a bunch of individual
+components being updated. That's important for wording purposes (whether one
+wants to think of it as a slice assignment is your own option, of course, but
+the language certainly would not consider it so).
+
+Specifically:
+    (A delta 1..3 => Foo)
+and (A delta 1 => Foo, 2 => Foo, 3 => Foo)
+
+have exactly the same canonical semantics, and there is no slice anywhere to
+be seen.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, September 29, 2016  4:57 PM
+
+> I haven't read Florian's write up yet, but discrete range choices and 
+> the like of aggregates are modeled as a loop in the language semantics 
+> -- the component value is evaluated and assigned for each value of the 
+> range (in an unspecified order).
+>
+> I would have expected Florian's write-up to keep the semantics of each 
+> kind of choice the same, so that there is as little new complication as possible.
+> (I'm sure he doesn't want to redescribe the various kinds of array 
+> choices and their semantics.)
+>
+> Ergo, there are no "slice assignments"; it's just a bunch of 
+> individual components being updated. That's important for wording 
+> purposes (whether one wants to think of it as a slice assignment is 
+> your own option, of course, but the language certainly would not consider it so).
+
+I agree with the above.
+
+> Specifically:
+>     (A delta 1..3 => Foo)
+> and (A delta 1 => Foo, 2 => Foo, 3 => Foo)
+>
+> have exactly the same canonical semantics, and there is no slice 
+> anywhere to be seen.
+
+Agreed.  But I also haven't gone through the proposed wording in detail yet!
+
+****************************************************************
+
+From: Edmond Schonberg
+Sent: Thursday, September 29, 2016  5:02 AM
+
+> Specifically:
+>    (A delta 1..3 => Foo)
+> and (A delta 1 => Foo, 2 => Foo, 3 => Foo)
+> 
+> have exactly the same canonical semantics, and there is no slice 
+> anywhere to be seen.
+> 
+
+Makes sense, and indeed the code will have to consist of individual
+assignments.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, September 29, 2016  5:13 PM
+
+Generally, looks good!
+
+But... I worry that we are referencing the semantics of 'Old and
+build-in-place in the dynamic semantics section.  I could see mentioning
+them in an AARM note.  But expecting the reader, as an aid to understanding
+the dynamic semantics of delta aggregates, to have to look forward to the
+definition of 'Old, followed by a perusal of the build-in-place rules, seems
+downright perverse! ;-)  You have these references in brackets, so I presume
+that means this is redundant information and hence not necessary to appear in
+normative RM text here. If so, I heartily suggest that the bracketed wording
+move to an AARM note.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, October 2, 2016  11:48 PM
+
+> ... But expecting the
+> reader, as an aid to understanding the dynamic semantics of delta 
+> aggregates, to have to look forward to the definition of 'Old, 
+> followed by a perusal of the build-in-place rules, seems downright 
+> perverse! ;-)
+
+I recognize the Hand of Baird in this text! ;-) Steve was originally a
+co-author on this AI.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, October 2, 2016  11:24 PM
+
+> This is my attempt at implementing everything that was discussed and 
+> recorded in the minutes (btw, thanks Randy for these, they are 
+> excellent!). I have also attached a patch for the text file version. 
+> This may be more convenient for you to apply. YMMV.
+
+One thing that was suggested in e-mail [by Bob, I think] (not the minutes)
+was to completely separate the syntax and rules for record_delta_aggregate
+and array_delta_aggregate, since they're mostly disjoint anyway. That should
+decrease the verbiage. I was expecting this change to be made (because it was
+obvious to me), but since it was left out of the minutes, I'm not surprised
+it wasn't.
+
+This could start something like:
+
+4.3.4 Delta Aggregates
+
+A (record or array) delta aggregate yields a composite value resulting from
+copying another value of the same type and then subsequently assigning to some
+(but typically not all) components of the copy.
+
+Syntax
+
+  record_delta_aggregate ::= (*base_*expression with delta
+                              record_component_association_list)
+ 
+  array_delta_aggregate ::= (*base_*expression with delta
+                              array_component_association_list)
+
+Name Resolution Rules
+
+The expected type for a record_delta_aggregate shall be a single record type or
+record extension. The expected type for an array_delta_aggregate shall be a
+single array type. The expected type for the *base_*expression of either of
+these agrgegates is the type of the enclosing record_delta_aggregate or
+array_delta_aggregate
+
+For a record_delta_aggregate, the expected type and applicable index constraint
+of the expression in each record_component_association is defined as for a
+record_component_association occurring within a record aggregate.
+
+For an array_delta_aggregate, the expected type for each discrete_choice in an
+array_component_association is the index type of type of the
+array_delta_aggregate.
+
+The expected type and applicable index constraint of the expression in
+array_component_association is defined as for an array_component_association
+occurring within an array aggregate of the type of the array_delta_aggregate.
+
+....
+
+You could even put them into separate clauses to get rid of all of the "for a
+record delta aggregate ..."s.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, October 2, 2016  11:35 PM
+
+Other comments on the draft:
+
+For a delta aggregate the expression in a record_component_association or a
+array_component_association shall not be of a limited type.
+
+Which expression is being discussed here? I'd guess that it is supposed to be
+the *base*_expression, and if that's the intent, this rule should say that. (Use
+the prefix if you go through the trouble to define it!) [P.S. I took the extra
+comma out of  your version.]
+
+---
+
+I second Tucker's comment about 'Old. I can't imagine what that has to do with 
+aggregate semantics; it would make more sense if 'Old had been described in
+terms of delta aggregate semantics.  I think that whatever semantics needs to
+be described normatively, needs to be described here, and the rest can go into
+an AARM note. We especially don't want a forward reference here.
+
+---
+
+In the examples, you need cross-references to where the objects/types are
+declared elsewhere in the RM. For instance, the first example should have
+something like "(See x.x.x for the declaration of D.)" as part of the comment.
+I'm not going to try to figure out where an object named "D" is declared in
+the RM! (Searching doesn't work for obvious reasons.)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, October 2, 2016  11:35 PM
+
+Two other comments: 
+
+> For a delta aggregate the expression in a record_component_association 
+> or a array_component_association shall not be of a limited type.
+> 
+> Which expression is being discussed here? I'd guess that it is 
+> supposed to be the *base*_expression, and if that's the intent, this 
+> rule should say that. (Use the prefix if you go through the trouble to 
+> define it!) [P.S. I took the extra comma out of  your version.]
+
+The rule added after 7.5(2.10/2) has the same issue.
+
+The reason this is important is by leaving out the prefix, the reader wonders
+if that was on purpose.
+
+---
+
+You didn't update the rest of the AI, particularly the !discussion. I deleted
+all of the multidimensional text, but otherwise left it unchanged.
+
+PLEASE do not get in the habit of just updating the wording and leaving the
+rest of it to the poor editor. The wording is often the easy part! And I am
+not good at guessing what your intent is (which is what goes in the
+discussion). I'll fix up headers and file e-mail, but that's it.
+
+There's one other ARG member who is in that habit whom I won't name but will
+identify as "Heave Beard", and it's important to point out that it isn't
+acceptable. I don't have much hope of fixing Heave Beard but I don't plan to
+let anyone else get away with it consistently.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent