!standard 3.9.2(10/2)                                  20-03-26  AI12-0243-2/01
!standard 4.9.1(2/5)
!standard 13.1.1(16/3)
!standard 13.1.1(30/3)
!class Amendment 18-01-11
!status work item 20-03-26
!status received 17-10-20
!priority Very_Low
!difficulty Medium
!subject Subtypes as primitive arguments and class-wide predicates
!summary

Allow non-first subtypes for controlling parameters and controlling
results. Add class-wode predicates to support using those are part of the
contracts of dispatching operations.

!problem

The use of subtypes with dynamic predicates can be used to factor out common
checks from the preconditions of an interface. This reduces code duplication
and reduces the chance of forgetting a check.

The technique is important enough that an example was provided in the Standard,
in the examples for subclause 3.2.4. It shows a hypothetical update to Text_IO
using subtypes with dynamic predicates to provide most of the precondition
checks needed.

However, if the type in question is tagged, Ada does not allow controlling
operands to have non-first subtypes. This means that the technique cannot be
used on the primitive operations of a tagged type.

[Editor's note: I have not considered in any detail the consequences of these
changes to "static matching", nor the consequences of a class-wide predicate
in contexts other than dispatching calls and initialization/assignment. I
haven't noticed any problems. Hopefully, Steve and like-minded language
lawyers will consider the effect on sprouted generics with formal interfaces
deriving renames of inherited routines and the like. :-)]

!proposal

(See Wording.)

!wording

Modify 3.2.4(1/3):

  The language-defined *predicate aspects* Static_Predicate and 
  Dynamic_Predicate may be used to define properties of subtypes.
  {In addition, a *class-wide predicate aspect* Dynamic_Predicate'Class
  may be used to define properties of tagged subtypes; the other predicate
  aspects are refered to as *specific predicate aspects*.} A *predicate 
  specification* is an aspect_specification for one of the [two]{three}
  predicate aspects. {A *class-wide predicate specification* is a
  specification for a class-wide predicate aspect; a *specific predicate
  aspect is similarly defined.} General rules for aspects and 
  aspect_specifications are found in Clause 13 (13.1 and 13.1.1 respectively). 

  AARM Discussion: When we talk about "predicate aspects" and "predicate
  specifications", we're talking about all of them; we only use the prefixes
  when the rules need to be different.

  AARM Reason: A class-wide predicate is designed to be used in the contract
  of dispatching operations, so that it can apply to all overridings of
  that operation. That allows it to be checked as part of the dispatching
  call rather than inside of the subprograms, and for users to be able to
  depend on it applying to all possible bodies. The rules to support this
  are similar to those for Pre'Class. 

Add after 3.2.4(2/3): [This is in the Name Resolution Rules.]

   Within the expression for a class-wide predicate specification for a 
   subtype S of a tagged type T, a name that denotes a formal parameter 
   (or S'Result) of type T is interpreted as though it had a (notional) 
   nonabstract type NT that is a formal derived type whose ancestor type 
   is T, with directly visible primitive operations. Similarly, a name that 
   denotes a formal access parameter (or S'Result) of type access-to-T is 
   interpreted as having type access-to-NT. [The result of this interpretation 
   is that the only operations that can be applied to such names are those 
   defined for such a formal derived type.]

   AARM Reason: This ensures that the expression is well-defined for any type 
   descended from T.

   AARM Ramification: The operations of NT are also nonabstract, so the rule 
   against a call of an abstract subprogram does not trigger for a class-wide
   precondition or postcondition. 

   [Author's note: I borrowed this wording intact from 6.1.1(7/5),
   adjusted for the context. The purpose is the same, so the rules should be
   the same. They're probably easier to implement if exactly the same, as well
   since one can share the implementation in that case.]

Add after 3.2.4(29.7/4):

   For the evaluation of a class-wide predicate aspect P for a subtype S of a
   tagged type T, the controlling tag value for any dispatching call of type T
   in the predicate expression of P is determined as follows:
     * if S is used in the controlling operand or result of a dispatching call
       C of type T, then the controlling tag value of the call C is used;

       AARM Discussion: Careful: This is a call that *uses* the predicate of
       subtype S, while the call mentioned in the lead-in is one found in the
       predicate expression. These are necessarily different calls!

     * otherwise, the tag value of the current instance of S is used.

Modify 3.9.2(10/2):

  [In the declaration of a dispatching operation of a tagged type,
  everywhere a subtype of the tagged type appears as a subtype of
  the profile (see 6.1), it shall statically match the first subtype
  of the tagged type. ]If the {declaration of a }dispatching operation 
  overrides an inherited subprogram, it shall be subtype conformant with the
  inherited subprogram.  The convention of an inherited dispatching operation 
  is the convention of the corresponding primitive operation of the parent or
  progenitor type. The default convention of a dispatching operation that 
  overrides an inherited primitive operation is the convention of the inherited
  operation; if the operation overrides multiple inherited operations, then 
  they shall all have the same convention. An explicitly declared dispatching
  operation shall not be of convention Intrinsic. 

Replace 4.9.1(2/5):

[Author's note: Switching this massive paragraph to bulleted form, only the 
predicate paragraph is changed:]

A subtype statically matches another subtype of the same type if:

  * they have statically matching constraints; and

  * all predicate specifications that apply to them come from the same 
    declarations or all of the predicate specifications are class-wide 
    predicate expressions and each predicate expression of one conforms 
    to a predicate expression of the other; and

    AARM Discussion: It's possible that this is not a one-to-one matching
    if two identical expressions apply to one of the subtypes, those could
    both match a single expression of the other. Note that this applies
    both ways; a subtype with no class-wide predicates cannot match one
    that has some class-wide predicates.

  * Object_Size (see 13.3) has been specified to have a nonconfirming value 
    for either both or neither, and the nonconfirming values, if any, are 
    the same; and

    [Author's note: Move the Object_Size AARM note here.]

  * for access subtypes, either both or neither exclude null.

Two anonymous access-to-object subtypes statically match if their
designated subtypes statically match, and either both or neither exclude null, 
and either both or neither are access-to-constant. Two anonymous 
access-to-subprogram subtypes statically match if their designated profiles are 
subtype conformant, and either both or neither exclude null. 

[Author's note: We may want to move some of the existing AARM notes between 
these bullets for enhanced readability.]

Add after 4.9.1(9/3): [Part of "static compatibility"]

   * all of the predicate specifications of S1 are class-wide 
    predicate expressions and each predicate expression of S1 conforms 
    to a predicate expression of S2; or

Modify 13.1.1(16/3):

If the aspect_mark includes 'Class, then the associated entity shall be a tagged 
{sub}type or a primitive subprogram of a tagged type.

Add after 13.1.1(30/3):

AARM Ramification: We do not specify any blanket application to other entities
for associated entities that are subtypes; generally we do not want any such
rules.


!discussion

The existing restriction to first subtypes is a methodlogical restriction. The
requirement for static matching for overriding routines ensures that every
dispatching call has the same constraints, regardless of which body is chosen.
So constraint (and predicate) checks can be performed at the (dispatching) 
call-site.

However, dynamic constraints and all non-trivial predicates can never statically
match (since a separate subtype definition is required, and static matching 
requires only a single definition). This means that many possible routines with 
non-first subtypes as controlling can never be overridden. When Ada 95 was 
designed, this was considered problematic, so the first subtype rule was adopted
to prevent such subprograms from being declared. (We do not know why a weaker
but sufficient rule, for instance that only null or static constraints are 
allowed, was not chosen instead.)

We know that in practice, many tagged types are designed without intending to
allow overriding. Indeed, we have heard a number of times that some users
would like a "final" mechanism that would not allow overriding. In such an
environment, it does not make sense for Ada to prohibit users writing useful
subprograms with proper subtyping just because those subprograms happen to be
primitives of a tagged type. That sort of methodlogical restriction should be
left to style guides and add-on tools (as well as possible compiler warnings).

However, this change does not really help the stated problem. A subtype with a
predicate cannot ever statically match, and thus no overriding would be 
allowed.

We considered relaxing the static matching requirement to ignore predicates
(or even constraints) for static matching. However, this means that predicates
have to be part of the dynamic semantics of a dispatching call (depending on
the body) rather than part of the dispatching contract. That is, predicates
work like Pre, while to make something part of the dispatching contract, one
needs to use Pre'Class.

What really is desired is a way to have a predicate that is part of the 
dispatching contract. Such a way would necessarily have to work like Pre'Class
so that LSP is preserved by construction. Therefore, we have defined a
Dynamic_Predicate'Class aspect with the appropriate semantics.

!example

  package Pkg1 is
     type Parent is tagged ... ;
     function Is_Wonderful (X : Parent) return Boolean;
     subtype S is Parent with Dynamic_Predicate'Class => Is_Wonderful (S);

     procedure Op (Y : in out S); -- Previously illegal, now legal.
  end Pkg1;

  with Pkg1;
  package Pkg2 is
     type Ext is new Pkg1.Parent with ... ;
     subtype S is Ext with Dynamic_Predicate'Class => Is_Wonderful (S);

     overriding
     procedure Op (Y : in out S); -- OK, statically matches inherited routine.
  end Pkg2;

Note that this also provides the effect of "final" for any subtype that has a
non-trivial (specific) dynamic predicate. One could declare a subtype like:

   subtype Final is Parent with Dynamic_Predicate => Final = Final;

   procedure Final_Op (Y : in out Final); -- Now legal, but no overridding possible.

----

If the implementation of a predicate is to create a subprogram which is passed
the object to be checked, a class-wide predicate would just need an additional
parameter to determine the tag to use for dispatching. Most uses would pass the
tag of the object; while those associated with dispatching calls would pass the
tag of the call.

!ASIS

None needed.

!ACATS test

An ACATS C-Test is needed to check that the new capabilities are supported.

!appendix

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