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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Wed, 14 Dec 2016 09:54:34 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <1af458a8-cf5b-4dd7-824d-eed1ed5ffb21@googlegroups.com> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32808 Date: 2016-12-14T09:54:34+01:00 List-Id: On 13/12/2016 23:32, Shark8 wrote: > On Tuesday, December 13, 2016 at 2:11:56 PM UTC-7, Dmitry A. Kazakov wrote: >> On 2016-12-13 19:25, Shark8 wrote: >>> On Tuesday, December 13, 2016 at 4:19:17 AM UTC-7, Dmitry A. Kazakov wrote: >>>> On 13/12/2016 11:39, G.B. wrote: >>>>> >>>>> Pre doesn't have to be object language as has now been >>>>> said and confirmed a number of times. >>>> >>>> Being a part of the body it does not belong to declarations. >>> >>> By that logic we shouldn't have something like: >>> type Item is null record; -- Stub >>> type Pointer is access Item; -- Access type >>> subtype Handle is not null Pointer; -- Subtype excluding null >>> >>> Procedure Something(Object : Handle); -- Object can't be null. >>> because we could instead say: >>> Procedure Something(Object : Pointer) is >>> begin >>> if Object = Null then --... >>> end; >>> >>> Or, really, any subtype. >> >> No. Type/subtype declarations are expressions involving type-algebraic >> operations [some operands are types, results are types]. > > And now we're back to the question I presented illustrating the > thrust of this thread* with the P0, P1, P2, & P3 examples. Why? Of course you can define a type by providing operation's body in a declaration. The objection was: it is bad language design. That point stands. Others tried to argue that such bodies are not bodies but magically "preconditions". No, they are still bodies, just misplaced ones. >> You cannot use them in the bodies. They implicitly define operations of >> the resulting type and the corresponding bodies. > > Nope. > Ada 83 LRM (3.3.2) says, in part: > "A type mark denotes a type or a subtype. If a type mark is the name > of a type, the type mark denotes this type and also the corresponding > unconstrained subtype. The base type of a type mark is, by definition, > the base type of the type or subtype denoted by the type mark." > > And (3.3) says, as its very first sentence: > "A type is characterized by a set of values and a set of operations." > > It is therefore *MOT* the subtype which defines the operations. There was a discussion on this topic in c.l.a. before. A subtype *is* a type, regardless how you read ARM. The proof is simple, a subtype has some operations that behave differently than ones of the unconstrained parent type, e.g. they raise Constraint_Error. Different operations, ergo different type. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de