CVS difference for ai05s/ai05-0153-3.txt
--- ai05s/ai05-0153-3.txt 2012/01/05 06:19:32 1.21
+++ ai05s/ai05-0153-3.txt 2012/04/20 01:24:18 1.22
@@ -1298,6 +1298,575 @@
!appendix
+From: Bob Duff
+Sent: Friday, October 8, 2010 5:07 PM
+
+Here is a new version of AI05-0153-1, Subtype predicates.
+[This is version /01 of AI05-0153-3 - Editor.]
+
+Comments welcome!
+
+I think I've dealt with all the (many!) e-mails on the subject.
+I tried to fairly address all the various concerns, even the ones I disagree
+with.
+
+This version is based primarily on AI05-0153-1/06, but I also incorporated all
+the useful functionality from AI05-0153-2, by defining certain subtypes with
+predicates to be static, and allowing those in case stms and for loops and
+whatnot.
+
+Problematic things like 'First are simply illegal in the presence of predicates
+(whether static or not).
+
+Robert has already done a prototype implementation in GNAT, which includes
+pretty-much all of the functionality described here (modulo a few bugs).
+
+****************************************************************
+
+From: Brad Moore
+Sent: Saturday, October 9, 2010 6:30 PM
+
+Just read this proposal, I have some minor editorial comments.
+
+1) "AARM Note: This is {the} usual way around the contract model."
+
+
+2) 5.4(7/3), "delete one of the two consecutive "that satisfy the predicate"
+
+
+"{AI05-0003-1} If the expression is a name [(including a
+ type_conversion, a qualified_expression, or a function_call)] having a
+ static and constrained nominal subtype, then each non-others
+ discrete_choice shall cover only values in that subtype
+ [{that satisfy the predicate}]{that satisfy the predicate},
+
+
+3) Put (Obj in Decimal_Rec); -- (3)
+
+Should that be Put (Boolean'Image(Obj in Decimal_Rec)); -- (3)
+
+Assuming Put refers to Text_IO.Put?
+
+Regarding the earlier question whether to go with one aspect or two, I am
+undecided, though I think if if we can accomplish the same thing more or less,
+with just one aspect, then I think that would be preferable.
+
+I need to have another look at the Set Constraints proposal, but at least the
+reasoning and ideas behind this proposal as presented here make sense to me,
+seem reasonable, and have appeal. It's good to have the comparison between
+invariants, predicates, and constraints, in particular invariants vs predicates,
+since those are both new features.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, October 11, 2010 11:03 AM
+
+> Just read this proposal, I have some minor editorial comments.
+
+Thanks for the review. I will hold off on updating the AI until more folks have
+had a chance to read it. I realize it's long, and many won't be bothered until
+the meeting.
+
+> 3) Put (Obj in Decimal_Rec); -- (3)
+>
+> Should that be Put (Boolean'Image(Obj in Decimal_Rec)); -- (3)
+>
+> Assuming Put refers to Text_IO.Put?
+
+I adapted this example from something somebody (Randy?) wrote, and I assume he
+meant Put to be "some misc procedure that writes booleans".
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, October 27, 2010 1:47 PM
+
+ > package falsetrue is
+ > type r is array (0 .. 7) of Boolean;
+ > pragma Pack (r);
+ >
+ > type s is new r with
+ > Pack => False;
+ > False : Boolean := True;
+ > end;
+
+The decision to delay all aspects means that type s is packed after all. The
+amount of mechanism needed in GNAT to accomodate this is truly annoying. I am
+tempted to ignore it, but according to the rules, this should work :-( :-(
+
+****************************************************************
+
+From: Bob Duff
+Sent: Wednesday, October 27, 2010 2:39 PM
+
+The latest version of the AI, which I sent out recently, does not allow "Pack =>
+False". This is not any official ARG decision -- just me shying away from
+wondering what "Atomic => False" might mean, so I simply required True for all
+of them. No ARG member has commented on that, much less voted on it.
+
+I'm a little surprised that the above is hard to implement, though. Seems like
+it would fall out naturally from the "delay resolution".
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, October 27, 2010 2:58 PM
+
+> The latest version of the AI, which I sent out recently, does not
+> allow "Pack => False". This is not any official ARG decision -- just
+> me shying away from wondering what "Atomic => False" might mean, so I
+> simply required True for all of them. No ARG member has commented on
+> that, much less voted on it.
+
+I think => False is really useful
+
+As to what Atomic => False means, not clear to me if Atomic is inherited for a
+derived type,
+
+ if so, False is useful and cancels the aspect
+
+ if not, still useful since it can be used to parametrize
+ (False = as though pragma were not specified).
+
+ This is all implemented in GNAT, and I don't intend to
+ unimplement it, since it is clearly useful I would say.
+
+
+ X : Integer with
+ Atomic => Integer_Atomic_On_This_Target;
+
+this kind of parametrization seems useful.
+
+If you don't allow False, there is no point in allowing True, just decide that
+you don't have a parameter at all in such cases. But I like the cancellation
+facility, it does not exist now, and is useful.
+
+> I'm a little surprised that the above is hard to implement, though.
+> Seems like it would fall out naturally from the "delay resolution".
+
+Well I was doing cancellation with short cuts. Indeed it should fall out ... I
+was checking specifically for a static expression with value False, and not
+delaying properly.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, October 28, 2010 12:40 AM
+
+> As to what Atomic => False means, not clear to me if
+> Atomic is inherited for a derived type,
+>
+> if so, False is useful and cancels the aspect
+
+That's the problem, canceling the aspect breaks the model of Atomic for generic
+formal derived types. We'd have to disallow Atomic generic formals altogether if
+turning off Atomic is possible. That seems bad. Not sure if there are other,
+similar problems with other aspects - don't really think it is worth the
+headaches.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, October 28, 2010 4:50 AM
+
+I really don't understand,
+
+ type R is ... with
+ Atomic => False;
+
+is just equivalent to not having the aspect at all.
+
+Can you give an example showing exactly what you have in mind?
+
+****************************************************************
+
+From: Bob Duff
+Sent: Thursday, October 28, 2010 7:40 AM
+
+> type R is ... with
+> Atomic => False;
+>
+> is just equivalent to not having the aspect at all.
+
+That can't be right -- if it's equivalent to nothing, then what's the use of it?
+
+I thought the point was that you wanted to override "True" aspects with "False".
+I'm not particularly opposed to that, so long as it doesn't cause trouble.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, October 28, 2010 8:07 AM
+
+> That can't be right -- if it's equivalent to nothing, then what's the
+> use of it?
+
+I have explained this before, it is useful for system configuration, as in
+
+ type R is ... with
+ Atomic => Target_Supports_Atomic;
+
+Since Ada is weak when it comes to this kind of configuration (lacking
+preprocessor capability), it is useful to have that kind of support in the
+language.
+
+then in the code you lock if Target_Supports_Atomic is False.
+
+> I thought the point was that you wanted to override "True" aspects
+> with "False". I'm not particularly opposed to that, so long as it
+> doesn't cause trouble.
+
+That's another use.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, October 28, 2010 10:40 PM
+
+The problem is with turning off Atomic on derived types. I don't recall the
+exact details, but Steve remembers sending me the message with an explanation of
+how that would cause trouble for the rules about Atomic types and parameter
+passing (so it's not my imagination). Hopefully Steve will explain.
+
+My more general point is that a lot of the rules about derived types were
+developed with the idea that certain aspects could not be removed. Eliminating
+that invariant means that we need to examine many of the rules about derived
+types (especially about the contract rules for generic derived types) to ensure
+that doesn't cause trouble. And I'm unsure that this capability is worth the
+likelyhood of introducing this sort of bug.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, October 29, 2010 1:47 PM
+
+sounds reasonable, of course you could simply say that such cancellation was not
+allowed for derived types, still retaining the useful configuration capability
+for other cases.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, October 29, 2010 8:47 AM
+
+Disallowing turning "off" certain aspects like Atomic or Volatile would seem
+preferable to disallowing the use of "with Atomic => False" altogether. I agree
+with Robert that there might be value to allowing the use of a static Boolean
+expression for specifying Atomic on a non-derived type.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, October 29, 2010 7:14 PM
+
+> 12 amendment AI's taken care of, out of 29 pending. No large changes on
+aspects, expression functions, quantified expressions, etc. On predicates,
+decision for two separate aspects: Dynamic_Predicate (pretty much anything
+goes) and Static_Predicate (aka discrete subtypes with holes, what everybody
+wants). Currently discussing the resolution rules for membership tests, more
+details later.
+
+OK, I think I will keep Predicate, covering both possibilities, and then
+implement Dynamic_Predicate and Static_Predicate on top of that, seems the
+easiest and most general approach.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, October 29, 2010 7:46 PM
+
+Interesting, unless you adopt a special rule, you can have both a static
+predicate and a dynamic predicate for the same type, since they are separate
+aspects. Personally I would forbid this, but it needs a special rule for sure.
+
+If you have both a static and a dynamic predicate it's a bit silly, since the
+result of anding them is clearly dynamic!
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, October 29, 2010 7:55 PM
+
+More fun and games, if you inherit a dynamic predicate, are you allowed to
+define a static predicate.
+
+I take the view in the implementation for now, that if you define a static
+predicate, then the entire predicate must be static, but the business of mixing
+static and dynamic predicates seems a bit of a mess, given they can possibly be
+mixed on a single entity, or inherited mixed.
+
+No big deal, ust need the rules.
+
+For the GNAT aspect predicate, it's simple you just AND together the inherited
+and current predicates and if the result is static, then you have a staic
+predicate, if not you have a dynamic predicate.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, October 29, 2010 8:40 PM
+
+> 1. procedure statdynampred1 (A : Integer) is
+> 2. subtype R1 is Integer with
+> 3. Static_Predicate => R1 > A; -- not static
+> |
+> >>> expression does not have required form for
+> static predicate
+>
+> 4.
+> 5. subtype R2 is Integer with
+> 6. Dynamic_Predicate => R2 in 3 .. 7;
+> 7.
+> 8. begin
+> 9. for J in R2 loop -- not a static predicate
+> |
+> >>> cannot use subtype "R2" with non-static
+> predicate for loop iteration
+>
+> 10. null;
+> 11. end loop;
+> 12. end;
+
+and a correct one
+
+> 1. with Text_IO; use Text_IO;
+> 2. procedure statdynampred2 is
+> 3. procedure SD (A : Integer) is
+> 4. subtype R1 is Integer with
+> 5. Dynamic_Predicate => R1 > A; -- not static
+> 6.
+> 7. subtype R2 is Integer with
+> 8. Static_Predicate => R2 in 3 .. 7;
+> 9.
+> 10. begin
+> 11. for J in R2 loop -- not a static predicate
+> 12. Put_Line (J'Img);
+> 13. end loop;
+> 14.
+> 15. Put_Line (Boolean'Image (100 in R1));
+> 16. Put_Line (Boolean'Image (10 in R1));
+> 17. end;
+> 18.
+> 19. begin
+> 20. SD (23);
+> 21. end;
+
+with the proper output:
+
+> 3
+> 4
+> 5
+> 6
+> 7
+> TRUE
+> FALSE
+
+:-)
+
+I am not sure I have the rules right for mixing static and dynamic predicates,
+because I don't know what they are :-) but I am sure any reasonable or
+unreasonable set of rules can be easily accomodated. I don't care too much,
+since I think in practice I would be more likely to use the more general GNAT
+predicate form than the two specific ones.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, November 19, 2010 2:32 PM
+
+Interesting, yes, immediate eval of booleans simplifies stuff some
+
+And not allowing cancellation of aspects on derived types saves some code
+
+BUT, I am finding that the error check that a boolean aspect on a derived type
+is confirming is more than replacing the complexity of those two items :-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, November 20, 2010 8:06 AM
+
+I am confused about exactly what we decided.
+
+First what exactly is the rule now, GNAT
+allows:
+
+> package q is type T1 is new integer; type T2 is new T1; pragma Atomic
+> (T2); end;
+
+Is it right to do so?
+
+If so, this is equivalent to
+
+> package q is type T1 is new integer; type T2 is new T1 with Atomic =>
+> True; end;
+
+which is a non-confirming boolean aspect on a derived types. At least at one
+point we said that boolean aspects on derived types could only be confirming,
+and the minutes confirm this:
+
+> Bob says that we simply should not allow boolean aspects on derived
+> types. Someone notes that we always allow confirming aspects. But you
+> can't change the inherited value.
+
+For sure in the Pack case you can pack a derived type when the parent is not
+packed, so it is definitely the case that Pack => True should be allowed for
+derived types.
+
+So I guess the rule about not changing an inherited value only applies if the
+inherited value is True, i.e. it is a rule that prohibits cancelling an
+inherited attribute.
+
+A question to sort out is exactly which boolean aspects are inherited by a
+derived type, not clear that all are.
+
+In GNAT we have the following list of boolean attributes:
+
+> Aspect_Ada_2005, -- GNAT
+> Aspect_Ada_2012, -- GNAT
+> Aspect_Atomic,
+> Aspect_Atomic_Components,
+> Aspect_Discard_Names,
+> Aspect_Favor_Top_Level, -- GNAT
+> Aspect_Inline,
+> Aspect_Inline_Always, -- GNAT
+> Aspect_No_Return,
+> Aspect_Pack,
+> Aspect_Persistent_BSS, -- GNAT
+> Aspect_Preelaborable_Initialization,
+> Aspect_Pure_Function, -- GNAT
+> Aspect_Shared, -- GNAT (equivalent to Atomic)
+> Aspect_Suppress_Debug_Info, -- GNAT
+> Aspect_Unchecked_Union,
+> Aspect_Universal_Aliasing, -- GNAT
+> Aspect_Unmodified, -- GNAT
+> Aspect_Unreferenced, -- GNAT
+> Aspect_Unreferenced_Objects, -- GNAT
+> Aspect_Volatile,
+> Aspect_Volatile_Components);
+
+plus the ones for library units, but inheritance does not come into play here
+because these do not apply to types. so we can ignore this second list
+
+> Aspect_All_Calls_Remote,
+> Aspect_Compiler_Unit, -- GNAT
+> Aspect_Elaborate_Body,
+> Aspect_Preelaborate,
+> Aspect_Preelaborate_05, -- GNAT
+> Aspect_Pure,
+> Aspect_Pure_05, -- GNAT
+> Aspect_Remote_Call_Interface,
+> Aspect_Remote_Types,
+> Aspect_Shared_Passive,
+> Aspect_Universal_Data, -- GNAT
+
+Now clearly for some of the GNAT ones such as Unreferenced, the aspect is not
+inherited from the parent (never has been) and so we can certainly say
+Unreferenced => False as a confirming clause (since it would be false anyway in
+the absence of setting it True).
+
+What about the language defined aspects that apply to types:
+
+> Aspect_Atomic,
+> Aspect_Atomic_Components,
+> Aspect_Discard_Names,
+> Aspect_Pack,
+> Aspect_Preelaborable_Initialization,
+> Aspect_Unchecked_Union,
+> Aspect_Volatile,
+> Aspect_Volatile_Components
+
+Are these all inherited from the parent? I think the answer is yes, so that
+means the above is the list for which we must check on "aspect => False" that we
+are not trying to cancel an aspect, but we do allow "aspect => True" for these
+cases for derived types.
+
+Although I must say Discard_Names is a bit dubious on a derived type. It does
+nothing, since the table of names is inherited for a derived type regardless.
+
+If it is allowed to use pragma Discard_Names on a derived type, I guess we
+should (in GNAT) add a warning that it does nothing.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, November 20, 2010 9:16 AM
+
+> I am confused about exactly what we decided.
+
+I think we decided that the "=> False" case must be confirming. The "=> True"
+case (and the case with no "=>...") can override the inherited value.
+
+> So I guess the rule about not changing an inherited value only applies
+> if the inherited value is True, i.e. it is a rule that prohibits
+> cancelling an inherited attribute.
+
+Right, that's another way of putting it.
+
+> Now clearly for some of the GNAT ones such as Unreferenced, the aspect
+> is not inherited from the parent (never has been) and so we can
+> certainly say Unreferenced => False as a confirming clause (since it
+> would be false anyway in the absence of setting it True).
+
+It seems to me that implementations should be allowed to define the semantics of
+implementation-defined things (aspects, pragmas, restrictions, etc). So the RM
+has no business telling GNAT what to do with Unreferenced.
+
+An implementation can have a Boolean aspect that is not required to be static,
+for example.
+
+> What about the language defined aspects that apply to
+> types:
+>
+> > Aspect_Atomic,
+> > Aspect_Atomic_Components,
+> > Aspect_Discard_Names,
+> > Aspect_Pack,
+> > Aspect_Preelaborable_Initialization,
+> > Aspect_Unchecked_Union,
+> > Aspect_Volatile,
+> > Aspect_Volatile_Components
+>
+> Are these all inherited from the parent?
+
+I think so.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, November 20, 2010 11:33 AM
+
+Just confirming that the implementation of the new approach for boolean aspects is straightforward:
+
+> 1. pragma Ada_2012;
+> 2. package baspect2 is
+> 3. type P is array (0 .. 31) of Boolean with
+> 4. Pack => True;
+> 5. type U is array (0 .. 31) of Boolean with
+> 6. Pack => False;
+> 7. type DP1 is new P with
+> 8. Pack => True; -- OK
+> 9. type DU1 is new U with
+> 10. Pack => False; -- OK
+> 11. type DP2 is new P with
+> 12. Pack => False; -- ERROR
+> |
+> >>> derived type "DP2" inherits aspect "pack", cannot cancel
+>
+> 13. type DU2 is new U with
+> 14. Pack => True; -- OK
+> 15. end;
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, November 20, 2010 11:54 AM
+
+Looks correct to me.
+
+****************************************************************
+
From: Jean-Pierre Rosen
Sent: Thursday, December 23, 2010 10:01 AM
Questions? Ask the ACAA Technical Agent