Re: Ada2012 Invariants and obaque types

[Martin <martin.dowie@btopenworld.com>]

On Jun 21, 11:43 am, Ludovic Brenta <ludo...@ludovic-brenta.org>
wrote:
> Martin Dowie wrote on comp.lang.ada:
>
>
>
>
>
>
>
>
>
> > A fairly common Ada idiom is to define the full view of a private type
> > using an incomplete declaration. Thus leaving the actual
> > implementation to the package spec. Trying this out with the public
> > view defined with an invariant lead to a compiler error - is this:
>
> > a) expected?
> > b) an unexpected consequence? or
> > c) a compiler bug?
>
> > Example:
> > package P1 is
> >    type T1 is tagged private
> >       with Invariant => Is_Valid (T1);
> >    function Create               return T1;
> >    function Is_Valid (This : T1) return Boolean;
> > private
> >    type Imp;
> >    type T1 is
> >       record
> >          I : Imp;
> >       end record;
> > end P1;
>
> > gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
> > gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
> > gnatA H:\Ada\test_invariants\src\p1.ads
> > p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> > declaration
> > p1.ads:13:09: full declaration of private type "T1" defined at line 3
> > must be a tagged type
> > p1.ads:15:14: invalid use of type before its full declaration
> > gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
> > [2011-06-21 09:46:55] process exited with status 4 (elapsed time:
> > 00.26s)
>
> This looks like a consequence of 13.14(8.2/1): "If an expression is
> implicitly converted to a type or subtype T, then at the place where
> the expression causes freezing, T is frozen." (where in this case the
> expression is T1, which stands for the current instance of the type,
> and the type T is also T1).
>
> This subclause however seems to contradict 13.14(7.2/3): "At the
> freezing point of the entity associated with an aspect_specification,
> any expressions or names within the aspect_specification cause
> freezing."; this subclause would defer the freezing point of T1 until
> the end of the enclosing package spec or the declaration of a constant
> of the type, whichever comes first (as is normal for tagged types).
>
> Another possible interpretation is that Is_Valid must be called as
> part of the elaboration of type T1, in which case the
> aspect_specification is a function call, which freezes the types of
> its parameters (per 13.14(10.1/3)).  But I doubt this is true.
>
> So, this looks like an area of the language definition that needs
> clarifying (but then again, freezing rules have always been difficult
> to understand). The behavior of the compiler definitely looks
> undesirable to me.  So I vote for b) an unexpected (and undesirable)
> consequence (of existing rules).
>
> --
> Ludovic Brenta.

Ok, thanks for that Ludovic...maybe need to post this one to ada-
auth...

-- Martin