Re: Ada.Strings.Bounded

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 23 Apr 2008 12:42:32 +0200, Georg Bauhaus wrote:

> But how about this:
> 
> procedure Ex is
>     type E is (A, B, C);
>     X: E;
> begin
>     X := E'pred(E'succ(C));
> end Ex;
> 
> In this case there is a static constraint error. Is this
> consistent with anything but the Ada LRM's exception for
> "integer convenience"?

But enumeration is finite. If we had extensible enumerations then it would
be reasonable to consider the set of enumeration values infinite, similarly
to signed integers.

Probably it could be possible to formalize such things by allowing the user
to describe certain properties of primitive operations. The case (A + B)
mod C relies on the group property of "+" and "mod":

   forall n   (A + nC) mod C = A mod C

There exists properties Ada compiler knows. For example:

  forall private T, (not X=Y) = (X/=Y)

But it does not know that  X - Y = X + (-Y), etc.

Also, supertyping should help. The anonymous types before the first named
subtype is nothing but a supertype, if you wanted to expose it. In the
cases when the user defines a primitive operation, the stuff like above
could to be defined in terms of the supertype or the class of
(contravariant).

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de