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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham 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!news1.google.com!newsfeed2.dallas1.level3.net!news.level3.com!newsfeed-00.mathworks.com!nntp.TheWorld.com!not-for-mail From: Robert A Duff Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Bounded Date: Mon, 21 Apr 2008 14:04:56 -0400 Organization: The World Public Access UNIX, Brookline, MA Message-ID: References: <013e1d52-c25f-49ea-83ef-6ac4860858bf@s13g2000prd.googlegroups.com> <8g2rpvi2ahu0$.1ebsyq5yu1whf.dlg@40tude.net> <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: shell01.theworld.com Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: pcls4.std.com 1208801096 31594 192.74.137.71 (21 Apr 2008 18:04:56 GMT) X-Complaints-To: abuse@TheWorld.com NNTP-Posting-Date: Mon, 21 Apr 2008 18:04:56 +0000 (UTC) User-Agent: Gnus/5.1008 (Gnus v5.10.8) Emacs/21.3 (irix) Cancel-Lock: sha1:a7Sqbq8oBLEhRFJeR9LDYGFmdns= Xref: g2news1.google.com comp.lang.ada:21018 Date: 2008-04-21T14:04:56-04:00 List-Id: Eric Hughes writes: > On Apr 21, 8:08 am, Robert A Duff > 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 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 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 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 > 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