Operator visibility question

Operator visibility question

[Rod Chapman]

Can anyone please tell me if the following code is legal?

package MT
is
   type T is range 0 .. 4;
end MT;

with MT;
--# inherit MT;
package VT
is
   function "+" (Left, Right : in MT.T) return MT.T renames MT."+";
   A : constant := 2;
   B : constant MT.T := 3;

   C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
end VT;

The SPARK Examiner rejects the declaration of C with the message:

   9     C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
                                         ^
***        Semantic Error    :309: Operator not visible for these types.

On the other hand, GNAT 3.13 accepts the code with no errors.  Can anyone
explain which is right, and (more importantly) why?
 Cheers,
  Rod Chapman
  SPARK Team
  Praxis Critical Systems

Re: Operator visibility question

[Jeff Creem]

I really should be quoting LRM paragraphs when I say something like this but
it seems to me that  GNAT is wrong here since < is not visible and I can not
think of any reason why it should be visible.


It seems that if both sides of the < are MT.T GNAT does detect it but if
one side is universal integer it does not.


It is times like this that I miss Robert Dewar!

Jeff



"Rod Chapman" <rod@praxis-cs.co.uk> wrote in message
news:ba18d5cb.0106030548.62aa45e2@posting.google.com...
> Can anyone please tell me if the following code is legal?
>
> package MT
> is
>    type T is range 0 .. 4;
> end MT;
>
> with MT;
> --# inherit MT;
> package VT
> is
>    function "+" (Left, Right : in MT.T) return MT.T renames MT."+";
>    A : constant := 2;
>    B : constant MT.T := 3;
>
>    C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
> end VT;
>
> The SPARK Examiner rejects the declaration of C with the message:
>
>    9     C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
>                                          ^
> ***        Semantic Error    :309: Operator not visible for these types.
>
> On the other hand, GNAT 3.13 accepts the code with no errors.  Can anyone
> explain which is right, and (more importantly) why?
>  Cheers,
>   Rod Chapman
>   SPARK Team
>   Praxis Critical Systems

Re: Operator visibility question

[Nacho Robledo]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1379 bytes --]

I am not a good ada programmer but try this piece of code:

    C: constant Boolean := MT."<"(A+2,B);

I am not sure if this will run well but i think is the most common thing you
can do....

Good luck!!!!!

--
--
 Ignacio Robledo Rosell
 mailto:rrilpm@arrakis.es
 http://zipi.fi.upm.es/~g990406
 ****************************************
 "When code matters more than comercials"
 ****************************************

"Rod Chapman" <rod@praxis-cs.co.uk> escribi� en el mensaje
news:ba18d5cb.0106030548.62aa45e2@posting.google.com...
> Can anyone please tell me if the following code is legal?
>
> package MT
> is
>    type T is range 0 .. 4;
> end MT;
>
> with MT;
> --# inherit MT;
> package VT
> is
>    function "+" (Left, Right : in MT.T) return MT.T renames MT."+";
>    A : constant := 2;
>    B : constant MT.T := 3;
>
>    C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
> end VT;
>
> The SPARK Examiner rejects the declaration of C with the message:
>
>    9     C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
>                                          ^
> ***        Semantic Error    :309: Operator not visible for these types.
>
> On the other hand, GNAT 3.13 accepts the code with no errors.  Can anyone
> explain which is right, and (more importantly) why?
>  Cheers,
>   Rod Chapman
>   SPARK Team
>   Praxis Critical Systems

Re: Operator visibility question

[Robert A Duff]

"Nacho Robledo" <rrilNOSPAMpm@arrakis.es> writes:

> I am not a good ada programmer but try this piece of code:
> 
>     C: constant Boolean := MT."<"(A+2,B);

No, please don't.  A good style rule is to never use this notation -- if
you have a binary operator, always use infix notation.  Say "use type"
if necessary to make that legal.

> I am not sure if this will run well but i think is the most common thing you
> can do....

- Bob

Re: Operator visibility question

[Rod Chapman]

It seems this really is a problem - several other compilers,
including trusty old DEC Ada, agree that that code fragment should
be rejected, so I'll submit it to ACT.
 - Rod

Re: Operator visibility question

[Nacho Robledo]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 951 bytes --]

i don't know which is te problem... I use the clause use with packages with
come with Ada but with my own packages i do not do it .... .i prefer to do
it like this...


--
--
 Ignacio Robledo Rosell
 mailto:rrilpm@arrakis.es
 http://zipi.fi.upm.es/~g990406
 ****************************************
 "When code matters more than comercials"
 ****************************************

"Robert A Duff" <bobduff@world.std.com> escribi� en el mensaje
news:wccae3pfhge.fsf@world.std.com...
> "Nacho Robledo" <rrilNOSPAMpm@arrakis.es> writes:
>
> > I am not a good ada programmer but try this piece of code:
> >
> >     C: constant Boolean := MT."<"(A+2,B);
>
> No, please don't.  A good style rule is to never use this notation -- if
> you have a binary operator, always use infix notation.  Say "use type"
> if necessary to make that legal.
>
> > I am not sure if this will run well but i think is the most common thing
you
> > can do....
>
> - Bob

Re: Operator visibility question

[Ted Dennison]

In article <3b1bcc2b_4@news.arrakis.es>, Nacho Robledo says...
>
>i don't know which is te problem... I use the clause use with packages with
>come with Ada but with my own packages i do not do it .... .i prefer to do
>it like this...
..
>> >     C: constant Boolean := MT."<"(A+2,B);


Not a bad rule. But most folks in that circumstance would still either do a "use
type", or a local function renames. The only time I've ever seen the above was
in the code of a BLISS/C hacker who was using Ada under protest and wanted to
make a point about how horrible it was.

---
T.E.D.    homepage   - http://www.telepath.com/dennison/Ted/TED.html
          home email - mailto:dennison@telepath.com

Re: Operator visibility question

[Florian Weimer]

rod@praxis-cs.co.uk (Rod Chapman) writes:

> The SPARK Examiner rejects the declaration of C with the message:
> 
>    9     C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
>                                          ^
> ***        Semantic Error    :309: Operator not visible for these types.

This error message seems to be correct.

> On the other hand, GNAT 3.13 accepts the code with no errors.  Can anyone
> explain which is right, and (more importantly) why?

If one argument of a comparison operator is a universal integer,
a universal real, a string, or an aggregate, then the visibility
check is not performed.  I guess the bug is in somehwere in
Sem_Ch4.Find_Comparison_Types.Try_One_Interp, but I'm not sure, and
it's probably due to the way GNAT deals with operators for universal
types.

Re: Operator visibility question

[Ted Dennison]

In article <87hexx34kt.fsf@deneb.enyo.de>, Florian Weimer says...
>
>If one argument of a comparison operator is a universal integer,
>a universal real, a string, or an aggregate, then the visibility
>check is not performed.  I guess the bug is in somehwere in

Hmmm. That makes me wonder exactly which "<" the compiler is using when it
generates the code?

---
T.E.D.    homepage   - http://www.telepath.com/dennison/Ted/TED.html
          home email - mailto:dennison@telepath.com

Re: Operator visibility question

[Florian Weimer]

Ted Dennison<dennison@telepath.com> writes:

> In article <87hexx34kt.fsf@deneb.enyo.de>, Florian Weimer says...
>>
>>If one argument of a comparison operator is a universal integer,
>>a universal real, a string, or an aggregate, then the visibility
>>check is not performed.
> 
> Hmmm. That makes me wonder exactly which "<" the compiler is using when it
> generates the code?

The one which is not visible. ;-)

If there's no matching operator, I don't think the code in question is
reached at all.

Re: Operator visibility question

[Rod Chapman]

I'm pleased to say that ACT report this problem is now fixed
(a mere 21 hours after I submitted it), so full marks to
ACT's support team!

I think this thread can be closed now.
 - Rod

Re: Operator visibility question

[Robert A Duff]

rod@praxis-cs.co.uk (Rod Chapman) writes:

> Can anyone please tell me if the following code is legal?

In what language -- Ada or SPARK?  ;-) ;-)

> package MT
> is
>    type T is range 0 .. 4;
> end MT;
> 
> with MT;
> --# inherit MT;
> package VT
> is
>    function "+" (Left, Right : in MT.T) return MT.T renames MT."+";
>    A : constant := 2;
>    B : constant MT.T := 3;
> 
>    C : constant Boolean := (A + 2) < B; -- Is "<" visible here?

There are several "<" operators directly visible here, including the one
for root_integer.  But none of them apply -- the "<" for MT.T is not
directly visible here.  So I believe this is illegal in Ada, unless I'm
missing something.

A and 2 are both of type universal_integer, and there are implicit
conversions from u_i to any integer type, but there is no implicit
conversion from MT.T to root_real.

Sounds like a GNAT bug.  Seems like SPARK is correct here.

> end VT;
> 
> The SPARK Examiner rejects the declaration of C with the message:
> 
>    9     C : constant Boolean := (A + 2) < B; -- Is "<" visible here?
>                                          ^
> ***        Semantic Error    :309: Operator not visible for these types.
> 
> On the other hand, GNAT 3.13 accepts the code with no errors.  Can anyone
> explain which is right, and (more importantly) why?
>  Cheers,
>   Rod Chapman
>   SPARK Team
>   Praxis Critical Systems