Re: Ada.Strings.Bounded

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

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

> On Wed, 16 Apr 2008 07:40:32 -0700 (PDT), Eric Hughes wrote:
>> By my
>> previous proof about universal_integer, the expression 'm+1' is also a
>> universal_integer.
>
> As a reference, that message was
> <b7c7de31-2e96-4f5b-882e-5e991d52ae93@a9g2000prl.googlegroups.com>.
>
> On Apr 16, 12:28 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
>> How so? Clearly "+" is not closed in Universal_Integer.
>
> No, addition is closed in universal integer.  It's an implication of
> its definition. From 3.5.4/14
>> Integer literals are all of the type universal_integer, the
>> universal type (see 3.4.1) for the class rooted at root_integer,
>> allowing their use with the operations of any integer type.
>
> Every universal_integer has a literal expression 'm'. The expression 'm
> +1' is also a literal.  All literals have type universal_integer (see
> 2.4/3).  Therefore 'm+1' is also a universal_integer.

No, that's not quite right.  There's no such thing as a "literal
expression" in Ada, so I don't know what you mean by that.  Static
expression?  Expression of type universal_integer?  No idea...
The expression 'm+1' is certainly NOT a literal -- it's a function
call, passing an identifier and a literal as the actual parameters.

An integer literal has type universal_integer, as you said, but
universal_integer has no "+" operator.  There is a "+" for root_integer,
and also for user-defined integer types.  Universal_integers can be
implicitly converted to various integer types.

The type of an expression like m+1 depends in part on the context.

M : constant := 123; -- M is of type universal_integer.
X : constant := M + 1; -- The "+" for root_integer is called.
                       -- X is of type universal_integer.

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.

In both of the above "+" calls, the universal_integer operands are
implicitly converted -- to root_integer in the first case, and to My_Int
in the second case.

Static expressions are calculated exactly (arbitrary range).
Dynamic expressions are limited to some implementation
defined ranges -- this includes run-time values of type
root_integer and universal_integer.

> I should have realized that this was the point of the agreement long
> before.  The ARM is wrong on this point, or at the very least
> inconsistent.  Either they'll have to just say it's not a type (that
> is, an implementable Ada type) or they'll have to change the rules
> about integer literals.  The above proof about 'm+1' can be taken as a
> proof of inconsistency, if you like.

I don't see any inconsistency here.  An inconsistency would be a case
where the RM contradicts itself about whether a certain program is
legal, or what the run-time semantics of the program is.  You have
proven nothing of the kind, as far as I can see.

Anyway, it might make your point clearer if you explain it again,
but using proper Ada terminology this time.  I'd be interesting
in understanding your point...

- Bob