Eric Hughes <eric.eh9@[EMAIL PROTECTED]
> 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@[EMAIL PROTECTED]
>.
>
> On Apr 16, 12:28 pm, "Dmitry A. Kazakov" <mail...@[EMAIL PROTECTED]
>
> 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


|