12.5 Formal Types
1/2
{
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.]
1.a
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.
Syntax
2
formal_type_declaration ::=
type defining_identifier[
discriminant_part]
is formal_type_definition;
3/2
{
AI95-00251-01}
formal_type_definition ::=
formal_private_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_definitionLegality Rules
4
{generic actual subtype}
{actual subtype}
{generic actual type}
{actual type}
For a generic formal subtype, the actual shall be
a
subtype_mark; it denotes the
(generic)
actual subtype.
4.a
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
5
{generic formal type}
{formal type}
{generic formal subtype}
{formal subtype}
A
formal_type_declaration
declares a
(generic) formal type, and its first subtype, the
(generic)
formal subtype.
5.a
Ramification: A subtype (other than the
first subtype) of a generic formal type is not a generic formal subtype.
6/2
{
AI95-00442-01}
{determined category
for a formal type} {category
determined for a formal type} {determined
class for a formal type} {class
determined for a formal type} 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).
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.
6.a
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.
6.b/2
{
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
7/2
{
AI95-00442-01}
The actual type shall be in the
category class
determined for the formal.
7.a/2
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.
7.b/2
{
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.
7.c/2
{
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 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.
7.d/2
{
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
8/2
{
8652/0037}
{
AI95-00043-01}
{
AI95-00233-01}
{
AI95-00442-01}
[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. [The rules specific
to formal derived types are given in
12.5.1.]
8.a/2
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.)
9
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.
9.a
Proof: This follows from the fact that
each formal_type_declaration declares a type.
10
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.
10.a
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
11
Examples of generic
formal types:
12
type Item is private;
type Buffer(Length : Natural) is limited private;
13
type Enum is (<>);
type Int is range <>;
type Angle is delta <>;
type Mass is digits <>;
14
type Table is array (Enum) of Item;
15
Example of a generic
formal part declaring a formal integer type:
16
generic
type Rank is range <>;
First : Rank := Rank'First;
Second : Rank := First + 1; -- the operator "+" of the type Rank
Wording Changes from Ada 83
16.a
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.
16.b
The matching rules are stated more concisely.
16.c
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
16.d/2
{
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.16.e/2
16.f/2
{
AI95-00442-01}
We use “determines a category” rather
than class, since not all interesting properties form a class.
Sponsored by Ada-Europe