!standard  3.2.2(7)                                   09-05-27    AI05-0153-1/01
!class Amendment 09-05-27
!status work item 09-05-27
!status received 09-05-27
!priority Medium
!difficulty Medium
!subject User-defined constraints

!summary


!problem

Ada's constraints are a powerful way to enhance the contract of an
object (including formal parameters). But the constraints that can
be expressed are limited.

For instance, it isn't possible to specify that a record type may
have any of several discriminant values - for discriminants we can
only specify a single value or allow all discriminants.

!proposal

Add user-defined constraints to the language.

!wording

Replace 3.2.2(7) with:

composite_constraint ::=
    index_constaint | discriminant_constraint | user_constraint

Add a new clause 3.12:

[Editor's note: This belongs in the non-existent "composite type"
clause. It doesn't make sense to put it into the array or discriminated
type clauses, as it applies to both. I put this last in section 3 to
avoid renumbering.

3.12  User constraints

A user_constraint provides an arbitrary user-created constraint
for a composite or access type.

user_constraint ::= when *Boolean_*expression

Legality Rules

A user_constraint is only allowed in a subtype_indication whose subtype_mark
denotes either an unconstrained array subtype, an unconstrained discriminated
subtype, or an unconstrained access subtype whose designated subtype is
an unconstrained array or discriminated subtype. However, in the case of an
access subtype, a user_constraint is legal only if any dereference of a value
of the access type is known to be constrained (see 3.3). In addition to the
places where Legality Rules normally apply (see 12.3), these rules apply also
in the private part of an instance of a generic unit.

AARM Reason:
We do not allow a user_constraint on a scalar subtype, as scalar subtypes can
be constrained multiple times. That works well for ranges, where it is only
necessary to check the bounds of the most recent constraint (and to check that
those bounds are inside of any existing constraint when the subtype is declared).
But arbitrary expressions (such as every odd value) are not so obvious. We could
have just required compilers to check all of the possible constraints in
succession, but that could add a lot of compiler and runtime overhead. It doesn't
seem useful enough for that.

We also don't allow user_constraints on types that have no constraints at all.
That would essentially allow constraining constrained subtypes, which is
uncomfortable. [Editor's note: See the !discussion below.]

See 3.7 for an explanation of the need for the restriction on access subtypes.
End AARM Reason.



!discussion

This proposal seems similar to type invariants on the surface. However,
these two constructs solve different problems. A type invariant is a
requirement on all values of a type outside of the type's defining
package(s). In particular, it does not vary depending on the view of
an object. A constraint (including user-defined constraints) is a
requirement on a particular view of an object. It can be different
on different views of the same object (as in a formal parameter). Thus
it can be used to specify temporary or transient requirements on an
object.

---

The syntax was chosen to be similar to that proposed for preconditions.
We also considered using "with" instead of "when":
    subtype Callable_Symbol is Symbol_Rec with
        (Symbol_Rec.D = Func or Symbol_Rec.D = Proc);
or a new keyword "requiring":
    subtype Callable_Symbol is Symbol_Rec requiring
        (Symbol_Rec.D = Func or Symbol_Rec.D = Proc);

We also considered requiring a user_constraint to be a Boolean function
with single parameter of the appropriate type. This would be easier to
explain the visibility rules for, but again it would be unnecessarily
different than preconditions.

---

We do not allow user_constraints on scalar types, because such constraints
can be combined, and the compiler would have to check all of the constraints
in succession:
    subtype Odd is Natural when (Odd mod 2) = 1;
    subtype Triple is Odd when (Triple mod 3) = 0;
    OK_Obj  : Triple := Func_returning_3;
    Bad_Obj : Triple := Func_returning_6; -- Hopefully raises Constraint_Error;

Both constraint expressions would have to be evaluated in order to make the check
(in general, the compiler cannot tell how the expressions relate).

We also do not allow user_constraints on access types. This seems like a loss,
but it is necessary to keep those constraints from being regularly violated.
We have rules strictly limiting discriminant_constraints on access types, and
those problems occur doubly for user_constraints (which do not necessarily
only have to depend on discriminants; they can also depend on other components).
For instance:
  procedure Test1 is
    type Rec is record
       A : Natural;
    end recordl
    type Acc_Rec is access Rec;
    Obj : aliased Rec := (A => 10);
    Ptr : Acc_Rec when ((Acc_Rec.A mod 10) = 0) := Obj'Access;
  begin
    Obj := (A => 5);
    if (Ptr.A mod 10 /= 0) then
       Put_Line("What kind of constraint is this??");
    end if;
  end Test1;



--!corrigendum H.4(19)

!ACATS test

Add ACATS B and C tests for this feature.

!appendix

This AI was created after discussion at the Tallahassee ARG meeting; it
is partially based on an old idea found in AC-0157.

From the Tallahassee minutes about type Invariants:

   Randy asks whether the user-defined constraint idea is worth looking at
   (either as an alternative or replacement). After discussion, we decide
   that it seems to solve a somewhat different problem - it allows adding
   contracts to particular parameters, objects, etc. User-defined constraints
   would be a way to deal with non-contiguous sets of discriminants, one-sided
   array constraints, and so on. There is sufficient interest to have that
   written up (it previously was discussed on Ada-Comment and filed as AC-0157).
   It's not very necessary on scalar types, so if the rules get too messy for
   them, don't allow them. (Randy notes when writing up these minutes that that
   would probably be a generic contract problem.) Steve notes that it would
   need a bounded error if the expression does not return the same value
   when called with the same value (we would want to be able to eliminate
   duplicate checks) -- the bounds are that the check is either made or not.

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

From: Randy Brukardt
Date: Wednesday, May 20, 2009  5:28 PM

At the last meeting, I was directed to write a proposal about user-defined
constraints. I was told to try to restrict them only to composite types,
because the "satisfability" rules would be hard to make work for scalar types,
while they are pretty much right for composite types already.

To do that brings up a generic contract model issue. We would need to use
an assume-the-worst rule for generic bodies. Essentially, any subtype that
is of a generic formal type (or a type derived from such a type) could not
have a user-defined constraint (since we don't allow reconstraining or use
on types that might not be composite). It would be possible to move those
constraints to the private part, however.

Is the latter workaround enough? It seems like it would be to me (it is the
same workaround we suggest for 'Access, for instance), but I wanted to get
other people's opinions on that before I spend a lot of effort writing up
the proposal. (I was going to ask the accessibility subcommittee in one of
our periodic calls, but we never got to it.)

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

From: Randy Brukardt
Date: Wednesday, May 27, 2009  11:59 PM

Here is a more fundamental question about user-defined constraints: Do they act
like real constraints (that is, they apply to the view during the entire time of
its existence) or do they only apply at the point that the language defines
subtype conversions?

If they act like real constraints, then they can only depend on bounds and
discriminants; that seems very limiting. (Only bounds and discriminants have the
necessary rules to prevent changes between checks.)

If they are just checks applied at particular points, then we have anomalies
where "constrained" values does not satisfy the constraint. Moreover, whether or
not Constraint_Error is raised can depend on the parameter passing mode:

   type Rec is record
       A : Natural;
   end record;
   subtype Decimal_Rec is Rec when Rec.A mod 10 = 0;

   Obj : Decimal_Rec := (A => 10);

   procedure Do_It (P : in out Decimal_Rec) is
   begin
       P.A := 5;
   end Do_It;

   Do_It (Obj); -- (1)

The call at (1) will raise Constraint_Error if Obj is passed by copy: the copy
back will fail the subtype conversion back to the original object. But if Obj is
passed by reference, the view conversion will succeed and there will not be any
check after the call.

I was considering only allowing these constraints on private types, but that is
uncomfortable for two reasons (1) you lose capability when you see the full type
[note however that this is the same rule implied for type invariants: they can
only be given for a private type]; (2) it still allows the body (anywhere in the
scope of the full declaration, in fact) to break the constraint.

    package Pack is
       type Priv is private;
       function Is_Decimal (P : Priv) return Boolean;
       function Decimal (N : Natural) return Priv;

       procedure Half (P : in out Priv);
    private
       type Priv is record
           A : Natural;
       end record;
    end Pack;

    package body Pack is
       function Is_Decimal (P : Priv) return Boolean is
       begin
           return P.A mod 10 = 0;
       end Is_Decimal;

       function Decimal (N : Natural) return Priv is
       begin
           return (A => N*10);
       end Decimal;

       procedure Half (P : in out Priv) is
       begin
           P.A := P.A / 2;
       end Half;
    end Pack;

    with Pack;
    procedure Test2 is
       subtype Decimal_Priv is Pack.Priv when Pack.Is_Decimal (Decimal_Priv);
       Obj : Decimal_Priv := Pack.Decimal(1);
    begin
       Pack.Half (Obj); -- (2)
    end Test2;

(2) is very much like (1); the user constraint is only checked on return if Priv
is passed by copy. So Obj most likely does not meet its constraint after the
call to Pack.Half.

We could probably fix this particular problem with some additional checking rule
on "in out" and "out" parameters, but I worry that this is just the camel's nose
-- it might turn into a mess of creeping additional run-time checks (especially
once Steve starting thinking about it).


I originally ran across this issue thinking about the limitations of access
types constrained by user-defined constraints. But eventually I realized that
the issue was pretty general -- it's not just a problem with designated objects
of access types.


So what do you all think? Should I write this up:

(1) Allowing these to apply only to bounds and discriminants? (The issues with
    those are well-understood, of course.)
(2) Allowing these to apply only to private types, with suitable additional
    checks defined on the return from the "defining subsystem" (the package
    containing the private type and its subsystem). The constraints would not
    meaningfully apply within the defining subsystem (it would be easy to change
    an object after the check).
(3) Combining (1) and (2).
(4) Neither (1) nor (2). (a) I've got a better idea; (b) don't bother.

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