CVS difference for ai12s/ai12-0321-1.txt

Differences between 1.5 and version 1.6
Log of other versions for file ai12s/ai12-0321-1.txt

--- ai12s/ai12-0321-1.txt	2019/03/15 05:39:29	1.5
+++ ai12s/ai12-0321-1.txt	2019/04/06 05:08:50	1.6
@@ -753,3 +753,271 @@
 
 ****************************************************************
 
+From: Brad Moore
+Sent: Sunday, March 17, 2019  10:56 AM
+
+>> 
+>> >    pragma Assert((for some I in 1..T'Size => T'Modulus = 2**I));
+>> 
+>> For "type T is mod 1;", T'Size = 0, 2**T'Size = 1, and T'Modulus = 1.
+>> 
+>> ;-)
+> 
+> Tucker noted that it isn't a very good assertion, since someone could
+> declare:
+> 
+>    type Biggie is mod 256 with Atomic, Size => 16;
+> 
+> OTOH, we could decide to explicitly not care about such corner cases.
+
+Given the choice in this case, I think it's probably better to have an 
+assertion that always works, rather than one that mostly works, even if it 
+is a bit more expensive.
+At least the assertion if enabled is only applied during generic instantiation.
+
+To address Bob's comment, it doesn't make sense to have bitwise operations on 
+a type that doesn't have any bits, so I would extend the assertion to;
+
+pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus = 2**I));
+
+
+In this case, it's too bad that Ada hadn't defined a nand keyword similar to 
+xor which could be used for logical or bitwise operations.
+That could be used to get the ones complement of any modular type. Currently, 
+we have the "not" keyword, but that only gives you a ones complement if the 
+modulus of the type is binary.
+
+If we had that, then we could write instead;
+
+pragma Assert((T'Last nand T'Last) = 0);
+
+>> Note to Brad:  Unlike signed integers, the base range of a modular 
+>> type is widened beyond the first subtype.
+> 
+> Every time I read this, I'm confused. I even went and looked it up in 
+> the RM to be sure. I think there is a "not" missing somewhere. Perhaps you meant:
+> 
+>   Note to Brad:  Unlike signed integers, the base range of a
+>   modular type is NOT widened beyond the first subtype.
+
+Bob later clarified that he had meant to put the NOT in.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 18, 2019  10:19 PM
+
+> To address Bob's comment, it doesn't make sense to have bitwise 
+> operations on a type that doesn't have any bits, so I would extend the 
+> assertion to;
+> 
+> pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus 
+> = 2**I));
+
+You probably need to guard against overflow when 
+T'Modulus = System.Max_Binary_Modulus, which is probably bigger than 
+root_integer'Last (which is a signed integer type). And this will be 
+evaluated using root_integer, since it is a universal_integer expression 
+that isn't static. 
+
+Moreover, you don't need the pretest, since the quantified expression doesn't 
+allow T'Modulus = 1 (2**1 being 2, last I checked :-). Ergo:
+
+pragma Assert(T'Modulus = System.Max_Binary_Modulus or else
+   (for some I in 1..T'Size => T'Modulus = 2**I);
+
+As written, this will still overflow on a machine with a 32-bit root_integer 
+for something like:
+    type Funny is mod 7 with Atomic, Size => 32; 
+but this is truly weird, and the assertion would fail anyway for Funny -- not 
+sure it's worth ensuring a particular exception in this case (that is, 
+Assertion_Error vs. Constraint_Error). 
+
+[And of course, change 32 to whatever the size of root_integer is, this will 
+fail on any machine unless it doesn't support maximum integer-sized atomics
+-- which seems unlikely.]
+
+...
+> If we had that, then we could write instead;
+> 
+> pragma Assert((T'Last nand T'Last) = 0);
+
+Tricky! We probably want the assertion to be understandable to the relatively 
+causal reader, and this is not that. (Otherwise, we'd have to repeat it in 
+English so people know what they're allowed to do, which defeats the point.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, March 19, 2019  3:59 AM
+
+In any case, I would separate this from the arithmetic operations, and probably 
+put it in a separate AI, that I at least would suggest deferring for now.
+
+****************************************************************
+
+From: Brad Moore
+Sent: Friday, March 22, 2019  12:25 AM
+
+>> To address Bob's comment, it doesn't make sense to have bitwise 
+>> operations on a type that doesn't have any bits, so I would extend 
+>> the assertion to;
+>> 
+>> pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus 
+>> = 2**I));
+> 
+> You probably need to guard against overflow when T'Modulus = 
+> System.Max_Binary_Modulus, which is probably bigger than 
+> root_integer'Last (which is a signed integer type). And this will be 
+> evaluated using root_integer, since it is a universal_integer expression 
+> that isn't static.
+
+Right, but what I had to do to get this to work involved jumping through a 
+rather extraordinary number of hoops. See below....
+
+> Moreover, you don't need the pretest, since the quantified expression 
+> doesn't allow T'Modulus = 1 (2**1 being 2, last I checked :-).
+
+Right.
+
+ Ergo:
+> 
+> pragma Assert(T'Modulus = System.Max_Binary_Modulus or else
+>   (for some I in 1..T'Size => T'Modulus = 2**I);
+> 
+> As written, this will still overflow on a machine with a 32-bit 
+> root_integer for something like:
+>    type Funny is mod 7 with Atomic, Size => 32; but this is truly 
+> weird, and the assertion would fail anyway for Funny -- not sure it's 
+> worth ensuring a particular exception in this case (that is, 
+> Assertion_Error vs. Constraint_Error).
+> 
+> [And of course, change 32 to whatever the size of root_integer is, 
+> this will fail on any machine unless it doesn't support maximum 
+> integer-sized atomics which seems unlikely.]
+
+This works ordinarily, but doesn't work for a generic formal modular type.
+Or at least it doesn't in GNAT.
+
+I get the following warnings for the compilation if I prepend the expression
+  Atomic_Type'Modulus = System.Max_Binary_Modulus or else
+
+atomic_operations-bitwise.ads:9:47: warning: non-static universal integer value out of range
+atomic_operations-bitwise.ads:9:47: warning: "Constraint_Error" will be raised at run time
+
+This makes sense to me, as the generic doesn't know that its actual type wont 
+have a non-binary modulus. I suspect an assume-the-worst rule is being applied 
+here. The limit for a non-binary modulus as defined in 
+System.Max_Nonbinary_Modulus on GNAT is 2 ** Integer'Size - 1, which is much 
+smaller than System.Max_Binary_Modulus which is based on the size of a 64 bit 
+integer.
+
+More below....
+
+> ...
+>> If we had that, then we could write instead;
+>> 
+>> pragma Assert((T'Last nand T'Last) = 0);
+> 
+> Tricky! We probably want the assertion to be understandable to the 
+> relatively causal reader, and this is not that. (Otherwise, we'd have 
+> to repeat it in English so people know what they're allowed to do, 
+> which defeats the point.)
+
+I think either assertion is likely to cause some head-scratching for the casual 
+reader (or even a causal reader ;-) ).
+
+I think a better solution is to define a boolean expression function whose 
+name describes the property, then the body of the expression function can 
+be more esoteric, tricky, or super-complicated, as it seems we need to do 
+in current Ada. The name of the function documents the intent.
+
+e.g
+
+generic
+   type Atomic_Type is mod <>  with Atomic;
+package Atomic_Operations.Bitwise with Pure, Nonblocking is
+
+   function Atomic_Type_Has_Binary_Modulus return Boolean is
+      ((T'Last nand T'Last) = 0)
+
+   pragma Assert (Atomic_Type_Has_Binary_Modulus);
+
+
+Note, to have the Assert call a function of the package, it needs to be an 
+expression function, otherwise you get a Program_Error due to elaboration 
+problems.
+
+So suppose we wanted to write this assertion using current Ada, without 
+adding a nand keyword to the language.
+
+This ended up being a real struggle for me, but this is what I ended up with, 
+that seems to work. This seems to handle any modular type, as well as any 
+combination of 'Size aspect applied to the type. (I think, although there may 
+be some cases that dont work. The ones I tried seem to work at least).
+
+generic
+   type Atomic_Type is mod <>  with Atomic;
+package Atomic_Operations.Bitwise with Pure, Nonblocking is
+
+ function Atomic_Type_Has_Binary_Modulus return Boolean is
+     (Atomic_Type'Mod (2) = 0 or else        
+        (for all I in 1 .. Atomic_Type'Size - 1 =>
+           (for some K in 1 .. I - 1 =>
+              2 * Atomic_Type (2**(K - 1)) < Atomic_Type (2**(K - 1)))
+           or else
+             (Atomic_Type'Last and 2 * Atomic_Type (2**(I - 1))) = 0
+           or else
+             (for all J in 0 .. I - 1 =>
+                (Atomic_Type'Last and Atomic_Type (2**J)) /= 0)));   
+
+   
+   pragma Assert (Atomic_Type_Has_Binary_Modulus);
+
+...
+
+
+I gave up on trying to use 'Modulus. Randy's suggestion worked for non-generic
+code, but when you try to use this attributes in a generic, I found it too 
+hard to compare the attribute result to test for overflow. 
+
+This is because 'Modulus result is a universal integer, which is non-static in 
+the generic specification, so you cant compare it to System.Max_Binary_Modulus.
+
+Similarly, the argument for the 'Mod attribute is a universal integer, so you 
+have to be careful to not pass in a value that is too large. I also ran into 
+trouble using the expression 2**I, because that the type of I is natural, and
+so 2**I is an integer expression, which can overflow. So I had to write 
+2**(I-1), then convert that to the atomic type, and then multiply by 2 to get 
+the modular value that I really wanted to work with. That multiplication by 2 
+is a modular operation (that can wrap around)
+
+The approach is to keep testing higher bits, and if a 1 is found, then check 
+all lower bits to see if there are any zeroes.
+If a zero bit is found, just ignore it and keep searching.
+
+The way I dealt with overflow is handled in the first part of the expression 
+function, where I test all previous iterations to see if the modular type 
+wrapped around. If a wrap around was found then we know we've already got the 
+answer, and just let the remaining iterations finish without checking the else 
+clauses.
+
+I must admit, this is a pretty complicated function to just check a modular 
+type to see if the modulus is a power two! There may be a simpler solution, 
+but every idea I came up with kept hitting roadblocks.
+
+It would sure be nice to have some sort of nand capability or similar, to make 
+writing such contracts simpler and easier to write.
+
+If not for Ada202x, then hopefully a next one after that.
+
+But at least it seems there is a way to do it in current Ada, but its not 
+pretty.
+
+Alternatively, we could do away with the assertion, and just document that 
+an instance of the generic will raise an exception if the Modular formal type
+has a modulus that is not a power of two. But it seems that in Ada 202x, one 
+ought to have visible contracts for such an assertion.
+
+****************************************************************
+

Questions? Ask the ACAA Technical Agent