!standard 3.10.2(8)                                  20-03-06  AI12-0371-1/01
!standard 6.1.1(40/5)
!standard 12.1(9)
!class Amendment 20-03-06
!status work item 20-03-06
!status received 20-01-06
!priority Low
!difficulty Easy
!subject Fix-ups for aspects in generic formal parts
!summary

(1) A generic formal part is a declaration list.

(2) Any Pre/Post that apply to a generic formal subprogram also apply to a
renaming of the formal subprogram.

(3) The accessibility of a renaming of a generic formal subprogram is that
of the instance.

!problem

There are a number of minor issues associated with aspects given in generic 
formal parameters:

(1) AI12-0272-1 adds pre/post conditions to the declarations of formal 
subprograms. The AI indicates that the intent is that expressions cannot make 
forward references to declarations in the public part of the enclosing generic 
package. 13.1.1(11/5) says that aspects are resolved at the end of the
enclosing declaration list, but nothing says that a generic_formal_part is
declaration list, nor is there any rule that would cause early resolution.

(2) When a formal subprogram is exported from a generic package with a
renaming, does the added pre/post also apply to the renaming? This is not
clear as pre/post evaluate only the pre/post that apply to the subprogram,
and it is unclear whether the formal pre/post apply to the subprogram when
viewed where the actual is available.

(3) The addition of pre/post conditions to formal subprograms opens up the
possibility of the pre/post expression accessing an object that does not
exist. For example:

  procedure Proc2 is
     type Proc_Ref is access procedure;
 
     Ptr : Proc_Ref;
 
     procedure Proc is null;
 
     procedure Nested is
        Local_Flag : Boolean := False;
 
        generic
          with procedure Formal_Proc with Pre => Local_Flag;
        package G is
          procedure Proc_Ren renames Formal_Proc;
        end;
 
        package I is new G (Formal_Proc => Proc);
     begin
        Ptr := I.Proc_Ren'Access; -- (Illegal by this AI.)
     end;
   begin
     Nested;
     Ptr.all;
   end;

!proposal

(See Summary.)

!wording

(1): Add after 12.1(9):

The list of generic_formal_parameter_declarations of a generic_formal_part 
form a *declaration list* of the generic unit.

AARM Ramification: Aspect specifications (see 13.1.1) given in a generic 
formal part can only use declarations given in the formal part, and not those
in the visible part of the generic unit.

(2): Add after 6.1.1(40/5):

AARM To Be Honest: The specific precondition and postcondition that apply to
a generic formal subprogram also apply to any renaming of that subprogram,
even if that renaming is visible in the instance and called from outside of 
the generic instance.

(3): Modify 3.10.2(8):

The accessibility level of a view of an object or subprogram defined by a 
renaming_declaration is the same as that of the renamed view{, unless the 
renaming is of a formal subprogram, in that case the accessibility level is
that of the instance}.

!discussion

For (1), we checked all of the uses of "declaration list" in the Standard.
The term is used in the definition of dispatching operation, and in a number 
of other rules that involve types that can't occur in a generic_formal_part.
So the only effect is on the rule that we want to invoke, that an aspect
specification is resolved at the end of the immediately enclosing declaration
list.

For (2), in general, we want a rename-as-body and a subprogram containing only 
a call on the renamed subprogram to work the same. Moreover, we want a normal
renaming and a renames-as-body to work the same if possible.

A call to a formal subprogram in a subprogram declared inside the generic 
unit would necessarily include the formal subprogram's Pre/Post, regardless
of whether that subprogram was called inside or outside of the generic unit.
Similarly, a renames-as-body of the formal subprogram would include the 
Pre/Post (since the renames-as-body would be inside the generic, and would
not be visible outside the generic).

Therefore, we want a renames that is visible outside the specification to
work the same way. Thus we note that the Pre/Post apply to the rename
and thus are included on any call of the rename. We don't believe any wording
is needed to accomplish this (the renaming doesn't disappear just because the
actual renamed subprogram is known for the instance).

For (3), while Ada declares code like that in the example in the !problem
erroneous, we don't want the addition of contracts (that are trying to make 
code safer) make the code less safe. So we need a fix here.

Note that a subprogram declared in the generic would not be allowed in the
'Access of this example, even if that was completed by a renames-as-body.

Moreover, the actual for a formal subprogram can be given by an expression 
that requires runtime evaluation. We don't want to call a subprogram stored
in a non-existent temporary (although that can be avoided depending on how
the renaming is implemented).

Finally, a code sharing implementation is likely to use a wrapper for a formal
subprogram, since the subtypes of the parameters don't have to match those in
the profile. As such, a wrapper is needed to make the checks for the declared
subtypes of the actual subprogram. Such a wrapper may access data stored in
the instance data.

Therefore, since the 'Access is dubious even in Ada 95 cases (as it will not
work for any implementation that needs a wrapper somewhere), we make it illegal
in this case.

We do that by defining the accessibility of the renaming to be the same as that
of the instance. The proposed accessibility rule covers both static and dynamic 
accessibility, so this is the only change needed.

We considered instead defining the renaming to be intrinsic. That would also
work, but it would prevent any use of this idiom even for library-level 
instances. Since this has been possible since the advent of Ada 95, it seems
unnecessarily incompatible to ban all uses of such a renames just because a 
nested one might be a problem.

This rule is still slightly incompatible with Ada 2012 (which arguably allows
the 'Access in the original example, assuming the newly allowed Pre is removed).
This example seems rather unlikely, as it requires both a generic with a need
to name the actual subprogram in the instance (which is unusual) and a need to
save an access to a subprogram in a nested instance (which is unusual and not 
allowed other than this renaming).

There is a simple workaround for any program made illegal by this new rule:

Replace:

       package I is new G (Formal_Proc => Proc);
     begin
        Ptr := I.Proc_Ren'Access; -- (Illegal by this AI.)

with:

       procedure Actual is Proc;
       package I is new G (Formal_Proc => Actual);
    begin
       Ptr := Actual'Access;

Note that this works even if the actual subprogram is an expression that needs
to be evaluated (as it might if it included a function returning an 
access-to-subprogram). Of course, the actual subprogram can also be used
directly in the 'Access if is just the static name of a subprogram.

!ASIS

No ASIS change.

!ACATS test

For (1), an ACATS B-test is needed to ensure that entities in the visible
part of a generic package are not allowed in both Pre/Post for formal
subprogram, and in Default_Initial_Condition for formal private types.

For (2), an ACATS B-Test is needed to demonstrate that the example is
rejected. (We don't need a C-test since dynamic checks are not used
on access-to-subprogram types.)

For (3), an ACATS C-Test is needed to ensure that the preconditions and
postconditions of the formal are reexported via a renaming.

!appendix

From: Edmond Schonberg
Sent: Monday, January 6, 2020  3:31 PM

The AI adds pre/post conditions to formal subprograms declarations, and
Default_Initial_Condition to formal private types. The name resolution rules 
for aspects (13.1.1 (11/5)) indicate that the expressions in aspect 
specifications are resolved at the end of the enclosing declaration_list.
The discussion in the AI indicates that these expressions cannot make forward 
references to declarations in the public part of the enclosing generic 
package,  but there is no indication that the generic_formal_part should be 
treated as a declaration_list (which is otherwise defined for a declarative 
part and for a package specification).  It might be clearer to state 
explicitly  that a generic_formal_part is a declaration_list.

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

From: Tucker Taft
Sent: Monday, January 6, 2020  3:52 PM

Interesting.  I wonder whether it would make sense to allow aspects on formals 
to be resolved by items in the visible part of the generic package.  Seems a 
bit too weird at this point, and probably simplest to do as you say, and 
require resolution at the end of the formal part.  We could conceivably at 
some point allow more flexibility, but better to start with the simpler rule.

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

From: Edmond Schonberg
Sent: Monday, January 6, 2020  4:07 PM

Note the following exchange between Steve and Randy in the genesis  of this AI;

> Along those lines, how would name resolution work? Could a 
> precondition for a formal subprogram of a generic package reference 
> something declared in the visible part of the package?

I'd expect just the things allowed in the formal part + parameters. But you
are right that some thought would be required to see if that enough.
Definitely wouldn't want anything inside of the package (lest you get 
recursive dependence between the formals and the instantiated routines).

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