Re: Ada.Strings.Bounded

[Eric Hughes <eric.eh9@gmail.com>]

On Apr 21, 12:04 pm, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> We all know there are an infinite number of integers, so why did
> you want to prove it?

The question was not about {\bb N}, but about universal_integer, which
two things are not _a priori_ the same thing.

> Sure.  But I don't see the need for all this song and dance,
> since AARM-3.5.4 says:
>
> 8     The set of values for a signed integer type is the (infinite) set of
> mathematical integers[, though only values of the base range of the type are
> fully supported for run-time operations]. The set of values for a modular
> integer type are the values from 0 to one less than the modulus, inclusive.

The argument was being made against the counter-assertion that
universal_integer is an ordinary integer type and thus has a finite
range.  And I wanted to make that argument from normative sources, not
from commentary.

> But you could rely on integer addition (for static values of type
> root_integer, for example).

Could I?  I'm not so sure.  If root_integer is a range, as ordinary
defined integer types are, then "+" is a partial function and not a
total one, breaking the argument.

Bob's example:
> type My_Int is range 1..100;
> Y : constant My_Int := 1 + 1; -- The "+" of My_Int is called.
>                               -- Y is of type My_Int.

Me:
> > Are there other places in Ada when the context of an operation
> > determines the type of the operands of the function and thus also the
> > function signature?

> Overload resolution always takes the context into account,
> for function calls.  Nothing special about "+" in that regard.
> If you say:
>
>     P(Param => F(X));
>
> Then the type of Param helps determine which F is called

OK.  Somehow I had missed the fact that Ada does overload resolution
based on assignment context.  So I read up on it in more detail.
Pardon me if I've missed something in the foregoing.

The overload resolution in the present example, though, doesn't seem
unique.  Could not "+" resolve to the "+" of root_integer?  It seems
to pass all of the requirements.  To test this, I wrote the following
three lines of code and ran them through GNAT:
    -- (Example A)
    Z0 : constant := Integer'Last - 1 ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
GNAT compiled it without a problem and it ran without error.  The
following program, however, did neither:
    -- (Example B)
    Z0 : constant := Integer'Last - 1 ;
    type Z is range 0 .. Z0 ;
    C : constant Z := Z0 + 1 ;
GNAT gave a warning that a constraint error would be raised and indeed
running it raised one.  Now I raise the upper bound by one:
    -- (Example C)
    Z0 : constant := Integer'Last ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
GNAT compiles this one fine and runs fine, just like Example A.
    -- (Example D)
    Z0 : constant := Integer'Last ;
    type Z is range 0 .. Z0 ;
    C : constant Z := Z0 + 1 ;
GNAT says "static expression fails Constraint_Check" and does not
compile.  Let's raise the upper bound one last time:
    -- (Example E)
    Z0 : constant := Integer'Last + 1 ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
Just fine, as usual.
    -- (Example F)
    Z0 : constant := Integer'Last + 1 ;
    type Z is range 0 .. Z0 ;
    C : constant Z := Z0 + 1 ;
GNAT gives the same warning as example B.

As an aside, GNAT is clearly doing something odd.  Of the three
declarations of "C", you have two warnings and one error, not the
same.  I'm not even sure that's a defect.

The real point, though, is that it just can't be true that the
addition and subtraction in examples A and C are those of type Z.  If
this were true, the expression
    ( Z0 + 1 ) - 1
should translate to something like this:
    Z_subtract( Z_add( Z0, 1 ), 1 )
If that were the case, then the Z_add expression should raise a
constraint error.  It doesn't.  Maybe this is a GNAT defect.  It seems
just as likely that overload resolution is taking the addition and
subtraction of root_integer.

And then I had an inspiration:
    -- (Example G)
    Z0 : constant := Long_Long_Integer'Last ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
    -- (Example H)
    Z0 : constant := Long_Long_Integer'Last + 1 ;
    type Z is range 0 .. Z0 ;
    B : constant Z := ( Z0 + 1 ) - 1 ;
Now we've hit the GNAT implementation limit.  Example H, finally,
fails to compile because "integer type definition bounds out of
range".  (I don't like this message because it's not clear that an
internal limit has been exceeded.)  Example G, however, compiles and
runs just fine.  Example G shows that, at least in this example, it's
doing arithmetic on universal_integer, because there's no other type
internally that it could be using.

> Choosing which function to call nondeterministically seems
> like an Obviously Bad Idea, to me, so perhaps I don't understand
> what you mean.

All the above examples seem to indicate that GNAT, at least, is
resolving overloaded addition operators.  The overload is between the
declared type, root_integer (or something like it), and possibly even
universal_integer.  With other types, ones where there is no universal
type, this would be an illegal ambiguity.  So it seems that GNAT is
nondeterministically resolving them.

It works here because all these types are compatible for such
resolution.  It doesn't cause any problems.  This is what I believe
could be declared explicitly.

Eric