CVS difference for ai05s/ai05-0153-3.txt

--- ai05s/ai05-0153-3.txt	2011/02/11 04:48:24	1.7
+++ ai05s/ai05-0153-3.txt	2011/02/11 04:57:17	1.8
@@ -1,4 +1,4 @@
-!standard  3.2.4(0)                                11-02-08    AI05-0153-3/03
+!standard  3.2.4(0)                                11-02-10    AI05-0153-3/04
 !class Amendment 09-05-27
 !status work item 09-05-27
 !status received 09-05-27
@@ -99,6 +99,8 @@
 Letter is also allowed in a 'for' loop, but nonstatic cases
 are not.
 
+Note that case_expression and if_expression are defined in AI05-0188-1.
+
 !wording
 
 This AI depends on AI05-0183-1, which defines the syntax for
@@ -166,9 +168,10 @@
 
     - a static expression that does not raise any exception;
 
-    - a membership test whose simple_expression is the current instance, and
-      whose membership_choice_list obeys the rules for a static membership test
-      given in 4.9;
+    - a membership test whose simple_expression is the current instance,
+      or a case_expression whose *selecting_*expression is the current instance,
+      if this expression would be static if the current instance
+      were replaced with a static expression;
 
     - a call to a predefined equality or ordering operator, where one operand
       is the current instance, and the other is a static expression;
@@ -211,19 +214,24 @@
 
 If any of the above Legality Rules is violated in an instance of a generic
 unit, Program_Error is raised.
-AARM Note: This is usual way around the contract model.
+In addition to the places where Legality Rules normally apply (see
+12.3), this rule applies also in the private part of an instance of a generic
+unit.
+
+AARM Note: This is usual way around the contract model. The "In addition..."
+wording is included for consistency with similar rules, even though it's
+not really necessary, since Program_Error will be raised anyway.
 
 
                           Implementation Permissions
 
-A Static_Predicate check may be omitted if the subtype with the predicate
-statically matches the nominal subtype of the value being checked.
+When the Dynamic Semantics calls for a check of a value against a
+Static_Predicate, the check may be omitted if every value that obeys the
+Static_Predicates of the nominal subtype of the value also obeys the
+Static_Predicate being checked against.
 
-AARM Reason: Well-behaved predicates should not have side effects that matter,
-so omitting the check is pretty harmless. It is possible to write
-non-well-behaved predicates, which is why the permission is needed. If the
-implementation does omit a predicate check, it cannot later assume that the
-predicate was True.
+AARM Reason: If the implementation does omit a predicate check, it cannot later
+assume that the predicate was True, unless that can be proven.
 
 
 NOTE: A predicate clause does not cause a subtype to be considered
@@ -312,16 +320,27 @@
 
   A constraint is statically compatible with a scalar subtype if it statically
   matches the constraint of the subtype, or if both are static and the
-  constraint is compatible with the subtype.  A constraint is statically
+  constraint is compatible with the subtype. A constraint is statically
   compatible with an access or composite subtype if it statically matches the
-  constraint of the subtype, or if the subtype is unconstrained.  One subtype
-  is statically compatible with a second subtype if the constraint of the first
-  is statically compatible with the second subtype, and in the case of an
-  access type, if the second subtype excludes null, then so does the first.
-  {Also, if either subtype has a user-defined predicate, then the first is
-  statically compatible with the second only if they statically match, or if
-  both subtypes are static, and every value that obeys the predicate of the
-  first obeys the predicate of the second.}
+  constraint of the subtype, or if the subtype is unconstrained. [One subtype is
+  statically compatible with a second subtype if the constraint of the first is
+  statically compatible with the second subtype, and in the case of an access
+  type, if the second subtype excludes null, then so does the first.]
+
+  {Two statically matching subtypes are statically compatible with each other.
+  In addition, a subtype S1 is statically compatible with a subtype S2 if:
+
+      - S1's constraint is statically compatible with S2, and
+
+      - if S2 excludes null, so does S1, and
+
+      - either:
+
+        - all predicate clauses that apply to S2 apply also to S1, or
+
+        - both subtypes are static, and every value that obeys S1's
+          predicate also obeys S2's predicate.}
+
 
 Modify 5.4(7/3), so the full coverage rules for case statements
 take predicates into account:
@@ -474,11 +493,33 @@
 Also, "and then" and "or else" are not included (if they were,
 they would mean the same thing as "and" and "or").
 
+A membership_test with a list of values can be used as a Static_Predicate:
+
+    type Animal is (Dog, Cat, Shark, Boa_Constrictor);
+
+    subtype Pet is Animal with Static_Predicate => Pet in Dog | Cat;
+
+But now if Parrot is added to Animal, there is no warning that the programmer
+had better decide whether it makes a good pet.  It might be better to use
+a case_expression, in order to benefit from the full coverage rule:
+
+    subtype Pet is Animal with
+        Static_Predicate =>
+            (case Pet is
+                when Dog | Cat => True,
+                when Shark | Boa_Constrictor => False);
+
+Now adding Parrot to Animal causes a compile-time error on Pet.
+
+In other words, a case_expression whose type is Boolean
+represents a set, with a requirement that you specify
+what's IN the set and also what's NOT IN the set.
+
 Note that the last bullet in the definition of "predicate-static" allows
-parentheses, but not qualification.  Qualification within a static
+parentheses, but not qualification. Qualification within a static
 subexpression is OK, but qualification of a subexpression involving the current
 instance leads to a non-predicate-static predicate. For example, "Cur_Inst >
-Natural'(2)" is predicate-static, but "Boolean'(Cur_Inst > 2)" is not.  The
+Natural'(2)" is predicate-static, but "Boolean'(Cur_Inst > 2)" is not. The
 reason is to ensure (without knowing the value of the current instance) that
 predicate-static expressions cannot raise exceptions.