Version 1.1 of ai12s/ai12-0328-1.txt

Unformatted version of ai12s/ai12-0328-1.txt version 1.1
Other versions for file ai12s/ai12-0328-1.txt

!standard 4.5.2(28.1/4)          19-04-05 AI12-0328-1/01
!class ramification 19-04-05
!status work item 19-04-05
!status received 19-03-28
!priority Low
!difficulty Easy
!subject Meaning of limited type and record type in 4.5.2(28.1/4)
!summary
The view of the type is irrelevant when determining whether a type is a record type or a limited type for the purposes of 4.5.2(28.1/4).
!question
RM 4.5.2(28-28.1/4) (A Dynamic Semantics rule) reads:
An individual membership test yields the result True if:
* The membership_choice is a choice_simple_expression, and the
tested_simple_expression is equal to the value of the membership_choice. If the tested type is a record type or a limited type, the test uses the primitive equality for the type; otherwise, the test uses predefined equality.
How does this work if the tested type is private? Does it depend on the view of the type? (No.)
!response
AARM 3.1(7-7.d/3) discuss the definition of "view of an entity", and when "view of" is implied. In particular, AARM 3.1(7.d/3) says:
On the other hand, run-time rules can work either way, so "view of" should not be assumed in Dynamic Semantics rules.
The rules discussed above are Dynamic Semantics rules, and "view of" does not appear. Moreover, it is usual that privacy is ignored for runtime rules, so this is not that unusual.
Therefore, private types are ignored when determining whether a type is a record type or a limited type for the purposes of determining the execution of a membership test.
!discussion
The basic idea is that a membership test works the same way as composition of equality, and predefined equality for a generic formal private type.
Thus, if we have:
package P1 is type P is private;
function "=" (Left, Right : P) return Boolean;
private type P is record ... end P1;
All three of those contexts will use the user-defined equality rather than the (overridden) predefined equality for type P. (Recall that Ada 2012 eliminated the distinction between tagged and untagged types on this point.)
In particular, a membership test for type P will use the user-defined equality.
Similarly, if one has an array type:
package P2 is type A is array (...) of ...;
function "=" (Left, Right : A) return Boolean; end P2;
The predefined equality is used to compose "=" and in generic units, and memberships do the same thing.
The concept of a limited type is more tied up with views (there isn't a private record type, but there is a limited private type). Consider for instance:
package P3 is type LP is limited private;
function "=" (Left, Right : LP) return Boolean;
private type LP is access ... end P3;
In this case, the full type elementary and nonlimited. The rule tells us that the predefined equality is used by a membership (outside of P3) in this case, even through a membership would be illegal if there was not an explicit definition for "=".
This admittedly is odd. Moreover, we don't have the composition (a type with a limited component is limited, and limited types don't have a predefined "=") nor generic formal private (a formal limited private type does not import "=") to guide us. We could talk about the re-emergence in a nested type, but the "=" can only be used in the body of P3 (and of its children), and the case is argubly a pathology.
We could consider using a view-based rule for cases like these. However, they lead to oddities where a membership on LP gets a different result in the body of P3 (where the full type for LP is visible) than in the specification and clients. This could be problematical for default expressions, where the value could depend on where it is evaluated, even if all of the denoted objects are the same.
[This concern comes to us courtesy of Steve Baird, who else? He and I disagree how a view-specific Dynamic Semantics rule would be applied in this case, and it probably is better to avoid the question in the first place. - Editor.]
[Author's aside: For the record, GNAT 18.1 gets all of this wrong. But it uses predefined equality for all memberships, including for types that are immutably limited and have no equality at all, rather than rejecting them. So I don't think this was a thought-out implementation, but rather just whatever fell out.]
!ASIS
No ASIS effect.
!ACATS test
ACATS tests C452004, C452005, and C452006 test various cases like these.
!appendix

From: Randy Brukardt
Sent: Thursday, march 28, 2019  10:32 PM

I'm spending a couple of days working on ACATS tests.

RM 4.5.2(28-28.1/4) (A Dynamic Semantics rule) reads:

An individual membership test yields the result True if: 

* The membership_choice is a choice_simple_expression, and the 
  tested_simple_expression is equal to the value of the membership_choice. 
  If the tested type is a record type or a limited type, the test uses the 
  primitive equality for the type; otherwise, the test uses predefined 
  equality.

AARM 3.1(7.d/3) says: "On the other hand, run-time rules can work either way, 
so "view of" should not be assumed in Dynamic Semantics rules." The above 
rule does not say "view of", so I presume that it ignores privacy.

This makes sense for records, as we want memberships to use the same "="
that is used for composition of equality. So in a case like:

   package P1 is
      type P is private;

      function "=" (Left, Right : P) return Boolean;

   private
      type P is record ...
   end P1;

We want the membership operation to use the primitive (user-defined) "=", not 
the predefined one. (The version of GNAT I have gets this wrong on the new 
ACATS test. Hope that's already been fixed.)

It's a bit weird that which equality is used for an array depends on whether 
the array type is limited, but of course there's no choice in the limited case 
(there's no predefined "=" to use), and the nonlimited case is consistent with 
composition and generic formal private types. And user-defined equality on 
array types isn't used that much.

Which brings us to my question. Consider (as in my new C452006 test):

   package P2 is
      type LP is private;

      function "=" (Left, Right : LP) return Boolean;

   private
      type LP is access ...
   end P2;

Here we have a type that is limited at the point of the membership, but the 
full view is nonlimited (and elementary).

The rule as written seems to imply that we ignore privacy and use the full 
view. In that case, the user-defined "=" is ignored by a membership operation, 
and the (hidden) predefined equality is used.

However, that is mighty strange; the programmer may have declared the type 
limited in the first place to ensure that the predefined equality wasn't used. 
They're not likely to be happy that it reappeared.

Note that there isn't any such existing case that's not pathological (unlike 
the array case): generic formal limited private types do not have "=", and 
there is no predefined equality for limited types, so there is no composition 
case to worry about. This sort of thing could happen only if a nested package 
declared a composite type with a component of the limited private type; in 
that case, the full view of the that type would have "="
and it would use the predefined "=" of the type -- but that "=" could only be 
used in the body of the (outer) package -- clients could never see it. (I 
consider this sort of case a pathology; Ada 83 should have banned it somehow 
rather than adopting a bunch of messy rules to make it work in an unexpected 
way, but of course it's way too late for that now.)

Also note that in the case where there is no visible "=", the membership is 
illegal. So we don't have to worry about *that* case.

I suspect that it would make more sense for the rule to be written in terms of 
whether the view of the type is visible. Of course, in that case, a membership 
in the body of P2 would act differently than the same membership elsewhere. 
Which I guess means we can't win. :-)

An alternative would be to write the rule in terms of immutably limited types 
to make it clearer that privacy is ignored. But in that case, we'd probably 
have to disallow writing a membership on a type whose full type is limited but 
not immutably limited. (Which would be incompatible.)

<Some time passes> I just read all of the discussion and minutes on the 
original AI, and didn't find anything about limited types other than Steve's 
"obvious" observation that we shouldn't be using "=" that doesn't exist or 
isn't visible (associated with adding the Legality Rule mentioned above).
Nothing about the Dynamic Semantics and views.

Thoughts on all of this?

****************************************************************

Questions? Ask the ACAA Technical Agent