Re: Ada.Strings.Bounded

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

On Apr 21, 8:08 am, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> Anyway, it might make your point clearer if you explain it again,
> but using proper Ada terminology this time.

I will endeavor to use Ada terminology when I can, but there is not
Ada terminology for some of the things I'm talking about.  I'll start
back at the beginning of the argument I made just previously.  I'm
stripping this argument down to its basics.  I've removed any piece of
the argument that includes anything that might be mistaken for an Ada
arithmetic operation.

Eric Hughes <eric....@gmail.com> writes:
> Every universal_integer has a literal expression 'm'.

Let N0 be the value in {\bb N} for this universal integer.  This N0 is
not an Ada natural, it's a mathematical one.  I will presume that
there is an injective map from universal_integer into {\bb Z} that
preserves value.  I would find it absurd to disagree with this
premise, but I'd rather make it explicit than not.

What I mean by what I said is that there a sequence of characters 'm'
that, when used as a static_expression in a number_declaration
(3.3.2/2), creates an Ada constant whose value is equal to N0.  'm' is
not an Ada construct, it's a sequence of characters valid for
substitution into an Ada program.  Furthermore, we can find such an
'm' that is valid as a 'numeral' (2.4.1/3), consisting only of
digits.  Since I was only discussing positive upper bounds and
'numeral' has no minus sign in its syntax, this sequence of characters
is unique and always exists.

Eric Hughes <eric....@gmail.com> writes:
> The expression 'm+1' is also a literal.

Let N1 = N0 + 1.  N1 is also in {\bb N}. There's another sequence of
characters, which I called 'm+1', again also valid as an Ada
'numeral', that has the value N1.  We compute this using outside-of-
Ada ordinary mathematical operations.  ARM 2.4.1 "Decimal Literals"
has no length limitation on 'numeral'.

Eric Hughes <eric....@gmail.com> writes:
> All literals have type universal_integer (see 2.4/3).
> Therefore 'm+1' is also a universal_integer.

Admittedly I was only talking about integer literals; other literals
have different types.  The term "integer literal" is defined in ARM
2.4/1:
> an integer literal is a numeric_literal without a point
Both sequences of characters 'm' and 'm+1' consist only of digits, so
each is also valid as an "integer literal".

So far I've only dealt with syntactic issues.  I need to now make an
assertion about type.  From ARM 2.4/3:
> The type of an integer literal is universal_integer.

I see two arguably-correct ways of interpreting this statement, one
absolute and one contingent:
-- Every integer literal has a type and that type is
universal_integer.
-- If an integer literal has a type, that type is universal_integer.
I believe the contingent version is not the meaning.  The ARM
statement is written in unconditional language.  "The type of an
integer literal" identifies the unique type associated with that
integer literal and implies that there is always such a type.  The
contingent version of this sentence would be "The type of an integer
literal, if any, is universal_integer."  But that's not what it says.

Hence both 'm' and 'm+1' have a type, and that that type is
universal_integer.  By induction, universal_integer has no upper
bound.


On Apr 21, 8:08 am, Robert A Duff <bobd...@shell01.TheWorld.com>
wrote:
> The expression 'm+1' is certainly NOT a literal -- it's a function
> call, passing an identifier and a literal as the actual parameters.

I redid the argument to get rid of this ambiguity.  Admittedly I had
not distinguished addition on {\bb N} and addition on Ada types.  My
argument doesn't rely upon addition on any Ada type.

> Universal_integers can be
> implicitly converted to various integer types.

This was the whole point of the discussion--why such implicit
conversions do not break the type system.  It's not like integers are
a tagged type.

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

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?

Context-dependent function selection need not break correctness of a
program, even when there's ambiguity in what function might be
selected (non-deterministic execution).  The conditions for this to
work are implicitly present with integer types.  I believe it's
possible to make them explicit for arbitrary types.

Eric