Annotated Ada Reference ManualLegal Information
Contents   Index   References   Search   Previous   Next 

12.5 Formal Types

{AI95-00442-01} [A generic formal subtype can be used to pass to a generic unit a subtype whose type is in a certain category class of types.] 
Reason: We considered having intermediate syntactic categories formal_integer_type_definition, formal_real_type_definition, and formal_fixed_point_definition, to be more uniform with the syntax rules for non-generic-formal types. However, that would make the rules for formal types slightly more complicated, and it would cause confusion, since formal_discrete_type_definition would not fit into the scheme very well. 


{AI05-0213-1} formal_type_declaration ::= 
    | formal_incomplete_type_declaration
 type defining_identifier[discriminant_partis formal_type_definition;
{AI05-0183-1} {AI05-0213-1} formal_complete_type_declaration ::= 
    type defining_identifier[discriminant_partis formal_type_definition
{AI05-0213-1} formal_incomplete_type_declaration ::= 
    type defining_identifier[discriminant_part] [is tagged];
{AI95-00251-01} formal_type_definition ::= 
    | formal_derived_type_definition
    | formal_discrete_type_definition
    | formal_signed_integer_type_definition
    | formal_modular_type_definition
    | formal_floating_point_definition
    | formal_ordinary_fixed_point_definition
    | formal_decimal_fixed_point_definition
    | formal_array_type_definition
    | formal_access_type_definition
    | formal_interface_type_definition

Legality Rules

For a generic formal subtype, the actual shall be a subtype_mark; it denotes the (generic) actual subtype
Ramification: When we say simply “formal” or “actual” (for a generic formal that denotes a subtype) we're talking about the subtype, not the type, since a name that denotes a formal_type_declaration denotes a subtype, and the corresponding actual also denotes a subtype.

Static Semantics

A formal_type_declaration declares a (generic) formal type, and its first subtype, the (generic) formal subtype
Ramification: A subtype (other than the first subtype) of a generic formal type is not a generic formal subtype.
{AI95-00442-01} {AI05-0213-1} The form of a formal_type_definition determines a category (of types) class to which the formal type belongs. For a formal_private_type_definition the reserved words tagged and limited indicate the category of types class (see 12.5.1). The reserved word tagged also plays this role in the case of a formal_incomplete_type_declaration. For a formal_derived_type_definition the category of types class is the derivation class rooted at the ancestor type. For other formal types, the name of the syntactic category indicates the category of types class; a formal_discrete_type_definition defines a discrete type, and so on. 
Reason: This rule is clearer with the flat syntax rule for formal_type_definition given above. Adding formal_integer_type_definition and others would make this rule harder to state clearly.
{AI95-00442-01} We use “category’ rather than “class” above, because the requirement that classes are closed under derivation is not important here. Moreover, there are interesting categories that are not closed under derivation. For instance, limited and interface are categories that do not form classes. 

Legality Rules

{AI95-00442-01} The actual type shall be in the category class determined for the formal. 
Ramification: {AI95-00442-01} For example, if the category class determined for the formal is the category class of all discrete types, then the actual has to be discrete.
{AI95-00442-01} Note that this rule does not require the actual to belong to every category class to which the formal belongs. For example, formal private types are in the category class of composite types, but the actual need not be composite. Furthermore, one can imagine an infinite number of categories classes that are just arbitrary sets of types that obey the closed-under-derivation rule, and are therefore technically classes (even though we don't give them names, since they are uninteresting). We don't want this rule to apply to those categories classes.
{AI95-00114-01} {AI95-00442-01} “Limited” is not an a “interesting” category class, but “nonlimited” is; it is legal to pass a nonlimited type to a limited formal type, but not the other way around. The reserved word limited limited really represents a category class containing both limited and nonlimited types. “Private” is not a category for this purpose class; a generic formal private type accepts both private and nonprivate actual types.
{AI95-00442-01} It is legal to pass a class-wide subtype as the actual if it is in the right category class, so long as the formal has unknown discriminants. 

Static Semantics

{8652/0037} {AI95-00043-01} {AI95-00233-01} {AI95-00442-01} {AI05-0029-1} [The formal type also belongs to each category class that contains the determined category class.] The primitive subprograms of the type are as for any type in the determined category class. For a formal type other than a formal derived type, these are the predefined operators of the type. For an elementary formal type, the predefined operators are implicitly declared immediately after the declaration of the formal type. For a composite formal type, the predefined operators are implicitly declared either immediately after the declaration of the formal type, or later immediately within the declarative region in which the type is declared in its immediate scope according to the rules of 7.3.1.; they are implicitly declared immediately after the declaration of the formal type. In an instance, the copy of such an implicit declaration declares a view of the predefined operator of the actual type, even if this operator has been overridden for the actual type and even if it is never declared for the actual type. [The rules specific to formal derived types are given in 12.5.1.]
Ramification: {AI95-00442-01} All properties of the type are as for any type in the category class. Some examples: The primitive operations available are as defined by the language for each category class. The form of constraint applicable to a formal type in a subtype_indication depends on the category class of the type as for a nonformal type. The formal type is tagged if and only if it is declared as a tagged private type, or as a type derived from a (visibly) tagged type. (Note that the actual type might be tagged even if the formal type is not.) 
Reason: {AI05-0029-1} The somewhat cryptic phrase “even if it is never declared” is intended to deal with the following oddity:
package Q is
    type T is limited private;
    type T is range 1 .. 10;
end Q;
    type A is array (Positive range <>) of T;
package Q.G is
    A1, A2 : A (1 .. 1);
    B : Boolean := A1 = A2;
end Q.G;
with Q.G;
package R is
   type C is array (Positive range <>) of Q.T;
   package I is new Q.G (C); -- Where is the predefined "=" for C?
end R;
An "=" is available for the formal type A in the private part of Q.G. However, no "=" operator is ever declared for type C, because its component type Q.T is limited. Still, in the instance I the name "=" declares a view of the "=" for C which exists-but-is-never-declared.
7  Generic formal types, like all types, are not named. Instead, a name can denote a generic formal subtype. Within a generic unit, a generic formal type is considered as being distinct from all other (formal or nonformal) types. 
Proof: This follows from the fact that each formal_type_declaration declares a type. 
8  A discriminant_part is allowed only for certain kinds of types, and therefore only for certain kinds of generic formal types. See 3.7
Ramification: The term “formal floating point type” refers to a type defined by a formal_floating_point_definition. It does not include a formal derived type whose ancestor is floating point. Similar terminology applies to the other kinds of formal_type_definition.


Examples of generic formal types: 
type Item is private;
type Buffer(Length : Natural) is limited private;
type Enum  is (<>);
type Int   is range <>;
type Angle is delta <>;
type Mass  is digits <>;
type Table is array (Enum) of Item;
Example of a generic formal part declaring a formal integer type: 
   type Rank is range <>;
   First  : Rank := Rank'First;
   Second : Rank := First + 1;  --  the operator "+" of the type Rank  

Wording Changes from Ada 83

RM83 has separate sections “Generic Formal Xs” and “Matching Rules for Formal Xs” (for various X's) with most of the text redundant between the two. We have combined the two in order to reduce the redundancy. In RM83, there is no “Matching Rules for Formal Types” section; nor is there a “Generic Formal Y Types” section (for Y = Private, Scalar, Array, and Access). This causes, for example, the duplication across all the “Matching Rules for Y Types” sections of the rule that the actual passed to a formal type shall be a subtype; the new organization avoids that problem.
The matching rules are stated more concisely.
We no longer consider the multiplying operators that deliver a result of type universal_fixed to be predefined for the various types; there is only one of each in package Standard. Therefore, we need not mention them here as RM83 had to. 

Wording Changes from Ada 95

{8652/0037} {AI95-00043-01} {AI95-00233-01} Corrigendum 1 corrected the wording to properly define the location where operators are defined for formal array types. The wording here was inconsistent with that in 7.3.1, “Private Operations”. For the Amendment, this wording was corrected again, because it didn't reflect the Corrigendum 1 revisions in 7.3.1.
{AI95-00251-01} Formal interface types are defined; see 12.5.5, “Formal Interface Types”.
{AI95-00442-01} We use “determines a category” rather than class, since not all interesting properties form a class.

Extensions to Ada 2005

{AI05-0183-1} An optional aspect_specification can be used in a formal_type_declaration. This is described in 13.1.1. 

Wording Changes from Ada 2005

{AI05-0029-1} Correction: Updated the wording to acknowledge the possibility of operations that are never declared for an actual type but still can be used inside of a generic unit.
{AI05-0213-1} {AI05-0299-1} Formal incomplete types are added; these are documented as an extension in the next subclause. 

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe