Re: Ada.Strings.Bounded

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

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

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

OK, thanks.  I think I get it now.

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

OK, so m is some sequence of characters -- an integer literal.
That's what I was confused about before.

(Nit: an implementation is allowed to restrict integer literals
to 200 characters.  See RM-2.2(14).  It is not required to do
so, and anyway, it doesn't change the fact that there are an
infinite number of integers.)

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

Yes.  Every integer literal has type univ_int.

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

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.

We all know there are an infinite number of integers, so why did
you want to prove it?  Universal_integer is not special in this
regard.  And for compile time (static) calculations, Ada places
no limit on the size of integers.

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

OK, I see.

But you could rely on integer addition (for static values of type
root_integer, for example).

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

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 (if there are
many functions called F that are directly visible).  The type of X also
helps determine which F is called -- and there might be several
overloaded X's.  There might also be several P's, some of which have
a Param.

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

Seems like "need not break" isn't good enough -- I want to prove that it
"does not break".  There could be a user-defined "+".

>...I believe it's
> possible to make them explicit for arbitrary types.

Hmm.  I guess I need an example to see what you're getting at.
Choosing which function to call nondeterministically seems
like an Obviously Bad Idea, to me, so perhaps I don't understand
what you mean.

- Bob