Some kind of repeating in Static_Predicate

Some kind of repeating in Static_Predicate

[ytomino]

Hello.

I'm trying to use a constant table (but that is unstable and may be changed in compile-time) in Static_Predicate.

 Set : constant String := ('T', 'a', 'b', 'l', 'e');
 
 subtype T is Character
    with Static_predicate => (for some I of Set => X = I);

Of cause, quantified expression in the static context is illegal.

 xx.ads:6:33: expression is not predicate-static (RM 3.2.4(16-22))

So, it have to be rewrote to

 subtype T is Character
    with Static_Predicate =>
       (T = Set (1)
          or else (Set'Last >= 2 and then T = Set (2))
          or else (Set'Last >= 3 and then T = Set (3))
          or else (Set'Last >= 4 and then T = Set (4))
          ...);

This looks stupid.
Is there any good alternative?

Thank you.

Re: Some kind of repeating in Static_Predicate

[Jacob Sparre Andersen]

ytomino <aghia05@gmail.com> writes:

> I'm trying to use a constant table (but that is unstable and may be
> changed in compile-time) in Static_Predicate.
>
>  Set : constant String := ('T', 'a', 'b', 'l', 'e');
>  
>  subtype T is Character
>     with Static_predicate => (for some I of Set => X = I);

Why not admit that it is a Dynamic_Predicate?

Alternatively:

   type T is ('T', 'a', 'b', 'l', 'e');

Or:

   subtype T is Character
      with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');

Greetings,

Jacob
-- 
"people who live in glass houses shouldn't be throwing rocks
 -- especially at those who don't live in glass houses"

Re: Some kind of repeating in Static_Predicate

[ytomino]

On Monday, June 4, 2018 at 3:26:56 PM UTC+9, Jacob Sparre Andersen wrote:
> ytomino <agh...@gmail.com> writes:
> 
> > I'm trying to use a constant table (but that is unstable and may be
> > changed in compile-time) in Static_Predicate.
> >
> >  Set : constant String := ('T', 'a', 'b', 'l', 'e');
> >  
> >  subtype T is Character
> >     with Static_predicate => (for some I of Set => X = I);
> 
> Why not admit that it is a Dynamic_Predicate?
> 
> Alternatively:
> 
>    type T is ('T', 'a', 'b', 'l', 'e');
> 
> Or:
> 
>    subtype T is Character
>       with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');
> 
> Greetings,
> 
> Jacob
> -- 
> "people who live in glass houses shouldn't be throwing rocks
>  -- especially at those who don't live in glass houses"

Thanks. But I want to separate the table and the subtype...
As an example:

(A): a platform-depended private package

 private package Mylib.Platform_Depended is -- for POSIX
    Separators : constant String := ('/', '\');
 end;

Or:

 private package Mylib.Platform_Depended is -- for Windows
    Separators : constant String := ('/', '\');
 end;

(B): using (A)

 private with Mylib.Platform_Depended;
 package Mylib.Path_Manipulators is
    Separators : constant String;
    subtype Directory_Separator is Character
       with Static_Predicate =>
          (for I of Separators => Directory_Separator = I); -- **error**
    function Compose (
       Path : String;
       Separator : Directory_Separator;
       Name : String) return String;
    ...
 private
    Separators : constant String := Platform_Depended.Separators;
 end;

The reason of it's not Dynamic_Predicate is, I wish compile-time warning if possible.

Re: Some kind of repeating in Static_Predicate

[Randy Brukardt]

"ytomino" <aghia05@gmail.com> wrote in message 
news:503aed95-bd48-4eeb-a2a2-0f7bcc8de307@googlegroups.com...
> On Monday, June 4, 2018 at 3:26:56 PM UTC+9, Jacob Sparre Andersen wrote:
>> ytomino <agh...@gmail.com> writes:
>>
>> > I'm trying to use a constant table (but that is unstable and may be
>> > changed in compile-time) in Static_Predicate.
>> >
>> >  Set : constant String := ('T', 'a', 'b', 'l', 'e');
>> >
>> >  subtype T is Character
>> >     with Static_predicate => (for some I of Set => X = I);
>>
>> Why not admit that it is a Dynamic_Predicate?
>>
>> Alternatively:
>>
>>    type T is ('T', 'a', 'b', 'l', 'e');
>>
>> Or:
>>
>>    subtype T is Character
>>       with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');
>>
>> Greetings,
>>
>> Jacob
>> -- 
>> "people who live in glass houses shouldn't be throwing rocks
>>  -- especially at those who don't live in glass houses"
>
> Thanks. But I want to separate the table and the subtype...

That seems backwards to me. You are wanting to declare a set subtype, and 
Ada uses the silly static predicate for doing so rather than having a proper 
set constraint. Either way, that's a subtype declaration.

So the operative thing here is the subtype. There's no "table" in a set 
description. If you need to check membership in the set, you just do that 
with "in".

Thus:

    subtype T is Character
       with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');

    if Param in T then ...

If you really needed a table, I'd construct that from the set. (But I can't 
imagine what the use would be, certainly in cases like the "separators" 
definition you showed in another mail.)

                                  Randy.

Re: Some kind of repeating in Static_Predicate

[ytomino]

On Tuesday, June 5, 2018 at 6:33:48 AM UTC+9, Randy Brukardt wrote:
> "ytomino" <agh...@gmail.com> wrote in message 
> news:503...@googlegroups.com...
> > On Monday, June 4, 2018 at 3:26:56 PM UTC+9, Jacob Sparre Andersen wrote:
> >> ytomino <agh...@gmail.com> writes:
> >>
> >> > I'm trying to use a constant table (but that is unstable and may be
> >> > changed in compile-time) in Static_Predicate.
> >> >
> >> >  Set : constant String := ('T', 'a', 'b', 'l', 'e');
> >> >
> >> >  subtype T is Character
> >> >     with Static_predicate => (for some I of Set => X = I);
> >>
> >> Why not admit that it is a Dynamic_Predicate?
> >>
> >> Alternatively:
> >>
> >>    type T is ('T', 'a', 'b', 'l', 'e');
> >>
> >> Or:
> >>
> >>    subtype T is Character
> >>       with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');
> >>
> >> Greetings,
> >>
> >> Jacob
> >> -- 
> >> "people who live in glass houses shouldn't be throwing rocks
> >>  -- especially at those who don't live in glass houses"
> >
> > Thanks. But I want to separate the table and the subtype...
> 
> That seems backwards to me. You are wanting to declare a set subtype, and 
> Ada uses the silly static predicate for doing so rather than having a proper 
> set constraint. Either way, that's a subtype declaration.
> 
> So the operative thing here is the subtype. There's no "table" in a set 
> description. If you need to check membership in the set, you just do that 
> with "in".
> 
> Thus:
> 
>     subtype T is Character
>        with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');
> 
>     if Param in T then ...
> 
> If you really needed a table, I'd construct that from the set. (But I can't 
> imagine what the use would be, certainly in cases like the "separators" 
> definition you showed in another mail.)
> 
>                                   Randy.

Thanks. I understood it's backwards.
Yes, the table is needless in run-time. I want only compile-time checking by Static_Predicate in this case. Also, types should be more primary than constants basically.
However, a subtype declaration can't be separated to another package... The table may be configured before compiling, like the example of directory separators.

Re: Some kind of repeating in Static_Predicate

[Randy Brukardt]

"ytomino" <aghia05@gmail.com> wrote in message 
news:675621d4-7f23-48bd-a7e0-4105b21ddfd7@googlegroups.com...
> On Tuesday, June 5, 2018 at 6:33:48 AM UTC+9, Randy Brukardt wrote:
...
>> > Thanks. But I want to separate the table and the subtype...
>>
>> That seems backwards to me. You are wanting to declare a set subtype, and
>> Ada uses the silly static predicate for doing so rather than having a 
>> proper
>> set constraint. Either way, that's a subtype declaration.
>>
>> So the operative thing here is the subtype. There's no "table" in a set
>> description. If you need to check membership in the set, you just do that
>> with "in".
>>
>> Thus:
>>
>>     subtype T is Character
>>        with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');
>>
>>     if Param in T then ...
>>
>> If you really needed a table, I'd construct that from the set. (But I 
>> can't
>> imagine what the use would be, certainly in cases like the "separators"
>> definition you showed in another mail.)
>
> Thanks. I understood it's backwards.
> Yes, the table is needless in run-time. I want only compile-time checking
>by Static_Predicate in this case. Also, types should be more primary than
>constants basically.
> However, a subtype declaration can't be separated to another package...

Of course a subtype can be declared in another package, I'm not sure why you 
say that. For subtypes, you can always declare another subtype in your 
primary package to get visibility:

    package Params is
        subtype Separators is Character with Static_Predicate => Separators 
in '/' | '\';
        -- other configuation parameters here.
   end Params;

   with Params;
   package File_Ops is
       subtype Separators is Params.Separators;
       -- Other file operations here.
   end File_Ops;

(Using the same exact name isn't a good idea if you are the sort to stick 
use clauses everywhere,but of course the names don't have to be identical.) 
Also note that "use type" and "use all type" will give you appropriate 
visibility on the operators (and primitive operations, in the case of "use 
all type") regardless of where the type is declared - another reason to 
prefer "use type" when possible.

>The table may be configured before compiling, like the example of directory
>separators.

Yes, see above.

                              Randy.

Re: Some kind of repeating in Static_Predicate

[ytomino]

On Monday, June 4, 2018 at 3:26:56 PM UTC+9, Jacob Sparre Andersen wrote:
> ytomino <agh...@gmail.com> writes:
> 
> > I'm trying to use a constant table (but that is unstable and may be
> > changed in compile-time) in Static_Predicate.
> >
> >  Set : constant String := ('T', 'a', 'b', 'l', 'e');
> >  
> >  subtype T is Character
> >     with Static_predicate => (for some I of Set => X = I);
> 
> Why not admit that it is a Dynamic_Predicate?
> 
> Alternatively:
> 
>    type T is ('T', 'a', 'b', 'l', 'e');
> 
> Or:
> 
>    subtype T is Character
>       with Static_Predicate => (T in 'T' | 'a' | 'b' | 'l' | 'e');
> 
> Greetings,
> 
> Jacob
> -- 
> "people who live in glass houses shouldn't be throwing rocks
>  -- especially at those who don't live in glass houses"

Thanks. But I want to separate the table and the subtype...
As an example:

(A): a platform-depended private package

 private package Mylib.Platform_Depended is -- for POSIX
    Separators : constant String := ('/');
 end;

Or:

 private package Mylib.Platform_Depended is -- for Windows
    Separators : constant String := ('/', '\');
 end;

(B): using (A)

 private with Mylib.Platform_Depended;
 package Mylib.Path_Manipulators is
    Separators : constant String;
    subtype Directory_Separator is Character
       with Static_Predicate =>
          (for I of Separators => Directory_Separator = I); -- **error**
    function Compose (
       Path : String;
       Separator : Directory_Separator;
       Name : String) return String;
    ...
 private
    Separators : constant String := Platform_Depended.Separators;
 end;

The reason of it's not Dynamic_Predicate is, I wish compile-time warning if possible.

Re: Some kind of repeating in Static_Predicate

[Marius Amado-Alves]

A constant that is unstable and may be changed ?!?!?!?!?

Re: Some kind of repeating in Static_Predicate

[ytomino]

On Wednesday, June 6, 2018 at 8:04:08 PM UTC+9, Marius Amado-Alves wrote:
> A constant that is unstable and may be changed ?!?!?!?!?

Sorry. I'm reflecting for my insufficient explanation. Probably my detailed intention is communicated to nobody.

This "change" is a story of compile-time.

* Calculating from another constants with static expressions
* Switching the source file depending on the platforms
* Generating the source file in Makefile
etc.

Re: Some kind of repeating in Static_Predicate

[Marius Amado-Alves]

I see, compile-time checks, sorry.

Interesting problem. Let us know how you did it the end.