!standard 3.10.2(7/3)                              13-05-30    AI12-0068-1/00
!class binding interpretation 13-05-30
!status work item 13-05-30
!status received 13-04-20
!priority Medium
!difficulty Medium
!qualifier Omission
!subject Predicates and the current instance of a subtype

!summary

The current instance of a subtype acts like an in-mode parameter during
the specification of a predicate aspect.

!question

For a predicate, is the current instance of the subtype an object or a
value? This matters in unusual cases. Consider:

     type T (Kind : T_Kind := Zoofle) is ... ;

     -- A variable is in this subtype if and only if it
     -- is ok to assign it a value whose Kind is Zoofle
     subtype Zoofleable is T with
       Dynamic_Predicate =>
         Zoofleable.Kind = Zoofle
         or else not Zoofleable'Constrained;

     procedure Zoofalize (X : out Zoofleable) is
     begin
         X := (Kind => Zoofle, ...);
         -- Assignment's discriminant check guaranteed to pass
     end;

     Y : T := (Foozle, ...); -- unconstrained, Kind /= Zoofle
     Z : T (Foozle) := Y; -- constrained, Kind /= Zoofle
   begin
     Zoofalize (Y); -- Works
     Zoofalize (Z); -- Fails predicate check (??)

Is it expected that the value of 'Constrained reflects that of the actual
object, or is this check on a value and the properties of the object aren't
querable? (Something. :-)

!recommendation

(See !summary.)

!wording

** TBD.

!discussion

Note that a current instance of a type and a subtype is a variable, since
it is not in the list of things that denote constant views in 3.3. That list
is supposed to be exhaustive (and we keep adding to it as things are missed).
Moreover, it is clear a variable by practice, as the Rosen trick depends on
that fact:

     type Outer;
     type Inner (Ref : access Outer) is limited null record;
       -- discriminant's type is access-to-variable

     type Outer is limited record
       Self : Inner (Outer'Access);
     end record;

This would not be legal if Outer was a constant view (as converting
an access-to-constant value to an access-to-variable value is illegal).

---

We select the model that the current instance of a subtype acts like an
in-mode parameter for the purposes of use in a predicate definition.

This is the most information that a predicate should be allowed to use, as
we want to allow compilers to implement a predicate as a Boolean function
with a parameter of the base type of the subtype. If the semantics diverges
too far from the parameter model, such an implementation would become
difficult.

An alternative semantics would be to define it as a constant value. In that
case, even using object attributes within a predicate would be illegal.
For instance, 'Size, 'Alignment, 'Access, and 'Address would all be illegal
as their prefix would not denote an object.

[Editor's note: Actually, the above sounds appealing, as "tricky" predicates
would then be statically illegal and no one would get caught expecting some
an example like the one in the question to work. OTOH, this is more work
and might make some sensible predicates illegal (can't pass as an in out
or out parameter, for instance). More thought required.]

!ACATS Test

The examples discussed in the mail (see !appendix) should be made into
ACATS tests (some will be legality rules and some will be determinable at
runtime).

!ASIS

No ASIS effect.


!appendix

From: Steve Baird
Sent: Saturday, April 20, 2013  4:54 PM

Randy and I were discussing whether predicates really work on values or on
objects.

The manual is not clear on this point:
   the current instance of a type is the object or value of
   the type that is associated with the execution that
   evaluates the usage name.

The following example illustrates the difference:

     type T (Kind : T_Kind := Zoofle) is ... ;

     -- A variable is in this subtype if and only if it
     -- is ok to assign it a value whose Kind is Zoofle
     --
     subtype Zoofleable is T with
       Dynamic_Predicate =>
         Zoofleable.Kind = Zoofle
         or else not Zoofleable'Constrained;

     procedure Zoofalize (X : out Zoofleable) is
     begin
         X := (Kind => Zoofle, ...);
         -- assignment's discrim check guaranteed to pass
     end;

     Y : T := (Foozle, ...); -- unconstrained, Kind /= Zoofle
     Z : T (Foozle) := Y; -- constrained, Kind /= Zoofle
   begin
     Zoofalize (Y); -- works
     Zoofalize (Z); -- fails predicate check

Is this supposed to work as the comments suggest (because the current instance
is the object), or should the use of Zoofleable'Constrained always return False
(because the current instance is a value)?

Randy suggests a more nuanced approach: a name denoting the current instance in
a predicate should behave as though it denotes an in-mode parameter where the
corresponding actual parameter is the current instance of the type.

This means that attributes such as Size, Address, and Alignment can be queried,
but they might not yield useful results in some cases.
Current_Instance'Constrained would then always yield True. This model also works
well with by-reference types. And like any equivalence rule, it has the
advantage of providing a clear implementation model.

Sounds right to me; this is probably how a predicate would be implemented anyway
so this model is probably consistent with existing practice.

However, note the use of "in-mode" above.

The current instance of a type is variable, not constant.

This is at the heart of the well established "Rosen trick", which allows
modification of a limited constant via a self-referential access-to-variable
discriminant.

A strict reading of the current wording
would allow the following (absurd) example:

      X : constant Integer := 123;

      function Is_456 (Y : out Integer) return Boolean is
      begin
         Y := 456; -- even if it wasn't 456 before, it is now
         return True;
      end;

      subtype S is Integer with Dynamic_Predicate =>
        Is_456 (S); -- should be illegal, but is legal because
                    -- name "S" denotes a variable

      pragma Assert (X = 123 and then (X in S) and then X = 456);

Do not waste your time trying to figure out what this ought to do at runtime; it
should be rejected at compile time. This is just a minor language hole that
needs to be plugged.

I think we need wording something like

    In an aspect specification for a type or subtype, a name
    denoting the current instance of the type or subtype denotes
    a constant view.

It seems to me that
    1) Randy's "treat the current instance like a parameter"
       model is right.
    2) The mode of that parameter needs to be In in the case of
       an aspect specification.

Do folks agree with these general ideas?

Wording, of course, is a separate question.

****************************************************************

From: Tucker Taft
Sent: Saturday, April 20, 2013  8:50 PM

> ... It seems to me that
>     1) Randy's "treat the current instance like a parameter"
>        model is right.
>     2) The mode of that parameter needs to be In in the case of
>        an aspect specification.
>
> Do folks agree with these general ideas?

Yes.

****************************************************************

From: Jean-Pierre Rosen
Sent: Sunday, April 21, 2013  4:26 AM

>     Zoofalize (Y); -- works
>     Zoofalize (Z); -- fails predicate check

At first, I had some sympathy with this. However, I think a precondition is more
appropriate for someone who wants to express that. And we don't have the same
problem in preconditions, have we?

[...]
> Randy suggests a more nuanced approach: a name denoting the current
> instance in a predicate should behave as though it denotes an in-mode
> parameter where the corresponding actual parameter is the current
> instance of the type.
>
> This means that attributes such as Size, Address, and Alignment can be
> queried, but they might not yield useful results in some cases.
> Current_Instance'Constrained would then always yield True. This model
> also works well with by-reference types. And like any equivalence
> rule, it has the advantage of providing a clear implementation model.
>
> Sounds right to me; this is probably how a predicate would be
> implemented anyway so this model is probably consistent with existing
> practice.
>
> However, note the use of "in-mode" above.
>
> The current instance of a type is variable, not constant.

You lost me here. Is the sentence above about the current wording, or the new
one? AFAIK, an in-parameter is a constant view.

> This is at the heart of the well established "Rosen trick", which
> allows modification of a limited constant via a self-referential
> access-to-variable discriminant.

I'd rather say that it is a constant view that carries an access to a variable
view of the same object.

> I think we need wording something like
>
>    In an aspect specification for a type or subtype, a name
>    denoting the current instance of the type or subtype denotes
>    a constant view.
>
> It seems to me that
>    1) Randy's "treat the current instance like a parameter"
>       model is right.
>    2) The mode of that parameter needs to be In in the case of
>       an aspect specification.

Are you proposing to say that it "denotes a constant view", or "it is an
in-parameter", or is it really equivalent?

****************************************************************

From: Steve Baird
Sent: Monday, April 22, 2013  1:29 PM

...
>>      Zoofalize (Y); -- works
>>      Zoofalize (Z); -- fails predicate check
> At first, I had some sympathy with this. However, I think a
> precondition is more appropriate for someone who wants to express
> that. And we don't have the same problem in preconditions, have we?

Right, because preconditions don't use the "current instance"
mechanism.

>> The current instance of a type is variable, not constant.
>
> You lost me here. Is the sentence above about the current wording, or
> the new one? AFAIK, an in-parameter is a constant view.

The above sentence is about the current wording (or really about the
well-established interpretation of the RM's lack of explicit wording about the
constancy of the current instance of a type).

If this were not the case, then this example would be illegal:

     type Outer;
     type Inner (Ref : access Outer) is limited null record;
       -- discriminant's type is access-to-variable

     type Outer is limited record
       Self : Inner (Outer'Access);
     end record;

> I'd rather say that it is a constant view that carries an access to a
> variable view of the same object.

Maybe it should work that way and that is a good way to think about it.
Strictly speaking, however, I think you are mistaken.

I think the current language definition allows, for example, passing the current
instance of a type as an out-mode actual parameter in default initialization
expression for a component (not something that I would recommend. although I
don't see that this introduces any definitional problems). One could argue that
the language should be changed to prevent this. Alternatively, one could argue
that disallowing something which is useless but well defined and unlikely to
occur accidentally is not worth the bother.

Note that we still have problems in this area even if the current instance
denotes a constant view. Given

     type T is
        record
           F, G : Component_Type := Some_Func (T);
        end record;

one of those two calls (whichever is evaluated first) is going to be passed a
value with an uninitialized component. Note that Component_Type could be an
access type, a task type, or anything.

>> I think we need wording something like
>>
>>     In an aspect specification for a type or subtype, a name
>>     denoting the current instance of the type or subtype denotes
>>     a constant view.
>>
>> It seems to me that
>>     1) Randy's "treat the current instance like a parameter"
>>        model is right.
>>     2) The mode of that parameter needs to be In in the case of
>>        an aspect specification.
>
> Are you proposing to say that it "denotes a constant view", or "it is
> an in-parameter", or is it really equivalent?

Constant view and in-parameter are not equivalent because of things like 'Size
and 'Alignment. Consider the current instance of a type T when declaring X of
type T where X'Alignment /= T'Alignment. What is Current_Instance'Allignment? If
we require it to be X'Alignment, then we are imposing distributed overhead on
any implementation which wants to use the reasonable implementation strategy of
implementing predicates via a compiler-generated boolean-valued function. Let's
not do that.

I didn't propose wording for the "it behaves like a parameter" approach.
The wording we end up with to get constancy right might depend on how that goes.

One possibility is that we define the "it behaves like a parameter" rule without
reference to the mode of the parameter; in that case we might need something
like the wording I proposed.

****************************************************************