Ada.Strings.Bounded
in [ADA]
|
From: Robert A Duff on 21 Apr 2008 10:08 Eric Hughes <eric.eh9(a)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(a)a9g2000prl.googlegroups.com>. > > On Apr 16, 12:28 pm, "Dmitry A. Kazakov" <mail...(a)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
From: Eric Hughes on 21 Apr 2008 12:35 On Apr 21, 8:08 am, Robert A Duff <bobd...(a)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....(a)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....(a)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....(a)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...(a)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
From: Robert A Duff on 21 Apr 2008 14:04 Eric Hughes <eric.eh9(a)gmail.com> writes: > On Apr 21, 8:08 am, Robert A Duff <bobd...(a)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....(a)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....(a)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....(a)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...(a)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
From: Dmitry A. Kazakov on 21 Apr 2008 14:50 On Mon, 21 Apr 2008 09:35:36 -0700 (PDT), Eric Hughes wrote: > ARM 2.4.1 "Decimal Literals" > has no length limitation on 'numeral'. Hmm, I don't see it saying this. Do you mean that the syntax rule specifies not limit? If so, we have visited this before, that would not prove your point. Putting no explicit limit does not require its absence. Consider German highways, there is no speed limit, alas only at certain places. Should it mean existence of cars moving faster that light? It is legal not to compile [some] legal programs. > On Apr 21, 8:08 am, Robert A Duff <bobd...(a)shell01.TheWorld.com> >> 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. I don't see any difference, except that the type tag is not stored in (more precisely, cannot be obtained from) the values. >> 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? The context does not define the types. It resolves overloaded symbols. > 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. The following program: with Ada.Text_IO; use Ada.Text_IO; procedure Test_Int is type My_Int is range 1..100; function "+" (L, R : My_Int) return My_Int is begin return 10; end "+"; Y : constant My_Int := 1 + 1; begin Put_Line (My_Int'Image (Y)); end Test_Int; illustrates Robert's point. It shall print 10. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Eric Hughes on 21 Apr 2008 20:19
On Apr 21, 12:04 pm, Robert A Duff <bobd...(a)shell01.TheWorld.com> wrote: > We all know there are an infinite number of integers, so why did > you want to prove it? The question was not about {\bb N}, but about universal_integer, which two things are not _a priori_ the same thing. > 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. The argument was being made against the counter-assertion that universal_integer is an ordinary integer type and thus has a finite range. And I wanted to make that argument from normative sources, not from commentary. > But you could rely on integer addition (for static values of type > root_integer, for example). Could I? I'm not so sure. If root_integer is a range, as ordinary defined integer types are, then "+" is a partial function and not a total one, breaking the argument. Bob's example: > 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. Me: > > 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 OK. Somehow I had missed the fact that Ada does overload resolution based on assignment context. So I read up on it in more detail. Pardon me if I've missed something in the foregoing. The overload resolution in the present example, though, doesn't seem unique. Could not "+" resolve to the "+" of root_integer? It seems to pass all of the requirements. To test this, I wrote the following three lines of code and ran them through GNAT: -- (Example A) Z0 : constant := Integer'Last - 1 ; type Z is range 0 .. Z0 ; B : constant Z := ( Z0 + 1 ) - 1 ; GNAT compiled it without a problem and it ran without error. The following program, however, did neither: -- (Example B) Z0 : constant := Integer'Last - 1 ; type Z is range 0 .. Z0 ; C : constant Z := Z0 + 1 ; GNAT gave a warning that a constraint error would be raised and indeed running it raised one. Now I raise the upper bound by one: -- (Example C) Z0 : constant := Integer'Last ; type Z is range 0 .. Z0 ; B : constant Z := ( Z0 + 1 ) - 1 ; GNAT compiles this one fine and runs fine, just like Example A. -- (Example D) Z0 : constant := Integer'Last ; type Z is range 0 .. Z0 ; C : constant Z := Z0 + 1 ; GNAT says "static expression fails Constraint_Check" and does not compile. Let's raise the upper bound one last time: -- (Example E) Z0 : constant := Integer'Last + 1 ; type Z is range 0 .. Z0 ; B : constant Z := ( Z0 + 1 ) - 1 ; Just fine, as usual. -- (Example F) Z0 : constant := Integer'Last + 1 ; type Z is range 0 .. Z0 ; C : constant Z := Z0 + 1 ; GNAT gives the same warning as example B. As an aside, GNAT is clearly doing something odd. Of the three declarations of "C", you have two warnings and one error, not the same. I'm not even sure that's a defect. The real point, though, is that it just can't be true that the addition and subtraction in examples A and C are those of type Z. If this were true, the expression ( Z0 + 1 ) - 1 should translate to something like this: Z_subtract( Z_add( Z0, 1 ), 1 ) If that were the case, then the Z_add expression should raise a constraint error. It doesn't. Maybe this is a GNAT defect. It seems just as likely that overload resolution is taking the addition and subtraction of root_integer. And then I had an inspiration: -- (Example G) Z0 : constant := Long_Long_Integer'Last ; type Z is range 0 .. Z0 ; B : constant Z := ( Z0 + 1 ) - 1 ; -- (Example H) Z0 : constant := Long_Long_Integer'Last + 1 ; type Z is range 0 .. Z0 ; B : constant Z := ( Z0 + 1 ) - 1 ; Now we've hit the GNAT implementation limit. Example H, finally, fails to compile because "integer type definition bounds out of range". (I don't like this message because it's not clear that an internal limit has been exceeded.) Example G, however, compiles and runs just fine. Example G shows that, at least in this example, it's doing arithmetic on universal_integer, because there's no other type internally that it could be using. > Choosing which function to call nondeterministically seems > like an Obviously Bad Idea, to me, so perhaps I don't understand > what you mean. All the above examples seem to indicate that GNAT, at least, is resolving overloaded addition operators. The overload is between the declared type, root_integer (or something like it), and possibly even universal_integer. With other types, ones where there is no universal type, this would be an illegal ambiguity. So it seems that GNAT is nondeterministically resolving them. It works here because all these types are compatible for such resolution. It doesn't cause any problems. This is what I believe could be declared explicitly. Eric |