Re: Ada.Strings.Bounded

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

On Mon, 14 Apr 2008 19:07:25 -0700 (PDT), Eric Hughes wrote:
> Seriously, we just disagree about this.  I can't take
> universal_integer seriously as a root class, because it's impossible
> to write down any representation of it.

On Apr 15, 2:02 am, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> Yes, because it is not what you wanted it be.

My belief about universal_integer is rooted in the language
definition.  I assert that that Ada as currently defined has no bound
on the size of numbers within universal_integer.  Here is my argument.

The best definition is in ARM 3.4.1(6/2-7).  (Defect report: this
doesn't appear in the index entry for universal_integer.)  Wherein:

> The set of values of a universal type is the undiscriminated
> union of the set of values possible for any definable type
> in the associated class.

The associated class to universal_integer is the signed integer type
(3.5.4), delineated by ranges given by static simple_expression.
There's no length limitation on an expression in the language, so
arbitrarily large ranges are possible.  Thus I can define the
following series of types:
    type I1 is range -2^10 .. 2^10 ;
    type I2 is range -2^100 .. 2^100 ;
    type I3 is range -2^1000 .. 2^1000 ;
    -- ...
The exponent in I(n) is an integer within the range of I(n-1).  The
type of an integer literal is universal_integer (2.4), which means
that if I(n-1) is well-defined, then so is I(n).  (Hence the
requirement for bignum arithmetic in the compiler.)  If you want to
exhibit a bound on universal_integer as a counterexample, I will take
its logarithm, round up, and add 1, and use that index to exhibit a
type definition that exceeds this bound.  Every integer is thus a
member of universal_integer.

If you can show me a Ada definition that can store a
universal_integer, only then will I believe you that it's the kind of
type that's just like an ordinary Ada type.

Perhaps you could explain what you want universal_integer to be.

Eric