Re: Ada 2012 Constraints (WRT an Ada IR)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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