!standard 13.11(5) 18-01-26 AI12-0236-1/02 !standard 13.11.4(3/3) !class Amendment 17-09-06 !status work item 17-09-06 !status received 17-06-21 !priority Low !difficulty Medium !subject declare expressions !summary Add a new expression, the declare expression, that allows one to declare local bindings in an expression context. !problem 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 to bind the result of an expression - for example a function call - to a name, in order to reuse its value. This often leads to repeating the same expression several times within contracts. Take the following subprogram and its post-condition into consideration: procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (if The_File (Cur_Position'Old) = EOF_Ch then Cur_Position = Cur_Position'Old and then Result = EOF elsif The_File (Cur_Position'Old) = ASCII.LF then Cur_Position = Cur_Position'Old and then Result = Character'Pos (ASCII.LF) else 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). !proposal A *declare expression* allows constant objects and renamings of constants to be declared within an expression. !wording Syntax declare_expression ::= (declare {declare_item} begin *body*_expression) declare_item ::= constant_declare_item | renaming_declare_item constant_declare_item ::= defining_identifier_list : constant [subtype_indication] := expression; renaming_declare_item ::= defining_identifier [: [null_exclusion] subtype_mark] renames object_name; [TBD: Should aspect_specifications be allowed on declare_items? Should we allow access_definition in declare_items? I think not. Should we allow "aliased" in constant_declare_items? Should we allow array_type_definition in constant_declare_items? I think not. I'm allowing multiple identifiers in constant_declare_items, for uniformity with object_declarations. I'm allowing "(declare begin expression)" with no declare_items, for uniformity with block statements, which also annoyingly allow a pointless "declare".] Static Semantics 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. [TBD: The above is intended to include static semantics, name resolution, legality, and dynamic semantics. 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 (expression must denote a constant view). That AI should contain the business about *typed declarative expression*, which allows to distinguish number_declarations from object_declarations. ] Name Resolution Rules The type of a declare_expression is the type of the *body*_expression. 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. [TBD: Above rule comes from 4.5.7(8/3) for conditional_expressions.] Dynamic Semantics 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. !discussion ** TBD. !examples Post => Fun'Result = (declare X : constant T1 := F(A, B); Y : constant T2 := G(C, D); begin (if X > Y then X else Y+X)) Type_Invariant => (M : constant := 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 (if W(Q, R) then F(Q) else Z(R))); 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): 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; 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)))); !ASIS ** TBD. !ACATS test ACATS B-Test and C-Tests are needed to check that the new capabilities are supported. !appendix From: Tucker Taft Sent: Wednesday, June 21, 2017 7:07 AM Peter Chapin of Vermont Technical College, user of Ada 2012/SPARK 2014 for the "cube" sat , indicated his most frequent annoyance about the contract features of Ada are the inability to give a name to a subexpression and use multiple times in a pre- or post-condition. In most functional languages this is solved using local "let" declarations. In Ada, there seems no need to introduce "let" as a reserved word, but "declare" or "for" or "constant" seem like reasonable keywords to use for this. Here are some examples using constant/declare/for: Post => F’Result = (constant X := F(A'Old, B); Y := G(C, D'Old) => (if X > Y the X else Y)) Type_Invariant => (for M := Integer’Max(T.A, T.B) => (if M > 0 then M > T.C else M < T.D) Dynamic_Predicate => (declare Q := H(S.A, S.B); R := G(S.C, S.D) => (if W(Q, R) then F(Q) else Z(R))); I think "constant" is my favorite, since these are all implicitly constants that must have initial values, while with "declare" one might expect that a type and "constant" be explicit, whereas this is really a different sort of declaration. Also, "for" is relying on the use of ":=" to distinguish it from other sorts of iterators. I have used ";" to allow multiple constant declarations, rather than using a chain of "=>" which would probably mean multiple levels of parentheses as well. You could go with "comma" instead, but that seems too easy to miss in this context. *************************************************************** From: Florian Schanda Sent: Wednesday, June 21, 2017 7:42 AM Note that Raphael already started a proposal for this, see his message on 30/08/2016 15:28. We (Altran + SPARK Team here) think this is an excellent idea. On Wednesday 21 Jun 2017 08:05:30 Tucker Taft @ adacore wrote: > Peter Chapin of Vermont Technical College, user of Ada 2012/SPARK 2014 > for the "cube" sat , indicated his most frequent annoyance about the > contract features of Ada are the inability to give a name to a > subexpression and use multiple times in a pre- or post-condition. In > most functional languages this is solved using local "let" > declarations. In Ada, there seems no need to introduce "let" as a reserved > word, but "declare" or "for" or "constant" > seem like reasonable keywords to use for this. > > Here are some examples using constant/declare/for: > > Post => F’Result = > (constant X := F(A'Old, B); Y := G(C, D'Old) => (if X > Y the X > else Y)) > > Type_Invariant => > (for M := Integer’Max(T.A, T.B) => (if M > 0 then M > T.C else M < > T.D) > > Dynamic_Predicate => > (declare Q := H(S.A, S.B); R := G(S.C, S.D) => (if W(Q, R) then > F(Q) else Z(R))); I believe we also had "in" in the hat: (declare X := Complex_Function (A, B, C); in X + X) > I think "constant" is my favorite, since these are all implicitly > constants that must have initial values, while with "declare" one > might expect that a type and "constant" be explicit, whereas this is > really a different sort of declaration. Also, "for" is relying on the > use of ":=" to distinguish it from other sorts of iterators. I would try to put a new keyword in the ring as well, "let" doesn't really sound like an identifier that people would have used. A grep in the gnat sources for example (1.1M LOC) does not have this as a single identifier (closest is LLet and ULet for lower and upper case letter). Doing the same thing to a big project here also provides no hits. (let X := Complex_Function (A, B, C); in X + X) Just my 2c. *************************************************************** From: Tucker Taft Sent: Wednesday, June 21, 2017 7:51 AM > Note that Raphael already started a proposal for this, see his message > on > 30/08/2016 15:28. Thanks, I was trying to find the earlier proposal, but I failed. I didn't mean to preempt Raphael's proposal. ... > I believe we also had "in" in the hat: > > (declare X := Complex_Function (A, B, C); in X + X) "; in" seems weird to me. But just "in" would be ambiguous with membership. So that kills the "in" syntax for me, at least. ... > I would try to put a new keyword in the ring as well, "let" doesn't > really sound like an identifier that people would have used. A grep in > the gnat sources for example (1.1M LOC) does not have this as a single > identifier (closest is LLet and ULet for lower and upper case letter). I am afraid "let" is just too likely to have been used in many existing Ada programs. Adding a new reserved word is a very heavy burden on any proposal. *************************************************************** From: Tucker Taft Sent: Wednesday, June 21, 2017 8:37 AM Apparently not everyone has seen this AI from Raphael, or (like me) has lost track of it. ===== !standard 11.5 ??-??-?? AI12-????-1/01 !class Amendment ??-??-?? !status work item ??-??-?? !status received ??-??-?? !priority Low !difficulty Low !subject declare expressions !summary Add a new expression, the declare expression, that allows one to declare local bindings in an expression context. !problem 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 to bind the result of an expression - for example a function call - to a name, in order to reuse its value. This often leads to repeating the same expression/function call several time within contracts. Take the following subprogram and its post-condition into consideration: procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (if The_File (Cur_Position'Old) = EOF_Ch then Cur_Position = Cur_Position'Old and then Result = EOF elsif The_File (Cur_Position'Old) = ASCII.LF then Cur_Position = Cur_Position'Old and then Result = Character'Pos (ASCII.LF) else 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). !proposal We propose introducing a new expression, the declare expression, that allows computation of one or several sub-expressions, and to bind the results to names, in the lexical scope of the expression. The declare expression would allow you to bind names to the computation of expressions where each name is bound to a constant view of an expression, akin to a renaming but with forced const-ness. We chose not to re-use the assignment syntax for the bindings, because the semantics are not the same. We also choose not to re-use the renames syntax, for the same reason. With a tentative syntax for the declare expression, the previous example's post-condition for the Fgetc procedure could be expressed as: procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (declare Old_Pos : Int is Cur_Position'Old; Old_Char : Character is The_File (Old_Pos); in (if Old_Char = EOF_Ch then Cur_Position = Old_Pos and then Result = EOF elsif Old_Char = ASCII.LF then Cur_Position = Old_Pos and then Result = Character'Pos (ASCII.LF) else Cur_Position = Old_Pos + 1 and then Result = Character'Pos (Old_Char))); We also propose making the type annotation optional, to allow the user to not clutter his expressions with types in simple cases: procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (declare Old_Pos is Cur_Position'Old; Old_Char is The_File (Old_Pos); in (if Old_Char = EOF_Ch then Cur_Position = Old_Pos and then Result = EOF elsif Old_Char = ASCII.LF then Cur_Position = Old_Pos and then Result = Character'Pos (ASCII.LF) else Cur_Position = Old_Pos + 1 and then Result = Character'Pos (Old_Char))); Syntax Here is what the BNF would look like for the proposed syntax: declare_expression ::= "declare" declare_expression_bindings "=>" expression declare_expression_bindings ::= constant_view_declaration {"," constant_view_declaration} constant_view_declaration ::= defining_identifier [":" (subtype_indication | access_definition | array_type_definition)] "is" expression The "constant" qualifier is not present because the bindings are implicitly constant. The expression is mandatory, but the type annotation is optional. We'll call the expression that has access to the bound constants the "inner expression" in the following paragraphs. Name Resolution Rules The type of a declare_expression is the type of the inner expression. The expected type for the inner expression is the expected type for the declare expression. As in declarative parts, each constant_view_declaration is visible to the subsequent ones, and a constant_view_declaration immediately hides outer declarations of the same name. The expected type for the expression of a constant_view_declaration is the type after the ":", if present, and any type otherwise. Legality Rules Every constant_view_declaration is implicitly constant. Meaning that: It’s illegal to pass it to a function as an out or in-out parameter It’s illegal to take a non-constant access on a constant view. Dynamic semantics For the evaluation of a declare_expression, the constant_view_declarations are elaborated in the order given. Then the expression of the declare_expression is evaluated, converted to the type of the declare_expression, and the resulting value is the value of the declare_expression. !discussion Legality Rules There was an overwhelming agreement that we should restrict what is possible to declare in declare expressions. This can be reconsidered if compelling arguments arise for supporting a specific construct. Syntax It is not yet clear what the delimiter between the object declarations and the inner expression should be. Using "in" is ambiguous: (declare X : Boolean := True in False .. True in X and X) If we use a ";" terminator, we can use in again: procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (declare Old_Pos : Int is Cur_Position'Old; Old_Char : Character is The_File (Old_Pos); in ...) We can use "begin": procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (declare Old_Pos : Int is Cur_Position'Old, Old_Char : Character is The_File (Old_Pos) begin ...) Some commented that it looks too much like a regular procedural declare block. We can use parentheses: procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (declare (Old_Pos : Int is Cur_Position'Old, Old_Char : Character is The_File (Old_Pos)) in ...) Some commented that it makes the object declaration looks like an aggregate. procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (declare Old_Pos : Int is Cur_Position'Old, Old_Char : Character is The_File (Old_Pos) => ...) Another possibility is to reverse the order and use "with": procedure Fgetc (Stream : File_Descr; Result : out Int) with Post => (if Old_Char = EOF_Ch then Cur_Position = Old_Pos and then Result = EOF elsif Old_Char = ASCII.LF then Cur_Position = Old_Pos and then Result = Character'Pos (ASCII.LF) else Cur_Position = Old_Pos + 1 and then Result = Character'Pos (Old_Char) with Old_Pos : Int is Cur_Position'Old, Old_Char : Character is The_File (Old_Pos)); This is similar to Haskell’s "where" clause. The syntax is nice and clean, but having the bindings at the end can be confusing when dealing with long expressions. Semantics There is a debate over the semantic of bound variables. Tucker has argued that renaming semantics are generally better in this context and that it should use a different syntax so as not confused with regular object declarations: (declare X is Something_Complicated(F), Y is X.A + B => X.C + Y) The rationale is that it would be worth the cognitive overload of making the user learn a new syntax ("is") and associated semantics, because it would result in a simpler model and a simpler and more useful feature: It works with limited and non limited, entities are constant by default. On my side, I originally thought that this choice is better left to the user, and that familiarity and consistency are more important, so we should have regular object_declarations. The issues about limited types can be side-stepped by having renaming_object_declaration included. The problems and solutions will hence be the same both for declare blocks and for declare expressions. Also I feel that, from the user point of view, 98% of the time, assignment will be enough. Steve proposes that we define the semantics of the feature by using an equivalence rule based on parameter passing rather than object declarations. A let-expression could be defined to be equivalent to introducing an anonymous expression function and then calling it. However, it's a little bit messy because we would need this anonymous function to have the right visibility (e.g. if the let expression occurs in a postcondition, then the anonymous expression function needs to be able to see the parameters etc. so that hoisting it out to the enclosing declaration list wouldn't work). The example in the AI Post => (declare Old_Pos : Int := Cur_Position'Old, Old_Char : Character := The_File (Old_Pos) => (if Old_Char = EOF_Ch then Cur_Position = Old_Pos and then Result = EOF elsif Old_Char = ASCII.LF then Cur_Position = Old_Pos and then Result = Character'Pos (ASCII.LF) else Cur_Position = Old_Pos + 1 and then Result = Character'Pos (Old_Char))); would then be equivalent to implicitly declaring (somewhere) function _Anonymous_Function_ (Old_Pos : Int; Old_Char : Character) return Boolean is (if Old_Char = EOF_Ch then Cur_Position = Old_Pos and then Result = EOF elsif Old_Char = ASCII.LF then Cur_Position = Old_Pos and then Result = Character'Pos (ASCII.LF) else Cur_Position = Old_Pos + 1 and then Result = Character'Pos (Old_Char))); and then calling it with actual parameter values corresponding to the values given in the let-expression Post => _Anonymous_Function _ (Old_Pos => Cur_Position'Old, Old_Char => The_File (Old_Pos) I think this method is too complicated and unnecessary. Also, it requires the user to think in terms of parameter-passing, which is priority inversion in terms of feature design in my opinion. Implicit constness In the current proposal, bindings are implicitly constant. This is good because we don’t mix expressions and statements, but also prevent some potentially useful use cases: function Next_Element (Result : out Element) returns Boolean; declare R : Element; Has_Element : constant Boolean := Next_Element (R); in (if Has_Element then R else No_Element) The pattern of using both an out parameter and a return value has wide-spread use in some libraries (GtkAda notably) and it is not clear whether we should support that. Generalizing constant_view_declaration Question is whether we should generalize constant_view_declaration to regular declare blocks. It could be useful because there is no way of making a renaming declaration constant at the moment. Also it would keep things coherent with other areas of the code. *************************************************************** From: Tullio Vardanega Sent: Wednesday, June 21, 2017 11:19 AM I like this notion and second the intent, including the "declare" element as per Raphael's phantom AI. *************************************************************** From: Gary Dismukes Sent: Wednesday, June 21, 2017 3:22 PM > I think "constant" is my favorite, since these are all implicitly constants > that must have initial values, while with "declare" one might expect that a > type and "constant" be explicit, whereas this is really a different sort of > declaration. Also, "for" is relying on the use of ":=" to distinguish it from > other sorts of iterators. Another possibility would be "with". (I note that Raphael used that in one of the examples in his "declare expression" AI, but at the end of the construct.) That scans well to me, and has an advantage of being short, though I suppose that some might feel that we shouldn't overload "with" further. > I have used ";" to allow multiple constant declarations, rather than using a > chain of "=>" which would probably mean multiple levels of parentheses as > well. You could go with "comma" instead, but that seems too easy to miss in > this context. I agree with using ';' for multiple decls. *************************************************************** From: Erhard Ploedereder Sent: Wednesday, June 21, 2017 8:12 PM I have semantic questions first, before I have an opinion on syntax: Is the scope of these ghost variables only the respective PRE or POST expression, or does the scope extend across PRE and POST? (The write-ups in most places imply the latter, in others the former. Raphael's analogies certainly go for the former; Tuck's write-up starts out speaking of both PRE and POST.) Intuitively, I am inclined to argue for the latter, since it would be a real nuisance to replicate the declarations in both PRE and POST, if needed in both places. Then the "let" or "where" syntax inside of PRE and POST clearly is not a good choice. Since both proposals work with type inference on ghosts, presumably calls on overloaded functions where the result type could disambuiate an otherwise ambigous call are illegal. Or does one get the chance to slip a type in? *************************************************************** From: Tucker Taft Sent: Thursday, June 22, 2017 1:20 AM These names are local to the parenthesized construct, similar to the scope of a loop variable inside a quantified expression. I frankly can’t imagine how we could bound the scope if we allowed it to extend past the matching right parenthesis. Sorry if I implied otherwise by one of my examples. The intent is that type annotations are optional, but are certainly allowed. Hence: Post => Fun'Result = (constant X : T1 := F(A, B); Y : T2 := G(C, D) => (if X > Y then X else Y+X)) By the way, I agree with Gary that replacing "constant" with "with" would also read well. *************************************************************** From: Tucker Taft Sent: Thursday, June 22, 2017 1:26 AM > These names are local to the parenthesized construct, similar to the scope > of a loop variable inside a quantified expression. I frankly can’t imagine > how we could bound the scope if we allowed it to extend past the matching > right parenthesis. Sorry if I implied otherwise by one of my examples. Sharing the declarations between Pre and Post would also be pretty difficult to define, in my view, since Pre and Post are evaluated at different times. *************************************************************** From: Erhard Ploedereder Sent: Thursday, June 22, 2017 7:19 AM I'll throw one more into the ring (it is similar to one of Raphael's but with different keywords): Post => Fun'Result = (with X = F(A, B), Y = T1'(G(C, D)) => (if X > Y then X else Y+X)) Syntax: 'with' ghost-decl_list ghost-decl_list -> identifier '=' expression {',' ghost_decl_list } Alternatively, see below: identifier '=' simple_expression {'and' ghost_decl_list } ---- I did not like the similarity, yet difference among constant X : T1 := F(A, B); vs. X : constant T1 := F(A, B); a ghost decl vs. an object declaration, where the "constant" goes elsewhere. ---- Use "=" in lieu of ":=", because PRE and POST are all about assertions, and here I assert that "X = something". Raphael uses "IS". I see no reason why not to use "=". Moreover, if eventually "constant" is not used then ":=" looks like assigments to ghosts are acceptable. ---- Use a qualified expression to disambiguate/document in lieu of not-quite declaration syntax. ---- On creating multiple ghosts, I am rather neutral on what is between them, but have a few comments: - ";" : with a semicolon I have a slight preference to repeat "with" i.e. "; with" - "," : o.k. to me - "and" : would be my preference in staying with the notion that this an assertion, even if this raises the spectre of the (via the use of simple_expression unambigous) with A = B and C = D+5 with A = (B and E) and C = D+5 *************************************************************** From: Tucker Taft Sent: Thursday, June 22, 2017 7:38 AM I agree there are some nice things about using "=", but it isn't consistent with Ada's current semantics. "=" is always symmetric in Ada, but now you are proposing that the left hand side is an implicit declaration, which is quite a shift in my mind. Even named numbers use ":=" in Ada, so it is quite consistent to use ":=" for introducing a constant. *************************************************************** From: Randy Brukardt Sent: Friday, June 23, 2017 2:25 PM Here's my 50 cents worth on this topic: Tucker wrote: > Apparently not everyone has seen this AI from Raphael, or (like me) > has lost track of it. I blame operator error. No one saw it, because he never sent it to the list. I went back and checked the logs for 8-29, 8-30, and 8-31, and no mail was received from Raphael on any of those days. But other people's mail was received from the Adacore server that his mail typically comes from on two of those days. And he's managed to send 48 other messages to the ARG list. Erhard said: > I did not like the similarity, yet difference among > constant X : T1 := F(A, B); vs. X : constant T1 := F(A, B); > a ghost decl vs. an object declaration, where the "constant" goes > elsewhere. This is a good point, but if you take that to the limit, you'd have to have (declare X : constant T1 := F(A, B) begin ... ) and even then the lack of an end is a difference (we decided when dealing with if expressions that we didn't want "end" in expressions, so I'm assuming that still holds). Those looking for a shorthand are going to want to be able to write less than this. And the syntax is never going to exactly the same. So I lean toward the "constant" version; the keyword "constant" MUST appear somewhere in or in front of these declarations, lest they be misinterpreted as variables. (I've always thought they WERE variables until Tucker made his proposal.) Making that the primary keyword seems like a useful compromise. Tucker said: > Sharing the declarations between Pre and Post would also be pretty difficult > to define, in my view, since Pre and Post are evaluated at different times. And in particular, the parameters may have different values when they are evaluated. Any long-term declaration of these things seem like madness. Tucker wrote: >The intent is that type annotations are optional, but are certainly allowed. I don't think that they can be optional, either philosophically or practically. Philosophically, Ada does not use type inference to declare anything. In the majority of cases where Ada allows the type name to be omitted, the type is uniquely determined by some other construct (the cursor type for an iterator, the element type for an iterator, for the lambda proposal it's determined by the access-to-subprogram type's parameter). The only exception that I can think of is the index type for a for loop; that gets determined by the range, but that itself isn't required to be specified. And that case has annoying hacks (fall back to Integer if all else fails), it certainly isn't a model that we'd want to emulate. Practically, there are a lot of likely expressions that wouldn't be allowed without a type name. Consider: (constant X := (if Some_Param > MAX then MAX else 10 => (if Some_Param > X then ...) The user probably would expect this to have type universal_integer, but they'd be wrong; this isn't a static expression, so the type preference to root_integer would apply (and has to apply, we've just discussed this in AI12-0227-1). Since root_integer isn't a nameable type, Some_Param has a different type and the expression (specifically the comparison of Some_Param to X) is illegal. This is not going to make us friends among Ada users. Similarly, the Bob Duff example for if expressions is outright ambiguous: (constant Item_Label := (if Items = 1 then "Item" else "Items) => ( ... raise Constraint_Error with "Failed with " & Items'Image & Item_Label)) This is ambiguous because a string literal can have any of the predefined string types. Moreover, if these are "annotations" rather than "specifications", then they shouldn't change the resolution. That means that neither of the above should work right even if the intended type name is given. People would string us up in trees if that was the case (and rightly so). (constant X : Integer := (if Some_Param > MAX then MAX else 10 => (if Some_Param > X then ...) (constant Item_Label : String := (if Items = 1 then "Item" else "Items) => ( ... raise Constraint_Error with "Failed with " & Items'Image & Item_Label)) It would be madness if either of these don't work as everyone expects. The only way that I can see allowing the type name being omitted is if the initializing expression is a type conversion, qualified expression, or a stand-alone object (those not allowing any overloading, so they unambiguously determine a type), or an indexed or selected expression with one of these as the prefix. That seems too wacky to me, but perhaps the value of allowing it for an extreme shorthand outweighs the weirdness. In any case, I think the type name has to be required in general, and if we allowed it at all, we could only allow omitting it for certain expressions. *************************************************************** From: Tucker Taft Sent: Friday, June 23, 2017 3:30 PM > ... > In any case, I think the type name has to be required in general, and > if we allowed it at all, we could only allow omitting it for certain > expressions. I think it is quite important to be allowed to omit the type name (this is a short hand after all). Iterators allow the type name to be omitted, and I see this as a close relative of iterators. But I agree with some of your concerns. Perhaps it can be omitted only if the initializing expression is syntactically a primary, which includes function calls, qualified expressions, conditional expressions, and many other useful things. *************************************************************** From: Randy Brukardt Sent: Friday, June 23, 2017 6:56 PM Both of the problematic cases I showed in the previous message are primaries (if expressions, specifically), so that wouldn't really help anything. I could see adding some explicit rules for conditional expressions. Perhaps we'd want a term so the rules would be easy to craft: A *typed declarative expression* is either: * a name statically denoting a stand-alone object; * a qualified expression; * a type conversion; * a parenthesized expression whose operand is a typed declarative expression; * a conditional expression where at least one operand is a typed declarative expression; * a predefined operator other than & where at least one operand is a typed declarative expression. All of these have a uniquely determined type, and it won't change because of future maintenance elsewhere (only direct changes, never a problem, or changing the type of the stand-alone object, hardly something that people would be surprised about). I don't think we can allow function calls, because adding/modifying a visible operation somewhere else could change the type of such a declaration (or make it illegal via ambiguity or this rule). Anyway, food for thought. *************************************************************** From: Tucker Taft Sent: Wednesday, January 31, 2018 9:00 AM [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 > (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. ... I missed or have forgotten the discussion of "typed declarative expressions." Who has that AI? 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. *************************************************************** From: Bob Duff Sent: Wednesday, January 31, 2018 2:16 PM > 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 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 > 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 > > 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. ... I believe Raphaël volunteered for the above-mentioned AI. I don't know if 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. So if we allow the compiler to deduce the type from the renamed object, it should work the same in both cases. I removed a bunch of verbiage about it from THIS AI, which Raphaël might want to copy (from the old version). Similar comments apply to the syntax "X: constant := expression;". That's a bit tricky, because what is now a named number should keep the same semantics. But I was hoping to allow "X: constant := Y;" where Y is of (say) a private type, and X is deduced to be of the same type. Both in a declare_expression, and as a normal declaration. I'm not sure we discussed the "constant" part, but I think it would be really weird to do other than I described above. *************************************************************** From: Randy Brukardt Sent: Wednesday, January 31, 2018 5:55 PM > 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 > constant_declare_item. A "typed declarative expression" is an expression that allows the omission of the type name in a constant declaration. I think requiring a special form would rather defeat the purpose (allowing shorter specification of constants in declare exprs). > > Here is a new version of AI12-0236-1 declare expressions. > > 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 > > subtype_mark (expression must denote a constant view). My recollection of the Lexington discussions was that we wanted this generally *only* for renames expressions, and for those, omitting the type would always be allowed, assuming of course that the "name" resolves without context. In particular, we did not want to allow the omission of the type name for constant declarations, because of confusion with named numbers and because of the violation of a principle that anything declared has a nominal subtype. 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 > > from object_declarations. ... We didn't want to do that; the "typed declarative expression" was simply about whether the subtype name could be omitted. I thought we had decided to drop that business in favor of pure resolution (that is, if the expression can be resolved without any context, you can drop the subtype name) in the case of "constants" in declarative expressions. 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. *************************************************************** From: Bob Duff Sent: Wednesday, January 31, 2018 7:46 PM > 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 mine. But it still seems to me that when it comes to inferring the type of an object, we should make renamings and constants work the same, and we should make these things work the same inside declare_expressions and as regular declarations. 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. 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 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 > perfect note-taking. Perhaps, but I bow down to your superior note-taking abilities. *************************************************************** From: Randy Brukardt Sent: Wednesday, January 31, 2018 8:27 PM ... > 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. keyword "static" in place of "constant"), and thus that there is no such thing 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 > a regular decl not in a declare_expr). I understand your point, but... 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. 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. Omitting it is just going to confuse readers; it's hard to figure out the nominal subtype of an expression in general. 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'd follow your principle and not allow dropping the subtype name anywhere from a constant declaration. (I'd also consider making a keyword "static" that could be used in number declarations -- optionally, for compatibility, sigh -- and allow a number declaration to have an expression of any type that can be static. That would be especially useful if we allowed user-defined static types and operations, but it appears that we're not doing that. End rather unrelated tangent.) However, everyone that really wants declare expressions also wants to be able to write them without as much text as possible, so I'm willing to allow dropping the subtype name there -- a constant in a declare expression is much more like a renames than it is an object declaration (especially if it is of a composite type) -- I hope we're not requiring copying here as we do for "real" constant declarations. Anyway, I'm trying to understand others concerns here and be flexible so long as that doesn't require making a hash out of basic Ada principles. *************************************************************** 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 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 > semantics of the constant declaration. 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 can think of several rules. Perhaps: the nominal subtype is the subtype of 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, > 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 Circus", by Dr. Seuss. You can pick up a copy here for $200.00: 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" >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 semantics in declare_expressions than for "real" constant decls. Isn't the whole point of allowing both constants and renamings is to let you choose "constant" semantics or "renaming" semantics? *************************************************************** 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 > it's not explicit in the constant decl). If we allow missing subtype indication ONLY in declare_exprs, we STILL need to define "nominal subtype", right? *************************************************************** From: Randy Brukardt 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 > > 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 > 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 it matters in various other places. I often find myself searching for a subtype name in order to write a "use type" clause. That requires finding the declaration (annoying enough, especially if it is in a different file) and then extracting the type name (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 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 subtype name. I'm only willing to do so for renames because (A) the subtype name given is a lie anyway, properties come from the original object; and (B) renames is rarely used in the code I've seen. I'd prefer to see less optional stuff in Ada, not more. (Initializers [with <> meaning explicit no initialization], ending ids, parameter modes all should be 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" >>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 >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 >let you choose "constant" semantics or "renaming" semantics? I thought it was because Steve thought he needed more never-used cases for his Bairdian execution examples. :-) There aren't a lot of good uses for renames (did you know that a rename actually makes the code worse in Janus/Ada? It prevents the name from getting evaluated in the a register, forcing extra memory writes). I wouldn't miss them if they didn't exist at all. OTOH, the idea of adding nested masters in the middle of expressions seems 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 composite objects); the ability to "ignore" these scopes would be eliminated. I was imagining that these objects would get assigned to temporaries (usually registers) and would never be materialized at all. That's not possible for composite objects (if real). The original proposal (which gave rename semantics to these guys) had the appropriate properties. I'm now thinking that we should only allow renames in declare exprs; that 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. ***************************************************************