From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,640b65cbfbab7216 X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!postnews.google.com!p39g2000prm.googlegroups.com!not-for-mail From: Eric Hughes Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Bounded Date: Mon, 21 Apr 2008 17:19:52 -0700 (PDT) Organization: http://groups.google.com Message-ID: <07e98c4f-9b79-412f-9e95-94dd04082355@p39g2000prm.googlegroups.com> References: <9a3ad8ca-9f44-42db-9f7c-c5f9e3ee60f3@w1g2000prd.googlegroups.com> <1jdzw15tbj376$.nyv9yml75wj4$.dlg@40tude.net> <80c6fdca-1a89-4d98-b61d-9a405e57d8e5@s13g2000prd.googlegroups.com> <1wh7cbu67y4wz$.7iu8likx0fct.dlg@40tude.net> <144w648u50r6q.1erjxxu0cplbw.dlg@40tude.net> <611360e0-595c-43a7-b5cb-137a278ec0c1@s13g2000prd.googlegroups.com> <15389tuelo6x6$.1c1a6yixordts$.dlg@40tude.net> <4c1be2a2-0178-4c1f-8c96-526020550f42@w4g2000prd.googlegroups.com> <15514187-d7d0-4650-a058-13ec5684be2c@w5g2000prd.googlegroups.com> NNTP-Posting-Host: 166.70.57.218 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1208823593 6504 127.0.0.1 (22 Apr 2008 00:19:53 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Tue, 22 Apr 2008 00:19:53 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: p39g2000prm.googlegroups.com; posting-host=166.70.57.218; posting-account=5RIiTwoAAACt_Eu87gmPAJMoMTeMz-rn User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.8.1.14) Gecko/20080404 Firefox/2.0.0.14,gzip(gfe),gzip(gfe) Xref: g2news1.google.com comp.lang.ada:21024 Date: 2008-04-21T17:19:52-07:00 List-Id: On Apr 21, 12:04 pm, Robert A Duff 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