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

Differences between 1.3 and version 1.4
Log of other versions for file ai12s/ai12-0236-1.txt

--- ai12s/ai12-0236-1.txt	2018/03/02 06:46:45	1.3
+++ ai12s/ai12-0236-1.txt	2018/10/13 02:08:04	1.4
@@ -1,5 +1,9 @@
-!standard 13.11(5)                                  18-01-26  AI12-0236-1/02
-!standard 13.11.4(3/3)
+!standard 3.9.2(3)                                    18-10-12  AI12-0236-1/03
+!standard 3.10.2(9.1/3)
+!standard 3.10.2(32.2/3)
+!standard 6.9(0)
+!standard 7.6.1(3/2)
+!standard 8.1(3)
 !class Amendment 17-09-06
 !status work item 17-09-06
 !status received 17-06-21
@@ -16,7 +20,7 @@
 Ada 2012 greatly enhanced the power of Ada expressions, primarily in order to
 make the writing of contracts easier. For that reason, if and case expressions
 were introduced into the language, as well as expression functions and
-quantifier expressions. However, a missing piece of functionality is the ability
+quantified expressions. However, a missing piece of functionality is the ability
 to bind the result of an expression - for example a function call - to a name,
 in order to reuse its value.
 
@@ -37,88 +41,130 @@
           Cur_Position = Cur_Position'Old + 1
           and then Result = Character'Pos (The_File (Cur_Position'Old)));
 
-The contract is not extremely complex in and of itself, but due to the fact that
-some expressions are repeated makes it more difficult to read - for example,
-Cur_Position'Old and The_File (Cur_Position'Old).
+The contract is not extremely complex in and of itself, but the fact
+that some expressions are repeated makes it more difficult to read - for
+example, Cur_Position'Old and The_File (Cur_Position'Old).
 
 !proposal
 
-A *declare expression* allows constant objects and renamings of constants to be
+A *declare expression* allows constant objects and renamings to be
 declared within an expression.
 
 !wording
 
+Add a new section 6.9, following 6.8 "Expression Functions":
+
+6.9 Declare Expressions
+
 Syntax
 
 declare_expression ::= (declare {declare_item} begin *body*_expression)
 
-declare_item ::= constant_declare_item | renaming_declare_item
+declare_item ::= object_declaration | renaming_declaration
 
-constant_declare_item ::=
-    defining_identifier_list : constant [subtype_indication] := expression;
+Legality Rules
 
-renaming_declare_item ::=
-    defining_identifier [: [null_exclusion] subtype_mark] renames object_name;
+A declare_item that is an object_declaration shall declare a
+constant.
 
-[TBD: Should aspect_specifications be allowed on declare_items?
+For a declare_item that is an object_declaration or
+object_renaming_declaration, the type of the object shall be
+elementary.
+
+AARM Rationale: We allow "(declare begin expression)" with no
+declare_items, for uniformity with block statements, which also allow a
+pointless "declare".
 
-Should we allow access_definition in declare_items?  I think not.
+Name Resolution Rules
 
-Should we allow "aliased" in constant_declare_items?
+If a declare_expression is expected to be of a type T, then the
+*body*_expression is expected to be of type T. Similarly, if a
+declare_expression is expected to be of some class of types, then the
+*body*_expression is subject to the same expectation. If a declare_expression
+shall resolve to be of a type T, then the *body*_expression shall resolve to be
+of type T.
 
-Should we allow array_type_definition in constant_declare_items?  I think not.
+[Editor's note: The above rule comes from 4.5.7(8/3) for
+conditional_expressions.]
 
-I'm allowing multiple identifiers in constant_declare_items, for uniformity with
-object_declarations.
+The type of a declare_expression is the type of the *body*_expression.
 
-I'm allowing "(declare begin expression)" with no declare_items, for uniformity
-with block statements, which also annoyingly allow a pointless "declare".]
+Dynamic Semantics
 
-Static Semantics
+For the evaluation of a declare_expression, the declare_items are
+elaborated in order, and then the *body_*expression is evaluated. The
+value of the declare_expression is that of the *body_*expression.
 
-The scope of a defining_identifier of a declare_item is the enclosing
-declare_expression. The semantics of a declare_item are the same as an
-object_declaration or object_renaming_declaration of the same form.
+[End of new 6.9]
 
-[TBD: The above is intended to include static semantics, name resolution,
-legality, and dynamic semantics.
+Add after the penultimate sentence of 3.9.2(3):
 
-I am assuming another AI will define the semantics of:
+    A declare_expression is statically, dynamically, or indeterminately
+    tagged according to its *body*_expression.
 
-    X: constant := expression; -- not as a named number!
-    Y renames expression;
+Add after 3.10.2(9.1/3):
 
-i.e. an object_declaration without a subtype_indication (must include
-"constant"), and an object_renaming_declaration without a subtype_mark
-(expression must denote a constant view).
+    The accessibility level of a declare_expression (see 6.9) is
+    the accessibility level of the *body*_expression.
 
-That AI should contain the business about *typed declarative expression*, which
-allows to distinguish number_declarations from object_declarations.
-]
+Add to the definition of "distributed accessibility" after 3.10.2(32.2/3):
 
-Name Resolution Rules
+   * a declare_expression (see 6.9); or
 
-The type of a declare_expression is the type of the *body*_expression.
+Modify the definition of "master" in 7.6.1(3/2):
 
-If a declare_expression is expected to be of a type T, then the
-*body*_expression is expected to be of type T. Similarly, if a
-declare_expression is expected to be of some class of types, then the
-*body*_expression is subject to the same expectation. If a declare_expression
-shall resolve to be of a type T, then the *body*_expression shall resolve to be
-of type T.
+  master: the execution of a body other than a package_body; the
+  execution of a statement{; the evaluation of a declare_expression}; or
+  the evaluation of an expression, function_call, or range that is not
+  part of an enclosing expression, function_call, range, or
+  simple_statement other than a simple_return_statement.
 
-[TBD: Above rule comes from 4.5.7(8/3) for conditional_expressions.]
+Add after 8.1(3):
 
-Dynamic Semantics
+    - a declare_expression
 
-For the evaluation of a declare_expression, the declare_items are elaborated and
-then the *body_*expression is evaluated. The value of the declare_expression is
-that of the *body_*expression.
+[Editor's note: This adds it to the list of constructs that have a
+declarative region. This, together with 8.2(2) means that the immediate
+scope of a declare_item goes from the beginning of the declare_item to
+the end of the innermost enclosing declare_expression.]
 
 !discussion
 
-** TBD.
+Note that AI12-0275-1 allows an object_renaming_declaration without a
+subtype_mark; this applies to declare_items. On the other hand, we
+continue to require a subtype_indication in an object_declaration,
+including as a declare_item.
+
+The restriction to elementary types is to avoid implementation
+difficulties related to build-in-place, task waiting, and controlled
+types. We could lift this restriction to allow any nonlimited type, if
+it turns out to be feasible to implement controlled types. We could
+further lift it to allow any type, if it turns out to be feasible to
+implement tasks and build in place.
+
+If we allow arrays, then we could consider allowing "others" array
+aggregates, by adding after 4.3.3(15.1):
+
+        For a declare_expression, the applicable index constraint for
+        the *body*_expression is that, if any, defined for the
+        declare_expression.
 
+If we allow composite types, we would need to add to the end of 6.2(10):
+
+    For a declare_expression, this object is the one associated with the
+    *body*_expression.
+
+If we allow composite types, we would need to add after 4.3.2(5.4),
+in the rule for extension aggregates:
+
+   * a declare_expression whose *body*_expression would violate this
+     rule.
+
+If we allow limited types, we would probably need to update 7.5(2.1).
+
+A declare expression cannot be static or predicate-static
+(see 4.9 and 3.2.4).
+
 !examples
 
    Post => Fun'Result =
@@ -126,13 +172,9 @@
          (if X > Y then X else Y+X))
 
    Type_Invariant =>
-      (M : constant := Integer'Max(T.A, T.B); begin
+      (M : constant Integer := Integer'Max(T.A, T.B); begin
         (if M > 0 then M > T.C else M < T.D))
 
-[TBD: I inherited the above example, but it seems to be illegal, because the
-call to 'Max is not a "typed declarative expression".  Perhaps it should be
-legal, but it seems like that's the subject of another AI.]
-
    Dynamic_Predicate =>
       (declare Q : constant Integer := H(S.A, S.B);
                R : constant Integer := G(S.C, S.D); begin
@@ -141,22 +183,22 @@
     X : T := (declare Temp renames Some_Array(Y..Z)
               begin Temp & Temp);
 
-The example in the !problem (assuming Cur_Position is a name statically denoting
-a stand-alone object, and therefore a typed declarative expression):
+The example in the !problem:
 
    procedure Fgetc (Stream : File_Descr; Result : out Int) with
      Post =>
        (declare
-          The_Char : constant Character := The_File (Cur_Position'Old);
-          Pos_Unchg : constant := Cur_Position = Cur_Position'Old;
+          Old_Pos : constant Position := Cur_Position'Old;
+          The_Char : constant Character := The_File (Old_Pos);
+          Pos_Unchg : constant Boolean := Cur_Position = Old_Pos;
         begin
            (if The_Char = EOF_Ch
               then Pos_Unchg and then Result = EOF
             elsif The_Char = ASCII.LF
               then Pos_Unchg and then Result = Character'Pos (ASCII.LF)
             else
-              Cur_Position = Cur_Position'Old + 1
-              and then Result = Character'Pos (The_File (Cur_Position'Old))));
+              Cur_Position = Old_Pos + 1
+              and then Result = Character'Pos (The_Char)));
 
 !ASIS
 
@@ -903,14 +945,14 @@
 [The following was in version /02 of this AI. - Editor.]
 
 > I am assuming another AI will define the semantics of:
-> 
+>
 >    X: constant := expression; -- not as a named number!
 >    Y renames expression;
-> 
-> i.e. an object_declaration without a subtype_indication (must include 
-> "constant"), and an object_renaming_declaration without a subtype_mark 
+>
+> i.e. an object_declaration without a subtype_indication (must include
+> "constant"), and an object_renaming_declaration without a subtype_mark
 > (expression must denote a constant view).
-> 
+>
 > That AI should contain the business about *typed declarative expression*,
 > which allows one to distinguish number_declarations from
 > object_declarations. ...
@@ -925,28 +967,28 @@
 From: Bob Duff
 Sent: Wednesday, January 31, 2018  2:16 PM
 
-> I missed or have forgotten the discussion of "typed declarative 
+> I missed or have forgotten the discussion of "typed declarative
 > expressions."  Who has that AI?
 
-I had forgotten also.  I looked it up in the minutes when I was writing the 
+I had forgotten also.  I looked it up in the minutes when I was writing the
 latest version of this AI.
 
-> ...Perhaps such an expression should be a different syntactic 
-> construct, or at least have some kind of italicized prefix so it 
+> ...Perhaps such an expression should be a different syntactic
+> construct, or at least have some kind of italicized prefix so it
 > stands out in the syntax for constant_declare_item.
 
 Sounds reasonable.
 
 > > I am assuming another AI will define the semantics of:
-> > 
+> >
 > >    X: constant := expression; -- not as a named number!
 > >    Y renames expression;
-> > 
-> > i.e. an object_declaration without a subtype_indication (must 
-> > include "constant"), and an object_renaming_declaration without a 
+> >
+> > i.e. an object_declaration without a subtype_indication (must
+> > include "constant"), and an object_renaming_declaration without a
 > > subtype_mark (expression must denote a constant view).
-> > 
-> > That AI should contain the business about *typed declarative 
+> >
+> > That AI should contain the business about *typed declarative
 > > expression*, which allows one to distinguish number_declarations from
 > > object_declarations. ...
 
@@ -954,7 +996,7 @@
 he's written it up, or if it has a number.
 
 I was thinking an object_renaming_declaration should have the same semantics
-(or as close as possible) whether it's inside a declare_expression, or not. 
+(or as close as possible) whether it's inside a declare_expression, or not.
 So if we allow the compiler to deduce the type from the renamed object, it
 should work the same in both cases.
 
@@ -975,15 +1017,15 @@
 From: Randy Brukardt
 Sent: Wednesday, January 31, 2018  5:55 PM
 
-> I missed or have forgotten the discussion of "typed declarative 
+> I missed or have forgotten the discussion of "typed declarative
 > expressions."  Who has that AI?
 
 My understanding of the discussion in Lexington is different than Bob's, so I
 think it belongs in *this* AI. See below.
 
 > Perhaps such an
-> expression should be a different syntactic construct, or at least have 
-> some kind of italicized prefix so it stands out in the syntax for 
+> expression should be a different syntactic construct, or at least have
+> some kind of italicized prefix so it stands out in the syntax for
 > constant_declare_item.
 
 A "typed declarative expression" is an expression that allows the omission of
@@ -995,12 +1037,12 @@
 > > This completes my homework.
 > > ...
 > > I am assuming another AI will define the semantics of:
-> > 
+> >
 > >    X: constant := expression; -- not as a named number!
 > >    Y renames expression;
-> > 
-> > i.e. an object_declaration without a subtype_indication (must 
-> > include "constant"), and an object_renaming_declaration without a 
+> >
+> > i.e. an object_declaration without a subtype_indication (must
+> > include "constant"), and an object_renaming_declaration without a
 > > subtype_mark (expression must denote a constant view).
 
 My recollection of the Lexington discussions was that we wanted this generally
@@ -1013,8 +1055,8 @@
 I note that the homework item for Raphael states that is about dropping type
 names for renames declarations; it isn't about doing that more generally.
 
-> > That AI should contain the business about *typed declarative 
-> > expression*, which allows one to distinguish number_declarations 
+> > That AI should contain the business about *typed declarative
+> > expression*, which allows one to distinguish number_declarations
 > > from object_declarations. ...
 
 We didn't want to do that; the "typed declarative expression" was simply about
@@ -1032,7 +1074,7 @@
 From: Bob Duff
 Sent: Wednesday, January 31, 2018  7:46 PM
 
-> My understanding of the discussion in Lexington is different than 
+> My understanding of the discussion in Lexington is different than
 > Bob's, so I think it belongs in *this* AI. See below.
 
 Probably your (Randy) understanding of the discussion is more accurate than
@@ -1050,9 +1092,9 @@
 "X: constant := F(Y);" can't resolve whereas "X renames F(Y);" can (as a
 regular decl not in a declare_expr).
 
-> Perhaps I didn't get this recorded well enough in the minutes; my 
-> excuse would be it was the last AI we discussed in Lexington and I 
-> probably was more interested in getting the meeting over with than 
+> Perhaps I didn't get this recorded well enough in the minutes; my
+> excuse would be it was the last AI we discussed in Lexington and I
+> probably was more interested in getting the meeting over with than
 > perfect note-taking.
 
 Perhaps, but I bow down to your superior note-taking abilities.
@@ -1063,7 +1105,7 @@
 Sent: Wednesday, January 31, 2018  8:27 PM
 
 ...
-> For ex., it would seem really weird to me if "X: constant := Y;" is a 
+> For ex., it would seem really weird to me if "X: constant := Y;" is a
 > named number in one context but not in the other.
 
 I'd prefer that static expressions were properly declared always (i.e.
@@ -1071,7 +1113,7 @@
 as a named number, but it's 40 years too late to get rid that.
 
 > Likewise, it would seem weird if (assuming only one visible function F),
-> "X: constant := F(Y);" can't resolve whereas "X renames F(Y);" can (as 
+> "X: constant := F(Y);" can't resolve whereas "X renames F(Y);" can (as
 > a regular decl not in a declare_expr).
 
 I understand your point, but...
@@ -1112,17 +1154,17 @@
 From: Bob Duff
 Sent: Thursday, February  1, 2018  9:14 AM
 
-> The subtype name in an object renames is (arguably) actively harmful, 
-> because the subtype parts (constraint, exclusions, predicates) are 
-> completely ignored. Therefore, I can support dropping it; omitting it 
-> can't be more confusing than having it and still having to ignore most 
-> of its properties. It's likely to be clearer to force one to look at 
+> The subtype name in an object renames is (arguably) actively harmful,
+> because the subtype parts (constraint, exclusions, predicates) are
+> completely ignored. Therefore, I can support dropping it; omitting it
+> can't be more confusing than having it and still having to ignore most
+> of its properties. It's likely to be clearer to force one to look at
 > the original object to find the properties.
 
 I agreed about renamings.
 
-> The reverse is true for constant declarations: the nominal subtype 
-> given in the declaration is important -- it even determines the 
+> The reverse is true for constant declarations: the nominal subtype
+> given in the declaration is important -- it even determines the
 > semantics of the constant declaration.
 
 I don't see what the big deal is.  We just need to define what the nominal
@@ -1133,7 +1175,7 @@
 the init expr, except if that has discrims, in which case it's the
 unconstrained subtype (and similar for arrays).
 
-> If I was running the circus (to steal one of your favorite sayings, 
+> If I was running the circus (to steal one of your favorite sayings,
 > and ignoring that in some sense I *am* running this circus :-),...
 
 I didn't make it up.  I got it from Steve, who got it from "If I Ran the
@@ -1141,7 +1183,7 @@
 
 https://www.biblio.com/book/i-ran-circus-seuss-dr-theodore/d/996641864?aid=frg&utm_source=google&utm_medium=product&utm_campaign=feed-details&gclid=EAIaIQobChMI9p3s2f6E2QIV2LXACh1LJw09EAQYASABEgLhzfD_BwE
 
->...I hope we're not requiring copying here as we do  for "real" 
+>...I hope we're not requiring copying here as we do  for "real"
 >constant declarations.
 
 On the contrary, I assumed it would copy (unless of course the compiler can
@@ -1156,8 +1198,8 @@
 From: Bob Duff
 Sent: Thursday, February  1, 2018  9:23 AM
 
-> I don't see what the big deal is.  We just need to define what the 
-> nominal subtype is, in the case of this new syntax (because obviously 
+> I don't see what the big deal is.  We just need to define what the
+> nominal subtype is, in the case of this new syntax (because obviously
 > it's not explicit in the constant decl).
 
 If we allow missing subtype indication ONLY in declare_exprs, we STILL need to
@@ -1169,17 +1211,17 @@
 Sent: Thursday, February 1, 2018  7:22 PM
 
 ...
-> > The reverse is true for constant declarations: the nominal subtype 
-> > given in the declaration is important -- it even determines the 
+> > The reverse is true for constant declarations: the nominal subtype
+> > given in the declaration is important -- it even determines the
 > > semantics of the constant declaration.
 object------------------------^
-> 
-> I don't see what the big deal is.  We just need to define what the 
-> nominal subtype is, in the case of this new syntax (because obviously 
+>
+> I don't see what the big deal is.  We just need to define what the
+> nominal subtype is, in the case of this new syntax (because obviously
 > it's not explicit in the constant decl).
 
 I didn't make my point very well (and the typo above doesn't help). The
-*reader* of the constant declaration needs to see the nominal subtype because 
+*reader* of the constant declaration needs to see the nominal subtype because
 it matters in various other places.
 
 I often find myself searching for a subtype name in order to write a "use
@@ -1188,7 +1230,7 @@
 (use clauses could complicate that step, but I rarely use them on type names
 anyway). If the type name isn't there, either, it could get very frustrating.
 
-Leaving subtype names out - anywhere - makes it hard on the readers. I was 
+Leaving subtype names out - anywhere - makes it hard on the readers. I was
 willing to do that for very short-lived entities, because they're not likely
 to be used in a way where the subtype really matters. Things that potentially
 live for a very long time (the entire life of the program) must never omit the
@@ -1203,16 +1245,16 @@
 required always). Obviously can't do that because of compatibility, but I
 definitely don't want to go in the wrong direction here.
 
->>...I hope we're not requiring copying here as we do  for "real" 
+>>...I hope we're not requiring copying here as we do  for "real"
 >>constant declarations.
 
->On the contrary, I assumed it would copy (unless of course the compiler 
->can prove it doesn't matter).  It would be confusing to have different 
+>On the contrary, I assumed it would copy (unless of course the compiler
+>can prove it doesn't matter).  It would be confusing to have different
 >semantics in declare_expressions than for "real" constant decls.
 
 You're right about this, but...
 
->Isn't the whole point of allowing both constants and renamings is to 
+>Isn't the whole point of allowing both constants and renamings is to
 >let you choose "constant" semantics or "renaming" semantics?
 
 I thought it was because Steve thought he needed more never-used cases for
@@ -1227,7 +1269,7 @@
 like a whole new level of unnecessary pain. Pain which becomes required if you
 allow/require copying of composite objects in declare expressions.
 (Can't have an object disappearing without being finalized!) For Janus/Ada,
-his means a thumb and a storage pool for each declare expression (plus the 
+his means a thumb and a storage pool for each declare expression (plus the
 composite objects); the ability to "ignore" these scopes would be eliminated.
 
 I was imagining that these objects would get assigned to temporaries (usually
@@ -1239,6 +1281,1259 @@
 would fix any pressure to drop the subtype names from constants. "Constant"
 and copying is OK for elementary types in declare exprs, but that's it. And
 that seems like a wart.
+
+***************************************************************
+
+From: Bob Duff
+Sent: Sunday, September 16, 2018  3:24 PM
+
+Here is a new version of AI12-0236-1, "declare expressions".
+
+It no longer restricts the syntax of the obj/renaming decls -- you can use any
+object_declaration or renaming_declaration. So the semantics (static and
+dynamic) just piggy-backs on the existing semantics.
+
+As agreed, no further attempt to allow "X : constant := ..."
+(without subtype indication).  Too bad (although I admit I got confused by
+Pos_Unchg below -- until I realized it's Boolean).
+
+I translated plain English into RM-ese.  ;-)
+
+[Followed by version /03 of the AI - Editor.]
+
+***************************************************************
+
+From: Tucker Taft
+Sent: Sunday, September 16, 2018  9:58 PM
+
+This restricts renaming to elementary types.  I thought we had concluded that
+we wanted to allow arbitrary renaming, but limit declaring new constants to 
+be of only an elementary type.
+
+***************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Monday, September 17, 2018  1:10 AM
+
+But if we allow renaming of the result of a function call with a 
+build-in-place result type, we can as well allow constants, right?
+
+***************************************************************
+
+From: Bob Duff
+Sent: Monday, September 17, 2018  2:13 PM
+
+> This restricts renaming to elementary types.
+
+Yes.  I also meant to restrict the type of the whole declare_expression to be
+elementary.  Some of the !discussion doesn't make sense without that 
+restriction ("If we allow composite types, we would need to...").
+
+> ...I thought we had concluded that we wanted to allow arbitrary 
+> renaming, but limit declaring new constants to be of only an 
+> elementary type.
+
+What do you mean by "we"?  ;-)
+
+I know you suggested it, but I don't get it.
+To be discussed, along with the additional restriction I suggested above.
+
+The discussion between you and me so far (not on arg@) went something like 
+this:
+
+Me: Let's disallow limited types, to avoid tasks and b-i-p.  I'd like to 
+restrict controlled types too, but I don't see how to do that without 
+breaking privacy (and although I'm not ALWAYS opposed to breaking privacy,
+this would be a pretty big breakage).  Note that my point here is purely 
+about implementation difficulty.
+
+You: Let's restrict constants to elementary, and allow renamings of anything.
+We already support assertions.
+
+Me: I don't see the connection to assertions.
+
+You: The original rationale for declare_expressions is all about assertions.
+
+That's where it ended, and I decided to move the discussion to arg@.  Your 
+last statement is true, but it seems like a non sequitur.  I mean, how can 
+the original rationale for a feature have anything to do with implementation 
+difficulty?
+
+You suggest that for "X : constant T := F(...);", T must be elementary, but 
+for "X : T renames F(...);", T can be controlled.  But the renaming is just 
+as hard to implement as the constant (if both are controlled).  Harder, in 
+fact, given my memory of a certain compiler bug.
+
+I think some compiler writer should implement this stuff, and if they can 
+manage to get controlled/tasks/b-i-p working, then allow those things.
+
+I admit that the suggested restrictions are kludges.  :-(
+
+***************************************************************
+
+From: Tucker Taft
+Sent: Monday, September 17, 2018  2:48 PM
+
+>> This restricts renaming to elementary types.  I thought we had 
+>> concluded that we wanted to allow arbitrary renaming, but limit 
+>> declaring new constants to be of only an elementary type.
+>> 
+> But if we allow renaming of the result of a function call with a 
+> build-in-place result type, we can as well allow constants, right?
+
+I would argue that supporting arbitrary renaming is no harder than supporting
+arbitrary function calls in assertions, preconditions, etc., which is already
+required.  On the other hand, supporting the creation of a new object could 
+be more involved, and might include the whole build-in-place thing and/or 
+invocation of "deep" Adjust, etc. which renaming does not require.  
+
+My mental model of renaming the result of a function call is that you just 
+defer cutting back the secondary stack, presuming it uses it.  This is not 
+based on specific knowledge of GNAT, so it might be way off, but I think from
+a language semantics point of view, renaming is fundamentally simpler than 
+creating a new object, as soon as you wander past elementary types.
+
+***************************************************************
+
+From: Bob Duff
+Sent: Monday, September 17, 2018  5:33 PM
+
+> I would argue that supporting arbitrary renaming is no harder than 
+> supporting arbitrary function calls in assertions, preconditions, 
+> etc., which is already required.
+
+I still don't get it.  If you do:
+
+    declare
+        X : T1 := F(...);
+        Y : T2 renames G(...);
+    begin
+        ... -- (1)
+    end;
+
+Then code at (1) can refer to X and Y in their unfinalized state, and they 
+both need to be finalized at the "end;".
+
+Both are hard to implement, and I'm not sure which is harder.
+
+With a declare_expression, we throw a result-of-the-declare into the mix, 
+which probably doesn't simplify things.
+
+And I don't see the comparison with pragma Assert.  Any function calls 
+returning controlled stuff in the pragma get finalized right there.
+Those objects don't outlast the pragma.
+
+***************************************************************
+
+From: Tucker Taft
+Sent: Monday, September 17, 2018  9:38 PM
+
+> Then code at (1) can refer to X and Y in their unfinalized state, and 
+> they both need to be finalized at the "end;".
+
+You need to be a be able to refer to the "unfinalized" state of G(...) in the
+following:
+
+   with Pre => (G(...).Comp > 5);
+
+I would think it would be no harder to implement:
+
+  with Pre => (declare Y : T2 renames G(...); begin Y.Comp > 5);
+
+The "unfinalized" state of the result of G has roughly the same lifetime as in
+the expression that didn't use any renaming -- they are both limited to the 
+evaluation of the Pre aspect.
+
+On the other hand, if you introduce a constant:
+
+   with Pre => (declare X : constant T1 := F(...); begin X.Comp > 7);
+
+there might be more semantics involved, since if F has any controlled parts, 
+you might need to call the appropriate Adjust procedures.  I suppose one might 
+be able to optimize away the copy in the function call case, but if we write:
+
+   with Pre => (declare X : constant T1 := FF; begin Q(X) > 7);
+
+where FF is an existing declared object, we definitely have to make a copy of 
+FF since who knows what happens inside Q.  Renaming would not require any 
+copying in such a case.
+
+> Both are hard to implement, and I'm not sure which is harder.
+> 
+> With a declare_expression, we throw a result-of-the-declare into the 
+> mix, which probably doesn't simplify things.
+> 
+> And I don't see the comparison with pragma Assert.  Any function calls 
+> returning controlled stuff in the pragma get finalized right there.
+> Those objects don't outlast the pragma.
+
+None of these things outlast the evaluation of the declare expression, so 
+lifetimes are never very long.  The only issue in my mind is that creating a 
+new object by copy of an existing object brings in more semantics, and so the
+limitation against composite objects seems justified.  In the renaming case, 
+I don't see any implementation requirement other than a need to postpone the 
+finalization of the result, and that doesn't seem enough to justify the 
+limitation to elementary types.  There is no extra finalization required, and
+definitely no calls on Adjust, etc., relative to a precondition/postcondition,
+etc. that has a call on a function returning something complicated.
+
+***************************************************************
+
+From: Edward Fish
+Sent: Tuesday, September 18, 2018  12:59 PM
+
+Question: The declare excludes declaration items, does this include USE 
+statements? Because I have seen, and written, a few expression-functions where 
+the ability to include such visibility within their scope w/o polluting the 
+enclosing scope would have been nice.
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Friday, September 21, 2018  8:33 PM
+
+I think that would be a bad idea, as it would mean that visibility could 
+differ wildly in different parts of expressions. It's hard enough to figure
+out the use of use clauses when they are used globally in a package or 
+subprogram, having part of an expression subject to a use clause and the rest
+not seems like madness.
+
+Object declarations are unlike most other declarations in that they aren't 
+overloadable; this means that any use of the object identifier outside of an
+expanded name *must* refer to the declared object (and any other such use
+*must* not) -- this means that they can be handled without actually putting
+the names into the symbol table (or index, in the case of a Diana-like 
+design). That's important since the symbols are generally treated as an 
+unchanging global to expression operations like resolution -- having to deal
+with a changing symboltable would require a whole lot of additional mechanism
+(and care in order of operations). As an implementer, I don't want to go there
+and would rather forget the entire idea rather than add that level of 
+complexity to an Ada compiler.
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Friday, September 21, 2018  9:06 PM
+
+> > I still don't get it.  If you do:
+> > 
+> >   declare
+> >       X : T1 := F(...);
+> >       Y : T2 renames G(...);
+> >   begin
+> >       ... -- (1)
+> >   end;
+> > 
+> > Then code at (1) can refer to X and Y in their unfinalized state, 
+> > and they both need to be finalized at the "end;".
+
+I don't get it, either.
+
+> You need to be a be able to refer to the "unfinalized" state of G(...) 
+> in the following:
+> 
+>    with Pre => (G(...).Comp > 5);
+
+Yes, but this is nothing new -- it exists in Ada 95 anywhere that "condition"s
+appear, for instance in an if statement or exit statement. And it was an issue
+for the return of large objects in Ada 83 -- it's always been handled.
+
+But the key here is that such finalization is always handled en-mass at the end
+of the expression. You don't have to do such finalization in the middle, which 
+a declare expression would require.
+
+> I would think it would be no harder to implement:
+> 
+>   with Pre => (declare Y : T2 renames G(...); begin Y.Comp > 5);
+> 
+> The "unfinalized" state of the result of G has roughly the same 
+> lifetime as in the expression that didn't use any renaming -- they are 
+> both limited to the evaluation of the Pre aspect.
+
+True, but that is irrelevant -- the declare is the outermost thing and thus 
+its semantics are indistinguishable from doing everything at the end. What 
+would be relevant is the following (assume type T needs finalization):
+
+    if (declare Obj1 : T renames F(...) begin ...) + 
+       (declare Obj2 : T renames G(...)) then
+
+In this expression, Obj1 and Obj2 have to finalized when the respective 
+declares end. That means that you could see:
+
+   Init Obj1
+   Fin  Obj1
+   Init Obj2
+   Fin  Obj2
+
+or the reverse (Obj2 before Obj1), but the natural:
+
+   Init Obj1
+   Init Obj2
+   Fin  Obj1
+   Fin  Obj2
+
+is definitely not allowed. (At least it shouldn't be allowed, it's pretty 
+obvious in the above that the user wanted the objects to be disjoint.) This is
+very likely to be an ACATS test (there are existing tests very much like this 
+for other constructs, I wouldn't want this one to be untested).
+
+> On the other hand, if you introduce a constant:
+> 
+>    with Pre => (declare X : constant T1 := F(...); begin X.Comp > 7);
+> 
+> there might be more semantics involved, since if F has any controlled 
+> parts, you might need to call the appropriate Adjust procedures.  I 
+> suppose one might be able to optimize away the copy in the function 
+> call case, but if we write:
+> 
+>    with Pre => (declare X : constant T1 := FF; begin Q(X) > 7);
+> 
+> where FF is an existing declared object, we definitely have to make a 
+> copy of FF since who knows what happens inside Q.
+> Renaming would not require any copying in such a case.
+
+I don't see any reason this would matter. Renaming of a function result means 
+making a temporary place to keep the function result, which either means a 
+copy or using some build-in-place mechanism (which is logically an assignment
+ -- that is, copy -- even if it isn't implemented that way).
+
+In any event, we shouldn't be designing the language around odd-ball 
+implementation techniques like a "secondary stack"; we need to stick to very 
+broad notions like "temporary" and "build-in-place" and "assignment".
+
+> > Both are hard to implement, and I'm not sure which is harder.
+> > 
+> > With a declare_expression, we throw a result-of-the-declare into the 
+> > mix, which probably doesn't simplify things.
+> > 
+> > And I don't see the comparison with pragma Assert.  Any function 
+> > calls returning controlled stuff in the pragma get finalized right there.
+> > Those objects don't outlast the pragma.
+> 
+> None of these things outlast the evaluation of the declare expression, 
+> so lifetimes are never very long.
+
+That's not the issue: the issue is the reverse -- the lifetime has to be 
+unnaturally short. There is no mechanism in Janus/Ada for dealing with any 
+such issues with a lifetime of less than an entire expression: finalization is
+done "between" expressions (usually between statements). That's echoed by 
+7.6.1's definition of a master.
+
+> The only issue
+> in my mind is that creating a new object by copy of an existing object 
+> brings in more semantics, and so the limitation against composite 
+> objects seems justified.  In the renaming case, I don't see any 
+> implementation requirement other than a need to postpone the 
+> finalization of the result, and that doesn't seem enough to justify 
+> the limitation to elementary types.  There is no extra finalization 
+> required, and definitely no calls on Adjust, etc., relative to a 
+> precondition/postcondition, etc. that has a call on a function 
+> returning something complicated.
+
+Your mind is rather different than mine. There is no such thing as renaming a 
+function result in implementation terms: there is nothing renamable in that 
+case (can't rename something with a very short lifetime). So it has to be 
+implemented as essentially a build-in-place object declaration. I don't see 
+any problem with calling Initialize or Adjust in the constant case -- one just
+does that when needed, BFD.
+
+The difficulty in both of these cases is the need to do finalization at some 
+unusual point (in the middle of an expression). We have to do the finalization
+"early" as the objects themselves go away early (can't finalize an object 
+after it is reclaimed).
+
+I suppose we could define that a declare block always acts (dynamically) as if
+it is given at the outermost level of an expression, but I think that would be
+a bad thing for users (it would be a lie). And it would be preventing a 
+possibly useful capability, given the example above:
+
+    if (declare Obj1 : T renames F(...) begin ...) + 
+       (declare Obj2 : T renames G(...)) then
+
+if T is potentially very large, an expression like this could be written to 
+avoid Storage_Error. I don't think we want to promise that.
+
+Moreover, as always, the restrictions Bob proposes would allow expansion in the
+future (perhaps when we know more about how this is used and thus should work).
+If we allow controlled types now and get it wrong (a near certainty given the 
+issues noted) we'll be stuck forever. And I worry as always that we'd be 
+making a useful and relatively cheap capability a lot more expensive and 
+complex -- we had better be certain that is necessary before doing that (lest
+the whole idea get dumped into the crapper).
+
+***************************************************************
+
+From: Steve Baird
+Sent: Friday, October 5, 2018  5:03 PM
+
+Bob and I have been discussing some issues with declare expressions.
+
+First a very minor problem, then a bigger one.
+
+1) The minor problem: fully conformant expressions.
+
+Consider
+
+      pragma Assertion_Policy (Check);
+
+      procedure Foo (X : Boolean :=
+        (declare
+           Flag1 : constant Boolean := ...;
+           Flag2 : constant Boolean := ...;
+           pragma Assert (Flag1 or not Flag2);
+         begin
+           Flag1 /= Flag2));
+
+      pragma Assertion_Policy (Ignore);
+
+      procedure Foo (X : Boolean :=
+        (declare
+           Flag1 : constant Boolean := ...;
+           Flag2 : constant Boolean := ...;
+           pragma Assert (Flag1 or not Flag2);
+         begin
+           Flag1 /= Flag2))
+      is begin ... end;
+
+This is legal, but is the pragma checked or ignored when the default parameter
+value is evaluated? Perhaps it depends on the assertion policy in effect at 
+the call site?
+
+We may want a rule that if some construct has an effect on a region of program 
+text (e.g., Pragma Assertion_Policy) and if text is duplicated as in the 
+example above, then what matters is the first copy of the replicated text.
+Thus the assertion policy in force for the second copy of the duplicated text 
+has no effect on any assertions within that copy.
+
+Alternatively, we could have a rule for a default parameter that what matters 
+is the assertion policy that is in force where the parameter is defaulted. The
+main point is that this should question should be nailed down one way or 
+another.
+
+Bob points out that this is nothing new; we already have a similar issue with 
+pragma Suppress.
+
+Suppose we have
+      procedure P (X : Integer := Some_Global_Variable + 1);
+
+and later we have a (conforming) completion for this declaration.
+And after that we have a call to this procedure which passes in the default 
+parameter value. If overflow checking is suppressed at some but not all of 
+these three points, what determines whether the check is suppressed? This 
+question has nothing to do with declare expressions, but we'd like to handle
+similar cases consistently.
+
+2) The bigger problem: Accessibility.
+
+Do we want to accept or reject this example?
+
+      type Ref is access all Integer;
+      type Rec is record F : aliased Integer := 0; end record;
+      Ptr : Ref := Rec'(declare Local : Rec; begin Local).F'Access;
+
+I think the example should be (by definition) equivalent to
+
+      type Ref is access all Integer;
+      type Rec is record F : aliased Integer := 0; end record;
+      function Foo return Rec is
+          Local : Rec;
+      begin
+          return Local;
+      end;
+      Ptr : Ref := Rec'(Foo).F'Access;
+
+where Foo is an identifier chosen by the compiler which occurs nowhere else 
+in the program.
+
+Therefore, I think we want to accept the example.
+
+The currently proposed wording for the AI includes
+>     The accessibility level of a declare_expression is
+>     the accessibility level of the *body*_expression.
+which means that the preceding example would be rejected.
+
+This is at least in part because I suggested to Bob that for this AI he should 
+look at all the RM changes that were made for conditional expressions (e.g.,
+in determining the applicable index constraint, the associated object, the 
+expected type, and that sort of thing) and we have a rule in 3.10.2 that
+   The accessibility level of a conditional_expression is the
+    accessibility level of the evaluated dependent_expression.
+[Incidentally, AFAIK this rule for conditional expressions is fine.]
+
+A function is allowed to return a local variable (or, more precisely, the 
+value of a local variable) because a function is defined to have a return 
+object and that return object has special accessibility rules, different than 
+for a local object of the function.
+
+So we want (IMO) declare expressions to have the same semantics as function 
+calls and those semantics include return objects.
+Unfortunately, the accessibility/master/finalization rules for functions are 
+quite complex (e.g., the static and dynamic checks which prevent "dangling 
+types" in the case of a function with a class-wide result; or the "determined
+by the point of call" rules) and we don't want to either duplicate each of 
+these rules for declare expressions or explicitly modify each of these rules
+to take declare expressions into account. This approach gets complicated.
+
+We've also got the 3.10.2(6) rule that defines the accessibility level of a
+master (recall that a declare expression, unlike a conditional expression, is
+a master). This rule also suggests that the example we are discussing is 
+illegal. Again, the problem is that the special rules for function results do 
+not apply in the case of a declare expression but we want them to.
+
+I think (and Bob tentatively agrees with me) that the best solution to all 
+this might be to define a declare expression in terms of an equivalent 
+function call. We define an equivalence rule and then let everything else (in
+particular, legality checks and dynamic semantics) follow from that. That 
+spares us from having to specifically deal with, for example,  stuff like 
+6.5(5.8/5) and 6.5(8/4) (these are static and dynamic "no dangling types" 
+rules).
+
+We might (or might not) want to disallow the case where the type of a declare 
+expression is anonymous, as in
+      X1 : access T := (declare ...);
+or
+      X2 : array (1 .. 10) of Element := (declare ...); if it turns out that 
+some of these cases lead to problems.
+For example, in the anonymous array type case, what would the result type of 
+our "equivalent" function be?
+
+There is a related question having to do with the applicable index constraint.
+
+Consider
+     Y1 : String (1 .. N) := (declare ... begin (others => ...));
+
+or even
+
+     type Rec (N : Natural) is record
+       Y2 : String (1 .. N) := (declare ... begin (others => ...));
+     end record;
+
+Perhaps we'd want to allow the Y1 example and disallow the Y2 example (because
+getting the result subtype for our "equivalent" function is too hard in that 
+case).
+
+The Y1 example would then be equivalent to something like
+
+     subtype Foo1 is String (1 .. N);
+     function Bar1 return Foo1 is ... begin return (others => ...); end;
+     Y1 : Foo1 := Bar1;
+
+You could imagine doing the same sort of thing with Y2 except that it isn't 
+clear where the subtype and the function would be declared.
+If we really want this case to work, one could imagine something complicated 
+and messy like
+
+     function Bar2 (N : Natural) is
+       ...
+       subtype Foo2 is String (1 .. N);
+     begin
+       return Foo2'(others => ...);
+     end;
+
+     type Rec (N : Natural) is record
+       Y2 : String (1 .. N) := Bar2 (N);
+     end record;
+
+but let's not try to define that.
+
+In any case, my main point is that we should explore rewording this AI in 
+terms of an equivalence rule instead of trying to duplicate/modify the 
+function-related accessibility rules piecemeal.
+
+***************************************************************
+
+From: Steve Baird
+Sent: Friday, October 5, 2018  5:12 PM
+
+> Therefore, I think we want to accept the example.
+
+Oops, I blew the example here.
+We don't want a named access type here, but rather
+
+   Ptr : access constant Integer
+      := Rec'(declare Local : Rec; begin Local).F'Access;
+
+and the claim is that this should be equivalent to
+
+   Ptr : access constant Integer := Rec'(Foo).F'Access;
+
+Or something like that.
+
+But even if we just ignore this example, the main point remains that we don't
+want to duplicate for declare expressions all of the accessibility-related 
+rules that we already have for functions.
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, October 9, 2018  9:02 PM
+
+> 1) The minor problem: fully conformant expressions.
+> 
+> Consider
+> 
+>       pragma Assertion_Policy (Check);
+> 
+>       procedure Foo (X : Boolean :=
+>         (declare
+>            Flag1 : constant Boolean := ...;
+>            Flag2 : constant Boolean := ...;
+>            pragma Assert (Flag1 or not Flag2);
+>          begin
+>            Flag1 /= Flag2));
+...
+
+The bug here seems to be allowing a pragma in the *middle* of an expression.
+That's not intended by the rules in 2.8 (they insist that a pragma only appear
+in places between statements or declarations), and seems to be happening here
+only by accident (the inclusion of a semicolon in this syntax). Pragma Assert
+itself might be harmless (although this example shows not completely), but I 
+wonder about other pragmas. For instance, consider Assertion_Policy and 
+Suppress. Those would require a much finer-grained management of the scopes
+than currently used in Ada compilers (the suppression and assertion states 
+don't currently change within an expression). Sounds like a lot of work (I 
+don't even know how to implement that in the current Janus/Ada, as expressions
+tend to be evaluated at very different times than they are defined 
+syntactically).
+
+As such, and since we're allowing only object decls and renames here (not even
+use clauses, which would have a similar massive impact), the most sensible 
+thing is to ban the use of a pragma in a declare expression. So, we should 
+modify 2.8(6):
+
+* After a semicolon delimiter, but not within a formal_part{,}[ or] 
+  discriminant_part{, or declare_expression.
+
+[Aside: We ought to check other new syntax for the inclusion of semicolons 
+that would also allow pragmas in the middle.]
+
+...
+> 2) The bigger problem: Accessibility.
+> 
+> Do we want to accept or reject this example?
+> 
+>       type Ref is access all Integer;
+>       type Rec is record F : aliased Integer := 0; end record;
+>       Ptr : Ref := Rec'(declare Local : Rec; begin Local).F'Access;
+
+Reject, of course. The natural idea is that a declare expression works rather 
+like a declare block. Certainly, 'Access of a local object should not work. It
+seems obvious that a copy of a very local object stays very local.
+
+Indeed, I believe this example should be illegal (ignoring the 'Access) if Rec 
+could be a by-reference type, because implementing it requires some sort of 
+copy. Arguably it should always be illegal except for elementary types; in 
+any case it should be very local.
+
+> I think the example should be (by definition) equivalent to
+> 
+>       type Ref is access all Integer;
+>       type Rec is record F : aliased Integer := 0; end record;
+>       function Foo return Rec is
+>           Local : Rec;
+>       begin
+>           return Local;
+>       end;
+>       Ptr : Ref := Rec'(Foo).F'Access;
+> 
+> where Foo is an identifier chosen by the compiler which occurs nowhere 
+> else in the program.
+
+Sounds like an overcomplication that could kill the entire proposal. Indeed, 
+it would be better (if this is a real concern, of which I'm skeptical) to only
+allow renames in declare expressions, as that would avoid these sorts of 
+questions (we're only dealing with existing objects in that case).
+There's no function anywhere to be seen.
+
+> Therefore, I think we want to accept the example.
+
+I don't see any reason that anyone would want this example to work, and using 
+a function model here is a massive complication.
+ 
+> The currently proposed wording for the AI includes
+> >     The accessibility level of a declare_expression is
+> >     the accessibility level of the *body*_expression.
+> which means that the preceding example would be rejected.
+
+Sounds good to me. But I think it has to go further and deny body expressions 
+that are a part of a local object and are of a by-reference type.
+
+> This is at least in part because I suggested to Bob that for this AI 
+> he should look at all the RM changes that were made for conditional 
+> expressions (e.g., in determining the applicable index constraint, the 
+> associated object, the expected type, and that sort of thing) and we 
+> have a rule in
+> 3.10.2 that
+>    The accessibility level of a conditional_expression is the
+>     accessibility level of the evaluated dependent_expression.
+> [Incidentally, AFAIK this rule for conditional expressions is fine.]
+
+This rule allows returning *existing* objects from a conditional expression, 
+which is fine. The same should be fine for declare_expressions. Allowing more
+seems unnecessary; it just makes massive work for implementers.
+
+> A function is allowed to return a local variable (or, more precisely, 
+> the value of a local variable) because a function is defined to have a 
+> return object and that return object has special accessibility rules, 
+> different than for a local object of the function.
+> 
+> So we want (IMO) declare expressions to have the same semantics as 
+> function calls and those semantics include return objects.
+
+Why does this follow? A declare expression has nothing to do with a function; 
+you're not returning anything.
+
+The motivating case for a declare expression is preconditions/postconditions 
+where a somewhat complex expression is used in multiple conditions, 
+something like:
+
+     (declare
+         X renames <lengthy expression>;
+      begin
+         (if X > 10 then F'Result > 10
+          elsif X = 10 then F'Result = 10
+          else F'Result < 10))
+
+There is no reason to return part of a local in this usage; I don't see any 
+need to allow it at all. Probably in the interest of avoiding arbitrary 
+restrictions we could allow it for either by-copy (elementary) types or for
+types that are known to not be by-reference (by-reference itself is a dynamic
+concept and can't be used for legality rules); in such a case, the object 
+would be a copy (and very, very local - any 'Access would be illegal).
+
+...
+<<Several pages of ramblings about the consequences of an equivalence that we
+would never want in the first place skipped.>> ...
+> In any case, my main point is that we should explore rewording this AI 
+> in terms of an equivalence rule instead of trying to duplicate/modify 
+> the function-related accessibility rules piecemeal.
+
+I'd argue that we have the basic rules right (your specific example should not 
+be allowed), and we might need an additional rule to avoid returning a 
+composite object that would have to be a copy of a local. KISS (Keep It 
+Simple, Stupid). :-) I'd need to see a compelling usage of a very local object
+that couldn't reasonably be done in some other way before I'd even consider 
+this level of complication.
+
+***************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, October 9, 2018  9:24 PM
+
+I generally agree with Randy's comments about keeping it simple.  I could go 
+so far as to require the type of a declare expression to be an elementary 
+type, since the main purpose is to use it in an assertion expression.  If we
+limit the types of the locally declared objects to being elementary, this all
+becomes pretty simple.  As I mentioned I have no problem with being more 
+liberal in the renamings, but others seem to worry about those.
+
+Again, we could start simple, and then get more flexible in a later iteration.
+I'd be curious what the SPARK folks have to say here...
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, October 10, 2018  12:13 AM
+
+> I generally agree with Randy's comments about keeping it simple.  I 
+> could go so far as to require the type of a declare expression to be 
+> an elementary type, since the main purpose is to use it in an 
+> assertion expression.
+
+I don't see much reason to go *that* far; we allow composites in conditional 
+expressions, which are pretty similar. It's best to avoid completely arbitrary
+restrictions. So I'd suggest a Legality Rule something like:
+
+If the name of an object declared in a declare_expression appears in a 
+*body_*expression, then the type of the declare_expression shall be 
+elementary.
+
+AARM Reason: This rule is intended to avoid complications caused by using an 
+object after its scope has exited. We allow elementary types as the 
+declare_expression can be a value rather than an object for such types.
+
+AARM Ramification: This is worded to cover nested declare_expressions as well
+as object declared locally. It does not include objects renamed in the 
+declare_expression, as the renamed object necessarily exists outside of the 
+declare_expression.
+
+***************************************************************
+
+From: Jeff Cousins
+Sent: Wednesday, October 10, 2018  2:30 AM
+
+I'm glad you replied Randy, that's pretty much my thinking but expressed more 
+coherently than I could have managed.
+
+***************************************************************
+
+From: Jeff Cousins
+Sent: Wednesday, October 10, 2018  1:29 PM
+
+Speaking to my erstwhile colleagues (well, the few that have any depth of 
+understanding of the language), they quite like conditional expressions as a 
+convenient shorthand, but think that weíve already gone too far in having ever
+more complicated forms of expressions, encouraging the writing of code that is
+not readily debuggable Ė one canít (directly) insert a line of Text_IO in an 
+expression, and how would a debugger step through a long expression?
+
+And personally, if one of the drivers for having more complicated forms of 
+expressions is to use them in postconditions, then arenít we going down a 
+slippery slope towards the postcondition just repeating the logic thatís in
+the body, but in the form of a complicated expression rather than a series of
+statements, and thus blurring the distinction between specs and bodies?
+
+(This is more general to the new expression stuff than specifically declare 
+expressions, but I think declare expressions would encourage the use of 
+over-complicated expressions).
+
+***************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, October 10, 2018  1:58 PM
+
+If you are trying to specify functional properties, they inevitably get 
+complicated.  A typical approach is to "model" the true data structure with 
+a simpler but less efficient structure, and then the postconditions can be 
+expressed in terms of the model data structure.  But it is inevitable that 
+the postconditions will still be relatively complex.  Without something like
+a declare expression, the postcondition is *longer* because you end up 
+repeating the same sub-expression multiple times.  So the point of a declare
+expression is to simplify the postcondtion expression.  You still only get 
+one expression, but you want it to be as concise as possible, without 
+repeating the same subexpression multiple times.
+
+From the SPARK users, this is actually their highest priority Ada 2020 items,
+and it is all about making postconditions smaller and more readable.
+
+>(This is more general to the new expression stuff than specifically declare 
+>expressions, but I think declare expressions would encourage the use of 
+>over-complicated expressions).
+
+The goal was the opposite.  It allows you to remove redundant subexpressions 
+and replace them with a nice name.
+
+***************************************************************
+
+From: Jeffery Cousins
+Sent: Wednesday, October 10, 2018  2:26 PM
+
+Declare expressions make it easier to write expressions that would otherwise 
+have repeated subexpressions, but I'm sceptical that postconditions that are 
+complicated enough to have repeated sub expressions are a good thing in the 
+first place.  I don't think that non-SPARK users were expecting postconditions
+to be much more than function Square has a non-negative result. Anyway, I was 
+shocked to find a group of users who would rather we hadn't bothered with some
+of the new features.
+
+***************************************************************
+
+From: Arnaud Charlet
+Sent: Wednesday, October 10, 2018  2:38 PM
+
+That's useful input although what would those users want to see in Ada 2020 
+instead? If the answer is "nothing, everything is fine as is" then this also
+tells us that these users are not the right target for Ada 2020.
+
+***************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, October 10, 2018  2:40 PM
+
+>Declare expressions make it easier to write expressions that would otherwise
+>have repeated subexpressions, but I'm sceptical that postconditions that are
+>complicated enough to have repeated sub expressions are a good thing in the 
+>first place.  I don't think that non-SPARK users were expecting postconditions
+>to be much more than function Square has a non-negative result.
+
+SPARK users are an important part of the "new" Ada community.  From a 
+marketing point of view, the security and safety guarantees that SPARK can 
+provide resonate very strongly in new markets where Ada has not succeeded 
+before.  I would agree many existing Ada users will never try to fully specify
+the full functionality of a subprogram, but if you are trying to build a 
+highly-secure application and formally verify that it implements its 
+specification in some formal way, you will find that the postconditions can be
+large, and a mechanism to simplify them is important.
+
+>Anyway, I was shocked to find a group of users who would rather we hadn't 
+>bothered with some of the new features.
+
+Many of the new features were admittedly added to allow the full formal 
+specification of functionality, as used in SPARK.   I believe Ada benefits a
+lot from being tied to SPARK, but for folks not doing formal specification, 
+some of the new features will probably not be used, and may seem like a waste.
+
+***************************************************************
+
+From: Ed Schonberg
+Sent: Wednesday, October 10, 2018  2:57 PM
+
+>Declare expressions make it easier to write expressions that would otherwise 
+>have repeated subexpressions, but I'm sceptical that postconditions that are 
+>complicated enough to have repeated sub expressions are a good thing in the 
+>first place.  I don't think that non-SPARK users were expecting postconditions
+>to be much more than function Square has a non-negative result. Anyway, I was 
+>shocked to find a group of users who would rather we hadn't bothered with some
+>of the new features.
+
+Repeated subexpressions ask for functions, and previously this meant an 
+enclosing body and a lack of proximity to the point of use, We now have 
+expression functions that can appear in the same specification, so I donít see 
+a strong motivation here for declare expressions.
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, October 10, 2018  3:16 PM
+
+Which brings us full circle: the comment that started this thread claimed that 
+a declare expression had to be equivalent to a function. If that's the case, 
+one has to wonder why we need the declare expression in the first place. 
+(Luckily for the proponents of this feature, I don't agree with the original 
+comment.)
+
+I viewed this as a cheap addition that would help in some very limited 
+circumstances. And clearly, some programmers will misuse it, but Ichbiah said 
+this best when (arguing for user-defined operators) he said something to the 
+effect that just because a feature can be misused doesn't mean that it isn't 
+valuable when used properly.
+
+If of course the feature stops being cheap (as in Steve's view), then it's 
+best not to do it at all.
+
+***************************************************************
+
+From: Steve Baird
+Sent: Wednesday, October 10, 2018  9:29 PM
+
+> If of course the feature stops being cheap (as in Steve's view)
+
+I disagree with that characterization of my position.
+
+My main point is that that we don't want to either duplicate or modify the 
+various specific rules that prevent accessibility problems for functions in
+order to avoid analogous problems with declare expressions.
+
+For example, I'm assuming that we don't want to allow this one:
+
+     type T1 (D : access Integer) is ... ;
+
+     X1 : T1 := (declare
+                Int1 : aliased Integer;
+                Y1 : T (D => Int'Access);
+              begin
+                Y);
+
+We could modify or duplicate the corresponding rule for return statements
+(6.5(5.9/5)) to handle this case, but I'm arguing against such a piecemeal
+approach. I think an equivalence rule would be a better way of dealing 
+with this sort of problem. It also resolves most any corner-case question.
+If you want to know whether some case is legal or how it behaves at 
+runtime, you apply the equivalence rule to transform your program into a
+program that doesn't have any declare expressions and then ask the 
+corresponding question of the transformed version of your example.
+
+That equivalence rule might turn out to have its own problems (exactly where
+is this implicitly-declared function declared? how does it interact with 
+freezing?).
+
+So perhaps an even better solution would be the sort of restrictions Bob 
+and others have mentioned: the type of a declare expression shall be scalar,
+or shall have no access/task/protected/tagged/private/limited
+parts, or something along those lines.
+
+I'm open to that approach.
+
+A restriction disallowing a pragma within a declare expression also seems 
+reasonable to me.
+
+So I don't think I am arguing for a more expensive definition for this 
+feature.
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, October 11, 2018  5:23 PM
+
+> > If of course the feature stops being cheap (as in Steve's view)
+> 
+> I disagree with that characterization of my position.
+> 
+> My main point is that that we don't want to either duplicate or modify 
+> the various specific rules that prevent accessibility problems for 
+> functions in order to avoid analogous problems with declare 
+> expressions.
+
+This statement is of course fine, but I don't see any such problems inherent 
+in the proposal. I've always imagined that a declare expression would be 
+itself a master (as a controlled object had better be finalized before it
+ceases to exist), and in that case, 'Access is essentially illegal in all
+uses except those involving access parameters.
+
+I haven't read Bob's latest version carefully to see what he says about 
+masters, but there needs to be some decision on that point (and not just
+because of accessibility, but also because of finalization). If we want to 
+avoid a declare expression being a master, then we have to prevent declaring
+objects that have controlled, task, or protected parts (all of which require
+non-trivial finalization or task waiting).
+
+> For example, I'm assuming that we don't want to allow this one:
+> 
+>      type T1 (D : access Integer) is ... ;
+> 
+>      X1 : T1 := (declare
+>                 Int1 : aliased Integer;
+>                 Y1 : T (D => Int'Access);
+>               begin
+>                 Y);
+
+I'm pretty sure we're not allowing this one, since Y isn't defined. :-) I 
+presume you meant Y1 at the end here.
+
+And in that case, we shouldn't allow this (regardless of the discriminant).
+See my previous proposed rule.
+
+> We could modify or duplicate the corresponding rule for return 
+> statements (6.5(5.9/5)) to handle this case, but I'm arguing against 
+> such a piecemeal approach. I think an equivalence rule would be a 
+> better way of dealing with this sort of problem. It also resolves most 
+> any corner-case question. If you want to know whether some case is 
+> legal or how it behaves at runtime, you apply the equivalence rule to 
+> transform your program into a program that doesn't have any declare 
+> expressions and then ask the corresponding question of the transformed 
+> version of your example.
+> 
+> That equivalence rule might turn out to have its own problems (exactly 
+> where is this implicitly-declared function declared?
+> how does it interact with freezing?).
+> 
+> So perhaps an even better solution would be the sort of restrictions 
+> Bob and others have mentioned: the type of a declare expression shall 
+> be scalar, or shall have no 
+> access/task/protected/tagged/private/limited
+> parts, or something along those lines.
+> 
+> I'm open to that approach.
+> 
+> A restriction disallowing a pragma within a declare expression also 
+> seems reasonable to me.
+> 
+> So I don't think I am arguing for a more expensive definition for this 
+> feature.
+
+You were, because you were arguing for a more complex solution rather than 
+a simpler one (don't allow 'Access, or other restrictions). Most users 
+should use renames here anyway, which is greatly helped by our new simpler
+syntax for that. So perhaps Tuck is right about allowing "only elementary 
+non-aliased objects". Then there is no problem with returning local objects
+(they'd be values anyway), and you could still return other existing objects
+(including a function result). And it gets rid of the need to worry about 
+finalization/task waiting.
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Friday, October 12, 2018  7:22 PM
+
+I've finally gotten around to reading Bob's AI here. (I did post it unchanged 
+except for spacing, a couple of editorial changes detailed below, and fixing 
+the !standard references lest John get mad at me again. :-)
+
+Bob Duff wrote last month:
+... 
+> > This restricts renaming to elementary types.
+> 
+> Yes.  I also meant to restrict the type of the whole 
+> declare_expression to be elementary.  Some of the !discussion doesn't 
+> make sense without that restriction ("If we allow composite types, we 
+> would need to...").
+
+Do you want/intend to make a correction to the AI to this effect? Or would you 
+rather I did it? Or not at all?
+
+I realize that subsequent discussion might have changed your intent a bit, so 
+I don't want to assume I know it. If it was me (today), I'd restrict new 
+constants to elementary, not sure about renames (finalization only matters 
+there for function results [as otherwise we're renaming an existing object 
+which won't get finalized here], which are temporaries otherwise inaccessible
+ - there's an argument that leaving them to be finalized with the entire 
+expression is not harmful as only pathological programs could care), and I 
+see no reason to restrict the result (if it works for an if expression, I 
+don't see why it shouldn't work for a declare expression; the restriction to
+elementary types for local constants ensures that the result can be handled 
+by value if it is local). Ergo, no correction seems needed (except to the 
+!discussion).
+
+If we make a correction, we also should correct the pragma rule to disallow 
+embedded pragmas in declare expressions, I'm sure we didn't intend to allow 
+that. (See that mail.)
+
+In any case, you're (that is, Bob) the author and I don't want to replace your 
+intent with mine (even if it's better ;-).
+
+---
+
+>Add a new section 6.9, following 6.8 "Expression Functions":
+>
+>6.9 Declare Expressions
+
+This seems like a curious place to put a new kind of subexpression (being in 
+the subprogram section). The closest analogs are conditional expressions and 
+declare blocks, so I would have expected it in one of those places. Probably 
+the most sense IMHO would be 4.5.9 (after quantified expressions, mainly to 
+avoid changing the number on those), as it is just another kind of 
+subexpression.
+
+The alternative of putting it after a declare block (that is, as 5.6.1) 
+doesn't work as well since we already have a new kind of block statement
+(the parallel block) in that slot.
+
+---
+
+>Modify the definition of "master" in 7.6.1(3/2):
+>
+>  master: the execution of a body other than a package_body; the  
+> execution of a statement{; the evaluation of a declare_expression}; or  
+> the evaluation of an expression, function_call, or range that is not  
+> part of an enclosing expression, function_call, range, or  
+> simple_statement other than a simple_return_statement.
+
+I would not make this change if you are restricting the types of the local 
+entities to elementary. In that case, it could only affect the result of 
+function calls that occur in initializers or the body_expression in that and 
+I suppose similar aggregates (everything else being an existing object).
+That would be different than the way parts (informal) of other expressions 
+are handled, would require additional restrictions on the body_expressions 
+compared to the otherwise identical dependent_expressions of an 
+if_expression, and clearly would require some complex implementation 
+gymnastics. If you don't change the definition of master, then the 
+implementation need make no changes to finalization at all. (Besides, my 
+understanding if the restriction to local elementary entities is to get 
+finalization out of the picture; it doesn't help any to then stick it back 
+in only in Bairdian corner-cases.)
+
+Specifically, assume F returns an object with a controlled part. The 
+following if_expression is legal and has a well-defined meaning and
+implementation:
+
+         (if B then F(1) else F(2))
+
+It would be surprising if a similar declare_expression wasn't legal or meant 
+something different:
+
+         (declare
+             Foo renames Natural'(...);
+          begin
+             F(Foo))
+
+[If this is a master, the result of F(Foo) would be finalized before it was 
+made the result, which doesn't make any sense.]
+
+It would be even more surprising if sticking the if expression into a declare 
+expression would change its meaning/legality:
+
+         (declare
+             Foo renames Natural'(...);
+          begin
+             (if Foo > 10 then F(1) else F(2))
+
+since this sort of thing seems to be the motivating case for 
+declare_expressions.
+
+---
+
+Trivial changes:
+
+You didn't put the /3 references into the paragraph numbers for the 3.10.2 
+changes. That always has to be done for inserted paragraphs as their numbers 
+can change from version to version. (We don't want doubly inserted numbers, 
+so they sometimes changes, as the following paragraphs will after these
+changes.)
+
+>Add after 3.10.2(9.1/3):
+>
+>    The accessibility level of a declare_expression is
+>    the accessibility level of the *body*_expression.
+
+The first forward reference in a subclause should always have a cross-reference 
+"(see 6.9)". You could complain that the conditional expression rule preceding 
+this one doesn't do that -- but that one's wrong, and two wrongs don't make a 
+right. :-) I've added a correction for that wrong to the "clean-up" AI.
+
+---
+
+>Add after the penultimate sentence of 3.9.2(3):
+>
+>    A declare_expression is statically, dynamically, or indeterminately
+>    tagged according to its *body*_expression.
+
+It's weird to have this here, and have the similar rule for conditional 
+expressions in 4.5.7. However, given that this 3.9.2 rule reads like a 
+complete listing of possibilities, it seems like it's the conditional 
+expression rule that is misplaced. (It would have helped to show the whole 
+rule in the AI.)
+
+Thus, I suggest at least adding a mention of conditional expressions into 
+3.9.2(3). Perhaps something like:
+
+Modify 3.9.2(3):
+
+A name or expression of a tagged type is either statically tagged, dynamically
+tagged, or tag indeterminate, according to whether, when used as a controlling
+operand, the tag that controls dispatching is determined statically by the 
+operand's (specific) type, dynamically by its tag at run time, or from context.
+A qualified_expression or parenthesized expression is statically, dynamically, 
+or indeterminately tagged according to its operand. {A declare_expression is 
+statically, dynamically, or indeterminately tagged according to its 
+*body*_expression. A conditional_expression is statically, dynamically, or 
+indeterminately tagged according to rules given in 4.5.7.} For other kinds of
+names and expressions, this is determined as follows: 
+
+Moving the 4.5.7 rule here is a bit unpleasant, as it is in multiple sentences 
+and includes a Legality Rule. So it is simpler to use the cop-out suggested 
+above.
+
+If we use the cop-out rule, we can add that in this AI, or do that in the 
+clean-up AI. It's easier for me to do it here (no conflict has to be managed, 
+'cause otherwise we have two separate changes to the same paragraph), but 
+I'll let you (Bob) decide.
+
+If you would prefer to fix this right (which means adding text to both
+3.9.2(3) and 3.9.2(9/1), and deleting 4.5.7(17/3), then it has to be in the 
+clean-up AI. But that seems to violate the Duff rule of RM changes:
+shuffling wording around like this is not going to change the behavior of 
+anyone. So I'm not expecting that.
+
+---
+
+That's it, I think.
+
+***************************************************************
+
+From: Bob Duff
+Sent: Friday, October 10, 2018  7:56 PM
+
+> I've finally gotten around to reading Bob's AI here.
+
+OK, thanks.  Just so folks know:  I have not yet had a chance to read the 
+last 40 or so emails to ARG on this subject, including the one I'm replying 
+to.
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Friday, October 10, 2018  8:55 PM
+
+I've been rereading most of them as I've been filing them in the AI, and 
+approximately none of them (starting with Steve's message on Friday the 5th) 
+have anything significant to do with your actual proposal (which doesn't allow
+declaring the objects that Steve was using in his example).
+
+So I'm biased, but I think you could save quite a bit of time and skip the 
+whole lot (except my message on your actual AI and perhaps Steve's part 1 and
+my reply to that) and you won't be missing much. (Besides, you could skip the
+three different suggestions I had for fixing a problem that your AI does not 
+have. :-)
 
 ***************************************************************
 

Questions? Ask the ACAA Technical Agent