Re: Ada2012 Invariants and obaque types

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

On Jun 21, 11:27 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Hi Martin,
>
> Unless I've missed something, I do not see the point. Whether or not you  
> use an invariant, if the public view assert the type is tagged, the full  
> view must be tagged. This was the same, even prior to Ada 2012. Otherwise,  
> how would you derive from a tagged public view and define class wide view,  
>  from a type whose private view isn't tagged ?
>
> Just out of curiosity: which GNAT flavor do you use for Ada 2012 ?
>
> Le Tue, 21 Jun 2011 10:53:31 +0200, Martin <martin.do...@btopenworld.com>  
> a écrit:
>
>
>
>
>
>
>
>
>
> > 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)
>
> --
> “Syntactic sugar causes cancer of the semi-colons.”  [Epigrams on  
> Programming — Alan J. — P. Yale University]
> “Structured Programming supports the law of the excluded muddle.” [Idem]
> Java: Write once, Never revisit

Sorry - the pearls of doing a 'quick' demo...

Replace "type T1 is" with " type T1 is tagged"

and you still get:

> > p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> > declaration
> > p1.ads:15:14: invalid use of type before its full declaration
> > gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error

Which is the really what I'm asking about...

-- Martin