Weird error with Dynamic_Predicate

Weird error with Dynamic_Predicate

[mockturtle]

Dear all,
I am experiencing an error that is making me crazy and I was wondering if someone can help.

Some background: I want to define a type that represents an "identifier."  The identifier can assume two forms: 
 - qualified (es. namespace.foo)
 - not qualified (es. foo)

The two components (namespace and name) have the usual syntax (letters, digits and underscore).  Note that there are at most two components.  I want to use the aspect Dynamic_Predicate to enforce (and document) the right syntax.

You can find prova.ads and prova.adb at the end of this message.  I am using GPS 5.2.1 (20130102) and when I try to compile I get the obscure message

  29:32 error: conversion to incomplete type
  29:32 confused by earlier errors, bailing out

on >> prova.ads <<.  If I try to do "check semantic" on prova.ads and prova.adb, everything is fine.  


Any ideas?  Is it a compiler bug or am I doing something wrong?  Updating the compiler in this moment it would be a little pain for me (for several reasons), so I would like to be sure that I am not doing some subtle error before trying the update path.

Thank you in advance 

Riccardo



--- prova.ads ---
with Ada.Characters.Handling;     use Ada.Characters.Handling;
with Ada.Strings.Fixed;

package Prova is
   type Identifier_Name is new
     String
       with Dynamic_Predicate =>
         ((for all I in Identifier_Name'Range =>
             Is_Alphanumeric (Identifier_Name (I))
           or Identifier_Name (I) = '_'
           or Identifier_Name (I) = '.')
          and
            (not (Identifier_Name (Identifier_Name'First) in '0' .. '9'))
          and
            (Identifier_Name (Identifier_Name'First) /= '.')
          and
            Ada.Strings.Fixed.Count (String (Identifier_Name), ".") <= 1);

   function Is_Qualified (Item : Identifier_Name) return Boolean
     is (Ada.Strings.Fixed.Count (String (Item), ".") = 1);

   subtype Namespace_Identifier is Identifier_Name
   with Dynamic_Predicate => not Is_Qualified (Namespace_Identifier);

   subtype Full_Identifier is Identifier_Name
   with Dynamic_Predicate => Is_Qualified (Full_Identifier);


   function Extract_Namespace (Nome : Full_Identifier)
                               return Namespace_Identifier;

end Prova;

--- prova.adb --- 

package body Prova is


   -----------------------
   -- Extract_Namespace --
   -----------------------

   function Extract_Namespace (Nome : Full_Identifier)
                               return Namespace_Identifier
   is
      Idx : Natural := Ada.Strings.Fixed.Index (String (Nome), ".");
   begin
      return Namespace_Identifier (Nome (Nome'First .. Idx - 1));
   end Extract_Namespace;

end Prova;
----

Re: Weird error with Dynamic_Predicate

[Peter Chapin]

On 2014-05-12 15:47, mockturtle wrote:

> package Prova is
>    type Identifier_Name is new
>      String
>        with Dynamic_Predicate =>
>          ((for all I in Identifier_Name'Range =>
>              Is_Alphanumeric (Identifier_Name (I))
>            or Identifier_Name (I) = '_'
>            or Identifier_Name (I) = '.')
>           and
>             (not (Identifier_Name (Identifier_Name'First) in '0' .. '9'))
>           and
>             (Identifier_Name (Identifier_Name'First) /= '.')
>           and
>             Ada.Strings.Fixed.Count (String (Identifier_Name), ".") <= 1);

This isn't related to your question but it seems like you might also
want to be sure Identifier_Name'First actually refers to a character. In
other words you should check that the Identifier_Name is not empty.

Peter

Re: Weird error with Dynamic_Predicate

[mockturtle]

On Monday, May 12, 2014 10:45:10 PM UTC+2, Peter Chapin wrote:
> 
> This isn't related to your question but it seems like you might also
> want to be sure Identifier_Name'First actually refers to a character. In
> other words you should check that the Identifier_Name is not empty.
> 

Right.  This escaped to me.  

By the way, if I rememeber correctly (I am on a different computer now) if I change the type of the input parameter of Extract_Namespace everything is OK, so it seems the fact that the input parameter has type Full_Identifier.

Re: Weird error with Dynamic_Predicate

[Adam Beneschan]

For what it's worth, here's the smallest reduced example I can come up with that gives the same error message:

package Prova is
   type Identifier_Name is new String with Dynamic_Predicate => true;
   function Extract_Namespace (Nome : Identifier_Name)
                               return Identifier_Name;
end Prova;

package body Prova is
   function Extract_Namespace (Nome : Identifier_Name)
                               return Identifier_Name
   is
      Idx : Natural := Ada.Strings.Fixed.Index (String (Nome), ".");
   begin
      return "ns";
   end Extract_Namespace;
end Prova;

This is with GCC 4.5.4 (20120510).

                            -- Adam


On Monday, May 12, 2014 12:47:41 PM UTC-7, mockturtle wrote:
> Dear all,
> 
> I am experiencing an error that is making me crazy and I was wondering if someone can help.
> 
> 
> 
> Some background: I want to define a type that represents an "identifier."  The identifier can assume two forms: 
> 
>  - qualified (es. namespace.foo)
> 
>  - not qualified (es. foo)
> 
> 
> 
> The two components (namespace and name) have the usual syntax (letters, digits and underscore).  Note that there are at most two components.  I want to use the aspect Dynamic_Predicate to enforce (and document) the right syntax.
> 
> 
> 
> You can find prova.ads and prova.adb at the end of this message.  I am using GPS 5.2.1 (20130102) and when I try to compile I get the obscure message
> 
> 
> 
>   29:32 error: conversion to incomplete type
> 
>   29:32 confused by earlier errors, bailing out
> 
> 
> 
> on >> prova.ads <<.  If I try to do "check semantic" on prova.ads and prova.adb, everything is fine.  
> 
> 
> 
> 
> 
> Any ideas?  Is it a compiler bug or am I doing something wrong?  Updating the compiler in this moment it would be a little pain for me (for several reasons), so I would like to be sure that I am not doing some subtle error before trying the update path.
> 
> 
> 
> Thank you in advance 
> 
> 
> 
> Riccardo
> 
> 
> 
> 
> 
> 
> 
> --- prova.ads ---
> 
> with Ada.Characters.Handling;     use Ada.Characters.Handling;
> 
> with Ada.Strings.Fixed;
> 
> 
> 
> package Prova is
> 
>    type Identifier_Name is new
> 
>      String
> 
>        with Dynamic_Predicate =>
> 
>          ((for all I in Identifier_Name'Range =>
> 
>              Is_Alphanumeric (Identifier_Name (I))
> 
>            or Identifier_Name (I) = '_'
> 
>            or Identifier_Name (I) = '.')
> 
>           and
> 
>             (not (Identifier_Name (Identifier_Name'First) in '0' .. '9'))
> 
>           and
> 
>             (Identifier_Name (Identifier_Name'First) /= '.')
> 
>           and
> 
>             Ada.Strings.Fixed.Count (String (Identifier_Name), ".") <= 1);
> 
> 
> 
>    function Is_Qualified (Item : Identifier_Name) return Boolean
> 
>      is (Ada.Strings.Fixed.Count (String (Item), ".") = 1);
> 
> 
> 
>    subtype Namespace_Identifier is Identifier_Name
> 
>    with Dynamic_Predicate => not Is_Qualified (Namespace_Identifier);
> 
> 
> 
>    subtype Full_Identifier is Identifier_Name
> 
>    with Dynamic_Predicate => Is_Qualified (Full_Identifier);
> 
> 
> 
> 
> 
>    function Extract_Namespace (Nome : Full_Identifier)
> 
>                                return Namespace_Identifier;
> 
> 
> 
> end Prova;
> 
> 
> 
> --- prova.adb --- 
> 
> 
> 
> package body Prova is
> 
> 
> 
> 
> 
>    -----------------------
> 
>    -- Extract_Namespace --
> 
>    -----------------------
> 
> 
> 
>    function Extract_Namespace (Nome : Full_Identifier)
> 
>                                return Namespace_Identifier
> 
>    is
> 
>       Idx : Natural := Ada.Strings.Fixed.Index (String (Nome), ".");
> 
>    begin
> 
>       return Namespace_Identifier (Nome (Nome'First .. Idx - 1));
> 
>    end Extract_Namespace;
> 
> 
> 
> end Prova;
> 
> ----

Re: Weird error with Dynamic_Predicate

[Randy Brukardt]

"Adam Beneschan" <adambeneschan@gmail.com> wrote in message 
news:3f9e21b4-868d-44de-9673-824eefb9e79e@googlegroups.com...
> For what it's worth, here's the smallest reduced example I can come up 
> with that gives the same error message:
>
> package Prova is
>   type Identifier_Name is new String with Dynamic_Predicate => true;
>   function Extract_Namespace (Nome : Identifier_Name)
>                               return Identifier_Name;
> end Prova;
>
> package body Prova is
>   function Extract_Namespace (Nome : Identifier_Name)
>                               return Identifier_Name
>   is
>      Idx : Natural := Ada.Strings.Fixed.Index (String (Nome), ".");
>   begin
>      return "ns";
>   end Extract_Namespace;
> end Prova;
>
> This is with GCC 4.5.4 (20120510).

The package body is missing a context clause of Ada.Strings.Fixed. With that 
corrected, it works with the GNAT I'm using for ACATS testing.

Similarly, the OP's code sample compiles without errors with that GNAT.

Ergo, this is a GNAT bug that's been fixed sometime in the past two years. 
The OP needs a compiler upgrade (whether its available at this time is an 
unknown question).

                                 Randy.

Re: Weird error with Dynamic_Predicate

[Simon Wright]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> "Adam Beneschan" <adambeneschan@gmail.com> wrote in message 

>> This is with GCC 4.5.4 (20120510).

> Similarly, the OP's code sample compiles without errors with that GNAT.
>
> Ergo, this is a GNAT bug that's been fixed sometime in the past two
> years.  The OP needs a compiler upgrade (whether its available at this
> time is an unknown question).

The OP's code fails to compile with GNAT GPL 2013 and FSF GCC 4.8.1. It
compiles without error messages with FSF GCC 4.9.0.

Likewise Adam's (after Randy's fix).

Re: Weird error with Dynamic_Predicate

[Shark8]

On 12-May-14 13:47, mockturtle wrote:
> Any ideas?

   -- Identifier:
   Type Identifier is new String
   with Dynamic_Predicate =>
         Validate_Identifier_String( String(Identifier) )
      or Validate_Qualified_Identifier_String( String(Identifier) );

-- Typecasting is desired so that the predicate doesn't depend on
-- the input checking the predicate and thereby infinite-looping.

-- ...

     -- Ensures conformance of identifiers.
     --
     -- EBNF:
     -- identifier ::= identifier_letter {[ "_" ] ( identifier_letter | 
digit )}
     -- identifier_letter ::= upper_case_letter | lower_case_letter
     -- digit ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"
     Function Validate_Identifier_String	( Input : String ) return Boolean;

-- body

     Function Validate_Identifier_String	( Input : String ) return 
Boolean is
         Use Ada.Characters.Handling;
         Head : Character renames Input(Input'First);

         Function Underscore_Alphanumeric(C : Character) return Boolean is
           ( C = '_' or else Is_Alphanumeric(C) );

         Subtype Tail is Positive Range Input'First+1..Input'Last;

     Begin
         Return Result : Boolean := True do
             -- Ensure that Input's first character is a letter.
             -- (Implicit: that there is a first character.)
             -- (Implicit: that there is a last character.)
             Result:= Result
               and then Input'Length in Positive
               and then Is_Letter(Head);

             -- All subsequent characters must be underscor or alphanumeric;
             -- also, there can be no double underscore.
             For Index in Tail loop
                 Exit when not Result;
                 declare
                     C : Character renames Input(Index);
                 begin
                     Result := Result and Underscore_Alphanumeric( C ) and
                               (if C = '_' then Input(Index-1) /= '_');
                 end;
             end loop;

             -- The last character cannot be an underscore.
             Result:= Result and Input(Input'Last) /= '_';
         End return;
     End Validate_Identifier_String;

--------
     Validate_Qualified_Identifier_String would take its input and, upon 
detection of '.' pass the two substrings to Validate_Identifier_String 
since both would have to be valid identifiers.

Re: Weird error with Dynamic_Predicate

[G.B.]

On 12.05.14 21:47, mockturtle wrote:
> Any ideas?

 From a different angle, a rule of contract-based design---
assuming the lessons learned from DbC---is not a substitute
for input checking. While I guess you have your reasons for
attaching the Dynamic_Predicate to a string type, if you
are preforming proofs, which DbC would oblige you to do,
there is a different strategy:

By the above rule (about DbC not being input checking),
some I/O routine would check the syntax;
then, if the characters form a well formed string, the object
can be converted to a different string type; this string
type does not have the dynamic check attached, since after
the checking routine is done, the type's objects are known
to have only good values.

Re: Weird error with Dynamic_Predicate

[Martin]

On Tuesday, May 13, 2014 1:46:39 PM UTC+1, G.B. wrote:
> On 12.05.14 21:47, mockturtle wrote:
> 
> > Any ideas?
> 
> 
> 
>  From a different angle, a rule of contract-based design---
> 
> assuming the lessons learned from DbC---is not a substitute
> 
> for input checking. While I guess you have your reasons for
> 
> attaching the Dynamic_Predicate to a string type, if you
> 
> are preforming proofs, which DbC would oblige you to do,
> 
> there is a different strategy:
> 
> 
> 
> By the above rule (about DbC not being input checking),
> 
> some I/O routine would check the syntax;
> 
> then, if the characters form a well formed string, the object
> 
> can be converted to a different string type; this string
> 
> type does not have the dynamic check attached, since after
> 
> the checking routine is done, the type's objects are known
> 
> to have only good values.



Right, it should be the 'constructor' that ensures the class invariant - the validity of the 'raw string' or raises an exception otherwise.

So you always want to force the user to use a proved 'constructor' function and no other, e.g.

package Valid_Strings is
   type Valid_String (<>) is tagged private;
   Invalid_String : exception;
   function Create (S : String) return Valid_String; -- or Invalid_String
private
   type Valid_String is tagged record
      ...
   end record;
   ...
end Valid_Strings;


-- Martin

Re: Weird error with Dynamic_Predicate

[mockturtle]

Thank you everyone for your comments. 




@Randy, @Adam

> Ergo, this is a GNAT bug that's been fixed sometime in the past two years. 
> The OP needs a compiler upgrade (whether its available at this time is an 
> unknown question).

Yes, I was afraid of that, especially after seeing the "reduced example" by Adam.  BTW, this morning, thinking about that example, I found a workaround that works even with my version:

  function Extract_Namespace (Nome : Full_Identifier)
                               return Namespace_Identifier
   is
      Idx : Natural;
   begin
      Idx := Ada.Strings.Fixed.Index (String (Nome), ".");
      return Namespace_Identifier (Nome (Nome'First .. Idx - 1));
   end Extract_Namespace;

In other words, instead of initializing Index to the result of Index, I assign Idx in the function body.  This buys me some time before the upgrade... :-) 



@G.B.

> From a different angle, a rule of contract-based design--- 
> assuming the lessons learned from DbC---is not a substitute 
> for input checking. While I guess you have your reasons for 
> attaching the Dynamic_Predicate to a string type, 

One of the reason for using Dynamic_Predicate is... to make experience (it sounds better than "to play" :-) with it.  This is a piece of SW that I am writing for myself and I am using the occasion to get familiar with these new features.  

> By the above rule (about DbC not being input checking), 
> some I/O routine would check the syntax; 
> then, if the characters form a well formed string, the object 
> can be converted to a different string type; this string 
> type does not have the dynamic check attached, since after 
> the checking routine is done, the type's objects are known 
> to have only good values. 

This is actually my case: most of the strings are read via a scanner that implements an automaton that recognizes the identifiers (the other identifiers are just constant strings in the code).  If was sure that the automaton is correct (nice 'if'), I would be granted that the identifiers have the correct syntax; but since an error could slip, (or I could write a constant with the wrong syntax) I am using the predicate as a "bug trap" kept on at debug time.

Oh, BTW, sorry for the question, but what does DbC mean? (I guess it has nothing to do with dB...)



@Martin

> it should be the 'constructor' that ensures the class invariant - the 
> validity of the 'raw string' or raises an exception otherwise. 
>
> So you always want to force the user to use a proved 'constructor' 
> function and no other, e.g. 
> 
> package Valid_Strings is 
>    type Valid_String (<>) is tagged private; 
>    Invalid_String : exception; 
>    function Create (S : String) return Valid_String; 

Yes, and often I used this type of solution.  In this case I felt that it
was maybe a bit an overkill, since my object is a String, not only as a representation but also "conceptually", only with an additional 
constraint. (As I said above, the identifiers in my code are 
constants or are read via a scanner and this should grant the correct syntax) Also this solution would make the code a bit heavier since I would loose the fact that a String is an array and I should provide functions for slicing, concatenation, searching and so on; at the very minimum I would need a function to convert a Valid_String back into a String.     Not big deal?  I agree... nevertheless the code is a bit more "natural" in this way.

--

Best regards,

Riccardo

Re: Weird error with Dynamic_Predicate

[Simon Wright]

Simon Wright <simon@pushface.org> writes:

> "Randy Brukardt" <randy@rrsoftware.com> writes:
>
>> "Adam Beneschan" <adambeneschan@gmail.com> wrote in message 
>
>>> This is with GCC 4.5.4 (20120510).
>
>> Similarly, the OP's code sample compiles without errors with that GNAT.
>>
>> Ergo, this is a GNAT bug that's been fixed sometime in the past two
>> years.  The OP needs a compiler upgrade (whether its available at this
>> time is an unknown question).
>
> The OP's code fails to compile with GNAT GPL 2013 and FSF GCC 4.8.1. It
> compiles without error messages with FSF GCC 4.9.0.
>
> Likewise Adam's (after Randy's fix).

Both OK with GNAT GPL 2014.

Re: Weird error with Dynamic_Predicate

[Georg Bauhaus]

On 13/05/14 20:55, mockturtle wrote:
> what does DbC mean?

DbC is short for Design by Contract™.

An original, including pragmatic insight:

http://se.ethz.ch/~meyer/publications/computer/contract.pdf

More in OOSC 2nd Ed. by the same author.

Re: Weird error with Dynamic_Predicate

[mockturtle]

On Tuesday, May 13, 2014 11:39:49 PM UTC+2, Georg Bauhaus wrote:
> On 13/05/14 20:55, mockturtle wrote:
> 
> > what does DbC mean?
> 
> DbC is short for Design by Contract�.
> 

Oh, right... I could have guessed that... 

Thank you