* Generic formals and Aspects
@ 2014-10-17 13:17 Simon Wright
2014-10-17 16:04 ` Shark8
` (2 more replies)
0 siblings, 3 replies; 10+ messages in thread
From: Simon Wright @ 2014-10-17 13:17 UTC (permalink / raw)
Recently on StackOverflow there was a question[1] about clamping a value
to a range.
The answer, so far, suggests a generic:
generic
type Source_Type is range <>;
type Destination_Type is range <>;
function Saturate (X : Source_Type) return Destination_Type;
with discussion about what happens if Destination_Type'Range is not a
subset of Source_Type'Range.
I see in AARM 13.1.1(4.b)[2] that a formal_type_declaration is allowed to
include an aspect specification, so tried
generic
type Source_Type is range <>
with Static_Predicate =>
Long_Long_Integer (Destination_Type'First)
>= Long_Long_Integer (Source_Type'First)
and Long_Long_Integer (Destination_Type'Last)
<= Long_Long_Integer (Source_Type'Last);
type Destination_Type is range <>;
function Saturate (X : Source_Type) return Destination_Type;
but GNAT (4.9.1, GPL 2014) said that Static_Predicate wasn't allowed
(nor was Dynamic_Predicate).
Predicate (GNAT-special?) was allowed, but had no effect: I was able to
instantiate with
type Source is new Integer range 10 .. 20;
type Destination is new Integer range 30 .. 40;
(a) what aspects are/should be allowed in a formal_type_declaration?
(b) how to write the generic to prevent this sort of mistake at compile
time? (easy enough to get a runtime CE).
[1] http://stackoverflow.com/questions/26390135/can-i-clamp-a-value-into-a-range-in-ada
[2] http://www.ada-auth.org/standards/12aarm/html/AA-13-1-1.html#p4.b
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2014-10-17 13:17 Generic formals and Aspects Simon Wright
@ 2014-10-17 16:04 ` Shark8
2014-10-17 18:51 ` Simon Wright
2014-10-18 1:43 ` Shark8
2016-07-19 15:49 ` olivermkellogg
2 siblings, 1 reply; 10+ messages in thread
From: Shark8 @ 2014-10-17 16:04 UTC (permalink / raw)
On 10/17/2014 7:17 AM, Simon Wright wrote:
> Predicate (GNAT-special?) was allowed, but had no effect
Hm, is your assertion-policy turned on?
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2014-10-17 16:04 ` Shark8
@ 2014-10-17 18:51 ` Simon Wright
0 siblings, 0 replies; 10+ messages in thread
From: Simon Wright @ 2014-10-17 18:51 UTC (permalink / raw)
Shark8 <OneWingedShark@gmail.com> writes:
> On 10/17/2014 7:17 AM, Simon Wright wrote:
>> Predicate (GNAT-special?) was allowed, but had no effect
>
> Hm, is your assertion-policy turned on?
No; I think that (at the moment) -gnata enables all assertions.
But I tried it anyway: no difference.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2014-10-17 13:17 Generic formals and Aspects Simon Wright
2014-10-17 16:04 ` Shark8
@ 2014-10-18 1:43 ` Shark8
2016-07-19 15:49 ` olivermkellogg
2 siblings, 0 replies; 10+ messages in thread
From: Shark8 @ 2014-10-18 1:43 UTC (permalink / raw)
The following does work, though it doesn't catch it at compile-time:
generic
type Source_Type is range <>;
type Destination_Type is range <>;
S_First : Long_Long_Integer:= Long_Long_Integer(Source_Type'First);
S_Last : Long_Long_Integer:= Long_Long_Integer(Source_Type'Last);
D_First : Long_Long_Integer:=
Long_Long_Integer(Destination_Type'First);
D_Last : Long_Long_Integer:=
Long_Long_Integer(Destination_Type'Last);
function Saturate (X : Source_Type) return Destination_Type
with Pre =>
D_First >= S_First
and D_Last <= S_Last
;
Maybe this would be a good thing to suggest for the corrigenda --
addition of SUBTYPE to generic formals; the purpose thereof would be to
"hang" Predicates on and [I think] Static_Predicate could be checked at
compile-time.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2014-10-17 13:17 Generic formals and Aspects Simon Wright
2014-10-17 16:04 ` Shark8
2014-10-18 1:43 ` Shark8
@ 2016-07-19 15:49 ` olivermkellogg
2016-07-19 16:04 ` J-P. Rosen
2016-07-19 16:05 ` Shark8
2 siblings, 2 replies; 10+ messages in thread
From: olivermkellogg @ 2016-07-19 15:49 UTC (permalink / raw)
On Friday, October 17, 2014 at 3:17:36 PM UTC+2, Simon Wright wrote:
> Recently on StackOverflow there was a question[1] about clamping a value
> to a range.
>
> The answer, so far, suggests a generic:
>
> generic
> type Source_Type is range <>;
> type Destination_Type is range <>;
> function Saturate (X : Source_Type) return Destination_Type;
>
> with discussion about what happens if Destination_Type'Range is not a
> subset of Source_Type'Range.
>
> I see in AARM 13.1.1(4.b)[2] that a formal_type_declaration is allowed to
> include an aspect specification, so tried
>
> generic
> type Source_Type is range <>
> with Static_Predicate =>
> Long_Long_Integer (Destination_Type'First)
> >= Long_Long_Integer (Source_Type'First)
> and Long_Long_Integer (Destination_Type'Last)
> <= Long_Long_Integer (Source_Type'Last);
> type Destination_Type is range <>;
> function Saturate (X : Source_Type) return Destination_Type;
>
> but GNAT (4.9.1, GPL 2014) said that Static_Predicate wasn't allowed
> (nor was Dynamic_Predicate).
>
> Predicate (GNAT-special?) was allowed, but had no effect: I was able to
> instantiate with
>
> type Source is new Integer range 10 .. 20;
> type Destination is new Integer range 30 .. 40;
>
>
> (a) what aspects are/should be allowed in a formal_type_declaration?
>
> (b) how to write the generic to prevent this sort of mistake at compile
> time? (easy enough to get a runtime CE).
>
> [1] http://stackoverflow.com/questions/26390135/can-i-clamp-a-value-into-a-range-in-ada
> [2] http://www.ada-auth.org/standards/12aarm/html/AA-13-1-1.html#p4.b
I share the sentiment.
Here is my use case:
-- File: big_endian_integer_buffer.ads
with Interfaces;
generic
type Discrete_Type_16_or_32_or_64 is (<>); -- CANDIDATE
package Big_Endian_Integer_Buffer is
function Get return Discrete_Type_16_or_32_or_64;
procedure Set (Value : Discrete_Type_16_or_32_or_64);
Size_In_Bytes : constant Positive := Discrete_Type_16_or_32_or_64'Size / 8;
type Buffer_Type is array (1 .. Size_In_Bytes) of Interfaces.Unsigned_8;
for Buffer_Type'Component_Size use 8;
Buffer : aliased Buffer_Type := (others => 0);
end Big_Endian_Integer_Buffer;
At the line marked CANDIDATE, I would have liked to write something like
type Discrete_Type_16_or_32_or_64 is (<>)
with Static_Predicate => Discrete_Type_16_or_32_or_64'Size in 16 | 32 | 64;
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2016-07-19 15:49 ` olivermkellogg
@ 2016-07-19 16:04 ` J-P. Rosen
2016-07-19 16:05 ` Shark8
1 sibling, 0 replies; 10+ messages in thread
From: J-P. Rosen @ 2016-07-19 16:04 UTC (permalink / raw)
Le 19/07/2016 à 17:49, olivermkellogg@gmail.com a écrit :
> generic
>> type Source_Type is range <>
>> with Static_Predicate =>
>> Long_Long_Integer (Destination_Type'First)
>> >= Long_Long_Integer (Source_Type'First)
>> and Long_Long_Integer (Destination_Type'Last)
>> <= Long_Long_Integer (Source_Type'Last);
>> type Destination_Type is range <>;
>> function Saturate (X : Source_Type) return Destination_Type;
>>
Tip: you don't need to convert to Long_Long_Integer here (non portable,
etc...). Use:
Destination_Type'Pos (Destination_Type'First)
>= Source_Type'Pos (Source_Type'First)
and Destination_Type'Pos (Destination_Type'Last)
<= Source_Type'Pos (Source_Type'Last);
Since 'Pos returns Universal_Integer, you can compare values of
different types.
FWIW...
--
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2016-07-19 15:49 ` olivermkellogg
2016-07-19 16:04 ` J-P. Rosen
@ 2016-07-19 16:05 ` Shark8
2016-07-19 18:00 ` olivermkellogg
1 sibling, 1 reply; 10+ messages in thread
From: Shark8 @ 2016-07-19 16:05 UTC (permalink / raw)
Try the following:
------ SPEC ------
generic
type Discrete_Type is (<>); -- CANDIDATE
package Big_Endian_Integer_Buffer is
function Get return Discrete_Type;
procedure Set (Value : Discrete_Type);
Private
type Internal is new Discrete_Type
with Static_Predicate => Internal'Size in 16 | 32 | 64;
Size_In_Bytes : constant Positive := Internal'Size / 8;
type Buffer_Type is array (1 .. Size_In_Bytes) of Interfaces.Unsigned_8
with Component_Size => 8;
Buffer : Buffer_Type := (others => 0);
end Big_Endian_Integer_Buffer;
------ BODY ------
package body Big_Endian_Integer_Buffer is
function Get return Discrete_Type is
Result : Discrete_Type
with Import, Address => Buffer'Address;
begin
Return Discrete_Type(Result);
End Get;
procedure Set (Value : Discrete_Type) is
Temp : Internal
with Import, Address => Buffer'Address;
begin
Temp := Internal(Value);
End Set;
end Big_Endian_Integer_Buffer;
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2016-07-19 16:05 ` Shark8
@ 2016-07-19 18:00 ` olivermkellogg
2016-07-19 19:23 ` Randy Brukardt
0 siblings, 1 reply; 10+ messages in thread
From: olivermkellogg @ 2016-07-19 18:00 UTC (permalink / raw)
On Tuesday, July 19, 2016 at 6:05:12 PM UTC+2, Shark8 wrote:
> Try the following:
>
>
> ------ SPEC ------
> generic
> type Discrete_Type is (<>); -- CANDIDATE
>
> package Big_Endian_Integer_Buffer is
>
> function Get return Discrete_Type;
> procedure Set (Value : Discrete_Type);
>
> Private
> type Internal is new Discrete_Type
> with Static_Predicate => Internal'Size in 16 | 32 | 64;
>
> Size_In_Bytes : constant Positive := Internal'Size / 8;
>
> type Buffer_Type is array (1 .. Size_In_Bytes) of Interfaces.Unsigned_8
> with Component_Size => 8;
>
> Buffer : Buffer_Type := (others => 0);
> end Big_Endian_Integer_Buffer;
>
>
> ------ BODY ------
> package body Big_Endian_Integer_Buffer is
>
> function Get return Discrete_Type is
> Result : Discrete_Type
> with Import, Address => Buffer'Address;
> begin
> Return Discrete_Type(Result);
> End Get;
>
> procedure Set (Value : Discrete_Type) is
> Temp : Internal
> with Import, Address => Buffer'Address;
> begin
> Temp := Internal(Value);
> End Set;
>
> end Big_Endian_Integer_Buffer;
Interesting.
Using your modified spec with the following test program:
-- File: beib_test.adb
with Interfaces;
with Big_Endian_Integer_Buffer;
procedure BEIB_Test is
package Pass is new Big_Endian_Integer_Buffer (Interfaces.Unsigned_64);
type RGB_T is mod 2 ** 24 with Size => 24;
package Fail is new Big_Endian_Integer_Buffer (RGB_T);
P : Interfaces.Unsigned_64;
F : RGB_T;
begin
P := Pass.Get;
F := Fail.Get;
end BEIB_Test;
I get the following message from GNAT:
beib_test.ads:6:04: instantiation error at big_endian_integer_buffer.ads:16
beib_test.ads:6:04: expression is not predicate-static (RM 3.2.4(16-22))
[...]
Line 6 is at the Pass instantiation. (The same error happens at the Fail instantiation.)
Hmm, too bad... I would have preferred getting a compile time error.
That said, after changing Static_Predicate to Dynamic_Predicate in the spec, the test program builds okay.
However, it runs without failure. (I would have expected a failure on the Fail instantiation.)
For completeness, here is the generic body that I am using:
-- File: big_endian_integer_buffer.adb
with System, Ada.Unchecked_Conversion;
package body Big_Endian_Integer_Buffer is
use type System.Bit_Order;
function Get return Discrete_Type is
function To_Discrete is new Ada.Unchecked_Conversion
(Buffer_Type, Discrete_Type);
begin
if System.Default_Bit_Order = System.High_Order_First then
return To_Discrete (Buffer);
end if;
declare
Native_Buf : Buffer_Type;
begin
for I in 1 .. Size_In_Bytes loop
Native_Buf (I) := Buffer (Size_In_Bytes - I + 1);
end loop;
return To_Discrete (Native_Buf);
end;
end Get;
procedure Set (Value : Discrete_Type) is
function To_Buffer is new Ada.Unchecked_Conversion
(Discrete_Type, Buffer_Type);
begin
if System.Default_Bit_Order = System.High_Order_First then
Buffer := To_Buffer (Value);
return;
end if;
declare
Native_Buf : constant Buffer_Type := To_Buffer (Value);
begin
for I in 1 .. Size_In_Bytes loop
Buffer (I) := Native_Buf (Size_In_Bytes - I + 1);
end loop;
end;
end Set;
end Big_Endian_Integer_Buffer;
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2016-07-19 18:00 ` olivermkellogg
@ 2016-07-19 19:23 ` Randy Brukardt
2016-07-20 15:09 ` olivermkellogg
0 siblings, 1 reply; 10+ messages in thread
From: Randy Brukardt @ 2016-07-19 19:23 UTC (permalink / raw)
<olivermkellogg@gmail.com> wrote in message
news:18aedafc-c66d-4bba-81ce-76dce495f59e@googlegroups.com...
> On Tuesday, July 19, 2016 at 6:05:12 PM UTC+2, Shark8 wrote:
>> Try the following:
>>
>>
>> ------ SPEC ------
>> generic
>> type Discrete_Type is (<>); -- CANDIDATE
>>
>> package Big_Endian_Integer_Buffer is
>>
>> function Get return Discrete_Type;
>> procedure Set (Value : Discrete_Type);
>>
>> Private
>> type Internal is new Discrete_Type
>> with Static_Predicate => Internal'Size in 16 | 32 | 64;
You could use a subtype here, if you don't want a new type:
subtype Internal is Discrete_Type
with Dynamic_Predicate => Internal'Size in 16 | 32 | 64;
BUT:
'Size shouldn't be allowed in either of these predicates, because "Internal"
is a value (the value of the "current instance" of the subtype), while Size
is the attribute of a subtype or object. (See AI12-0068-1.) This is
necessary so that the properties of the object can't be queried in a
predicate; that wasn't the purpose of predicates and it would allow some
truly bizarre uses. (See "Zoofable" in the question of that AI.)
Specifically, 8.6(17.1/4) says:
Within an aspect_specification for a type or subtype, the current
instance represents a value of the type; it is not an object. The
nominal subtype of this value is given by the subtype itself (the
first subtype in the case of a type_declaration), prior to applying
any predicate specified directly on the type or subtype. If the type or
subtype is by-reference, the associated object with the value is the
object associated (see 6.2) with the execution of the usage name.
AARM Ramification: For the purposes of Legality Rules, the current
instance acts as a value within an aspect_specification. It might
really be an object (and has to be for a by-reference type), but
that isn't discoverable by direct use of the name of the current
instance.
Looks like an ACATS test is needed.
>> Size_In_Bytes : constant Positive := Internal'Size / 8;
...
...
> That said, after changing Static_Predicate to Dynamic_Predicate in the
> spec, the test program builds okay.
> However, it runs without failure. (I would have expected a failure on the
> Fail instantiation.)
Did you remember to enable assertions? GNAT has the Assertion_Policy as
Ignore by default. (This is implementation-defined in the Standard, mainly
because we didn't have enough votes to make GNAT change.) If you're
depending on assertions (like a predicate), you always need to appropriately
place a Assertion_Policy pragma (or the equivalent command-line option,
whatever it is).
Randy.
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Generic formals and Aspects
2016-07-19 19:23 ` Randy Brukardt
@ 2016-07-20 15:09 ` olivermkellogg
0 siblings, 0 replies; 10+ messages in thread
From: olivermkellogg @ 2016-07-20 15:09 UTC (permalink / raw)
On Tuesday, July 19, 2016 at 9:23:34 PM UTC+2, Randy Brukardt wrote:
> >> [...]
> >> type Internal is new Discrete_Type
> >> with Static_Predicate => Internal'Size in 16 | 32 | 64;
>
> You could use a subtype here, if you don't want a new type:
>
> subtype Internal is Discrete_Type
> with Dynamic_Predicate => Internal'Size in 16 | 32 | 64;
>
> BUT:
>
> 'Size shouldn't be allowed in either of these predicates, because "Internal"
> is a value (the value of the "current instance" of the subtype), while Size
> is the attribute of a subtype or object. (See AI12-0068-1.) This is
> necessary so that the properties of the object can't be queried in a
> predicate; that wasn't the purpose of predicates and it would allow some
> truly bizarre uses. (See "Zoofable" in the question of that AI.)
> Specifically, 8.6(17.1/4) says:
>
> Within an aspect_specification for a type or subtype, the current
> instance represents a value of the type; it is not an object. The
> nominal subtype of this value is given by the subtype itself (the
> first subtype in the case of a type_declaration), prior to applying
> any predicate specified directly on the type or subtype. If the type or
> subtype is by-reference, the associated object with the value is the
> object associated (see 6.2) with the execution of the usage name.
>
> AARM Ramification: For the purposes of Legality Rules, the current
> instance acts as a value within an aspect_specification. It might
> really be an object (and has to be for a by-reference type), but
> that isn't discoverable by direct use of the name of the current
> instance.
>
> Looks like an ACATS test is needed.
>
> >> Size_In_Bytes : constant Positive := Internal'Size / 8;
> ...
> ...
> > That said, after changing Static_Predicate to Dynamic_Predicate in the
> > spec, the test program builds okay.
> > However, it runs without failure. (I would have expected a failure on the
> > Fail instantiation.)
>
> Did you remember to enable assertions? GNAT has the Assertion_Policy as
> Ignore by default. (This is implementation-defined in the Standard, mainly
> because we didn't have enough votes to make GNAT change.) If you're
> depending on assertions (like a predicate), you always need to appropriately
> place a Assertion_Policy pragma (or the equivalent command-line option,
> whatever it is).
>
Yes, I added both
pragma Assertion_Policy (Check);
on the package spec and "-gnata" on compiling; no change on execution.
Thanks for your insights.
^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2016-07-20 15:09 UTC | newest]
Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-10-17 13:17 Generic formals and Aspects Simon Wright
2014-10-17 16:04 ` Shark8
2014-10-17 18:51 ` Simon Wright
2014-10-18 1:43 ` Shark8
2016-07-19 15:49 ` olivermkellogg
2016-07-19 16:04 ` J-P. Rosen
2016-07-19 16:05 ` Shark8
2016-07-19 18:00 ` olivermkellogg
2016-07-19 19:23 ` Randy Brukardt
2016-07-20 15:09 ` olivermkellogg
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox