Re: Ada.Strings.Bounded

[Robert A Duff <bobduff@shell01.TheWorld.com>]

Eric Hughes <eric.eh9@gmail.com> writes:

> 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.

The above-quoted paragraph 3.5.4(8) is normative.  It comes right out
and says in plain language exactly what you were trying to prove in a
circuitous manner -- that the the set of values is infinite.

Note that it does not say anything special about root_int or univ_int.
It applies to ALL signed integer types, including user-defined ones.

You should read about static expressions, which will clear up some of
your confusings below.  You should also make sure you understand the
difference between overflow checks and range checks.

Also, there's a rule (which I'm too lazy to look up right now),
which says that at run time, the compiler is always allowed to get the
right answer.

So for a static expression that is outside the base range of its type,
the compiler must calculate the right answer.  For a non-static
expression, the compiler may raise Constraint_Error if the value is
outside the base range, or it may choose to get the right mathematical
answer.  It can even roll dice to decide whether to get the right
answer.

>> 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.

No, the semantics of "+" are different depending on whether the
expression is static.  NOT depending on whether the type is root_int.
For static expressions, "+" is not a partial function.

> 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?

No.  The "+" of root_integer returns root_integer, and there is no
implicit conversion from root_integer to My_Int, so the "+" of
root_integer can't be used in the above example.

>...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.

It is obeying the language rules.  You might say the language rules are
odd, and I would agree.  I don't much like the fact that static
expressions have subtly different evaluation rules from normal
run-time calculations.

>...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.

It's not a defect in GNAT -- read the section on static expressions.

> 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.

No.  Static expressions cannot overflow.  The "+" used in those two
examples is that of type Z.

Note that the "-" that occurs in some of your declarations of Z0 is the
"-" on root_integer.  Look at the special rules for named numbers in
3.3.2, and the special preference rule in 8.6(29).  But 8.6(29) has
nothing to do with the B and C constants in your examples.

>...It doesn't.  Maybe this is a GNAT defect.

No.

>...It seems
> just as likely that overload resolution is taking the addition and
> subtraction of root_integer.

No, as I explained, that "+" and "-" return the wrong type!

> 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.

Right.  Note that it complains about type Z, not about the named number
Z0.  GNAT is not allowed to complain about Z0 in Example H.

>...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.)

A fair complaint.

>...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.

No.  It is using the "+" on Z.  There is no "+" on universal_integer,
and the one on root_integer has the wrong result type.

>> 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.

No.  There is no nondeterministic overload resolution in Ada.

> 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.

Well, in the last sentence, "This" refers to some incorrect
interpretations of some (annoyingly complicated) Ada language rules,
so I still don't know what you mean (sorry).

- Bob