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!w5g2000prd.googlegroups.com!not-for-mail From: Eric Hughes Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Bounded Date: Mon, 21 Apr 2008 09:35:36 -0700 (PDT) Organization: http://groups.google.com Message-ID: <15514187-d7d0-4650-a058-13ec5684be2c@w5g2000prd.googlegroups.com> 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> 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 1208795737 4910 127.0.0.1 (21 Apr 2008 16:35:37 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 21 Apr 2008 16:35:37 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: w5g2000prd.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:21016 Date: 2008-04-21T09:35:36-07:00 List-Id: 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. 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'. 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. 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 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